bool_pred

add_equality(X,Y,Res) :-
    (get_bool_pred_info(X,NX,List)
    -> put_bool_pred_info(X,NX,[eqcheck(Y,Res)|List])
    ; add_new_equality(X,Y,Res)
).

add_new_equality(X,Y,Res) :-
    put_bool_pred_info(NX,X,[]),% NX is a fresh variable, no need to go through negate/2
    put_bool_pred_info(X,NX,[eqcheck(Y,Res)]).

blocking_force_eq3(Res,X,Y) :-
    when((?=(Res,X) ; ?=(Res,Y) ; ?=(X,Y) ; nonvar(Res) ; nonvar(X) ; nonvar(Y)), bool_equality(X,Y,Res)).

bool_equality(X,Y,Res) :- %print(bool_equality(X,Y,Res)),nl, %% enter_log(bool_equality(X,Y,Res)),
    ( nonvar(X) -> eq1(X,Y,Res)
    ; nonvar(Y) -> eq1(Y,X,Res)
    ; nonvar(Res) -> eq1(Res,X,Y)
    ; X==Y -> Res=pred_true
    ; X==Res -> Y=pred_true % Warning: Y could expect bool_true !
    ; Y==Res -> X=pred_true % Warning: X could expect bool_true !
    ; get_bool_pred_info(X,NX,XList)
    -> (NX==Y -> Res=pred_false % Y is the negation of X
    ; NX==Res -> Y=pred_false % Warning: Y could expect bool_false !
    ; put_bool_pred_info(X,NX,[eqcheck(Y,Res)|XList]),
    add_equality(Y,X,Res)
    ),
    blocking_force_eq3(Res,X,Y)
    ; add_new_equality(X,Y,Res),add_equality(Y,X,Res),
    blocking_force_eq3(Res,X,Y)
). % ,exit_log(eq(X,Y,Res)).

bool_negate_check(X,Y) :- get_bool_pred_info(X,OtherX,_),Y==OtherX.

check_equalities([],_,_,true) --> [].

check_equalities([eqcheck(V2,Res)|T],V1,NegV1,Goal) -->
    ( {V2==V1} -> {Goal=(Res=pred_true,G2)}
    ; {V2==NegV1} -> {Goal=(Res=pred_false,G2)}
    ; {V1==Res} -> {Goal=(V2=pred_true,G2)} % Warning: V2 could expect bool_true !
    ; {NegV1==Res} -> {Goal=(V2=pred_false,G2)} % Warning: V2 could expect bool_false !
    ; %{print(no_new_info),nl},
    [eqcheck(V2,Res)], {Goal=G2}
    ),check_equalities(T,V1,NegV1,G2).

check_inst_equalities([],_).

check_inst_equalities([eqcheck(V2,Res)|T],V1) :-
    (nonvar(V2) -> (V1=V2 -> Res=pred_true ; Res=pred_false)
    ; V1=pred_true -> Res=V2
    ; negate(V2,Res)
    ), check_inst_equalities(T,V1).

enter_log(X) :- retract(logging_level(L)),
    indent_ws(L),print(X), print(','),nl,
    L1 is L+1, assertz(logging_level(L1)).

eq1(pred_true,X,X).

eq1(pred_false,X,Y) :- negate(X,Y).

exit_log(G) :- retract(logging_level(L)),
    (L>0 -> L1 is L-1, assertz(logging_level(L1)), indent_ws(L1), print('exit '), print(G),nl
    ; add_internal_error('*** negative - logging level !',L),
    assertz(logging_level(L))).

free_var(X) :- var(X), \+ get_bool_pred_info(X,_,_).

get_bool_pred_info(Var,Neg,ReifList) :- get_atts(Var,+bool_pred_info(Neg,ReifList)).

indent_ws(X) :- X<1,!.

indent_ws(X) :- print(' '), X1 is X-1, indent_ws(X1).

logging_level(0).

negate(X,Y) :- %enter_log(negate(X,Y)),
    (nonvar(X) -> negate3(X,Y)
    ; nonvar(Y) -> negate3(Y,X)
    ; get_bool_pred_info(X,OtherX,_) -> Y=OtherX, X \== Y, update_bool_pred_negation(Y,X)
    ; get_bool_pred_info(Y,OtherY,_) -> put_bool_pred_info(X,Y,[]), X=OtherY, X \== Y
    ; X \== Y, put_bool_pred_info(Y,X,[]), put_bool_pred_info(X,Y,[])
).% ,exit_log(negate(X,Y)).

negate3(pred_true,pred_false). % for kernel_equality,... results

negate3(pred_false,pred_true).

put_bool_pred_info(Var,Neg,ReifList) :- put_atts(Var,+bool_pred_info(Neg,ReifList)).

update_bool_pred_negation(X,_NegX) :- nonvar(X),!.

update_bool_pred_negation(X,NegX) :-
    (get_bool_pred_info(OtherX,_,_) -> OtherX=NegX
    ; put_bool_pred_info(X,NegX,[])).

verify_attributes(ThisVar,Value,Goal) :- get_atts(ThisVar,+bool_pred_info(NegThis,ThisReifList)),!,
    % enter_log(ThisVar=Value), %% print(verify(ThisVar,Value,NegThis,ThisReifList)),nl,
    (var(Value) -> (get_atts(Value,+bool_pred_info(NegValue,ValReifList))
    -> Goal=[NegThis=NegValue,ThisVar\==NegThis,EqGoal1,EqGoal2],
    check_equalities(ThisReifList,Value,NegValue,EqGoal1,NewReifList,RR),
    check_equalities(ValReifList,ThisVar,NegThis,EqGoal2,RR,[]),
    (nonvar(Value) -> print(verify_attribute_instantiated_value(Value)),nl /* check equalities could have forced value to be known now; should not happen */
    ; put_atts(Value,+bool_pred_info(NegValue,NewReifList)))
    ; put_atts(Value,+bool_pred_info(NegThis,ThisReifList)), Goal=[]
    )
    ; (ThisReifList=[]
    -> Goal=[negate3(Value,NegThis)] %(var(NegThis) -> Goal=[negate3(Value,NegThis)] ; Goal=[])
    ; Goal=[negate3(Value,NegThis),check_inst_equalities(ThisReifList,Value)])
). %, exit_log(Goal),trace. %, print(done_verify(ThisVar,Value,Goal)),nl.

verify_attributes(_, _, [] ).