b_to_cnf

add_translation_failure(Msg,Arg) :- add_message(b_to_cnf,Msg,Arg),fail.

add_translation_failure(Msg,Arg,Span) :- add_message(b_to_cnf,Msg,Arg,Span),fail.

all_one([]) --> [].

all_one([Lit1|T]) --> [[Lit1]], all_one(T).

all_zero([]) --> [].

all_zero([Lit1|T]) --> {negate_lit(Lit1,NLit1)}, [[NLit1]], all_zero(T).

at_least_one(List) --> [List]. % disjunction of literals; at least one must be true

at_least_one_false(List) --> {maplist(negate_lit,List,NList)}, at_least_one(NList).

attr_unify_hook(_, Value) :- var(Value),!.

attr_unify_hook(_, pred_true) :- !.

attr_unify_hook(_, pred_false) :- !.

attr_unify_hook(_, Value) :-
    add_error_fail(b_to_cnf_attr_unify_hook,'Tried to bind variable with attached SAT variable to non-boolean value', Value).

b_disj_create_one_sat_var(State,Disjunct,OneSatVar) :-
    WF = no_wf_available,
    b_optimize(Disjunct,State,NewDisj,WF),
    % write('disj: '),translate:print_bexpr(NewDisj),nl,
    b_to_cnf(NewDisj,State,CNFList,[]),
    (CNFList = [[]] -> OneSatVar=2 % candidate for certain in the set
    ; CNFList=[[OneSatVar]] -> true % the sat var corresponds to one candidate in the set
    ; CNFList = [] -> OneSatVar=1 % one candidate for certain not in the set
    ; add_error_fail(b_to_cnf,'Cannot reify disjunct to one sat variable:',Disjunct)
).

b_neg_to_cnf(b(Expr,_,Info),State) --> !,b_neg_to_cnf_aux(Expr,State,Info).

b_neg_to_cnf(In,_,_,_) :-
    add_error_fail(b_neg_to_cnf,'Not properly wrapped:', In).

b_neg_to_cnf_aux(falsity,_,_) --> [].

b_neg_to_cnf_aux(truth,_,_) --> [[]].

b_neg_to_cnf_aux(disjunct(A,B),State,_) --> !, % not(A or B) --> not(A) & not(B)
    b_neg_to_cnf(A,State),
    b_neg_to_cnf(B,State).

b_neg_to_cnf_aux(implication(A,B),State,_) --> !, % not(A => B) --> A & not(B)
    b_to_cnf(A,State),
    b_neg_to_cnf(B,State).

b_neg_to_cnf_aux(equal(A,B),State,_) --> b_neg_to_cnf_equal_aux(A,B,State),!. % does not cover all cases

b_neg_to_cnf_aux(equivalence(A,B),State,_) --> !, % not(A<=>B) --> A <=> not(B)
    {negate_pred(B,NotB)},
    b_to_cnf_aux(equivalence(A,NotB),State).

b_neg_to_cnf_aux(conjunct(A,B),State,_) --> !, b_neg_to_cnf_conj_aux(A,B,State).

b_neg_to_cnf_aux(BOP,State,_) --> {negate_op(BOP,NBOP)}, !,b_to_cnf_aux(NBOP,State).

b_neg_to_cnf_aux(let_predicate(Ids,Exprs,Body),State,Info) --> {expand_let_predicate(Ids,Exprs,Body,NewBody)},!,
    b_neg_to_cnf_aux(NewBody,State,Info).

b_neg_to_cnf_aux(Quant,State,Info) --> {is_quantifier(Quant)},!,
    {instantiate_quantifier(Quant,Info,Expansion,State)},
    ({get_texpr_expr(Expansion,Q),\+ is_quantifier(Q)} ->
    {b_optimize(Expansion,State,NewTyped,no_wf_available)}, % maybe we can now pre-compile more
    b_neg_to_cnf(NewTyped,State)
    ;{add_error_fail(b_neg_to_cnf,'Cannot expand negated quantifier: ',b(Expansion,pred,[]))}
).

b_neg_to_cnf_aux(A,State,_,[[Res]|Acc],Acc) :- % deals with equal
    b_to_cnf_aux(A,State,[[V]],[]), % very limited form of treatment of negation: TODO: improve
    negate_lit(V,Res).

b_neg_to_cnf_conj_aux(D1,D2,State) -->
    {negate_pred(D1,NegD1)},
    {negate_pred(D2,NegD2)},
    b_to_cnf_disj_aux(NegD1,NegD2,State).

b_neg_to_cnf_equal_aux(A,B,State) -->
    {( get_boolean_value(B,VAL), nonvar(VAL) -> LHS=A
    ; get_boolean_value(A,VAL) -> LHS=B
    )},
    !,
    ({VAL==pred_true}
    -> b_neg_to_cnf(LHS,State)
    ; {VAL == pred_false} ->
    {create_texpr(value(pred_true),boolean,[],True)},
    b_to_cnf_aux(equal(LHS,True),State)
    ; % this must be two boolean variables that are compared
    b_neg_to_cnf_aux(equivalence(A,B),State,[])
).

b_optimize(Expansion,State,NewTyped,WF) :-
    %tools:start_ms_timer(T1),
    b_compiler:b_optimize(Expansion,[],[],State,NewTyped,WF).

b_pred_to_cnf_wf(b(Expr,_,Info),State,_WF,Ai,Ai,sat) -->
    b_to_cnf_aux(Expr,State), % TODO: pass WF so that we can try and reify inner predicates)
    !,
    {add_source_location_hits(Info,1)}.

b_pred_to_cnf_wf(Pred,State,WF,Ai,Ao,prob) -->
    {add_message(b_to_cnf,'Cannot convert to CNF, solving with ProB: ',Pred,Pred),
    get_texpr_info(Pred,Info),add_source_location_hits(Info,0),
    copy_wf_start(WF,l_b_to_cnf_wf,CWF),
    b_interpreter:b_test_boolean_expression(Pred,[],State,CWF,Ai,Ao),
    copy_wf_finish(WF,CWF),
    ground_det_wait_flag(WF) % ground so that things are pre-computed for next conjunct
}.

b_to_cnf(b(Expr,_,Info),State,Out) :-
    b_to_cnf_aux(Expr,State,Res,[]), !,
    (Res=Out -> true
    ; add_error(b_to_cnf,'CNF conversion result does not match template:', Res, Info),
    fail).

b_to_cnf(In,_State,_) :- In = b(_,_,Info),
    add_error(b_to_cnf,'CNF conversion failed', In, Info),
    fail.

b_to_cnf(b(Expr,_,_Info),State) --> !, b_to_cnf_aux(Expr,State).

b_to_cnf(In,_,_,_) :-
    add_error_fail(b_to_cnf,'Not properly wrapped:', In).

b_to_cnf_aux(truth,_) --> [].

b_to_cnf_aux(falsity,_) --> [[]].

b_to_cnf_aux(identifier(Name),State) -->
    {lookup_id(Name,State,X)},
    b_to_cnf_val_aux(X,Name).

b_to_cnf_aux(value(X),_) --> b_to_cnf_val_aux(X,unknown).

b_to_cnf_aux(equal(A,B),State) --> b_to_cnf_equal_aux(A,B,State).

b_to_cnf_aux(not_equal(A,B),State) --> b_neg_to_cnf_aux(equal(A,B),State,[]).

b_to_cnf_aux(less_equal(A,B),State) --> b_to_cnf_less_equal_aux(A,B,State).

b_to_cnf_aux(greater_equal(A,B),State) --> b_to_cnf_less_equal_aux(B,A,State).

b_to_cnf_aux(less(A,B),State) --> b_to_cnf_less_aux(A,B,State).

b_to_cnf_aux(greater(A,B),State) --> b_to_cnf_less_aux(B,A,State).

b_to_cnf_aux(negation(A),State) --> b_neg_to_cnf(A,State).

b_to_cnf_aux(implication(A,B),State) -->
    {create_texpr(negation(A),pred,[],NotA)},
    b_to_cnf_aux(disjunct(NotA,B),State).

b_to_cnf_aux(equivalence(A,B),State) -->
    b_to_cnf_aux(implication(A,B),State),
    b_to_cnf_aux(implication(B,A),State).

b_to_cnf_aux(disjunct(D1,D2),State) --> b_to_cnf_disj_aux(D1,D2,State).

b_to_cnf_aux(conjunct(A,B),State) -->
    b_to_cnf(A,State),
    b_to_cnf(B,State).

b_to_cnf_aux(let_predicate(Ids,Exprs,Body),State) --> {expand_let_predicate(Ids,Exprs,Body,NewBody)},!,
    b_to_cnf_aux(NewBody,State).

b_to_cnf_aux(Quant,State) --> {is_quantifier2(Quant,Span)},
    {instantiate_quantifier(Quant,[],Expansion,State)},
    ({get_texpr_expr(Expansion,Q),\+ is_quantifier(Q)} ->
    % {write('Expanded: '), translate:print_bexpr(Quant),nl},
    % {write('Expansion: '), translate:print_bexpr(Expansion),nl},
    {b_optimize(Expansion,State,NewTyped,no_wf_available)}, % maybe we can now pre-compile more
    %{write('Compiled: '), translate:print_bexpr(NewTyped),nl},
    (b_to_cnf(NewTyped,State) -> []
    ; {add_translation_failure('Cannot translate body of expanded quantifier: ',NewTyped,Span)}
    )
    ; {add_translation_failure('Cannot expand quantifier: ',Expansion,Span)}
).

b_to_cnf_card_equal(0,List) --> !, all_zero(List).

b_to_cnf_card_equal(1,List) --> !, % exactly one
    at_least_one(List),
    b_to_cnf_card_less_equal(1,List). % at most one

b_to_cnf_card_equal(Len,List) --> {length(List,Len)}, !, all_one(List).

b_to_cnf_card_equal(Nr,List) --> {length(List,Len), Nr > Len}, !, [[]]. % contradiction

b_to_cnf_card_equal(Nr,List) -->
    b_to_cnf_card_less_equal(Nr,List),
    b_to_cnf_card_greater_equal(Nr,List),!.

b_to_cnf_card_equal(_Card,A) -->
    {add_translation_failure('Cannot convert card(.) equality to SAT:',A)}.

b_to_cnf_card_greater_equal(0,_List) --> !, []. % TODO: register variables in List to avoid pending co-routines

b_to_cnf_card_greater_equal(Nr,List) --> {length(List,Len)}, b_to_cnf_geq3(Nr,List,Len).

b_to_cnf_card_less_equal(0,List) --> !, all_zero(List).

b_to_cnf_card_less_equal(Nr,_List) --> {Nr<0},!, [[]]. % contradiction

b_to_cnf_card_less_equal(Nr,List) --> {length(List,Len)}, b_to_cnf_leq3(Nr,List,Len).

b_to_cnf_disj_aux(D1,D2,State) -->
    {get_texpr_expr(D1,conjunct(A,B))}, !,
    {create_texpr(disjunct(A,D2),pred,[],DJ1),
    create_texpr(disjunct(B,D2),pred,[],DJ2)},
    b_to_cnf_aux(conjunct(DJ1,DJ2),State).

b_to_cnf_disj_aux(D1,D2,State) -->
    {get_texpr_expr(D2,conjunct(A,B))}, !,
    {create_texpr(disjunct(D1,A),pred,[],DJ1),
    create_texpr(disjunct(D1,B),pred,[],DJ2)},
    b_to_cnf_aux(conjunct(DJ1,DJ2),State).

b_to_cnf_disj_aux(D1,D2,State,Res,Acc) :-
    b_to_cnf(D1,State,Res1),
    !,
    ( Res1 = [] -> Res=Acc % no clauses added
    ; b_to_cnf(D2,State,Res2),
    !,
    ( Res1 = [[]] -> append(Res2,Acc,Res)
    ; Res2 = [] -> Res = Acc % no clauses added
    ; Res2 = [[]] -> append(Res1,Acc,Res)
    ; Res1=[ResD1], Res2=[ResD2] -> Res = [Res12|Acc], append(ResD1,ResD2,Res12)
    ; join_clauses(Res1,Res2,Res,Acc) -> true
    ; add_error_fail(b_to_cnf_disj,'Cannot join clauses: ',Res1:Res2)
)
).

b_to_cnf_equal_aux(A,B,State) -->
    { get_integer(B,Card), get_card_as_sat_list(A,State,List) -> true
    ; get_integer(A,Card), get_card_as_sat_list(B,State,List)},
    !,
    b_to_cnf_card_equal(Card,List).

b_to_cnf_equal_aux(A,B,State) -->
    {( get_boolean_value(B,VAL), nonvar(VAL) -> LHS=A
    ; get_boolean_value(A,VAL) -> LHS=B
    )},
    !,
    ({VAL==pred_true}
    -> b_to_cnf(LHS,State)
    ; {VAL == pred_false} ->
    {create_texpr(value(pred_true),boolean,[],True)},
    b_neg_to_cnf_aux(equal(LHS,True),State,[])
    ; % this must be two boolean variables that are compared
    b_to_cnf_aux(equivalence(A,B),State)
).

b_to_cnf_equal_aux(A,B,State) --> {simplify_equality(A,B,SA,SB)},!,
    b_to_cnf_equal_aux(SA,SB,State).

b_to_cnf_equal_aux(A,B,_,_,_) :-
    %write(eq(A,B)),nl,
    add_translation_failure('Cannot convert equality to SAT variable: ',b(equal(A,B),pred,[])).

b_to_cnf_geq3(Len,List,Len) --> !, all_one(List). % all candidates must be in the set

b_to_cnf_geq3(Nr,_List,Len) --> {Nr > Len}, !, [[]]. % contradiction

b_to_cnf_geq3(1,List,_) --> !, at_least_one(List).

b_to_cnf_geq3(Nr,List,Len) --> {K is 1+Len-Nr}, no_k_false_at_same_time(List,K),!.

b_to_cnf_leq3(Nr,_List,Len) --> {Nr >= Len}, !, []. % tautology, TODO: register List

b_to_cnf_leq3(Nr,List,Len) --> {Nr is Len-1}, !, at_least_one_false(List).

b_to_cnf_leq3(Nr,List,_) --> {K is Nr+1}, no_k_true_at_same_time(List,K),!.

b_to_cnf_less_aux(A,B,State) --> % card(A) < B
    { get_integer(B,Card), get_card_as_sat_list(A,State,List), C1 is Card-1 },
    !,
    b_to_cnf_card_less_equal(C1,List).

b_to_cnf_less_aux(A,B,State) --> % A < card(B)
    { get_integer(A,Card), get_card_as_sat_list(B,State,List), C1 is Card+1 },
    !,
    b_to_cnf_card_greater_equal(C1,List).

b_to_cnf_less_aux(A,B,_,_,_) :-
    add_translation_failure('Cannot convert inequality to SAT variable: ',b(less(A,B),pred,[])).

b_to_cnf_less_equal_aux(A,B,State) --> % card(A) <= B
    { get_integer(B,Card), get_card_as_sat_list(A,State,List) },
    !,
    b_to_cnf_card_less_equal(Card,List).

b_to_cnf_less_equal_aux(A,B,State) --> % A =< card(B)
    { get_integer(A,Card), get_card_as_sat_list(B,State,List) },
    !,
    b_to_cnf_card_greater_equal(Card,List).

b_to_cnf_less_equal_aux(A,B,_,_,_) :-
    add_translation_failure('Cannot convert inequality to SAT variable: ',b(less_equal(A,B),pred,[])).

b_to_cnf_val_aux(X,_) --> {X==pred_true}, !, backend_truth.

b_to_cnf_val_aux(X,_) --> {X==pred_false}, !, backend_falsity.

b_to_cnf_val_aux(X,Name) --> {var(X)},!, backend_sat_variable(VarForSatSolver),
    {get_corresponding_var(X,VarForSatSolver), %print(attaching_b2cnf(X,_Name,VarForSatSolver)),nl,
    bind_corresponding_var(X,Name,VarForSatSolver)}.

b_to_cnf_val_aux(X,Name) -->
    {add_error(b_to_cnf,'Variable has non-ground non-boolean value:',X,Name)},
    [[1]].

b_to_cnf_wf(Pred,State,Out,WF) :-
    empty_avl(Ai),
    conjunction_to_list(Pred,List),
    %set_prolog_flag(profiling, on),
    l_b_to_cnf_wf(List,State,WF,Ai,_,Out,[]). %, set_prolog_flag(profiling, off), print_profile.

backend_falsity --> [[2]]. % literal 2 stands for false

backend_sat_variable(VarForSatSolver) --> [[VarForSatSolver]].

backend_truth --> [[1]]. % literal 1 stands for truth

bind_corresponding_var(X,Name,VarForSatSolver) :- var(VarForSatSolver),
    %format('Instantiated B variable for ~w: ~w --> SAT: ~w~n',[Name,X,VarForSatSolver]),
    !,
    (X=pred_true -> VarForSatSolver=pred_true
    ; X=pred_false -> VarForSatSolver=pred_false
    ; add_error(bind_corresponding_var,'Illegal B value: ',Name:X)
).

bind_corresponding_var(X,_,VarForSatSolver) :-
    (integer(VarForSatSolver) -> true % this happens in numbervars when numbering literals; will be backtracked
    ; X=VarForSatSolver).

encode_k_true_at_same_time([],LastRow,_,LastRow) --> [].

encode_k_true_at_same_time([X1|T],LastRow,K,FinalRow) -->
    gen_new_row(LastRow,0,NewRow,X1,1,K),
    encode_k_true_at_same_time(T,NewRow,K,FinalRow).

expand_let_predicate(Ids,Exprs,Body,exists(Ids,NewBody)) :-
    generate_let_equality_pred(Ids,Exprs,EqPreds),
    append(EqPreds,[Body],AllPreds),
    conjunct_predicates(AllPreds,NewBody).

expand_set_to_sat_variable_list(b(comprehension_set(Paras,Body),_,Info),State,SatVarList) :-
    % write('CARD FOR: '),translate:print_bexpr(Body),nl,
    instantiate_card_quantifier(Paras,Body, Info, ListOfCandidates),
    %we have to ensure that disjunct in expansion corresponds really to one possible distinct candidate!
    % :sat f:1..n --> BOOL & n=3 & f(1)=TRUE & !i.(i:2..n => f(i) /= f(i-1)) & card({i|i:1..3 & (f(i)=TRUE or i=1)})=3
    (maplist(b_disj_create_one_sat_var(State),ListOfCandidates,CNFList)
    -> SatVarList=CNFList % ,write(list(CNFList)),nl
    ; add_error(b_to_cnf,'Cannot convert comprehension set body to single clause:',Body,Info),fail
).

gen_impl_clause(Xi,PrevSatVar,NewSatVar) --> {PrevSatVar==0},!, {negate_lit(Xi,NXi)},
    [[NXi,NewSatVar]].

gen_impl_clause(Xi,PrevSatVar,NewSatVar) -->
    {negate_lit(Xi,NXi),negate_lit(PrevSatVar,NP)},
    [[NXi,NP,NewSatVar]]. % if Xi is true and we have reached k-1 in last row we reach k now

gen_new_row([],PrevSatVar,NewRow,Xi,Nr,K) --> {Nr =< K},!,
    {NewRow = [NewSatVar]}, % this row has one more sat variable than before
    gen_impl_clause(Xi,PrevSatVar,NewSatVar).

gen_new_row([],_,[],_,_,_) --> [].

gen_new_row([SatVar|LastRowT],PrevSatVar,[NewSatVar|NewRowT],Xi,Nr,K) -->
    % NewSatVar: we have reached at least Nr 1s up to current row
    {negate_lit(SatVar,NegSatVar)},
    [[NegSatVar,NewSatVar]], % if we have reached Nr Elements in previous row then NewSatVar is also true
    gen_impl_clause(Xi,PrevSatVar,NewSatVar),
    {N1 is Nr + 1},
    gen_new_row(LastRowT,SatVar,NewRowT,Xi,N1,K).

generate_let_equality_pred([],[],[]).

generate_let_equality_pred([ID|T],[Exp|TE],[EqPred|TR]) :-
    EqPred = b(equal(ID,Exp),pred,[]), % TO DO: update WD info
    generate_let_equality_pred(T,TE,TR).

get_boolean_value(b(V,boolean,_),Value) :- getv_aux(V,Value).

get_card_as_sat_list(b(card(Set),integer,_),State,List) :- expand_set_to_sat_variable_list(Set,State,List).

get_corresponding_var(BVar,CorrespondingVar) :-
    get_attr(BVar,b_to_cnf,corresponding_sat_var(CorrespondingVar)), !.

get_corresponding_var(BVar,CorrespondingVar) :-
    put_attr(BVar,b_to_cnf,corresponding_sat_var(CorrespondingVar)).

get_instantiation_options(Options) :-
    Options = [instantiate_quantifier_limit(QLIM),instantiate_deferred_sets,
    expansion_time_out(XTO),
    instantiate_precisely_only],
    % precise instantiation ensures we can make use of e.g. symmetry breaking constraints during expansion
    get_preference(solver_strength,SS),
    QLIM is 15000+SS*100,
    XTO is 100 + SS.

getv_aux(value(Value),Value).

getv_aux(boolean_true,pred_true).

getv_aux(boolean_false,pred_fakse).

instantiate_card_quantifier(TIDs,LHS,Info,Bodies) :-
    get_instantiation_options(Options),
    instantiate_exists_to_list(TIDs,LHS,Info,Options,Bodies).

instantiate_quantifier(Quant,Info,Expansion,_State) :-
    %tools:start_ms_timer(T1),
    % we could pass reference_state(State) option for compiling
    get_instantiation_options(Options),
    instantiate_quantifiers(Options, b(Quant,pred,Info), Expansion).

is_quantifier(exists(_,_)).

is_quantifier(forall(_,_,_)).

is_quantifier2(exists(_,b(_,_,Span)),Span).

is_quantifier2(forall(_,b(_,_,Span),_),Span).

join_clauses([],_) --> [].

join_clauses([Clause1|T],Clauses2) --> join_clauses2(Clause1,Clauses2), join_clauses(T,Clauses2).

join_clauses2(_,[]) --> [].

join_clauses2(Clause1,[Clause2|T]) --> {append(Clause1,Clause2,NewClause)}, [NewClause], join_clauses2(Clause1,T).

l_b_to_cnf_wf([],_,_WF,A,A) --> [].

l_b_to_cnf_wf([Pred|T],State,WF,Ai,Ao) -->
    b_pred_to_cnf_wf(Pred,State,WF,Ai,A2,sat),!,
    l_b_to_cnf_wf(T,State,WF,A2,Ao).

l_b_to_cnf_wf([Pred|T],State,WF,Ai,Ao) -->
    b_pred_to_cnf_wf(Pred,State,WF,Ai,A2,prob),
    l_b_to_cnf_wf2(T,State,WF,A2,Ao).

l_b_to_cnf_wf2([],_,_WF,A,A) --> [].

l_b_to_cnf_wf2([Pred|T],State,WF,Ai,Ao) -->
    {b_optimize(Pred,State,NewPred,WF)}, % optimize potentially useful as we executed a predicate to the left by ProB
    b_pred_to_cnf_wf(NewPred,State,WF,Ai,A2,_),
    l_b_to_cnf_wf2(T,State,WF,A2,Ao).

lookup_id(Name,State,Value) :-
    (member(bind(Name,Val),State) -> Value=Val
    ; add_error_fail(b_to_cnf,'Cannot find identifier in state:',Name),fail).

negate_lit(V,Res) :- var(V),!, Res=neg(V).

negate_lit(neg(V),Res) :- !, Res=V.

negate_lit(1,Res) :- !, Res=2. % true -> false

negate_lit(2,Res) :- !, Res=1. % false -> true

negate_lit(Lit,_) :- add_translation_failure('Cannot negate literal: ',Lit).

negate_op(not_equal(A,B),equal(A,B)).

negate_op(less_equal(A,B),greater(A,B)).

negate_op(less(A,B),greater_equal(A,B)).

negate_op(greater(A,B),less_equal(A,B)).

negate_op(greater_equal(A,B),less(A,B)).

negate_pred(B,NotB) :- create_texpr(negation(B),pred,[],NotB).

no_k_false_at_same_time(List,K) -->
    {maplist(negate_lit,List,NList)},
    no_k_true_at_same_time(NList,K).

no_k_true_at_same_time(List,K) -->
    encode_k_true_at_same_time(List,[],K,LastRow),
    % LastRow contains Sat variables which indicate whether a given cardinality was reached in the entire list
    {last(LastRow,LastSatVar)},
    [[neg(LastSatVar)]]. % this stipulates that cardinality K was not reached

simplify_equality(b(value(V1),T,I1),b(value(V2),T,I2),TS1,TS2) :-
    simplify_value_equality(V1,V2,T,Change,S1,S2,NewT),
    Change==change,
    !,
    TS1=b(value(S1),NewT,I1),
    TS2=b(value(S2),NewT,I2).

simplify_value_equality(V1,V2,T,_,R1,R2,NewT) :- (var(V1);var(V2)),!, R1=V1, R2=V2, NewT=T.

simplify_value_equality((A1,B1),(A2,B2),couple(_,TB),change,R1,R2,NewT) :-
    A1==A2,!,
    simplify_value_equality(B1,B2,TB,_,R1,R2,NewT).

simplify_value_equality((A1,B1),(A2,B2),couple(TA,_),change,R1,R2,NewT) :-
    B1==B2,!,
    simplify_value_equality(A1,A2,TA,_,R1,R2,NewT).

simplify_value_equality(V1,V2,T,_,V1,V2,T).