b2setlog

add_translation_error(Env,Msg,TE) :-
    (do_not_generate_errors(Env)
    -> debug_mode(on),
    add_message(b2setlog,Msg,TE,TE)
    ; add_error(b2setlog,Msg,TE,TE)
).

add_typing_pred(BPred,BPred2) :-
    find_typed_identifier_uses(BPred,TypedIds), % we will have to do this also for quantifiers/set compr. later
    include(can_translate_typing_to_setlog,TypedIds,TranslatableIds),
    generate_typing_predicates(TranslatableIds,TypingPreds),
    %translate:nested_print_bexpr(TypingPreds),nl,
    conjunct_predicates([BPred|TypingPreds],BPred2).

arith_bin_op(add(A,B),A,B,'+').

arith_bin_op(div(A,B),A,B,'div').

arith_bin_op(minus(A,B),A,B,'-').

arith_bin_op(modulo(A,B),A,B,'mod').

arith_bin_op(multiplication(A,B),A,B,'*').

arith_bin_op(power_of(A,B),A,B,'**'). %% Not sure if this works

arith_un_op(unary_minus(A),A,'-').

b2arithe(integer(I),_,true,I) :- !.

b2arithe(UNOP,Env,SetLogConstr,SLOG) :- % ditto
    arith_un_op(UNOP,A,SetLogOperator),!,
    barithexpr2setlog(A,Env,SetLogConstr,RA),
    SLOG =.. [SetLogOperator,RA].

b2arithe(BOP,Env,SetLogConstr,SLOG) :- % ditto
    arith_bin_op(BOP,A,B,SetLogOperator),!,
    barithexpr2setlog(A,Env,CA,RA), barithexpr2setlog(B,Env,CB,RB),
    SLOG =.. [SetLogOperator,RA,RB],
    sconj([CA,CB],SetLogConstr).

b2arithe(BExpr,Env,SetLogConstr,Res) :- b2e(BExpr,Env,SetLogConstr,Res).

b2e(UnOP,Env,SetLogConstr,Res) :- % Res is a fresh existential variable
    un_op(UnOP,A,SetLogOperator),!,
    bexpr2setlog(A,Env,CA,RA),
    SLOG =.. [SetLogOperator,RA,Res],
    sconjoin(CA,SLOG,SetLogConstr).

b2e(BOP,Env,SetLogConstr,Res) :- % ditto
    bin_op(BOP,A,B,SetLogOperator),!,
    bexpr2setlog(A,Env,CA,RA), bexpr2setlog(B,Env,CB,RB),
    SLOG =.. [SetLogOperator,RA,RB,Res],
    sconj([CA,CB,SLOG],SetLogConstr).

b2e(UNOP,Env,SetLogConstr,Res) :- % ditto
    arith_un_op(UNOP,A,SetLogOperator),!,
    barithexpr2setlog(A,Env,CA,RA),
    SLOG =.. [SetLogOperator,RA],
    sconj([CA,'is'(Res,SLOG)],SetLogConstr).

b2e(BOP,Env,SetLogConstr,Res) :- % ditto
    arith_bin_op(BOP,A,B,SetLogOperator),!,
    barithexpr2setlog(A,Env,CA,RA), barithexpr2setlog(B,Env,CB,RB),
    SLOG =.. [SetLogOperator,RA,RB],
    sconj([CA,CB,'is'(Res,SLOG)],SetLogConstr).

b2e(identifier(ID),Env,true,PrologVar) :- % var is not fresh and cannot be freely unified
    lookup_identifier(Env,ID,PrologVar). % could also be global_set or global constant

b2e(integer(I),_,true,I).

b2e(empty_set,_,true,'{}').

b2e(string(S),_,true,string(S)).

b2e(boolean_false,_,true,pred_false).

b2e(boolean_true,_,true,pred_true).

b2e(max_int,_,true,MaxInt) :-
    get_preference(maxint, MaxInt).

b2e(min_int,_,true,MinInt) :-
    get_preference(minint, MinInt).

b2e(bool_set,Env,Constr,R) :-
    b2sext([b(boolean_false,boolean,[]),
    b(boolean_true, boolean,[])],Env,Constr,R).

b2e(cartesian_product(A,B),Env,Constr,R) :-
    bexpr2setlog(A,Env,CA,RA),bexpr2setlog(B,Env,CB,RB),
    sconjoin(CA,CB,Constr), R=cp(RA,RB).

b2e(interval(A,B),Env,Constr,R) :-
    bexpr2setlog(A,Env,CA,RA),bexpr2setlog(B,Env,CB,RB), sconjoin(CA,CB,Constr), R=int(RA,RB).

b2e(couple(A,B),Env,Constr,R) :- bexpr2setlog(A,Env,CA,RA),bexpr2setlog(B,Env,CB,RB),
    sconjoin(CA,CB,Constr),R=[RA,RB].

b2e(first_projection(A),Env,Constr,R) :- bexpr2setlog(A,Env,CA,RA),sconjoin(CA,RA=[R,_],Constr). % existential Prolog variable could be problem inside negation

b2e(second_projection(A),Env,Constr,R) :- bexpr2setlog(A,Env,CA,RA),sconjoin(CA,RA=[_,R],Constr).

b2e(set_extension(L),Env,Constr,R) :- b2sext(L,Env,Constr,R).

b2e(value(Val),Env,Constr,R) :- b2v(Val,Env,Constr,R).

b2e(comprehension_set(Ids,Body),Env,true,Res) :-
    Ids=[ID], % TODO: support multiple ids
    extract_membership(Body,ID,Env,MemberConstr,RestBody),
    Res = ris(MemberConstr,FilterConstr,Pattern), % intensional setlog set
    bexpr2setlog(ID,Env,CA,Pattern),
    bpred2setlog(RestBody,Env,CB),
    sconjoin(CA,CB,FilterConstr).

b2e(pow_subset(BSet),Env, Constr, GIS) :-
    GIS = '{}'(':'(X,subset(X,SET))),
    bexpr2setlog(BSet,Env,Constr,SET).

b2mem(pow_subset(A),Element,Env,Constr) :- !,
    create_subset(Element,A,Env,Constr).

b2mem(pow1_subset(A),Element,Env,Constr) :- !,
    create_subset(Element,A,Env,SubsetConstr),
    sconj([SubsetConstr,'neq'(Element,'{}')],Constr).

b2mem(fin_subset(A),Element,Env,Constr) :- !, % Same, because Setlog only has finite sets anyway!
    b2mem(pow_subset(A),Element,Env,Constr).

b2mem(fin1_subset(A),Element,Env,Constr) :- !, % Same, because Setlog only has finite sets anyway!
    b2mem(pow1_subset(A),Element,Env,Constr).

b2mem(relations(A,B),Element,Env,Constr) :- !,
    create_domain(A,Element,Env,DomConstr),
    create_range(B,Element,Env,RanConstr),
    sconj([rel(Element),DomConstr,RanConstr],Constr).

b2mem(partial_function(A,B),Element,Env,Constr) :- !,
    create_dom_pf(A,Element,Env,DomConstr),
    create_range(B,Element,Env,RanConstr),
    sconj([pfun(Element),DomConstr,RanConstr],Constr).

b2mem(total_function(A,B),Element,Env,Constr) :- !,
    create_dom_tf(A,Element,Env,DomConstr),
    create_range(B,Element,Env,RanConstr),
    sconj([pfun(Element),DomConstr,RanConstr],Constr).

b2mem(Set,Element,Env,Constr) :-
    is_symbolic_set(Set,Element,Env,ElConstr,_), !, % NATURAL(1)
    Constr = ElConstr.

b2not_mem(relations(A,B),Element,Env,Constr) :- !,
    create_not_domain(A,Element,Env,NotDomConstr),
    is_just_type_and_infinite(B), % TODO: extend and disjoin
    sconj([rel(Element),NotDomConstr],Constr).

b2not_mem(pow_subset(A),Element,Env,Constr) :- !,
    create_not_subset(Element,A,Env,Constr).

b2not_mem(pow1_subset(A),Element,Env,Constr) :- !,
    create_not_subset(Element,A,Env,SubsetConstr),
    sdisjoin(SubsetConstr,'='(Element,'{}'),Constr).

b2not_mem(fin_subset(A),Element,Env,Constr) :- !, % Same, because Setlog only has finite sets anyway!
    b2not_mem(pow_subset(A),Element,Env,Constr).

b2not_mem(fin1_subset(A),Element,Env,Constr) :- !, % Same, because Setlog only has finite sets anyway!
    b2not_mem(pow1_subset(A),Element,Env,Constr).

b2not_mem(partial_function(A,B),Element,Env,Constr) :- !,
    create_not_domain(A,Element,Env,DomConstr),
    create_not_range(B,Element,Env,NotRanConstr),
    sdisj([npfun(Element),DomConstr,NotRanConstr],Constr).

b2not_mem(Set,Element,Env,Constr) :-
    is_symbolic_set(Set,Element,Env,_,NegElConstr), !, % NATURAL(1)
    Constr = NegElConstr.

b2p(BOP,Env,SetLogConstr) :-
    bin_pred(BOP,A,B,SetLogOperator),!,
    bexpr2setlog(A,Env,CA,RA),
    bexpr2setlog(B,Env,CB,RB),
    SLOG =.. [SetLogOperator,RA,RB],
    sconj([CA,CB,SLOG],SetLogConstr).

b2p(truth,_,true).

b2p(falsity,_,false). % TODO: check this

b2p(not_subset_strict(A,B),Env,Constr) :-
    bexpr2setlog(A,Env,CA,RA),
    bexpr2setlog(B,Env,CB,RB),
    create_not_subset(RA,B,Env,NotSubsetConstr),
    sdisjoin('='(RA,RB),NotSubsetConstr,Disj),
    sconj([CA,CB,Disj],Constr).

b2p(subset(A,B),Env,Constr) :-
    bexpr2setlog(A,Env,CA,RA),
    create_subset(RA,B,Env,SubsetConstr),
    sconj([CA,SubsetConstr],Constr).

b2p(not_subset(A,B),Env,Constr) :-
    bexpr2setlog(A,Env,CA,RA),
    create_not_subset(RA,B,Env,NotSubsetConstr),
    sconj([CA,NotSubsetConstr],Constr).

b2p(member(A,B),Env,Constr) :-
    bexpr2setlog(A,Env,CA,RA),
    bmember2setlog(B,RA,Env,CB), sconjoin(CA,CB,Constr).

b2p(not_member(A,B),Env,Constr) :-
    bexpr2setlog(A,Env,CA,RA),
    bnotmember2setlog(B,RA,Env,CB), sconjoin(CA,CB,Constr).

b2p(equal(A,B),Env,Constr) :-
    bexpr2setlog(A,Env,CA,RA),
    bexpr2setlog(B,Env,CB,RB),
    (can_be_unified_in_translation(RA,A,RB,B)
    -> RA=RB, sconjoin(CA,CB,Constr) % perform unification here to avoid creating internal fresh Prolog vars
    ; sconj([CA,CB,'='(RA,RB)],Constr)).

b2p(not_equal(A,B),Env,Constr) :-
    bexpr2setlog(A,Env,CA,RA),
    bexpr2setlog(B,Env,CB,RB),
    (can_be_unified_in_translation(RA,A,RB,B),
    can_be_negated(CA,NCA)
    -> RA=RB, sconjoin(CB,NCA,Constr) % perform unification here to avoid creating internal fresh Prolog vars
    ; can_be_unified_in_translation(RA,A,RB,B),
    can_be_negated(CB,NCB)
    -> RA=RB, sconjoin(CA,NCB,Constr)
    ; sconj([CA,CB,'neq'(RA,RB)],Constr)).

b2p(negation(A),Env,CA) :- bnegpred2setlog(A,Env,CA).

b2p(conjunct(A,B),Env,Constr) :- bpred2setlog(A,Env,CA), bpred2setlog(B,Env,CB), sconjoin(CA,CB,Constr).

b2p(disjunct(A,B),Env,or(CA,CB)) :- bpred2setlog(A,Env,CA), bpred2setlog(B,Env,CB).

b2p(implication(A,B),Env,implies(CA,CB)) :- bpred2setlog(A,Env,CA), bpred2setlog(B,Env,CB).

b2p(equivalence(A,B),Env,Constr) :-
    bpred2setlog(A,Env,CA), bpred2setlog(B,Env,CB),
    sconjoin(implies(CA,CB),implies(CB,CA),Constr).

b2p(exists(TypedIds,Body),Env,Constr) :-
    exclude(can_translate_typing_to_setlog,TypedIds,Rest),
    Rest=[],!, % TODO: extract typing from Body
    Constr = exists(Typing,CB),
    generate_typing_predicates(TypedIds,TypingPreds),
    conjunct_predicates(TypingPreds,TPS),
    bpred2setlog(TPS,Env,Typing), bpred2setlog(Body,Env,CB).

b2p(forall(TypedIds,LHS,RHS),Env,Constr) :-
    include(can_translate_typing_to_setlog,TypedIds,Translatable),
    generate_typing_predicates(Translatable,TypingPreds),
    conjunct_predicates(TypingPreds,TPS),
    bpred2setlog(TPS,Env,Typing),
    bpred2setlog(LHS,Env,CLHS), % TODO: filter LHS into setlog typing and rest and provide warnings
    sconjoin(Typing,CLHS,SetLogLHS),
    Constr = foreach(SetLogLHS,SetLogRHS),
    bpred2setlog(RHS,Env,SetLogRHS).

b2p_neg(Pred,Env,CA) :- negate_pred(Pred,NPred),!, b2p(NPred,Env,CA).

b2p_neg(negation(A),Env,CA) :- !, bpred2setlog(A,Env,CA).

b2p_neg(disjunct(A,B),Env,Constr) :- !, bnegpred2setlog(A,Env,CA), bnegpred2setlog(B,Env,CB), sconjoin(CA,CB,Constr).

b2p_neg(conjunct(A,B),Env,or(CA,CB)) :- !, bnegpred2setlog(A,Env,CA), bnegpred2setlog(B,Env,CB).

b2p_neg(implication(A,B),Env,Constr) :- !, % not(a=>b) = not(not(a) or b) = a & not(b)
    bpred2setlog(A,Env,CA), bnegpred2setlog(B,Env,CB), sconjoin(CA,CB,Constr).

b2p_neg(equivalence(A,B),Env,Constr) :- !, % not(a<=>b) = (a & not(b) or (not(a) & b))
    NB = b(negation(B),pred,[]),
    ANB = b(conjunct(A,NB),pred,[]),
    NA = b(negation(A),pred,[]),
    NAB = b(conjunct(NA,B),pred,[]),
    b2p(disjunct(ANB,NAB),Env,Constr).

b2p_neg(A,Env,neg(CA)) :- bpred2setlog(A,Env,CA).

b2sext([],Env,Constr,Res) :- !, b2e(empty_set,Env,Constr,Res).

b2sext([A],Env,Constr,Res) :- !, Res = '{}'(RA), bexpr2setlog(A,Env,Constr,RA).

b2sext([A|T],Env,Constr,Res) :- bexpr2setlog(A,Env,CA,RA),
    Res = '{}'(RA/RT), % Setlog {RA/RT}
    b2sext(T,Env,CT,RT),
    sconjoin(CA,CT,Constr).

b2v(Val,Env,_,_) :- var(Val),!,
    add_translation_error(Env,'Cannot convert compiled B value variable to setlog:',Val),fail.

b2v(pred_false,_,true,pred_false).

b2v(pred_true,_,true,pred_true).

b2v(int(I),_,true,I).

b2v(string(S),_,true,string(S)).

b2v(fd(Nr,Set),_,true,SetlogTerm) :- translate_global_fd_value(Nr,Set,SetlogTerm).

b2v([],Env,C,R) :- b2e(empty_set,Env,C,R).

b2v(couple(A,B),Env,Constr,R) :- b2v(A,Env,CA,RA),b2v(B,Env,CB,RB),
    sconjoin(CA,CB,Constr),R=[RA,RB].

b2v(avl_set(A),Env,Constr,R) :-
    expand_custom_set_to_list(avl_set(A),List,_,b2v),
    b2vlist(List,Env,Constr,R).

b2v(global_set(A),Env,Constr,R) :-
    expand_custom_set_to_list(global_set(A),List,_,b2v), % for deferred sets this will use the scope of ProB
    b2vlist(List,Env,Constr,R).

b2v(Val,Env,_,_) :- print(Val),nl,
    add_translation_error(Env,'Cannot convert compiled B value to setlog:',Val), fail.

b2vlist([],Env,Constr,Res) :- !, b2e(empty_set,Env,Constr,Res).

b2vlist([A],Env,Constr,Res) :- !, Res = '{}'(RA), b2v(A,Env,Constr,RA).

b2vlist([A|T],Env,Constr,Res) :- b2v(A,Env,CA,RA),
    Res = '{}'(RA/RT), % Setlog {RA/RT}
    b2vlist(T,Env,CT,RT),
    sconjoin(CA,CT,Constr).

barithexpr2setlog(b(E,_T,_I),Env,SetLogConstr,Res) :- b2arithe(E,Env,C,R),!, SetLogConstr=C,Res=R.

barithexpr2setlog(TE,Env,_,_) :-
    add_translation_error(Env,'Cannot convert B arithmetic expression to setlog:',TE),fail.

bexpr2setlog(b(E,_Type,_I),Env,SetLogConstr,Res) :- b2e(E,Env,C,R),!, SetLogConstr=C,Res=R.

bexpr2setlog(TE,Env,_,_) :- add_translation_error(Env,'Cannot convert B expression to setlog:',TE),fail.

bin_op(union(A,B),A,B,un).

bin_op(intersection(A,B),A,B,inters).

bin_op(set_subtraction(A,B),A,B,diff).

bin_op(function(A,B),A,B,apply).

bin_op(rel_composition(A,B),A,B,comp).

bin_op(image(A,B),A,B,rimg).

bin_op(domain_restriction(A,B),A,B,dres).

bin_op(domain_subtraction(A,B),A,B,dares).

bin_op(range_restriction(A,B),A,B,rres).

bin_op(range_subtraction(A,B),A,B,rares).

bin_op(overwrite(A,B),A,B,oplus).

bin_pred(subset_strict(A,B),A,B,ssubset).

bin_pred(less(A,B),A,B,'<').

bin_pred(less_equal(A,B),A,B,'=<').

bin_pred(greater(A,B),A,B,'>').

bin_pred(greater_equal(A,B),A,B,'>=').

bmember2setlog(b(Set,_,_),Element,Env,Constr) :-
    b2mem(Set,Element,Env,Constr),!.

bmember2setlog(Set,Element,Env,Constr) :- % default case: no special rule available
    bexpr2setlog(Set,Env,CA,RSet),
    sconjoin(CA,in(Element,RSet),Constr).

bnegpred2setlog(b(E,_T,_I),Env,SetLogConstr) :- b2p_neg(E,Env,C),!, SetLogConstr=C.

bnegpred2setlog(TE,Env,_) :- add_translation_error(Env,'Cannot convert negated B predicate to setlog:',TE),fail.

bnotmember2setlog(b(Set,_,_),Element,Env,Constr) :-
    b2not_mem(Set,Element,Env,Constr),!.

bnotmember2setlog(Set,Element,Env,Constr) :- % default case: no special rule available
    bexpr2setlog(Set,Env,CA,RSet),
    sconjoin(CA,nin(Element,RSet),Constr).

bpred2setlog(b(E,_T,_I),Env,SetLogConstr) :- b2p(E,Env,C),!, SetLogConstr=C.

bpred2setlog(TE,Env,_) :-
    add_translation_error(Env,'Cannot convert B predicate to setlog:',TE),
    fail.

can_be_negated(un(A,B),nun(A,B)).

can_be_negated(inters(A,B),ninters(A,B)).

can_be_negated(diff(A,B),ndiff(A,B)).

can_be_negated(inv(A,B),ninv(A,B)).

can_be_negated(id(A,B),nid(A,B)).

can_be_negated(dom(A,B),ndom(A,B)).

can_be_negated(dompf(A,B),ndompf(A,B)).

can_be_negated(ran(A,B),nran(A,B)).

can_be_negated(comp(A,B,C),ncomp(A,B,C)).

can_be_negated(dres(A,B,C),ndres(A,B,C)).

can_be_negated(dares(A,B,C),ndares(A,B,C)).

can_be_negated(drres(A,B,C),nrres(A,B,C)).

can_be_negated(rares(A,B,C),nrares(A,B,C)).

can_be_negated(oplus(A,B,C),noplus(A,B,C)).

can_be_negated(rimg(A,B,C),nrimg(A,B,C)).

can_be_negated(apply(A,B,C),napply(A,B,C)).

can_be_unified_in_translation(RA,A,_,_) :- fresh_result_variable(RA,A).

can_be_unified_in_translation(_,_,RB,B) :- fresh_result_variable(RB,B).

can_translate_to_setlog(b(E,_T,_I)) :-
    b2p(E,[bind('$NO_ERRORS',pred_true)|_Env],_C),!.

can_translate_to_setlog(E) :-
    debug_mode(on),
    add_message(b2setlog,'Ignoring hypothesis: ',E,E),fail.

can_translate_typing_to_setlog(b(identifier(ID),Type,Pos)) :-
    (simple_finite_type(Type) -> true
    ; only_infinite_type(Type) -> fail
    % TODO: we can check things like set(couple(integer,boolean)) by using range(f) <: BOOL
    ; add_message(b2setlog,'Not translating to Setlog typing for ',ID,Pos),fail
).

convert_setlog_result(success,_). % keep variable, will be bound to solution(_) later

convert_setlog_result(failure,contradiction_found).

convert_setlog_result(time_out,no_solution_found(time_out)).

convert_setlog_result(timeout,no_solution_found(time_out)).

create_dom_pf(A,_,_,Constr) :- is_just_type_and_infinite(A),!,
    % for finite types like BOOL we need to create the constraints below to let Setlog know the cardinality
    Constr=true.

create_dom_pf(A,Func,Env,Constr) :-
    create_subset(Domain,A,Env,SubsetConstr),
    sconj([dompf(Func,Domain),SubsetConstr],Constr).

create_dom_tf(A,Func,Env,Constr) :-
    bexpr2setlog(A,Env,CA,DomType),
    sconj([CA,dompf(Func,DomType)],Constr).

create_domain(A,_,_,Constr) :- is_just_type_and_infinite(A),!, Constr=true.

create_domain(A,Func,Env,Constr) :-
    create_subset(Domain,A,Env,SubsetConstr),
    sconj([dom(Func,Domain),SubsetConstr],Constr).

create_not_dom_pf(A,_,_,Constr) :- is_just_type_and_infinite(A),!,
    % for finite types like BOOL we need to create the constraints below to let Setlog know the cardinality
    Constr=false.

create_not_dom_pf(A,Func,Env,Constr) :-
    create_not_subset(Domain,A,Env,NotSubsetConstr),
    sconj([dompf(Func,Domain),NotSubsetConstr],Constr).

create_not_domain(A,_,_,Constr) :- is_just_type_and_infinite(A),!, Constr=false.

create_not_domain(A,Func,Env,Constr) :-
    create_not_subset(Domain,A,Env,SubsetConstr),
    sconj([dom(Func,Domain),SubsetConstr],Constr).

create_not_range(A,_,_,Constr) :- is_just_type_and_infinite(A),!, Constr=false.

create_not_range(A,Func,Env,Constr) :-
    create_not_subset(Range,A,Env,SubsetConstr),
    sconj([ran(Func,Range),SubsetConstr],Constr).

create_not_subset(SetlogSet1,b(Set2,_,_),Env,Constr) :-
    b2not_mem(Set2,VAR,Env,VAR_NegConstr),!, % we can create a not-membership constraint
    Constr = exists(in(VAR,SetlogSet1),VAR_NegConstr).

create_not_subset(SetlogSet1,BSet2,Env,Constr) :-
    bexpr2setlog(BSet2,Env,CA,SetlogSet2),
    sconj([CA,nsubset(SetlogSet1,SetlogSet2)],Constr).

create_range(A,_,_,Constr) :- is_just_type_and_infinite(A),!, Constr=true.

create_range(A,Func,Env,Constr) :-
    create_subset(Range,A,Env,SubsetConstr),
    sconj([ran(Func,Range),SubsetConstr],Constr).

create_subset(SetlogSet1,b(Set2,_,_),Env,Constr) :-
    b2mem(Set2,VAR,Env,VAR_Constr),!, % we can create a membership constraint
    Constr = foreach(in(VAR,SetlogSet1),VAR_Constr).

create_subset(SetlogSet1,BSet2,Env,Constr) :-
    bexpr2setlog(BSet2,Env,CA,SetlogSet2),
    sconj([CA,subset(SetlogSet1,SetlogSet2)],Constr).

creates_bound_result_variable(b(identifier(_),_,_)).

do_not_generate_errors(Env) :- nonvar(Env), Env=[bind('$NO_ERRORS',V)|_], V==pred_true.

extract_membership(b(member(TID1,Set),pred,_),TID2,Env,Constr,Rest) :-
    same_id(TID1,TID2,_), Rest=b(truth,pred,[]),
    b2p(member(TID1,Set),Env,Constr),
    Constr = in(_,_). % just a simple in constraint; TODO: maybe perform type inference

extract_membership(b(conjunct(LHS,RHS),pred,_),TID,Env,Constr,Rest) :-
    (extract_membership(LHS,TID,Env,Constr,LRest)
    -> conjunct_predicates([LRest,RHS],Rest)
    ; extract_membership(RHS,TID,Env,Constr,RRest),
    conjunct_predicates([LHS,RRest],Rest)
).

fresh_result_variable(RA,BExpr) :- var(RA), \+ creates_bound_result_variable(BExpr).

get_atom(A,R) :- atom(A),!,R=A.

get_atom(Nr,Atom) :- number(Nr), number_codes(Nr,C),atom_codes(Atom,C).

get_path_to_setlog_cli_wrapper_qlf(Path) :-
    absolute_file_name(prob_lib('setlog-cli.qlf'), Path),
    (file_exists(Path) -> true
    ; add_warning(b2setlog,'No setlog wrapper available at: ',Path),
    check_lib_contents(user_error,setlog,verbose),
    fail
).

get_variable_name(Var,Name=Var) :-
    write_to_codes(Var,Codes),
    atom_codes(Name,Codes).

is_just_type_and_infinite(A) :- is_just_type(A),
    get_texpr_type(A,Type),
    is_infinite_type(Type).

is_symbolic_set(integer_set('NATURAL'),VAR,_,'>='(VAR,0),'<'(VAR,0)).

is_symbolic_set(integer_set('NATURAL1'),VAR,_,'>'(VAR,0),'=<'(VAR,0)).

lookup_identifier(Var,ID,Value) :- (var(Var) ; Var==[]), !,
    (lookup_global_constant(ID,Val) -> b2v(Val,[],true,Value) % TODO: remove Env and Constr from b2v pred
    ; b_global_set(ID) -> b2v(global_set(ID),[],true,Value)
    ; Var = [bind(ID,Value)|_]). % add fresh value to environment, this var is not fresh and cannot be freely unified

lookup_identifier([bind(ID1,Val1)|T],ID,Value) :-
    (ID=ID1 -> Value=Val1 % identifier already exists in environment
    ; lookup_identifier(T,ID,Value)).

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

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

negate_pred(member(A,B),not_member(A,B)).

negate_pred(not_member(A,B),member(A,B)).

negate_pred(subset(A,B),not_subset(A,B)).

negate_pred(not_subset(A,B),subset(A,B)).

negate_pred(subset_strict(A,B),not_subset_strict(A,B)).

negate_pred(not_subset_strict(A,B),subset_strict(A,B)).

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

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

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

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

only_infinite_type(integer).

only_infinite_type(real).

only_infinite_type(string).

only_infinite_type(set(T)) :- only_infinite_type(T).

only_infinite_type(couple(A,B)) :- only_infinite_type(A), only_infinite_type(B).

procces_setlog_result_term(setlog_variable_bindings(Bindings),VarNames,_) :- !,
    maplist(process_setlog_binding(VarNames),Bindings).

procces_setlog_result_term(setlog_version(Version),_,_) :- !,
    format('Setlog version: ~w~n',[Version]).

procces_setlog_result_term(setlog_result(Result),_,Res) :- !,
    format('Setlog result: ~w~n',[Result]), % should be success for solved constraint
    (convert_setlog_result(Result,Res) -> true
    ; add_error(b2setlog,'Illegal setlog result:',Result),
    Res = error).

procces_setlog_result_term(_,_,_).

process_setlog_binding(_,true) :- !.

process_setlog_binding(VarNames,'='(VariableName,Term)) :-
    debug_format(9,'~q~n',[equality(VariableName,Term,VarNames)]),
    member(VariableName=Var,VarNames),!,
    if(Var=Term,true,
    format('Cannot apply setlog binding to B: ~w=~w~n',[VariableName,Term])).

process_setlog_binding(_,Binding) :-
    add_error(b2setlog,'Illegal setlog result binding:',Binding).

process_setlog_result([],_,_) :- !.

process_setlog_result(Codes,VarNames,Res) :-
    append("setlog_",_,Codes), % we have a setlog result fact
    skip_until_eol(Codes,Line1,Rest),!,
    %format('Processing : ~s~n',[Line1]),
    read_term_from_codes(Line1,Term,[variable_names(_VN2)]),
    debug_format(19,'Read term: ~w~n',[Term]),
    procces_setlog_result_term(Term,VarNames,Res),
    process_setlog_result(Rest,VarNames,Res).

process_setlog_result(Codes,VarNames,Res) :-
    skip_until_eol(Codes,_Skipping,Rest),!,
    process_setlog_result(Rest,VarNames,Res).

prove_sequent_with_setlog(TGoal,THypotheses,Options,Res) :-
    % build predicate H1 & H2 .... & not Goal
    create_negation(TGoal,NegatedGoal),
    (can_translate_to_setlog(NegatedGoal)
    -> include(can_translate_to_setlog,THypotheses,OkHyps),
    conjunct_predicates([NegatedGoal|OkHyps],Predicate),
    (debug_mode(on) -> write('SETLOG:'),nl,translate:nested_print_bexpr(Predicate),nl ; true),
    solve_pred_with_setlog(Predicate,_,Options,Res)
    ; Res = no_solution_found(cannot_translate_goal)
    ),
    format('Setlog prover result: ~w~n',[Res]).

prove_using_setlog(Goal,Hypotheses,Opts,TimeOutMs,Res) :-
    % quite often 0 or 1 ms are enough for TimeOutMs
    (member(disprover_option(po_label(Label)),Opts) -> true ; Label='?'),
    format('Starting Setlog Prover (timeout ~w ms) for \'~w\' ~n',[TimeOutMs,Label]),
    start_ms_timer(Timer),
    prove_sequent_with_setlog(Goal,Hypotheses,[timeout(TimeOutMs)],Res),
    stop_ms_timer_with_msg(Timer,'Setlog Prover completed').