ast_cleanup_for_smt

assure_single_rules([],_Rule) :- !.

assure_single_rules(AppliedRules,Rule) :-
    assure_single_rules2(AppliedRules,Rule).

assure_single_rules2(_AppliedRules,none) :- !.

assure_single_rules2(AppliedRules,Rule) :-
    \+ member(Rule, AppliedRules).

bmaxint(b(max_int,integer,[])).

bminint(b(min_int,integer,[])).

bone(b(integer(1),integer,[])).

bzero(b(integer(0),integer,[])).

clean_up(Expr,CExprOut,Path,ACOut,IDsOut) :-
    cleanups(pre,Expr,[],TPExpr,Path,ACPre,IDsPre),
    remove_bt(TPExpr,PExpr,LExpr,TLExpr),
    syntaxtransformation(PExpr,Subs,_,NewSubs,LExpr),
    functor(PExpr,F,N),
    % recursively clean up sub-expressions
    maplist(internal_clean_up,ACPre,ACPreClean),
    clean_up_l(Subs,NewSubs,F/N,1,Path,ACL,IDsL),
    maplist(internal_clean_up,ACL,ACLClean),
    cleanups(post,TLExpr,[],CExpr,Path,ACPost,IDsPost),
    maplist(internal_clean_up,ACPost,ACPostClean),
    append([ACPreClean,ACLClean,ACPostClean],AC),
    append([IDsPre,IDsL,IDsPost],IDs),
    (AC \= [], get_texpr_type(CExpr,pred)
    -> combine_pred_and_ac(CExpr,AC,IDs,CExprOut),
    % the accumulator contains additional constraints and new existentially quantified vars IDs
    IDsOut = [], ACOut = []
    ; CExprOut = CExpr, ACOut = AC, IDsOut = IDs).

clean_up_l([],[],_Functor,_Nr,_Path,[],[]).

clean_up_l([Expr|Rest],[CExpr|CRest],Functor,ArgNr,Path,AC,IDs) :-
    clean_up(Expr,CExpr,[arg(Functor,ArgNr)|Path],ACC,IDsC),
    A1 is ArgNr+1,
    clean_up_l(Rest,CRest,Functor,A1,Path,ACL,IDsL),
    append(ACC,ACL,AC),
    append(IDsC,IDsL,IDs).

cleanup_phase(Phase,OTExpr,NTExpr,Mode/Rule,Path,AC,IDs) :-
    create_texpr(OExpr,OType,OInfo,OTExpr),
    create_texpr(NExpr,NType,NInfo,NTExpr),
    cleanup_phase2(Phase,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path,AC,IDs).

cleanup_phase2(pre,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,_Path,AC,IDs) :-
    cleanup_pre(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule,AC,IDs),
    (functor(Mode_Rule,'/',2) -> Mode_Rule = Mode/Rule
    ; add_internal_error('Illegal cleanup_pre rule, missing mode: ',Mode_Rule),fail).

cleanup_phase2(post,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path,AC,IDs) :-
    cleanup_post_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule,Path,AC,IDs),
    (functor(Mode_Rule,'/',2)
    -> Mode_Rule = Mode/Rule %,format(' cleanup_post Rule: ~w/~w~n',[Mode,Rule])
    ; add_internal_error('Illegal cleanup_post rule, missing mode: ',Mode_Rule),fail).

cleanup_post(subset(A,B),pred,I,truth,pred,[was(subset(A,B))|I],multi/remove_type_subset) :-
    is_just_type(B), !.

cleanup_post(member(X,B),pred,I,truth,pred,[was(member(X,B))|I],multi/remove_type_member) :-
    is_just_type(B), !.

cleanup_post(not_member(X,B),pred,I,falsity,pred,[was(not_member(X,B))|I],multi/remove_type_not_member) :-
    is_just_type(B), !.

cleanup_post_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,_Path,[],[]) :-
    cleanup_post(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule).

cleanup_pre(div(A,B),integer,I,div(A,B),integer,[smt_wd_added|I],multi/div_wd,[AC],[]) :-
    \+ member(smt_wd_added,I), !,
    create_texpr(not_equal(B,b(integer(0),integer,[])),pred,[],AC).

cleanup_pre(value(closure(['_zzzz_unary'],T,P)),Type,I,Expr,Type,I,multi/rewrite_prob_closure,[],[]) :-
    replace_prob_closure(closure(['_zzzz_unary'],T,P), Expr).

cleanup_pre(union(A,B),Type,_,reflexive_closure(Rel),Type,I,multi/replace_not_equal,[],[]) :-
    A = b(event_b_identity,_,_),
    B = b(closure(Rel),Type,I).

cleanup_pre(not_equal(A,B),pred,I,negation(Equal),pred,[],multi/replace_not_equal,[],[]) :-
    create_texpr(equal(A,B),pred,I,Equal).

cleanup_pre(not_member(A,B),pred,I,negation(Member),pred,[],multi/replace_not_member,[],[]) :-
    create_texpr(member(A,B),pred,I,Member).

cleanup_pre(not_subset_strict(A,B),pred,I,negation(Subset),pred,[],multi/replace_not_subset_strict,[],[]) :-
    create_texpr(subset_strict(A,B),pred,I,Subset).

cleanup_pre(greater(Card,Integer0),pred,I,Res,pred,I,multi/replace_card_0_with_neq_empty,[],[]) :-
    % card(S) > 0 --> S /= {}
    Card = b(card(Set),integer,_),
    (Integer0 = b(integer(0),integer,_); Integer0 = b(value(int(0)),integer,_)),
    !,
    get_texpr_type(Set, SetType),
    Res = not_equal(Set,b(empty_set,SetType,[])).

cleanup_pre(less(Integer0,Card),pred,I,Res,pred,I,multi/replace_card_0_with_neq_empty,[],[]) :-
    % 0 < card(S) --> S /= {}
    Card = b(card(Set),integer,_),
    (Integer0 = b(integer(0),integer,_); Integer0 = b(value(int(0)),integer,_)),
    !,
    get_texpr_type(Set, SetType),
    Res = not_equal(Set,b(empty_set,SetType,[])).

cleanup_pre(not_equal(Card,Integer0),pred,I,Res,pred,I,multi/replace_card_0_with_neq_empty,[],[]) :-
    % card(S) /= 0 --> S /= {}
    Card = b(card(Set),integer,_),
    (Integer0 = b(integer(0),integer,_); Integer0 = b(value(int(0)),integer,_)),
    !,
    get_texpr_type(Set, SetType),
    Res = not_equal(Set,b(empty_set,SetType,[])).

cleanup_pre(not_equal(Integer0,Card),pred,I,Res,pred,I,multi/replace_card_0_with_neq_empty,[],[]) :-
    % 0 /= card(S) --> S /= {}
    Card = b(card(Set),integer,_),
    (Integer0 = b(integer(0),integer,_); Integer0 = b(value(int(0)),integer,_)),
    !,
    get_texpr_type(Set, SetType),
    Res = not_equal(Set,b(empty_set,SetType,[])).

cleanup_pre(equal(Card,Integer0),pred,I,Res,pred,I,multi/replace_card_0_with_eq_empty,[],[]) :-
    % card(S) = 0 --> S = {}
    Card = b(card(Set),integer,_),
    (Integer0 = b(integer(0),integer,_); Integer0 = b(value(int(0)),integer,_)),
    !,
    get_texpr_type(Set, SetType),
    Res = equal(Set,b(empty_set,SetType,[])).

cleanup_pre(equal(Integer0,Card),pred,I,Res,pred,I,multi/replace_card_0_with_eq_empty,[],[]) :-
    % 0 = card(S) --> S = {}
    Card = b(card(Set),integer,_),
    (Integer0 = b(integer(0),integer,_); Integer0 = b(value(int(0)),integer,_)),
    !,
    get_texpr_type(Set, SetType),
    Res = equal(Set,b(empty_set,SetType,[])).

cleanup_pre(FiniteCardConstraint,pred,I,Res,pred,I,multi/RuleDescr,[],[]) :-
    rewrite_finite_card(FiniteCardConstraint, Res, RuleDescr).

cleanup_pre(member(A,B),pred,I,Out,pred,I,multi/replace_member_interval,[],[]) :-
    is_interval(B,Low,Up),
    !, % A:Low..Up <==> A>=Low & A<=Up % important for e.g. :z3-cns mxint = 500 & goal : -mxint ..mxint
    Out = conjunct(b(greater_equal(A,Low),pred,[]),b(greater_equal(Up,A),pred,[])).

cleanup_pre(member(A,B),pred,I,Out,pred,I,multi/replace_member_pow1_or_fin1,[],[]) :-
    is_pow1_subset(B,Set),
    get_texpr_type(Set, SetType),
    !, % A:POW1(Set) <==> A <: Set & A /= {}
    Out = conjunct(b(subset(A,Set),pred,[]),b(not_equal(A,b(set_extension([]),SetType,[])),pred,[])).

cleanup_pre(member(A,B),pred,I,Out,pred,I,multi/replace_member_pow_or_fin,[],[]) :-
    is_pow_subset(B,Set),
    !, % A:POW(Set) <==> A <: Set
    % A/:POW(Set) <==> A /<: Set ; does not really seem to be necessary as negation rewritten before
    Out = subset(A,Set).

cleanup_pre(member(A,B),pred,I,Disj,pred,I,multi/replace_finite_member_by_disj,[],[]) :-
    % rewrite finite set membership to disjunction of equalities
    B = b(value(avl_set(AvlSet)),set(InnerType),_),
    !,
    avl_to_list(AvlSet, EnumValueList),
    findall(Equality, (member(EnumValue-_, EnumValueList), Equality = b(equal(A,b(value(EnumValue),InnerType,[])),pred,[])), Equalities),
    disjunct_predicates(Equalities, DisjAst),
    DisjAst = b(Disj,_,_).

cleanup_pre(not_subset(A,B),pred,I,negation(Subset),pred,[],multi/replace_not_subset,[],[]) :-
    create_texpr(subset(A,B),pred,I,Subset).

cleanup_pre(subset_strict(A,B),pred,I,conjunct(NotEqual,Subset),pred,[],multi/replace_not_member,[],[]) :-
    create_texpr(subset(A,B),pred,I,Subset),
    create_texpr(not_equal(A,B),pred,I,NotEqual).

cleanup_pre(equal(R,S),pred,I,POut,pred,I,multi/replace_struct_equality,[],[]) :-
    % e.g., rewrite Dom = struct(f1:{1,2},f2:{1,2}) to Dom = {rec(f1:1,f2:1),rec(f1:1,f2:2),rec(f1:2,f2:1),rec(f1:2,f2:2)}
    S = b(value(closure(['_zzzz_unary'],[record(_)],_)),_,_),
    get_texpr_expr(R, identifier(IdName)),
    get_texpr_type(R, set(record(FieldTypes))),
    solver_interface:solve_predicate(b(equal(R,S),pred,I), Bindings, _),
    member(bind(IdName,Set), Bindings),
    % only for finite records
    Set \= closure(_,_,_),
    !,
    POut = equal(R,b(value(Set),set(record(FieldTypes)),[])).

cleanup_pre(member(R,S),pred,I,POut,pred,I,multi/replace_struct_membership,[],[]) :-
    % rewrite ProB closures introduced by b_compile/6
    get_texpr_expr(R,identifier(_)),
    S = b(value(ProBClosure),_,_),
    replace_prob_closure(ProBClosure, ClosureExpr),
    ClosureExpr = struct(Proto),
    Proto = b(value(rec(Fields)),_,_),
    ( maplist(replace_prob_closure_record_field, Fields, TFields)
    -> NFields = TFields
    ; NFields = Fields
    ),
    !,
    maplist(rewrite_struct_ids(R),NFields,Constraints),
    conjunct_predicates(Constraints,Conj),
    get_texpr_expr(Conj,POut).

cleanup_pre(member(R,S),pred,I,POut,pred,I,multi/replace_struct_membership,[],[]) :-
    get_texpr_expr(R,identifier(_)),
    get_texpr_expr(S,struct(Proto)),
    get_texpr_expr(Proto,value(rec(Fields))),
    maplist(rewrite_struct_ids(R),Fields,Constraints),
    conjunct_predicates(Constraints,Conj),
    get_texpr_expr(Conj,POut).

cleanup_pre(member(E,S),pred,I,disjunct(M1,M2),pred,I,multi/split_union_in_member,[],[]) :-
    get_texpr_expr(S,union(S1,S2)),
    create_texpr(member(E,S1),pred,I,M1),
    create_texpr(member(E,S2),pred,I,M2).

cleanup_pre(member(E,S),pred,I,conjunct(M1,M2),pred,I,multi/split_intersection_in_member,[],[]) :-
    get_texpr_expr(S,intersection(S1,S2)),
    create_texpr(member(E,S1),pred,I,M1),
    create_texpr(member(E,S2),pred,I,M2).

cleanup_pre(member(E,S),pred,I,conjunct(M1,NotM2),pred,I,multi/split_set_subtraction_in_member,[],[]) :-
    get_texpr_expr(S,set_subtraction(S1,S2)),
    create_texpr(member(E,S1),pred,I,M1),
    create_texpr(member(E,S2),pred,I,M2),
    create_negation(M2,NotM2).

cleanup_pre(member(E,F),pred,I,C,pred,I,multi/rewrite_member_of_function,[],[]) :-
    %translation_type(axiomatic),
    rewrite_member_of_function(E,F,C).

cleanup_pre(member(E,S),pred,I,C,pred,I,multi/rewrite_member_to_disequalities,[],[]) :-
    get_texpr_type(E,integer),
    get_texpr_type(S,set(integer)),
    rewrite_member_to_ge_le(E,S,C).

cleanup_pre(equal(S,GlobalIntSet),pred,I,C,pred,I,multi/rewrite_equal_to_disequalities,[],[]) :-
    get_texpr_type(S,set(integer)),
    get_texpr_expr(GlobalIntSet,integer_set(_)),
    rewrite_equal_to_ge_le(S,GlobalIntSet,C).

cleanup_pre(subset(Sub,Super),pred,I,C,pred,I,multi/rewrite_subset_of_integer_set_or_interval,[],[]) :-
    get_texpr_type(Sub,set(integer)),
    (get_texpr_expr(Super,integer_set(_)) ; get_texpr_expr(Super,interval(_,_))),
    rewrite_subset_of_integer_set(Sub,Super,C).

cleanup_pre(interval(From,To),set(integer),I,NExpr,set(integer),I,multi/rewrite_constant_interval,[],[]) :-
    precompute_values(b(interval(From,To),set(integer),I), [instantiate_quantifier_limit(0)], Precomputed),
    Precomputed = b(TExpr,_,_),
    TExpr \= interval(From,To),
    !,
    NExpr = TExpr.

cleanup_pre(interval(From,To),set(integer),I,comprehension_set([UIdD],Pred),set(integer),I,multi/rewrite_interval_to_set_comprehension,[],[]) :-
    translation_type(axiomatic),
    unique_typed_id("_smt_tmp",integer,UIdD),
    create_texpr(greater_equal(UIdD,From),pred,[],Pred1),
    create_texpr(less_equal(UIdD,To),pred,[],Pred2),
    conjunct_predicates([Pred1,Pred2],Pred).

cleanup_pre(pow_subset(Set),set(set(T)),I,comprehension_set([UIdD],Pred),set(set(T)),I,multi/rewrite_pow_subset,[],[]) :-
    translation_type(axiomatic),
    unique_typed_id("_smt_tmp",set(T),UIdD),
    create_texpr(subset(UIdD,Set),pred,[],Pred).

cleanup_pre(pow1_subset(Set),set(set(T)),I,comprehension_set([UIdD],Pred),set(set(T)),I,multi/rewrite_pow1_subset,[],[]) :-
    translation_type(axiomatic),
    unique_typed_id("_smt_tmp",set(T),UIdD),
    create_texpr(subset(UIdD,Set),pred,[],PredSubset),
    create_texpr(empty_set,set(T),[],EmptySet),
    create_texpr(not_equal(UIdD,EmptySet),pred,[],PredNotEqual),
    conjunct_predicates([PredSubset,PredNotEqual],Pred).

cleanup_pre(fin_subset(Set),set(set(T)),I,comprehension_set([UIdD],Pred),set(set(T)),I,multi/rewrite_fin_subset,[],[]) :-
    unique_typed_id("_smt_tmp",set(T),UIdD),
    create_texpr(subset(UIdD,Set),pred,[],Pred1),
    create_texpr(finite(Set),pred,[],Pred2),
    conjunct_predicates([Pred1,Pred2],Pred).

cleanup_pre(fin1_subset(Set),set(set(T)),I,comprehension_set([UIdD],Pred),set(set(T)),I,multi/rewrite_fin1_subset,[],[]) :-
    unique_typed_id("_smt_tmp",set(T),UIdD),
    create_texpr(subset(UIdD,Set),pred,[],PredSubset),
    create_texpr(empty_set,set(T),[],EmptySet),
    create_texpr(not_equal(UIdD,EmptySet),pred,[],PredNotEqual),
    create_texpr(finite(Set),pred,[],PredIsFinite),
    conjunct_predicates([PredSubset,PredNotEqual,PredIsFinite],Pred).

cleanup_pre(direct_product(SetA,SetB),Type,I,comprehension_set([UIdE,UIdF,UIdG],Pred),Type,I,multi/rewrite_direct_product,[],[]) :-
    translation_type(axiomatic),
    Type = set(couple(E,couple(F,G))),
    % TODO: the typing of the comprehension set ids creates a set of couples with a different nesting !!
    % {x,y,z|(x,y):a & (x,z):b} is not type compatible with a >< b
    % this is corrected by the translation later to quantifiers
    unique_typed_id("_smt_tmp",E,UIdE),
    unique_typed_id("_smt_tmp",F,UIdF),
    unique_typed_id("_smt_tmp",G,UIdG),
    create_texpr(couple(UIdE,UIdF),couple(E,F),[],CEF),
    create_texpr(couple(UIdE,UIdG),couple(E,G),[],CEG),
    create_texpr(member(CEF,SetA),pred,[],M1),
    create_texpr(member(CEG,SetB),pred,[],M2),
    conjunct_predicates([M1,M2],Pred).

cleanup_pre(parallel_product(SetA,SetB),Type,I,comprehension_set([UIdE,UIdG,UIdF,UIdH],Pred),Type,I,multi/rewrite_parallel_product,[],[]) :-
    translation_type(axiomatic),
    Type = set(couple(couple(E,G),couple(F,H))),
    % TODO: the typing of the comprehension set ids creates a set of couples with a different nesting !!
    unique_typed_id("_smt_tmp",E,UIdE),
    unique_typed_id("_smt_tmp",F,UIdF),
    unique_typed_id("_smt_tmp",G,UIdG),
    unique_typed_id("_smt_tmp",H,UIdH),
    create_texpr(couple(UIdE,UIdF),couple(E,F),[],CEF),
    create_texpr(couple(UIdG,UIdH),couple(G,H),[],CGH),
    create_texpr(member(CEF,SetA),pred,[],M1),
    create_texpr(member(CGH,SetB),pred,[],M2),
    conjunct_predicates([M1,M2],Pred).

cleanup_pre(composition(Rel1,Rel2),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_composition,[],[]) :-
    % change in Z3: lambda inside recursive functions was declared unsupported until proper support is provided (see https://github.com/Z3Prover/z3/issues/5813)
    % see mk_op_iteration_func_decl in /extensions/z3interface/src/cpp/main.cpp
    %translation_type(axiomatic),
    get_texpr_type(Rel1,set(couple(TD,TI))),
    unique_typed_id("_smt_tmp",TD,UIdD),
    unique_typed_id("_smt_tmp",TR,UIdR),
    unique_typed_id("_smt_tmp",TI,UIdI),
    create_texpr(couple(UIdD,UIdI),couple(TD,TI),[],CoupleDomToI),
    create_texpr(couple(UIdI,UIdR),couple(TI,TR),[],CoupleIToRan),
    create_texpr(member(CoupleDomToI,Rel1),pred,[],Member1),
    create_texpr(member(CoupleIToRan,Rel2),pred,[],Member2),
    conjunct_predicates([Member1,Member2],Inner),
    create_exists([UIdI],Inner,Pred).

cleanup_pre(domain_restriction(Set,Rel),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_domain_restriction,[],[]) :-
    translation_type(axiomatic),
    unique_typed_id("_smt_tmp",TD,UIdD),
    unique_typed_id("_smt_tmp",TR,UIdR),
    create_texpr(couple(UIdD,UIdR),couple(TD,TR),[],Couple),
    create_texpr(member(Couple,Rel),pred,[],MemberOfRel),
    create_texpr(member(UIdD,Set),pred,[],MemberOfSet),
    conjunct_predicates([MemberOfRel,MemberOfSet],Pred).

cleanup_pre(domain_subtraction(Set,Rel),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_domain_subtraction,[],[]) :-
    translation_type(axiomatic),
    unique_typed_id("_smt_tmp",TD,UIdD),
    unique_typed_id("_smt_tmp",TR,UIdR),
    create_texpr(couple(UIdD,UIdR),couple(TD,TR),[],Couple),
    create_texpr(member(Couple,Rel),pred,[],MemberOfRel),
    create_texpr(member(UIdD,Set),pred,[],MemberOfSet),
    create_negation(MemberOfSet,NotMemberOfSet),
    conjunct_predicates([MemberOfRel,NotMemberOfSet],Pred).

cleanup_pre(range_restriction(Rel,Set),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_range_restriction,[],[]) :-
    translation_type(axiomatic),
    unique_typed_id("_smt_tmp",TD,UIdD),
    unique_typed_id("_smt_tmp",TR,UIdR),
    create_texpr(couple(UIdD,UIdR),couple(TD,TR),[],Couple),
    create_texpr(member(Couple,Rel),pred,[],MemberOfRel),
    create_texpr(member(UIdR,Set),pred,[],MemberOfSet),
    conjunct_predicates([MemberOfRel,MemberOfSet],Pred).

cleanup_pre(range_subtraction(Rel,Set),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_range_subtraction,[],[]) :-
    translation_type(axiomatic),
    unique_typed_id("_smt_tmp",TD,UIdD),
    unique_typed_id("_smt_tmp",TR,UIdR),
    create_texpr(couple(UIdD,UIdR),couple(TD,TR),[],Couple),
    create_texpr(member(Couple,Rel),pred,[],MemberOfRel),
    create_texpr(member(UIdR,Set),pred,[],MemberOfSet),
    create_negation(MemberOfSet,NotMemberOfSet),
    conjunct_predicates([MemberOfRel,NotMemberOfSet],Pred).

cleanup_pre(overwrite(Set1,Set2),set(couple(TD,TR)),I,union(Set2,DomSub),set(couple(TD,TR)),I,multi/rewrite_overwrite,[],[]) :-
    create_texpr(domain(Set2),set(TD),[],DomainSet2),
    create_texpr(domain_subtraction(DomainSet2,Set1),set(couple(TD,TR)),[],DomSub).

cleanup_pre(reverse(Set),set(couple(TA,TB)),I,UnwrappedId,set(couple(TA,TB)),I,multi/reverse_to_forall,[AC],[UId]) :-
    translation_type(axiomatic),
    % the reverse is replaced by an identifier (uid)
    unique_typed_id("_smt_tmp",set(couple(TA,TB)),UId),
    get_texpr_expr(UId,UnwrappedId),
    % the identifer carries an additional constraint:
    % !(ida,idb).((ida,idb) : set <-> (idb,ida) : uid)
    unique_typed_id("_smt_tmp",TA,UIdA),
    unique_typed_id("_smt_tmp",TB,UIdB),
    create_texpr(couple(UIdA,UIdB),couple(TA,TB),[],CoupleAB),
    create_texpr(couple(UIdB,UIdA),couple(TB,TA),[],CoupleBA),
   
    create_texpr(member(CoupleAB,UId),pred,[],MemberA),
    create_texpr(member(CoupleBA,Set),pred,[],MemberB),
    create_implication(MemberA,MemberB,Direction1),
    create_implication(MemberB,MemberA,Direction2),
    % use two foralls instead of equivalence!
    create_forall([UIdA,UIdB],Direction1,AC1),
    create_forall([UIdA,UIdB],Direction2,AC2),
    conjunct_predicates([AC1,AC2],AC).

cleanup_pre(cartesian_product(SetA,SetB),set(couple(TR,TD)),I,comprehension_set([UIdR,UIdD],Pred),set(couple(TR,TD)),I,multi/cartesian_product_to_set_comprehension,[],[]) :-
    translation_type(axiomatic),
    unique_typed_id("_smt_tmp",TD,UIdD),
    unique_typed_id("_smt_tmp",TR,UIdR),
    create_texpr(member(UIdR,SetA),pred,[],MemberOf1),
    create_texpr(member(UIdD,SetB),pred,[],MemberOf2),
    conjunct_predicates([MemberOf1,MemberOf2],Pred).

cleanup_pre(Input,pred,I,C,pred,I2,multi/function_application_in_predicate_position_1,[],[]) :-
    Input =.. [Pred,E,Arg],
    \+ is_list(E), % avoids quantifiers
    is_texpr(E), is_texpr(Fun),
    get_texpr_expr(E,function(Fun,Elem)),
    get_texpr_type(Fun,set(couple(RanT,DomT))),
    unique_typed_id("_smt_tmp",DomT,UId),
    create_texpr(couple(Elem,UId),couple(RanT,DomT),[],Couple),
    create_texpr(member(Couple,Fun),pred,[],CoupleInFun),
    Output =.. [Pred,UId,Arg],
    create_texpr(Output,pred,I,UIdInS),
    conjunct_predicates([CoupleInFun,UIdInS],Inner),
    create_exists([UId],Inner,b(C,pred,I2)).

cleanup_pre(Input,pred,I,C,pred,I2,multi/function_application_in_predicate_position_2,[],[]) :-
    Input =.. [Pred,E,Arg],
    \+ is_list(Arg), % avoids quantifiers
    is_texpr(Arg), is_texpr(Fun),
    get_texpr_expr(Arg,function(Fun,Elem)),
    get_texpr_type(Fun,set(couple(RanT,DomT))),
    unique_typed_id("_smt_tmp",DomT,UId),
    create_texpr(couple(Elem,UId),couple(RanT,DomT),[],Couple),
    create_texpr(member(Couple,Fun),pred,[],CoupleInFun),
    Output =.. [Pred,E,UId],
    create_texpr(Output,pred,I,UIdInS),
    conjunct_predicates([CoupleInFun,UIdInS],Inner),
    create_exists([UId],Inner,b(C,pred,I2)).

cleanup_pre(function(F,X),Type,I,UnwrappedId,Type,I,multi/function_application_to_membership,[AC],[UId]) :-
    unique_typed_id("_smt_tmp",Type,UId),
    get_texpr_expr(UId,UnwrappedId),
    get_texpr_type(F,set(FunType)),
    create_texpr(couple(X,UId),FunType,[],CoupleInFunction),
    create_texpr(member(CoupleInFunction,F),pred,[],AC).

cleanup_pre(integer_set('INTEGER'),set(integer),I,UnwrappedId,set(integer),I,multi/rewrite_integer_set_if_above_fails,[AC],[UId]) :-
    % the integer set is replaced by an identifier (uid)
    unique_typed_id("_smt_tmp",set(integer),UId),
    get_texpr_expr(UId,UnwrappedId),
   
    % the identifer carries an additional constraint:
    % !(id).(id : uid)
    unique_typed_id("_smt_tmp",integer,IdToQuantify),
   
    create_texpr(member(IdToQuantify,UId),pred,[],MemberIn),
   
    create_forall([IdToQuantify],MemberIn,AC).

cleanup_pre(min_real(Set),real,I,UnwrappedId,real,I,multi/min_real_to_definition,Args,Ids) :-
    cleanup_pre(min(Set),real,I,UnwrappedId,real,I,_,Args,Ids).

cleanup_pre(max_real(Set),real,I,UnwrappedId,real,I,multi/max_real_to_definition,Args,Ids) :-
    cleanup_pre(max(Set),real,I,UnwrappedId,real,I,_,Args,Ids).

cleanup_pre(min(Set),IntOrReal,I,UnwrappedId,IntOrReal,I,multi/min_to_definition,[AC1,AC2],[UId]) :-
    (IntOrReal == integer; IntOrReal == real),
    unique_typed_id("_smt_tmp",IntOrReal,UId),
    get_texpr_expr(UId,UnwrappedId),
    % two axioms:
    % !(x).(x : Set => uid <= x)
    % #(x).(x : Set & uid = x)
   
    unique_typed_id("_smt_tmp",IntOrReal,QuantifiedVar),
   
    create_texpr(less_equal(UId,QuantifiedVar),pred,[],LessEqual),
    create_texpr(equal(UId,QuantifiedVar),pred,[],Equal),
    create_texpr(member(QuantifiedVar,Set),pred,[],QuantifiedInSet),
   
    conjunct_predicates([QuantifiedInSet,Equal],ExistsInner),
    create_implication(QuantifiedInSet,LessEqual,ForallInner),
   
    create_exists([QuantifiedVar],ExistsInner,AC1),
   
    create_forall([QuantifiedVar],ForallInner,AC2).

cleanup_pre(max(Set),IntOrReal,I,UnwrappedId,IntOrReal,I,multi/max_to_definition,[AC1,AC2],[UId]) :-
    (IntOrReal == integer; IntOrReal == real),
    unique_typed_id("_smt_tmp",IntOrReal,UId),
    get_texpr_expr(UId,UnwrappedId),
    % two axioms:
    % !(x).(x : Set => uid >= x)
    % #(x).(x : Set & uid = x)
   
    unique_typed_id("_smt_tmp",IntOrReal,QuantifiedVar),
   
    create_texpr(greater_equal(UId,QuantifiedVar),pred,[],GreaterEqual),
    create_texpr(equal(UId,QuantifiedVar),pred,[],Equal),
    create_texpr(member(QuantifiedVar,Set),pred,[],QuantifiedInSet),
   
    conjunct_predicates([QuantifiedInSet,Equal],ExistsInner),
    create_implication(QuantifiedInSet,GreaterEqual,ForallInner),
   
    create_exists([QuantifiedVar],ExistsInner,AC1),
   
    create_forall([QuantifiedVar],ForallInner,AC2).

cleanup_pre(card(Set),integer,I,UnwrappedId,integer,I,multi/card_to_exists,[AC1,AC2],[UId]) :-
    unique_typed_id("_smt_tmp",integer,UId),
    get_texpr_expr(UId,UnwrappedId),
    get_texpr_type(Set,set(SetT)),
    unique_typed_id("_smt_tmp",set(couple(integer,SetT)),ForExists),
    create_texpr(interval(b(integer(1),integer,[]),UId),set(integer),[],Interval),
    create_texpr(total_bijection(Interval,Set),set(set(couple(integer,SetT))),[],Bijection),
    create_texpr(member(ForExists,Bijection),pred,[],MemberOf),
    create_exists([ForExists],MemberOf,AC1),
    % without the following constraint, the empty set could have any (negative) cardinality
    create_texpr(greater_equal(UId,b(integer(0),integer,[])),pred,[],AC2).

cleanup_pre(finite(Set),pred,I,ExistsExpr,pred,I,multi/finite_to_forall,[],[]) :-
    % #(b,f).(b:NATURAL & f: Set --> 0..b)
    get_texpr_type(Set,set(ST)),
    unique_typed_id("_smt_tmp",integer,IDB),
    create_texpr(interval(b(integer(0),integer,[]),IDB),set(integer),[],Interval0ToB),
    unique_typed_id("_smt_tmp",set(couple(ST,integer)),IDFun),
    create_texpr(total_injection(Set,Interval0ToB),set(set(couple(ST,integer))),[],Functions),
    create_texpr(member(IDFun,Functions),pred,[],Member),
    create_exists([IDB,IDFun],Member,Exists),
    get_texpr_expr(Exists,ExistsExpr).

cleanup_pre(comprehension_set(Identifiers,Pred),set(X),I,UnwrappedId,set(X),I,multi/comprehension_set_to_forall,[AC],[UId]) :-
    % NOTE: currently the comprehension sets generated are not valid according to B typing rules
    % expr_list_to_couple_expr corrects this
    %(
    translation_type(axiomatic),
    %; translation_type(constructive), % we use Z3's lambda for constructive translation
    % \+ (member(b(_,_,LambdaIdInfo), Identifiers), member(lambda_result(_), LambdaIdInfo))
    %),
    %print(X),nl, print(Identifiers),nl,
    ( expr_list_to_couple_expr(Identifiers,X,IDCouple)
    -> true
    ; add_message(cleanup_pre, 'Could not transform comprehension_set into quantifiers:~n ', b(comprehension_set(Identifiers,Pred),set(X),I))
    ),
    % the set comprehension is replaced by an identifier (uid)
    unique_typed_id("_smt_tmp",set(X),UId),
    get_texpr_expr(UId,UnwrappedId),
    % the identifer carries an additional constraint:
    % !(id).(Pred(id) <-> id : uid)
    create_texpr(member(IDCouple,UId),pred,[],MemberInComprehension),
    create_implication(Pred,MemberInComprehension,Direction1),
    create_implication(MemberInComprehension,Pred,Direction2),
    % use two foralls instead of equivalence!
   
    create_forall(Identifiers,Direction1,AC1),
    create_forall(Identifiers,Direction2,AC2),
    conjunct_predicates([AC1,AC2],AC).

cleanup_pre(domain(Set),set(TD),I,UnwrappedId,set(TD),I,multi/domain_to_forall,[AC],[UId]) :-
    translation_type(axiomatic),
    % the alternative translation of domain and range using lambda is not supported by the incremental solver
    % because an existential quantification is used in the body of the lambda ("internalization of exists is not supported")
    % we thus rewrite these operators here if the incremental solver is used, otherwise they are translated in z3interface/../main.cpp
    % the domain is replaced by an identifier (uid)
    get_texpr_type(Set,set(couple(TD,TR))),
    unique_typed_id("_smt_tmp",set(TD),UId),
    get_texpr_expr(UId,UnwrappedId),
    % the identifer carries an additional constraint:
    % !(id).(id : uid <-> #(idr) : (id,idr) : set)
    unique_typed_id("_smt_tmp",TD,UIdInDomain),
    unique_typed_id("_smt_tmp",TR,UIdInRange),
   
    create_texpr(couple(UIdInDomain,UIdInRange),couple(TD,TR),[],CoupleDR),
    create_texpr(member(CoupleDR,Set),pred,[],CoupleInSet),
    create_exists([UIdInRange],CoupleInSet,ExistsRanElement),
   
    create_texpr(member(UIdInDomain,UId),pred,[],MemberInDomain),
   
    create_implication(ExistsRanElement,MemberInDomain,Direction1),
    create_implication(MemberInDomain,ExistsRanElement,Direction2),
    % use two foralls instead of equivalence!
   
    create_forall([UIdInDomain],Direction1,AC1),
    create_forall([UIdInDomain],Direction2,AC2),
    conjunct_predicates([AC1,AC2],AC).

cleanup_pre(range(Set),set(TR),I,UnwrappedId,set(TR),I,multi/range_to_forall,[AC],[UId]) :-
    (member(no_lambda_translation, I); translation_type(axiomatic)),
    % the range is replaced by an identifier (uid)
    get_texpr_type(Set,set(couple(TD,TR))),
    unique_typed_id("_smt_tmp",set(TR),UId),
    get_texpr_expr(UId,UnwrappedId),
    % the identifer carries an additional constraint:
    % !(id).(id : uid <-> #(idd) : (idd,id) : set)
    unique_typed_id("_smt_tmp",TD,UIdInDomain),
    unique_typed_id("_smt_tmp",TR,UIdInRange),
   
    create_texpr(couple(UIdInDomain,UIdInRange),couple(TD,TR),[],CoupleDR),
    create_texpr(member(CoupleDR,Set),pred,[],CoupleInSet),
    create_exists([UIdInDomain],CoupleInSet,ExistsDomElement),
   
    create_texpr(member(UIdInRange,UId),pred,[],MemberInRange),
    create_implication(ExistsDomElement,MemberInRange,Direction1),
    create_implication(MemberInRange,ExistsDomElement,Direction2),
    % use two foralls instead of equivalence!
   
    create_forall([UIdInRange],Direction1,AC1),
    create_forall([UIdInRange],Direction2,AC2),
    conjunct_predicates([AC1,AC2],AC).

cleanup_pre(image(Function,Set),set(TR),I,UnwrappedId,set(TR),I,multi/image_to_forall,[AC],[UId]) :-
    translation_type(axiomatic),
    % the image is replaced by an identifier (uid)
    get_texpr_type(Function,set(couple(TD,TR))),
    unique_typed_id("_smt_tmp",set(TR),UId),
    get_texpr_expr(UId,UnwrappedId),
    % the identifer carries an additional constraint:
    % !(idr).(idr : uid <-> #(idd) : idd:set & (idd,idr) : function)
    unique_typed_id("_smt_tmp",TD,UIdInDomain),
    unique_typed_id("_smt_tmp",TR,UIdInRange),
   
    create_texpr(couple(UIdInDomain,UIdInRange),couple(TD,TR),[],CoupleDR),
    create_texpr(member(CoupleDR,Function),pred,[],CoupleInFunction),
    create_texpr(member(UIdInDomain,Set),pred,[],DomElementInSet),
    conjunct_predicates([CoupleInFunction,DomElementInSet],ExistsInner),
    create_exists([UIdInDomain],ExistsInner,RHS),
   
    create_texpr(member(UIdInRange,UId),pred,[],LHS),
   
    create_implication(LHS,RHS,Direction1),
    create_implication(RHS,LHS,Direction2),
    % use two foralls instead of equivalence!
   
    create_forall([UIdInRange],Direction1,AC1),
    create_forall([UIdInRange],Direction2,AC2),
    conjunct_predicates([AC1,AC2],AC).

cleanup_pre(external_pred_call('LEQ_SYM',_),pred,I,truth,pred,I,multi/remove_leq_sym,[],[]) :-
    debug_println(19,'Ignoring LEQ_SYM predicate').

cleanups(Phase,Expr,AppliedRules,Result,Path,ACS,IDs) :-
    start_profile_rule(RuleInfos),
    assure_single_rules(AppliedRules,Rule),
    ( cleanup_phase(Phase,Expr,NExpr,Mode/Rule,Path,ACPhase,IDsPhase)
    -> % try to apply a rule (matching the current phase)
    ( Mode == single
    -> AppRules = [Rule|AppliedRules] % if the rule is marked as "single", we add to the list of already applied rules
    ; Mode == multi
    -> AppRules = AppliedRules % if "multi", we do not add it to the list, the rule might be applied more than once
    ; add_error_fail(ast_cleanup_for_smt,'Unexpected rule mode ',Mode)
    ),
    %format('Applied smt cleanup rule ~w (mode:~w)~n',[Rule,Mode]), translate:print_bexpr(NExpr),nl,
    stop_profile_rule(Rule,Mode,Phase,Expr,RuleInfos),
    cleanups(Phase,NExpr,AppRules,Result,Path,ACRec,IDsRec), % continue recursively with the new expression
    append(ACPhase,ACRec,ACS),
    append(IDsPhase,IDsRec,IDs)
    ; % if no rule matches anymore,
    stop_profile_rule(finalise,finished,Phase,Expr,RuleInfos),
    Result = Expr, % we leave the expression unmodified
    ACS = [], IDs = [],
    Rule = none
). % and unblock the co-routine (see assure_single_rules/2)

combine_pred_and_ac(Pred,AC,IDs,Out) :-
    conjunct_predicates(AC,ACPred),
    conjunct_predicates([Pred,ACPred],OutInnerPred),
    extract_equalities_in_quantifier(IDs,OutInnerPred,I2,P2), % used in create_and_simplify_exists; can be expensive
    create_exists(I2,P2,Out). % TO DO: use more intelligence from create_exists_opt or similar??

expr_list_to_couple_expr(Exprs,TypeOfCoupleExpr,Result) :-
    expr_list_to_couple_expr(Exprs,TypeOfCoupleExpr,[],Result).

expr_list_to_couple_expr([T],_Type,[],R) :- !, T=R.

expr_list_to_couple_expr([E|Es],couple(TA,TR),Rest,R) :-
    get_texpr_type(E,TA),!, % type is matching
    expr_list_to_couple_expr(Es,TR,Rest,RHS),
    get_texpr_type(RHS,RHST), get_texpr_type(E,ET),
    create_texpr(couple(E,RHS),couple(ET,RHST),[],R).

expr_list_to_couple_expr(Es,couple(TA,TR),Rest,R) :-
    TA = couple(SA,SB),
    expr_list_to_couple_expr(Es,SA,TRest,LHS),
    !,
    expr_list_to_couple_expr(TRest,SB,TRest2,RHS),
    get_texpr_type(RHS,RHST), get_texpr_type(LHS,LHST),
    create_texpr(couple(LHS,RHS),couple(LHST,RHST),[],R1),
    expr_list_to_couple_expr(TRest2,TR,Rest,R2),
    !,
    get_texpr_type(R1,R1T), get_texpr_type(R2,R2T),
    create_texpr(couple(R1,R2),couple(R1T,R2T),[],R).

expr_list_to_couple_expr([T|Ts],_Type,Ts,R) :- !, T=R.

get_ids_not_in_state([], _, Acc, Acc).

get_ids_not_in_state([IdName|T], State, Acc, IdsNotInState) :-
    ( (
    member(bind(IdName,_), State),
    \+ unfixed_deferred_set(IdName)
    )
    -> get_ids_not_in_state(T, State, Acc, IdsNotInState)
    ; get_ids_not_in_state(T, State, [IdName|Acc], IdsNotInState)
).

internal_clean_up(ExprWithoutSeq,Out) :-
    clean_up(ExprWithoutSeq,CExpr,[],AC,IDs),
    !,
    combine_pred_and_ac(CExpr,AC,IDs,Out).

is_interval(BT,Low,Up) :-
    get_texpr_expr(BT,B),
    ( B = interval(Low,Up) -> true
    ; B = value(Val), nonvar(Val),
    is_interval_closure(Val,L,U) ->
    Low = b(integer(L),integer,[]),
    Up = b(integer(U),integer,[])).

replace_prob_closure(closure(['_zzzz_unary'],_,P), NExpr) :-
    P = b(member(b(identifier('_zzzz_unary'),_,_),ClosurePred),pred,_),
    find_typed_identifier_uses(ClosurePred, [], UsedIds),
    UsedIds == [],
    !,
    get_texpr_expr(ClosurePred, NExpr).

replace_prob_closure(closure(['_zzzz_unary'],T,P), value(ComputedVal)) :-
    normalise_value_for_var(solver_result, force, closure(['_zzzz_unary'],T,P), ComputedVal),
    ComputedVal \== closure(['_zzzz_unary'],T,P).

replace_prob_closure_record_field(field(FName,Val), NField) :-
    Val = closure(['_zzzz_unary'],[InnerType],_),
    replace_prob_closure(Val, NVal),
    !,
    NField = field(FName,b(NVal,set(InnerType),[])).

rewrite_equal_to_ge_le(ID,GlobalSet,Constraint) :-
    unique_typed_id("_smt_tmp",integer,UId),
    create_texpr(member(UId,ID),pred,[],UIdInSet),
    rewrite_member_to_ge_le(UId,GlobalSet,GeLeConstraints),
    create_texpr(GeLeConstraints,pred,[],GeLeTexpr),
    create_implication(UIdInSet,GeLeTexpr,Direction1),
    create_implication(GeLeTexpr,UIdInSet,Direction2),
   
    create_forall([UId],Direction1,FA1),
    create_forall([UId],Direction2,FA2),
    Constraint = conjunct(FA1,FA2).

rewrite_global_set_nat_or_int_value(b(value(global_set('NATURAL')),set(integer),Info), Out) :-
    !,
    Out = b(integer_set('NATURAL'),set(integer),Info).

rewrite_global_set_nat_or_int_value(b(value(global_set('NATURAL1')),set(integer),Info), Out) :-
    !,
    Out = b(integer_set('NATURAL1'),set(integer),Info).

rewrite_global_set_nat_or_int_value(b(value(global_set('NAT')),set(integer),Info), Out) :-
    !,
    Out = b(integer_set('NAT'),set(integer),Info).

rewrite_global_set_nat_or_int_value(b(value(global_set('NAT1')),set(integer),Info), Out) :-
    !,
    Out = b(integer_set('NAT1'),set(integer),Info).

rewrite_global_set_nat_or_int_value(b(value(global_set('INT')),set(integer),Info), Out) :-
    !,
    Out = b(integer_set('INT'),set(integer),Info).

rewrite_global_set_nat_or_int_value(In, In).

rewrite_member_of_function(ID,Function,TypeConstraintOut) :-
    get_texpr_expr(Function,relations(Dom,Ran)),
    get_texpr_type(Function,set(set(couple(DomT,RanT)))),
    % relations: only typing constraint !(x,y).((x,y) : ID => x : Dom & y : Ran)
    unique_typed_id("_smt_tmp",DomT,UIdDom),
    unique_typed_id("_smt_tmp",RanT,UIdRan),
    create_texpr(couple(UIdDom,UIdRan),couple(DomT,RanT),[],UIdCouple),
    create_texpr(member(UIdCouple,ID),pred,[],LHS),
    create_texpr(member(UIdDom,Dom),pred,[],RHS1),
    create_texpr(member(UIdRan,Ran),pred,[],RHS2),
    conjunct_predicates([RHS1,RHS2],RHS),
    create_implication(LHS,RHS,TypeConsInner),
   
    create_forall([UIdDom,UIdRan],TypeConsInner,TypeConstraint),
    get_texpr_expr(TypeConstraint,TypeConstraintOut).

rewrite_member_of_function(ID,Function,ConstraintOut) :-
    get_texpr_expr(Function,total_relation(Dom,Ran)),
    get_texpr_type(Function,set(set(couple(DomT,RanT)))),
    % total_relation: relation & !(x).(x : Dom => #(y).(y : Ran & (x,y):Id))
    unique_typed_id("_smt_tmp",DomT,UIdDom),
    unique_typed_id("_smt_tmp",RanT,UIdRan),
    create_texpr(couple(UIdDom,UIdRan),couple(DomT,RanT),[],UIdCouple),
    create_texpr(member(UIdCouple,ID),pred,[],CoupleInID),
    create_exists([UIdRan],CoupleInID,RHS),
    create_texpr(member(UIdDom,Dom),pred,[],LHS),
    create_implication(LHS,RHS,FunConsInner),
    create_forall([UIdDom],FunConsInner,FunConstraint),
    create_texpr(relations(Dom,Ran),set(set(couple(DomT,RanT))),[],Relations),
    create_texpr(member(ID,Relations),pred,[],IsRelation),
    ConstraintOut = conjunct(IsRelation,FunConstraint).

rewrite_member_of_function(ID,Function,ConstraintOut) :-
    get_texpr_expr(Function,surjection_relation(Dom,Ran)),
    get_texpr_type(Function,set(set(couple(DomT,RanT)))),
    % surjection_relation: relation & ran = T
    create_texpr(range(ID),set(RanT),[],Range),
    create_texpr(equal(Range,Ran),pred,[],FunConstraint),
    create_texpr(relations(Dom,Ran),set(set(couple(DomT,RanT))),[],Relations),
    create_texpr(member(ID,Relations),pred,[],IsRelation),
    ConstraintOut = conjunct(IsRelation,FunConstraint).

rewrite_member_of_function(ID,Function,ConstraintOut) :-
    get_texpr_expr(Function,total_surjection_relation(Dom,Ran)),
    get_texpr_type(Function,set(set(couple(DomT,RanT)))),
    % total_surjection_relation: total_relation & surjection_relation
    create_texpr(total_relation(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalRelations),
    create_texpr(member(ID,TotalRelations),pred,[],IsTotalRelation),
    create_texpr(surjection_relation(Dom,Ran),set(set(couple(DomT,RanT))),[],SurjectionRelations),
    create_texpr(member(ID,SurjectionRelations),pred,[],IsSurjectionRelation),
    ConstraintOut = conjunct(IsTotalRelation,IsSurjectionRelation).

rewrite_member_of_function(ID,Function,ConstraintOut) :-
    get_texpr_expr(Function,partial_function(Dom,Ran)),
    get_texpr_type(Function,set(set(couple(DomT,RanT)))),
    % partial_function: relation & !(x,y,z).((x,y) : ID & (x,z) : ID => y = z)
    unique_typed_id("_smt_tmp",DomT,UIdDom),
    unique_typed_id("_smt_tmp",RanT,UIdRan),
    unique_typed_id("_smt_tmp",RanT,UIdRan2),
    create_texpr(couple(UIdDom,UIdRan),couple(DomT,RanT),[],UIdCouple),
    create_texpr(couple(UIdDom,UIdRan2),couple(DomT,RanT),[],UIdCouple2),
    create_texpr(member(UIdCouple,ID),pred,[],C1InID),
    create_texpr(member(UIdCouple2,ID),pred,[],C2InID),
    create_texpr(equal(UIdRan,UIdRan2),pred,[],RHS),
    conjunct_predicates([C1InID,C2InID],LHS),
    create_implication(LHS,RHS,FunConsInner),
   
    create_forall([UIdDom,UIdRan,UIdRan2],FunConsInner,FunConstraint),
    % add typing: is a relation
    create_texpr(relations(Dom,Ran),set(set(couple(DomT,RanT))),[],Relations),
    create_texpr(member(ID,Relations),pred,[],IsRelation),
    ConstraintOut = conjunct(IsRelation,FunConstraint).

rewrite_member_of_function(ID,Function,ConstraintOut) :-
    get_texpr_expr(Function,total_function(Dom,Ran)),
    get_texpr_type(Function,set(set(couple(DomT,RanT)))),
    % total_function: partial_function & !(x).(x : Dom => #(y).(y : Ran & (x,y):Id))
    unique_typed_id("_smt_tmp",DomT,UIdDom),
    unique_typed_id("_smt_tmp",RanT,UIdRan),
    create_texpr(couple(UIdDom,UIdRan),couple(DomT,RanT),[],UIdCouple),
    create_texpr(member(UIdCouple,ID),pred,[],CoupleInID),
    create_exists([UIdRan],CoupleInID,RHS),
    create_texpr(member(UIdDom,Dom),pred,[],LHS),
    create_implication(LHS,RHS,FunConsInner),
    create_forall([UIdDom],FunConsInner,FunConstraint),
    % add typing: is a partial_function
    create_texpr(partial_function(Dom,Ran),set(set(couple(DomT,RanT))),[],PFunctions),
    create_texpr(member(ID,PFunctions),pred,[],IsPFunction),
    ConstraintOut = conjunct(IsPFunction,FunConstraint).

rewrite_member_of_function(ID,Function,ConstraintOut) :-
    get_texpr_expr(Function,partial_injection(Dom,Ran)),
    get_texpr_type(Function,set(set(couple(DomT,RanT)))),
    % partial_injection: partial_function & !(x1,x2,y).((x1,y) : ID & (x2,y) : ID => x1 = x2)
    unique_typed_id("_smt_tmp",DomT,UIdDom1),
    unique_typed_id("_smt_tmp",DomT,UIdDom2),
    unique_typed_id("_smt_tmp",RanT,UIdRan),
    create_texpr(couple(UIdDom1,UIdRan),couple(DomT,RanT),[],UIdCouple),
    create_texpr(couple(UIdDom2,UIdRan),couple(DomT,RanT),[],UIdCouple2),
    create_texpr(member(UIdCouple,ID),pred,[],C1InID),
    create_texpr(member(UIdCouple2,ID),pred,[],C2InID),
    create_texpr(equal(UIdDom1,UIdDom2),pred,[],RHS),
    conjunct_predicates([C1InID,C2InID],LHS),
    create_implication(LHS,RHS,FunConsInner),
   
    create_forall([UIdDom1,UIdDom2,UIdRan],FunConsInner,FunConstraint),
    % add typing: is a partial_function
    create_texpr(partial_function(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialFunctions),
    create_texpr(member(ID,PartialFunctions),pred,[],IsPartialFunction),
    ConstraintOut = conjunct(IsPartialFunction,FunConstraint).

rewrite_member_of_function(ID,Function,ConstraintOut) :-
    get_texpr_expr(Function,total_injection(Dom,Ran)),
    get_texpr_type(Function,set(set(couple(DomT,RanT)))),
    % total_injection: total_function & partial_injection
    create_texpr(total_function(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalFunctions),
    create_texpr(member(ID,TotalFunctions),pred,[],IsTotalFunction),
    create_texpr(partial_injection(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialInjections),
    create_texpr(member(ID,PartialInjections),pred,[],IsPartialInjection),
    ConstraintOut = conjunct(IsTotalFunction,IsPartialInjection).

rewrite_member_of_function(ID,Function,ConstraintOut) :-
    get_texpr_expr(Function,partial_surjection(Dom,Ran)),
    get_texpr_type(Function,set(set(couple(DomT,RanT)))),
    % partial_surjection: partial_function & ran = T
    create_texpr(range(ID),set(RanT),[],TRange),
    % TO DO: there is a bug when translating this range as a lambda function, happens for card, possible bug in Z3
    add_texpr_infos(TRange, [no_lambda_translation], Range),
    create_texpr(equal(Range,Ran),pred,[],FunConstraint),
    % add typing: is a partial_function
    create_texpr(partial_function(Dom,Ran),set(set(couple(DomT,RanT))),[],PFunctions),
    create_texpr(member(ID,PFunctions),pred,[],IsPFunction),
    ConstraintOut = conjunct(IsPFunction,FunConstraint).

rewrite_member_of_function(ID,Function,ConstraintOut) :-
    get_texpr_expr(Function,total_surjection(Dom,Ran)),
    get_texpr_type(Function,set(set(couple(DomT,RanT)))),
    % total_surjection: total_function & partial_surjection
    create_texpr(total_function(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalFunctions),
    create_texpr(member(ID,TotalFunctions),pred,[],IsTotalFunction),
    create_texpr(partial_surjection(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialSurjections),
    create_texpr(member(ID,PartialSurjections),pred,[],IsPartialSurjection),
    ConstraintOut = conjunct(IsTotalFunction,IsPartialSurjection).

rewrite_member_of_function(ID,Function,ConstraintOut) :-
    get_texpr_expr(Function,partial_bijection(Dom,Ran)),
    get_texpr_type(Function,set(set(couple(DomT,RanT)))),
    % partial_bijection: partial_surjection & partial_injection
    create_texpr(partial_surjection(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialSurjections),
    create_texpr(member(ID,PartialSurjections),pred,[],IsPartialSurjection),
    create_texpr(partial_injection(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialInjections),
    create_texpr(member(ID,PartialInjections),pred,[],IsPartialInjection),
    ConstraintOut = conjunct(IsPartialSurjection,IsPartialInjection).

rewrite_member_of_function(ID,Function,ConstraintOut) :-
    get_texpr_expr(Function,total_bijection(Dom,Ran)),
    get_texpr_type(Function,set(set(couple(DomT,RanT)))),
    % total_bijection: total_surjection & total_injection
    create_texpr(total_surjection(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalSurjections),
    create_texpr(member(ID,TotalSurjections),pred,[],IsTotalSurjection),
    create_texpr(total_injection(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalInjections),
    create_texpr(member(ID,TotalInjections),pred,[],IsTotalInjection),
    ConstraintOut = conjunct(IsTotalSurjection,IsTotalInjection).

rewrite_member_to_ge_le(ID,Set,Constraint) :-
    get_texpr_expr(Set,interval(Low,High)),
    create_texpr(greater_equal(ID,Low),pred,[],Lower),
    create_texpr(greater_equal(High,ID),pred,[],Higher),
    Constraint = conjunct(Lower,Higher).

rewrite_member_to_ge_le(ID,Set,Constraint) :-
    rewrite_global_set_nat_or_int_value(Set, NSet),
    get_texpr_expr(NSet,integer_set(Kind)), % no cut here see rule below
    bzero(BZero), bone(BOne), bminint(MinInt), bmaxint(MaxInt),
    create_texpr(greater_equal(ID,LowerBound),pred,[],Lower),
    create_texpr(greater_equal(UpperBound,ID),pred,[],Higher),
    Constraint = conjunct(Lower,Higher),
    (Kind = 'NAT' -> LowerBound = BZero, UpperBound = MaxInt ;
    Kind = 'NAT1' -> LowerBound = BOne, UpperBound = MaxInt ;
    Kind = 'INT' -> LowerBound = MinInt, UpperBound = MaxInt).

rewrite_member_to_ge_le(ID,Set,Constraint) :-
    rewrite_global_set_nat_or_int_value(Set, NSet),
    get_texpr_expr(NSet,integer_set(Kind)), !,
    bzero(BZero), bone(BOne),
    (Kind = 'NATURAL' -> Constraint = greater_equal(ID,BZero) ;
    Kind = 'NATURAL1' -> Constraint = greater_equal(ID,BOne)).