kernel_equality

and_equality(X,Y,Res) :-
    ( X==pred_true -> Res=Y
    ; X==pred_false -> Res=pred_false
    ; Y==pred_true -> Res=X
    ; Y==pred_false -> Res=pred_false
    ; Res==pred_true -> X=pred_true, Y=pred_true
    ; Res==pred_false -> and_equality2(X,Y,Res) % we know that one of X,Y must be pred_false; if X==Y we could infer X=Y=pred_false
    ; add_error_fail(and_equality,'Illegal call: ',and_equality(X,Y,Res))
).

and_equality2(X,Y,Res) :-
    ( X==pred_true -> Res=Y
    ; X==pred_false -> Res=pred_false
    ; Y==pred_true -> Res=X
    ; Y==pred_false -> Res=pred_false
    ; add_error_fail(and_equality,'Illegal call: ',and_equality2(X,Y,Res))
).

bin_eq_atomic(X,Y,Res,V1,V2) :- nonvar(Res),!,
    %print(forcing_bin_eq_atomic(X,Y,Res,V1,V2)),nl,
    (Res=pred_true -> X=Y
    ; %print(bin_dif(X,Y)),nl,
    (X=V1,Y=V2 ; X=V2,Y=V1)
). % difference with eq_atomic: we now know the value !

bin_eq_atomic(X,Y,Res,_,_) :-
    %print(triggering_bin_eq(X,Y,Res)), translate:print_frozen_info(Res),nl,
    (X==Y -> Res=pred_true ; Res=pred_false).

block_eq_cons_avl_set(A,H1,T1,Res,_,WF) :- Res==pred_true,!,
    kernel_objects:equal_custom_explicit_set_cons_wf(avl_set(A),H1,T1,WF).

block_eq_cons_avl_set(A,H1,T1,Res,_,WF) :-
    element_can_be_added_or_removed_to_avl(H1),!, % should hopefully be true as H1 is now ground
    (remove_element_from_explicit_set(avl_set(A),H1,RA)
    -> equality_objects_with_expansion(T1,RA,Res,WF) %%% PROBLEM: T1 has to be in list form !
    ; Res = pred_false
).

block_eq_cons_avl_set(A,H1,T1,Res,_,WF) :-
    % TO DO: we could call propagate_avl_element_information(X,AVL,ApproxSize,WF) if Res=pred_true and with WF or something similar higher up to detect when an element cannot be within the AVL set
    expand_custom_set_wf(avl_set(A),ExpSet,block_eq_cons_avl_set,WF),
    eq_cons1(ExpSet,H1,T1,Res,WF).

bool_dif(A,B) :- bool_pred:negate(A,B).

call_check_element_of_wf0(X,Set,WF) :- get_wait_flag0(WF,WF0),
    kernel_mappings:check_element_of_wf0(X,Set,WF,WF0,unknown).

cartesian_pair_test_wf((X,Y),XType,YType,Res,WF) :- check_cartesian_pair1(X,XType,Y,YType,Res,WF).

check_and_remove(Set,ElementToRemove,ResultingSet,Res) :-
    check_and_remove_wf(Set,ElementToRemove,ResultingSet,Res,no_wf_available).

check_and_remove2(pred_true, _H,T,_ElementToRemove,T,successful,_).

check_and_remove2(pred_false,H,T,ElementToRemove,[H|RT],Res,WF) :-
    check_and_remove_wf(T,ElementToRemove,RT,Res,WF).

check_and_remove_wf([],_,ResultingSet,Res,_) :- !, ResultingSet=[],Res=not_successful.

check_and_remove_wf([H|T],ElementToRemove,ResultingSet,Res,WF) :- !,
    equality_objects_wf_no_enum(H,ElementToRemove,RH,WF),
    %%print(equality_objects_result(H,ElementToRemove,RH)),nl,
    check_and_remove2(RH,H,T,ElementToRemove,ResultingSet,Res,WF).

check_and_remove_wf(CS,ElementToRemove,ResultingSet,Res,WF) :-
    expand_custom_set_to_list_wf(CS,ESet,_,check_and_remove,WF),
    check_and_remove_wf(ESet,ElementToRemove,ResultingSet,Res,WF).

check_cartesian_pair1(X,XType,Y,YType,Res,WF) :-
    ((var(X),nonvar(Y)) -> check_cartesian_pair2(Y,YType,X,XType,Res,WF)
    ; check_cartesian_pair2(X,XType,Y,YType,Res,WF)).

check_cartesian_pair2(X,XType,Y,YType,Res,WF) :- prop_pred_true(Res,MemResX),
    membership_test_wf(XType,X,MemResX,WF),
    ((var(MemResX), is_definitely_maximal_set(YType)) % TO DO: maybe actually also call membership_test_wf
    -> Res=MemResX
    ; check_cartesian_pair3(MemResX,Y,YType,Res,WF)).

check_cartesian_pair3(pred_true,Y,YType,Res,WF) :- membership_test_wf(YType,Y,Res,WF).

check_cartesian_pair3(pred_false,_Y,_YType,pred_false,_WF).

check_less_than_equal_inf(Low1,_,Res) :- Low1==minus_inf,!,Res=pred_true.

check_less_than_equal_inf(_,Low2,Res) :- Low2==inf,!,Res=pred_true.

check_less_than_equal_inf(Low1,_,Res) :- Low1==inf,!,Res=pred_false.

check_less_than_equal_inf(_,Low2,Res) :- Low2==minus_inf,!,Res=pred_false.

check_less_than_equal_inf(X,Y,Res) :- check_less_than_equal(X,Y,Res).

conjoin_test(A,B,AB,WF) :-
    conjoin(A,B,AB,b(truth,pred,[conjoin_test]),b(truth,pred,[conjoin_test]),WF).

cons_el_of(HX_EQRES,T,X,MEMRES,WF) :- var(HX_EQRES),!, %print(cons_el_of(HX_EQRES,T,X,MEMRES)),nl,
    (MEMRES=pred_false -> HX_EQRES=pred_false, /* otherwise element of set */
    membership_not_el(T,X,WF)
    % MEMRES must be pred_true
    ; (T==[] -> %print(forcing_cons_el_of(T,X,MEMRES)),nl,
    HX_EQRES=pred_true
    ; cons_el_of_mem_obj(HX_EQRES,T,X,WF)) /* we have to wait for result of comparison with X */
).

cons_el_of(pred_true,_,_,pred_true,_WF).

cons_el_of(pred_false,T,X,Res,WF) :-
    (Res==pred_true -> non_empty_chk(T) ; true),
    membership_test_wf(T,X,Res,inner,WF).

cons_el_of_mem_obj(pred_true,_,_,_WF).

cons_el_of_mem_obj(pred_false,T,X,WF) :-
    % Instantiation of T will be done by membership_test_wf, relevant for test 1273
    membership_test_wf(T,X,pred_true,inner,WF).

delay_check_pred_false(pred_false).

dif(boolean,A,B) :- !,
    bool_pred:negate(A,B). % was: bool_dif(A,B).

dif(integer,A,B) :- !, integer_dif(A,B).

dif(global(T),A,B) :- !, neq_fd(A,B,T).

dif(_,A,B) :- dif(A,B).

empty_cartesian_product_wf(Set1,Set2,EqRes,WF) :- % TO DO: pass WF
    eq_empty_set_wf(Set1,EqRes1,WF),
    (EqRes1==pred_true -> EqRes=pred_true /* avoid inspecting Set2 */
    ; or_eq_obj(EqRes1,EqRes2,EqRes),
    eq_empty_set_wf(Set2,EqRes2,WF)).

empty_set_test(Set,EqRes) :- eq_empty_set_attr_wf(Set,EqRes,no_wf_available).

empty_set_test_wf(Set,EqRes,WF) :- eq_empty_set_attr_wf(Set,EqRes,WF).

enum_equality_result_smt_mode_wf(Res,PP,WF) :- var(Res),
    preferences:preference(use_smt_mode,true),!,
    enum_equality_result_wf(Res,PP,WF).

enum_equality_result_smt_mode_wf(_,_,_).

enum_equality_result_wf(Res,PP,WF) :-
    get_last_wait_flag(PP,WF,LWF),
    force_equality_result(Res,LWF).

eq_atomic(X,Y,_Type,Res) :- nonvar(X),nonvar(Y),!,
    (X=Y -> Res=pred_true ; Res=pred_false).

eq_atomic(X,Y,_,Res) :- % check for attached dif co-routines; later we should probably use CHR
    frozen_dif(X,Y),!, Res=pred_false.

eq_atomic(X,Y,Type,Res) :- when((?=(X,Y);nonvar(Res)),eq_atomic2(X,Y,Type,Res)).

eq_atomic2(X,Y,Type,Res) :- nonvar(Res),!,
    (Res=pred_true -> X=Y ; dif(Type,X,Y)).

eq_atomic2(X,Y,_Type,Res) :-
    (X=Y -> Res=pred_true
    ; Res=pred_false).

eq_atomic_simple(X,Y,Type,Res) :- when((?=(X,Y);nonvar(Res)),eq_atomic2(X,Y,Type,Res)).

eq_cons([],_,_,Res,_) :- !, Res=pred_false.

eq_cons([H2|T2],H1,T1,Res,WF) :- !, % T2==[] checked? TODO: call eq_singleton_set_cons
    check_and_remove_wf([H2|T2],H1,NewSet2,RemoveSuccesful,WF),
    %% print(removed(H1,H2,T2,NewSet2,RemoveSuccesful)),
    eq_cons2(RemoveSuccesful,H1,T1,H2,T2,NewSet2,Res,WF).

eq_cons(avl_set(A),H1,T1,Res,WF) :- !,
    eq_cons_avl_set(A,H1,T1,Res,WF).

eq_cons(global_set(G),_H,T,Res,WF) :- %print(chk(G,H,T)),nl,
    is_infinite_global_set(G,_),!,
    expand_custom_set_to_list_wf(T,_ET,_Done,eq_cons,WF), % this will either succeed and we have a finite list ; or it will raise an enumeration warning exception
    Res = pred_false.

eq_cons(ES,H1,T1,Res,WF) :- is_custom_explicit_set(ES,eq_cons),
    expand_custom_set_wf(ES,ExpSet,eq_cons,WF),
    eq_cons1(ExpSet,H1,T1,Res,WF).

eq_cons1(ExpSet,H1,T1,Res,WF) :- eq_cons(ExpSet,H1,T1,Res,WF).

eq_cons2(RemoveSuccesful, H1,T1,H2,T2, _NewSet2,Res,WF) :- var(RemoveSuccesful),!,
    % result has been instantiated before Remove finished; now force equal_object or not_equal_object
    % note: without this the remove could be pending (see test 1112, 1105)
    % TO DO: look whether we could force remove and continue from there ?
    equality_objects2([H1|T1],[H2|T2],Res,WF).

eq_cons2(not_successful, _,_T1,_,_, _NewSet2,pred_false,_).

eq_cons2(successful, _, T1,_,_, NewSet2,Res,WF) :- equality_objects_wf_no_enum(T1,NewSet2,Res,WF).

eq_cons_avl_set(A,H1,T1,Res,WF) :- is_one_element_avl(A,AEl),
    !,
    eq_singleton_set_cons(AEl,H1,T1,Res,WF).

eq_cons_avl_set(A,H1,T1,Res,WF) :-
    (var(Res) -> kernel_tools:ground_value_check(H1,GrH1) ; true), % if Res already bound, no need to do ground check
    block_eq_cons_avl_set(A,H1,T1,Res,GrH1,WF).

eq_empty_set_attr_wf(Set,PredRes,WF) :- var(PredRes), var(Set),!,
    get_empty_set_attr(Set,PredRes,ExistsAlready), % get attribute or create one if it does not exist
    (ExistsAlready=is_empty_attr_exists
    -> true % no need to compute the predicate; another call will already do it
    ; eq_empty_set_wf(Set,PredRes,WF)).

eq_empty_set_attr_wf(X,R,WF) :- eq_empty_set_wf(X,R,WF).

eq_empty_set_wf(X,R,WF) :- var(X),!,
    (R=pred_true -> empty_set_wf(X,WF) ; not_empty_set_wf(X,WF)).

eq_empty_set_wf([],R,_) :- !,R=pred_true.

eq_empty_set_wf([_|_],R,_) :- !,R=pred_false.

eq_empty_set_wf(CS,R,WF) :- is_custom_explicit_set(CS,eq_empty_set_wf),!,
    test_empty_explicit_set_wf(CS,R,WF).

eq_empty_set_wf(S,R,WF) :-
    (S==term(undefined)
    -> add_error_wf(eq_empty_set_wf,'Accessing uninitialised set value','',unknown,WF)
    ; add_internal_error('Illegal Set: ',eq_empty_set_wf(S,R,_))
    ),fail.

eq_singleton2(H2,H1,T1Empty,Res,WF) :- T1Empty==pred_true,!,
    equality_objects_wf_no_enum(H2,H1,Res,WF).

eq_singleton2(_,_,T1Empty,Res,_) :- T1Empty==pred_false,!,
    Res=pred_false. % if T1 is not empty, [H1|T1] is different from [H2]

eq_singleton2(H2,H1,T1Empty,Res,WF) :- Res==pred_true,!,T1Empty=pred_true,
    equal_object_wf(H2,H1,eq_singleton2,WF).

eq_singleton2(H2,H1,T1Empty,Res,WF) :- Res==pred_false,!,
    when(nonvar(T1Empty),eq_singleton2(H2,H1,T1Empty,Res,WF)).

eq_singleton_set_cons(H2,H1,T1,Res,WF) :- T1==[], !, equality_objects_wf_no_enum(H2,H1,Res,WF).

eq_singleton_set_cons(H2,H1,T1,Res,WF) :- empty_set_test_wf(T1,T1Empty,WF),
    % TODO: we could also call equality_objects(H2,H1,H2H1Eq) if T1Empty is not known and conjoin it
    eq_singleton2(H2,H1,T1Empty,Res,WF).

eq_term_wf(TX,TY,Res,_WF) :- nonvar(TX),TX = floating(FX),!,
    TY=floating(FY), eq_atomic(FX,FY,real,Res). % TODO: use a proper equality check for reals/floats

eq_term_wf(TY,TX,Res,_WF) :- nonvar(TX),TX = floating(FX),!,
    TY=floating(FY), eq_atomic(FX,FY,real,Res).

eq_term_wf(TX,TY,Res,_) :- eq_atomic(TX,TY,term,Res).

equality_can_be_decided_by_unification(V) :- var(V),!,fail.

equality_can_be_decided_by_unification(pred_false).

equality_can_be_decided_by_unification(pred_true).

equality_can_be_decided_by_unification(int(N)) :- integer(N).

equality_can_be_decided_by_unification(string(S)) :- atom(S).

equality_can_be_decided_by_unification(fd(N,GS)) :- atom(GS),integer(N).

equality_can_be_decided_by_unification((A,B)) :-
    equality_can_be_decided_by_unification(A),equality_can_be_decided_by_unification(B).

equality_fd_objects(X,Y,_,Res) :- number(X),number(Y),!,
    (X=Y -> Res=pred_true ; Res= pred_false).

equality_fd_objects(X,Y,_,Res) :- % check for attached dif co-routines; later we should probably use CHR
    fd_frozen_dif(X,Y),!,
    % THIS DROPS THE PERFORMANCE OF probsli ../prob_examples/examples/B/ClearSy/alloc_large.mch -init -p TIME_OUT 5000
    Res=pred_false.

equality_fd_objects(X,Y,Type,Res) :-
    nonvar(Type),b_global_sets:b_get_fd_type_bounds(Type,LowBnd,UpBnd),!,
    (LowBnd=UpBnd
    -> X=Y,Res=pred_true /* only one object of Type exists */
    ; LB1 is LowBnd+1,
    (LB1 = UpBnd
    -> bin_eq_atomic(X,Y,Res,LowBnd,UpBnd) /* two objects exist */
    ; eq_atomic_simple(X,Y,global(Type),Res),
    (var(Res),(var(X);var(Y))
    -> clpfd_in_domain(X,LowBnd,UpBnd), % just like X in LowBnd..UpBnd but can deal with UpBnd=inf
    clpfd_in_domain(Y,LowBnd,UpBnd),
    % still required ! even with fd_utils_clpfd ! (for v8 of Bosch CrCtl_Comb2_Final_mch.eventb)
    equality_fd(X,Y,Res)
    ; true
)
)
).

equality_fd_objects(X,Y,Type,Res) :-
    add_internal_error('Unknown type: ',equality_fd_objects(X,Y,Type,Res)),
    eq_atomic_simple(X,Y,global(Type),Res).

equality_fields([],[],pred_true,_).

equality_fields([field(Name1,V1)|T1],[field(Name2,V2)|T2],Res,WF) :-
    % should we wait for Name1 or Name2 to become nonvar?
    check_field_name_compatibility(Name1,Name2,equality_fields),
    and_equality(RH,RT,Res),
    equality_objects_wf_no_enum(V1,V2,RH,WF),
    (RH==pred_false -> true
    ; equality_fields(T1,T2,RT,WF)).

equality_freeval_content(pred_false,_Value1,_Value2,_,_).

equality_freeval_content(pred_true,Value1,Value2,Res,WF) :-
    % if we do not wait until we now that the case is the same,
    % an internal type error might be raised
    equality_objects_wf_no_enum(Value1,Value2,Res,WF).

equality_int(X,Y,Res) :- nonvar(X),nonvar(Y),!,
    (X=Y -> Res=pred_true ; Res=pred_false).

equality_int(X,Y,Res) :-
    % check for attached dif co-routines; diabled if CHR is used (no dif coroutine needed)
    % !! there might still be dif coroutines set up by equality_expr and dis
    % preferences:preference(use_chr_solver,false),
    fd_frozen_dif(X,Y),!, Res=pred_false.

equality_objects(X,Y,R) :- equality_objects_wf_no_enum(X,Y,R,no_wf_available).

equality_objects0(X,Y,R,WF) :- nonvar(R),!, % we know the result of the comparison
    ( R=pred_true -> equal_object_wf(X,Y,equality_objects0,WF)
    ; R=pred_false -> not_equal_object_wf(X,Y,WF)
    ; add_error_fail(equality_objects0,'Illegal result: ',equality_objects0(X,Y,R,WF))
).

equality_objects0(X,Y,R,WF) :-
    (nonvar(Y)
    -> (X==[] -> eq_empty_set_wf(Y,R,WF)
    ; equality_objects1(Y,X,R,WF)
    )
    ; equality_objects1(X,Y,R,WF)
).

equality_objects1(pred_true /* bool_true */,X,Res,_WF) :- !,
    X=Res. % equivalent to bool_equality(pred_true /* bool_true */,X,Res).

equality_objects1(pred_false /* bool_false */,X,Res,_WF) :- !,
    bool_pred:negate(X,Res). % equivalent to bool_equality(pred_false /* bool_false */,X,Res).

equality_objects1(int(X),IY,Res,_WF) :- !, IY=int(Y), equality_int(X,Y,Res).

equality_objects1(term(X),TY,Res,WF) :- !, TY=term(Y), eq_term_wf(X,Y,Res,WF).

equality_objects1(string(X),SY,Res,_WF) :- !, SY=string(Y), eq_atomic(X,Y,string,Res).

equality_objects1(fd(X,Type),FY,Res,_WF) :- !,
    b_global_sets:get_global_type_value(FY,Type,Y),
    equality_fd_objects(X,Y,Type,Res).

equality_objects1(freeval(Id,Case1,Value1),FY,Res,WF) :- !, FY=freeval(Id,Case2,Value2),
    (nonvar(Id), freetype_with_single_case(Id,Case)
    -> (Case,Case)=(Case1,Case2), % cases must match
    equality_objects_wf_no_enum(Value1,Value2,Res,WF)
    ; and_equality(CaseRes,ValueRes,Res),
    eq_atomic(Case1,Case2,freeval_case,CaseRes),
    equality_freeval_content(CaseRes,Value1,Value2,ValueRes,WF),
    (var(Id) -> instantiate_freetype_case(Id,Case1,Case2) ; true)
).

equality_objects1(rec(X),RY,Res,WF) :- !, RY=rec(Y), equality_fields(X,Y,Res,WF).

equality_objects1((X,Y),XY2,Res,WF) :- !, XY2=(X2,Y2),
    equality_objects_wf_no_enum(X,X2,RX,WF),
    and_equality(RY,RX,Res), % typically Res is var, hence it is better to call and_equality after X
    (RX==pred_false -> true
    ; equality_objects_wf_no_enum(Y,Y2,RY,WF)).

equality_objects1([],S,R,WF) :- !,eq_empty_set_wf(S,R,WF).

equality_objects1(X,Y,R,WF) :- equality_objects2(X,Y,R,WF).

equality_objects2(X,Y,Res,WF) :- nonvar(Res),!,% we know the result of the comparison
    ( Res=pred_true -> %% print(forcing_equal(X,Y)),nl,
    equal_object_wf(X,Y,equality_objects2_1,WF)
    ; Res=pred_false -> not_equal_object_wf(X,Y,WF)
    ; add_error_fail(equality_objects2,'Illegal result: ',equality_objects2(X,Y,Res,WF))
).

equality_objects2([H|T],S,Res,WF) :- !,eq_cons(S,H,T,Res,WF). % move to equality_objects1 ?!

equality_objects2(avl_set(A),S,Res,WF) :-
    (S=[H|T] -> !, eq_cons(avl_set(A),H,T,Res,WF)
    ; S = [] -> !, (A=empty -> add_warning(equality_objects2,'Empty avl_set'), Res=pred_true
    ; Res=pred_false)).

equality_objects2(ES1,ES2,Res,WF) :-
    equality_explicit_sets_wf(ES1,ES2,ERes,WF), !,
    Res=ERes.

equality_objects2(ES1,S,Res,WF) :- is_custom_explicit_set(ES1,eq_cons),!, % move to custom_explicit_sets?
    % S = [] or ES1 = [] is already covered above
    (S=[H|T] -> eq_cons(ES1,H,T,Res,WF) % maybe we can avoid expanding ES1
    ; is_infinite_explicit_set(ES1),is_custom_explicit_set(S,eq_cons)
    -> expand_custom_set_wf(S,ExpSet,equality_objects2,WF),
    equality_objects0(ExpSet,ES1,Res,WF)
    ; expand_custom_set_wf(ES1,ExpSet,equality_objects2,WF), equality_objects0(ExpSet,S,Res,WF)
).

equality_objects2(X,Y,Res,WF) :-
    add_internal_error('Unknown objects:',equality_objects2(X,Y,Res,WF)), % could happen with abort(.) terms ?
    (equal_object_wf(X,Y,equality_objects2_2,WF),Res=pred_true
    ;
    not_equal_object_wf(X,Y,WF),Res=pred_false
).

equality_objects_block_wf(X,Y,R,WF) :-
    equality_objects0(X,Y,R,WF).

equality_objects_lwf(X,Y,Res,LWF,WF) :-
    equality_objects_wf_no_enum(X,Y,Res,WF),
    force_equality_objects_lwf2(X,Y,Res,LWF).

equality_objects_wf(X,Y,Res,no_wf_available) :- !,
    equality_objects(X,Y,Res).

equality_objects_wf(X,Y,Res,WF) :-
    equality_objects_lwf(X,Y,Res,LWF,WF),
    (var(Res) -> get_last_wait_flag(equality_objects_wf,WF,LWF) ; true).

equality_objects_wf_no_enum(X,Y,R,WF) :-
    (X==Y % could be expensive for long lists
    -> R=pred_true
    ; equality_objects_block_wf(X,Y,R,WF)).

equality_objects_with_expansion(X,Y,R,WF) :-
    nonvar(Y), is_custom_explicit_set_nonvar(Y),!,
    expand_custom_set_wf(Y,ExpSet,equality_objects_with_expansion,WF),
    equality_objects_wf_no_enum(X,ExpSet,R,WF).

equality_objects_with_expansion(X,Y,R,WF) :-
    equality_objects_wf_no_enum(X,Y,R,WF).

equality_objects_with_type_wf(boolean,X,Y,R,_) :- !, bool_pred:bool_equality(X,Y,R).

equality_objects_with_type_wf(_,X,Y,R,WF) :-
    (X==Y -> R=pred_true ; equality_objects_block_wf(X,Y,R,WF)).

force_equality_int_clpfd(_X,_Y,Res) :- %print(try_force_equality_int_clpfd(Res,_X,_Y)),nl,
    catch_clpfd_overflow_call3(Res=pred_true,silent,Overflow=true),
    (Overflow==true
    -> !, debug_println(19,'Not forcing equality to true due to CLPFD overflow') % hope that enumeration will work
    ; true).

force_equality_int_clpfd(_X,_Y,Res) :-
    catch_clpfd_overflow_call3(Res=pred_false,message,
    (debug_println(19,'Not forcing equality to false due to CLPFD overflow'),
    delay_check_pred_false(Res))).

force_equality_objects_lwf2(X,Y,Res,LWF) :-
    % tools_printing:print_term_summary(force_equality(X,Y,Res,LWF)),nl,
    ( nonvar(Res) -> true
    ; nonvar(X), X=int(_),
    number(LWF), LWF>= 1152921504606844951, % only catch overflows if equality's priority low
    preferences:preference(use_clpfd_solver,true)
    -> force_equality_int_clpfd(X,Y,Res)
    ; ( % print(forcing_equal(_X,_Y,_LWF)),nl,
    % alternative would be to propagate LWF down to and_equality ?
    %Res \== pred_false, equal_object(X,Y,force_equality_objects_lwf2), % not required anymore as and_equality can propagate pred_true down (commented out 27.2.2015)
    % this can trigger CLPFD overflow; e.g., for x>1 & y:NATURAL & y=x+x & z={y,x}
    Res=pred_true
    ; %Res \== pred_true, not_equal_object(X,Y), % note required anymore (commented out 27.2.2015)
    Res=pred_false
)).

force_equality_result(pred_true,_).

force_equality_result(pred_false,_).

geq_test(X,Y,Res) :- % TO DO: use CHR ?
    ( Res==pred_true -> kernel_objects:less_than_equal_direct(Y,X)
    ; Res==pred_false -> kernel_objects:less_than_direct(X,Y)
    ; X >= Y -> Res=pred_true
    ; Res = pred_false
).

get_cardinality_powset_wait_flag(Set,Info,WF,CardSet,LWF) :-
    cardinality_as_int_for_wf(Set,CardSet),
    get_cardinality_powset_wait_flag2(CardSet,Info,WF,LWF).

get_cardinality_powset_wait_flag2(X,Info,WF,LWF) :-
    safe_pow2(X,X2),
    %safe_mul(X2,10000,X3), % as generating subsets this way will generate repetitions
    (is_inf_or_overflow_card(X2)
    -> integer_pow2_priority(R), get_wait_flag(R,powset_card(Info),WF,LWF)
    ; get_bounded_wait_flag(X2,powset_card(Info),WF,LWF) % finite prio; ensure we do not exceed infinite prios if X2 very large
).

get_cardinality_relation_over_wait_flag(Dom,Ran,WF,LWF,MaxCardOfRel,MaxNrOfRels) :-
    cardinality_as_int_for_wf(Dom,X),
    cardinality_as_int_for_wf(Ran,Y),
    get_cardinality_relation_over_wait_flag2(X,Y,WF,LWF,MaxCardOfRel,MaxNrOfRels).

get_cardinality_relation_over_wait_flag2(X,Y,WF,LWF,MaxCardOfRel,MaxNrOfRels1) :-
    safe_mul(X,Y,MaxCardOfRel),
    safe_pow2(MaxCardOfRel,MaxNrOfRels),
    safe_add_card(MaxNrOfRels,1,MaxNrOfRels1), /* add 1 to give priority to tighter_enum */
    get_bounded_wait_flag(MaxNrOfRels1,powset_rel_card,WF,LWF).

get_cardinality_wait_flag(Set,Info,WF,LWF) :-
    get_cardinality_wait_flag(Set,Info,WF,_Card,LWF).

get_cardinality_wait_flag(Set,Info,WF,Card,LWF) :-
    cardinality_as_int_for_wf(Set,Card),
    % when(nonvar(X), (print(get_card_waitflag(X,Set,WF,LWF)),nl)),
    (var(Card)
    -> kernel_waitflags:get_last_wait_flag(get_cardinality_wait_flag(Info),WF,LastWF)
    ; true), % ensure that we trigger choice points waiting on LWF before infinite enumeration starts
    get_cardinality_wait_flag2(Card,Info,WF,LastWF,LWF).

get_cardinality_wait_flag2(X,_Info,_WF,LastWF,LWF) :- var(X),!,LWF=LastWF.

get_cardinality_wait_flag2(X,Info,WF,_,LWF) :- get_bounded_wait_flag(X,Info,WF,LWF).

ground_list_with_fd(V) :- var(V),!,fail.

ground_list_with_fd([H|T]) :- nonvar(H),ground_val(H),ground_list_with_fd(T).

ground_list_with_fd([]).

ground_val(int(X)) :- number(X).

ground_val(pred_false).

ground_val(pred_true).

ground_val(fd(X,T)) :- number(X),ground(T).

ground_val((A,B)) :- nonvar(A),ground_val(A),ground_value(B).

ground_val(rec(Fields)) :- nonvar(Fields), Fields = [field(Name,V)|TFields], ground(Name),
    ground_val(V),
    ground_value(rec(TFields)).