smt_solvers_interface

add_clause(Solver,LitAvl,Clause,ClauseRef) :-
    maplist(translate_literal(Solver,LitAvl),Clause,ExprList),
    debug_format(9,'Sending clause to solver ~w~n',[ExprList]),
    smt_solver_interface_call(Solver,mk_op_arglist(sat,disjunct,ExprList,ClauseRef)).

add_literal(Solver,Number,Number-Z3Ref) :-
    number_to_atom(Number,Atom),
    smt_solver_interface_call(Solver,mk_bounded_var(sat,boolean,Atom,Z3Ref)).

add_state_to_bindings([], FullBindings, FullBindings).

add_state_to_bindings([bind(IdName,Value)|T], Bindings, FullBindings) :-
    ( member(binding(IdName,ModelValue,_), Bindings)
    -> equal_object(Value, ModelValue),
    NewAcc = Bindings
    ; infer_value_type(Value, Type),
    translate_bexpression(b(value(Value),Type,[]), PrettyValue),
    NewAcc = [binding(IdName,Value,PrettyValue)|Bindings]
    ),
    !,
    add_state_to_bindings(T, NewAcc, FullBindings).

add_state_to_bindings([bind(IdName,_)|_], _, _) :-
    add_error_fail(add_state_to_bindings, 'The synchronisation of the model found by Z3 with the global state bindings failed.', [IdName]).

add_translation_for_solver(TranslationType, Solver, ProBState, Pred, Options, TranslationsAcc, NewAcc, IsUnfilteredTruth, Result) :-
    start_ms_timer(T0),
    smt_clean_up_post(TranslationType, Pred, Options, CPred),
    ( CPred = b(truth,pred,_)
    -> Result = solution([])
    ; CPred = b(falsity,pred,_)
    -> Result = contradiction_found
    ; get_full_pred(TranslationType, Solver, CPred, ProBState, FullPred, FullProBState, Filtered, SkippedVars, UnsupportedLPs),
    stop_ms_timer_with_debug_msg(T0,add_translation_for_solver_preprocessing(TranslationType,Solver)),
    start_ms_timer(T1),
    ( nonvar(FullPred), FullPred = b(truth,pred,_)
    -> % fail if all operators are unsupported
    ( Filtered == false
    -> IsUnfilteredTruth = true,
    NewAcc = TranslationsAcc
    ; add_message(smt_solvers_interface, 'Could not translate predicate for solver: ', Solver:TranslationType),
    add_message(smt_solvers_interface, 'Unsupported predicates: ', UnsupportedLPs),
    fail
    )
    ; IsUnfilteredTruth = false,
    setup_sets(TranslationType, Solver, GlobalIdentifiers),
    find_typed_identifier_uses(FullPred, Ids),
    create_smt_state(TranslationType, Solver, Ids, IdState, _),
    append(IdState, GlobalIdentifiers, GlobalState),
    mk_expr(FullPred, TranslationType, Solver, [], GlobalState, PExpr),
    %format("~w:~n", [TranslationType]), translate:nested_print_bexpr_as_classicalb(FullAxmPred),nl,
    ( debug:debug_mode(on)
    -> translate_bexpression(FullPred, PPPred),
    format('Sending to ~w translation to ~w: ~w~n', [TranslationType,Solver,PPPred])
    ; true
    ),
    flush_output,
    % comment next line in if you want to directly test ProB on the translated constraint:
    %write(solving_with_prob(TranslationType)),nl,(solver_interface:solve_predicate(FullPred,_,3,[],CBCResult) -> write(CBCResult) ; write(fail)),nl,
    Translation = (TranslationType,PExpr,ProBState,FullProBState,Ids,GlobalState,Filtered,SkippedVars,UnsupportedLPs),
    NewAcc = [Translation|TranslationsAcc]
    ),
    stop_ms_timer_with_debug_msg(T1,add_translation_for_solver_core(TranslationType,Solver))
).

backjump_on_symbol(Symbol) :-
    backjumping_symbols(Symbols),
    member(Symbol,Symbols),
    debug_format(9,'smt check for backjump:~ncurrent symbol: ~w~nbackjumping symbols: ~w~n',[Symbol,Symbols]),
    !, debug_format(9,'backjumping!',[]), fail.

backjump_on_symbol(_) :-
    retractall(backjumping_symbols(_)).

binary_operator(floored_div).

binary_operator(equivalence).

binary_operator(implication).

binary_operator(less).

binary_operator(less_equal).

binary_operator(less_real).

binary_operator(less_equal_real).

binary_operator(greater).

binary_operator(greater_equal).

binary_operator(add).

binary_operator(modulo).

binary_operator(minus).

binary_operator(multiplication).

binary_operator(div).

binary_operator(power_of).

binary_operator(member).

binary_operator(subset).

binary_operator(union).

binary_operator(intersection).

binary_operator(set_subtraction).

binary_operator(add_real).

binary_operator(minus_real).

binary_operator(multiplication_real).

binary_operator(div_real).

bind_in_prob_state(Bindings,bind(Id,Val)) :-
    member(binding(Id,Z3Val,_),Bindings), %format('~w: ~w = ~w~n',[Id,Z3Val,Val]),nl,
    % Z3 may return solution in list form, ProB had it in AVL form: hence use equal_object
    equal_object(Z3Val,Val).

check_sat(SelectedSolvers, Solver, UsesDefSet, Translations, Options, Result, SolvedTranslation) :-
    start_ms_timer(T1),
    catch(check_sat_aux(SelectedSolvers, Solver, UsesDefSet, Translations, Options, Result, SolvedTranslation),
    SolverException,
    treat_exception(Solver, SolverException, Result)),
    stop_ms_timer_with_debug_msg(T1,check_sat(SelectedSolvers,Solver, Options)).

check_sat_aux(_, cvc4, UsesDefSet, Translations, Options, Result, SolvedTranslation) :-
    memberchk((axiomatic,AxmPExpr,_,_,_,_,_,_,_), Translations),
    get_smt_time_out(Options,TO),
    smt_solver_interface_call(cvc4, cvc4interface:smt_solve_query(AxmPExpr, TO, SMTResult)),
    get_model_or_return_result(SMTResult, UsesDefSet, TO, axiomatic, Translations, cvc4, Result, SolvedTranslation),
    SolvedTranslation == axiomatic.

check_sat_aux(SelectedSolvers, z3, UsesDefSet, Translations, Options, Result, SolvedTranslation) :-
    ( memberchk((axiomatic,AxmPExpr,_,_,_,_,_,_,_), Translations),
    !
    ; AxmPExpr = -1 % do not solve any Z3 formula with axiomatic solver
    ),
    ( memberchk((constructive,CnsPExpr,_,_,_,_,_,_,_), Translations),
    !
    ; CnsPExpr = -1 % do not solve any Z3 formula with constructive solver
    ),
    ( memberchk((sat,SatPExpr,_,_,_,_,_,_,_), Translations),
    !
    ; SatPExpr = -1
    ),
    get_smt_time_out(Options,TO),
    % format('Calling Z3 with time-out ~w, solvers:~w (~w:~w)~n',[TO,SelectedSolvers,AxmPExpr,CnsPExpr]),
    % Selected Solvers can be axm_inc, axm_ninc, sat or cns_ninc
    smt_solver_interface_call(z3, z3interface:smt_solve_query(SelectedSolvers, AxmPExpr, CnsPExpr, SatPExpr, TO, SMTResultData)),
    ( debug_level_active_for(9)
    -> write('; SMT TRANSLATION: '), nl, pretty_print_smt(z3), nl
    ; true
    ),
    SMTResultData = result_tuple(TempSolvedTranslation,SMTResult),
    %format('Calling get_model_or_return_result ~w~n',[SMTResult]),
    get_model_or_return_result(SMTResult, UsesDefSet, TO, TempSolvedTranslation, Translations, z3, Result, SolvedTranslation).

cleanup_core_for_backjumping([],[]).

cleanup_core_for_backjumping([E|Es],[CE|CEs]) :-
    split_atom(E,['|'],[CE]),
    cleanup_core_for_backjumping(Es,CEs).

clear_state :-
    reset_interface(z3),
    garbage_collect,
    trimcore,
    retractall(solve_in_state),
    model_translation:clear_translation_state.

combine_satisfiable_component_results([], SatComponentResult, NResultAcc) :-
    !,
    NResultAcc = SatComponentResult.

combine_satisfiable_component_results(solution(AccBindings), solution(ComponentBindings), NResultAcc) :-
    append(AccBindings, ComponentBindings, NAccBindings),
    NResultAcc = solution(NAccBindings).

constraint_uses_unfixed_deferred_set(Constraint, UsesDefSet) :-
    find_typed_identifier_uses(Constraint, [], UsedIds),
    ( list_contains_unfixed_deferred_set_id(UsedIds)
    -> UsesDefSet = true
    ; UsesDefSet = false
).

contains_introduced_identifiers(FreeIDs,TExpr) :-
    syntaxtraversion(TExpr,_,Type,Infos,Subs,_),
    (member(introduced_by(_),Infos) % identifier that has been introduced
    -> % check if it is not bound by some quantifiers
    get_texpr_id(TExpr,Identifier),
    member(b(identifier(Identifier),Type,_),FreeIDs)
    ; some(contains_introduced_identifiers(FreeIDs),Subs)).

contains_solver_name_with_prefix(Prefix, SelectedSolvers) :-
    member(Name, SelectedSolvers),
    atom_prefix(Prefix, Name),
    !.

contains_unsupported_aux(TranslationType, Solver, TExpr, Expr) :-
    get_texpr_expr(TExpr, Expr),
    get_texpr_type(TExpr, Type),
    ( unsupported_type(TranslationType, Type, Solver)
    -> debug:debug_println(9,unsupported_type(TranslationType,Type,Solver))
    ; ( unsupported_expr(TranslationType, Expr, Type, Solver)
    -> functor(Expr,F,A),
    debug:debug_println(9,unsupported_expr(TranslationType,F/A))
)
).

contains_unsupported_type_or_expression(TranslationType, Solver, TExpr) :-
    contains_unsupported_type_or_expression(TranslationType, Solver, TExpr, _).

contains_unsupported_type_or_expression(TranslationType, Solver, TExpr, Unsupported) :-
    map_over_typed_bexpr(smt_solvers_interface:contains_unsupported_aux(TranslationType, Solver), TExpr, Unsupported).

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

convert_to_cnf_model([_-X|T],Nr,[Lit|TM]) :-
    is_bool(X,Val),!,
    (Val=true -> Lit=Nr ; Lit is -Nr),
    N1 is Nr+1,
    convert_to_cnf_model(T,N1,TM).

convert_to_cnf_model(L,_,R) :- add_error(smt_solvers_interface,'Invalid model value:',L),R=[].

create_bounded_smt_identifier(TranslationType, Solver, b(identifier(Id),Type,_Infos), id(Id,Expr), Expr) :-
    ground(Id),
    !,
    smt_solver_interface_call(Solver,mk_bounded_var(TranslationType, Type,Id,Expr)).

create_bounded_smt_identifier(_, _, b(identifier(_),Type,_Infos), _, _) :-
    add_error_fail(create_bounded_smt_identifier, 'Identifier name is not ground for type ~w~n', [Type]).

create_bounded_smt_state(TranslationType, Solver,Identifiers,State,Exprs) :-
    maplist(create_bounded_smt_identifier(TranslationType, Solver),Identifiers,State,Exprs).

create_enum_element_smt_state([], [], []).

create_enum_element_smt_state([IdName|TIds], [EnumExpr|TExprs], [id(IdName,EnumExpr)|T]) :-
    create_enum_element_smt_state(TIds, TExprs, T).

create_exprs_for_rec_value_fields([], [], _, _, _, _, []).

create_exprs_for_rec_value_fields([field(Name,Type)|TT], [field(Name,Value)|FT], TranslationType, Solver, LS, GS, [Expr|NT]) :-
    mk_value(Type, Value, TranslationType, Solver, LS, GS, Expr),
    create_exprs_for_rec_value_fields(TT, FT, TranslationType, Solver, LS, GS, NT).

create_let_state([],[],_,_,S,_,S).

create_let_state([ID|IDs],[Def|Defs],TranslationType, Solver,StateSoFar,GS,State) :-
    get_texpr_id(ID,UnwrappedId),
    mk_expr(Def,TranslationType, Solver,StateSoFar,GS,Expr),
    create_let_state(IDs,Defs,TranslationType, Solver,[id(UnwrappedId,Expr)|StateSoFar],GS,State).

create_smt_identifier(TranslationType, Solver,b(identifier(Id),Type,_Infos),id(Id,Expr),Expr) :-
    ground(Id),
    !,
    smt_solver_interface_call(Solver,mk_var(TranslationType, Type,Id,Expr)).

create_smt_identifier(_, _, b(identifier(_),Type,_Infos), _, _) :-
    add_error_fail(create_smt_identifier, 'Identifier name is not ground for type ~w~n', [Type]).

create_smt_state(TranslationType, Solver,Identifiers,State,Exprs) :-
    exclude(is_external_function_identifier,Identifiers,LessIdentifiers),
    maplist(create_smt_identifier(TranslationType, Solver),LessIdentifiers,State,Exprs).

create_term_size_pairs([], []).

create_term_size_pairs([component(C,_)|T], [NTS-C|NT]) :-
    term_size(C, TS),
    NTS is TS * -1, % so that we can use keysort which sorts in ascending order
    create_term_size_pairs(T, NT).

create_virtual_enum_elms(DefaultSetSize, DefSet, DefElms) :-
    create_virtual_enum_elms(1, DefaultSetSize, DefSet, DefElms).

create_virtual_enum_elms(Counter, DefaultSetSize, _, Out) :-
    Counter > DefaultSetSize,
    !,
    Out = [].

create_virtual_enum_elms(Counter, DefaultSetSize, DefSet, [EnumElm|NT]) :-
    number_codes(Counter, NC),
    atom_codes(AC, NC),
    atom_concat(DefSet, AC, EnumElm),
    Counter1 is Counter + 1,
    assert_virtual_deferred_set_id(EnumElm, fd(Counter,DefSet)),
    create_virtual_enum_elms(Counter1, DefaultSetSize, DefSet, NT).

filter_unsupported_types_or_expressions(_, _, [], [], []).

filter_unsupported_types_or_expressions(TranslationType, Solver, [LP|T], FilteredLPs, UnsupportedLPs) :-
    contains_unsupported_type_or_expression(TranslationType, Solver, LP),
    !,
    UnsupportedLPs = [LP|TUnsupportedLPs],
    filter_unsupported_types_or_expressions(TranslationType, Solver, T, FilteredLPs, TUnsupportedLPs).

filter_unsupported_types_or_expressions(TranslationType, Solver, [LP|T], [LP|TFilteredLPs], UnsupportedLPs) :-
    filter_unsupported_types_or_expressions(TranslationType, Solver, T, TFilteredLPs, UnsupportedLPs).

gen_leading_zeros(Nr,Lim) --> {Nr>Lim},!.

gen_leading_zeros(Nr,Lim) --> [0'0], {N1 is Nr*10}, gen_leading_zeros(N1,Lim).

get_couple_types_comp_args([Arg1,Arg2|T], CoupleTypes) :-
    Arg1 = b(identifier(_),Type1,_),
    Arg2 = b(identifier(_),Type2,_),
    get_couple_types_comp_args(T, couple(Type1,Type2), [couple(Type1,Type2)|D]-D, CoupleTypes).

get_couple_types_comp_args([], _, CoupleTypes-D, CoupleTypes) :-
    D = [].

get_couple_types_comp_args([Arg|T], LastCoupleType, Acc-D, CoupleTypes) :-
    Arg = b(identifier(_),Type,_),
    D = [couple(LastCoupleType,Type)|ND],
    get_couple_types_comp_args(T, couple(LastCoupleType,Type), Acc-ND, CoupleTypes).

get_full_pred(TranslationType, Solver, Pred, ProBState, FullPred, FullProBState, Filtered, SkippedVars, UnsupportedLPs) :-
    find_typed_identifier_uses(Pred, Identifiers),
    remove_useless_bindings(ProBState, Identifiers, FullProBState),
    create_state_pred(Identifiers, [], FullProBState, StatePred, [skipped_variables(SkippedVars)]),
    % print(state),nl,translate:nested_print_bexpr(StatePred),nl,
    safe_create_texpr(conjunct(StatePred,Pred), pred, [], FullConj),
    conjunction_to_list(FullConj, LPs),
    filter_unsupported_types_or_expressions(TranslationType, Solver, LPs, FilteredLPs, UnsupportedLPs),
    ( same_length(LPs, FilteredLPs)
    -> Filtered = false
    ; Filtered = true,
    ( debug_mode(off)
    -> true
    ; include(contains_unsupported_type_or_expression(TranslationType, Solver), LPs, Unsupported),
    conjunct_predicates(Unsupported,US),
    add_message(Solver, 'Unsupported constraints were discarded for SMT solver: ', US, US)
    )
    ),
    conjunct_predicates(FilteredLPs, FullPred).

get_model_or_return_result(unsat, UsesDefSet, _, SolvedTranslation, _, _, Solution, SolvedTranslationOut) :-
    get_preference(z3_solve_for_animation, true), % behave such as ProB by considering DEFAULT_SETSIZE
    !,
    SolvedTranslation = SolvedTranslationOut,
    ( (UsesDefSet == true, \+ solve_in_state)
    -> Solution = no_solution_found(unfixed_deferred_sets)
    ; Solution = contradiction_found
).

get_model_or_return_result(unsat, _, _, SolvedTranslation, _, _, contradiction_found, SolvedTranslation).

get_model_or_return_result(unknown, _, _, SolvedTranslation, _, _, no_solution_found(solver_answered_unknown), SolvedTranslation).

get_model_or_return_result(time_out, _, _, SolvedTranslation, _, _, time_out, SolvedTranslation).

get_model_or_return_result(sat, _, TO, SolvedTranslation, Translations, Solver, Solution, SolvedTranslation) :-
    memberchk((SolvedTranslation,_,ProBState,_,Ids,GlobalState,_,_,UnsupportedLPs), Translations),
    ( UnsupportedLPs \== []
    -> add_message(get_model_or_return_result, 'A solution has been found but some predicates are not supported and were not considered: ', UnsupportedLPs),
    Solution = no_solution_found(solver_answered_unknown)
    ; exclude(is_smt_temp_var, Ids, FilteredIDs),
    % we replaced ProBState ids with values in ast_cleanup_for_smt so we add them to the solution here
    ( catch(
    translate_smt_model_to_b_values_with_timeout(TO,Solver, GlobalState, FilteredIDs, Bindings),
    E,
    (add_error(smt_solvers_interface,'Exception in model translation: ',E),
    throw(model_translation_failed)))
    -> ( (
    get_preference(z3_solve_for_animation, true),
    % Z3 behaves as ProB by considering its deferred set size preference
    \+ consistent_deferred_set_sizes
    )
    -> Solution = no_solution_found(unfixed_deferred_sets)
    ; add_state_to_bindings(ProBState, Bindings, FullBindings),
    maplist(bind_in_prob_state(FullBindings), ProBState)
    -> % for this solution, Z3 possibly considered a smaller deferred set size than ProB
    % if Z3 considered a larger deferred set size, an error would have been thrown by model_translation:handle_globalsets_fdrange_contradiction/2
    ( \+ consistent_deferred_set_sizes
    -> add_message(get_model_or_return_result, 'Deferred set size considered by Z3 is smaller than the one of ProB (DEFAULT_SETSIZE)')
    ; true
    ),
    Solution = solution(FullBindings)
    ; throw(model_solution_extraction_failed)
    )
    ; add_warning(smt_solvers_interface,'Failure in model translation: ',Solver),
    throw(model_translation_failed)
)
).

get_smt_time_out(Options,TO) :-
    member(smt_time_out_factor(TOFactor),Options),!,
    get_time_out_with_factor(TOFactor,TO).

get_smt_time_out(_,TO) :- get_preference(time_out, TO).

init_smt_supported_interpreter :-
    retractall(backjumping_symbols(_)), %clean smt backjumping information
    (get_preference(smt_supported_interpreter,true) -> init_interface(z3) ; true).

is_bool('z3-define-fun'([],'Bool',Val),Val).

is_external_function_identifier(Id) :-
    get_texpr_id(Id,Name),
    is_external_function_name(Name).

is_ground_real(b(unary_minus_real(Real),real,_)) :-
    is_ground_real(Real).

is_ground_real(b(real(_),real,_)).

is_ground_real(b(value(_),real,_)).

known_solver_exception(model_translation_failed, model_translation_failed).

known_solver_exception(z3_exception(Reason), Reason).

known_solver_exception(logic_exception(Reason), Reason).

known_solver_exception(error(representation_error(nofit(integer)),representation_error(_,_,nofit(integer))), integer_overflow).

lookup(Id,LS,GS,Expr) :-
    ( member(id(Id,Expr),LS) % id defined in local store
    ; member(id(Id,Expr),GS) % id defined in global store
).

lookup_literal(Literal,LitAvl,Z3Expr) :-
    avl_fetch(Literal,LitAvl,Z3Expr).

mk_deferred_set_identifiers(_, cvc4, _, []).

mk_deferred_set_identifiers(TranslationType, z3, DeferredSets, DefSetIdentifiers) :-
    maplist(mk_deferred_set_identifiers2(TranslationType), DeferredSets, DefSetIdentifiers).

mk_deferred_set_identifiers2(TranslationType, SetName, id(SetName, SetExpression)) :-
    smt_solver_interface_call(z3, mk_full_set(TranslationType, set(global(SetName)), SetExpression)).

mk_expr(b(Op,Type,_Infos),TranslationType,Solver,LS,GS,Expr) :-
    mk_expr_aux(Op,Type,TranslationType,Solver,LS,GS,Expr).

mk_expr_aux(first_of_pair(Couple), _, TranslationType, Solver, LS, GS, Expr) :-
    get_texpr_type(Couple, CoupleType),
    mk_expr(Couple, TranslationType, Solver, LS, GS, AE),
    smt_solver_interface_call(Solver, mk_op_couple_prj(TranslationType, first, AE, CoupleType, Expr)).

mk_expr_aux(second_of_pair(Couple), _, TranslationType, Solver, LS, GS, Expr) :-
    get_texpr_type(Couple, CoupleType),
    mk_expr(Couple, TranslationType, Solver, LS, GS, AE),
    smt_solver_interface_call(Solver, mk_op_couple_prj(TranslationType, second, AE, CoupleType, Expr)).

mk_expr_aux(interval(A1,A2), _, TranslationType, Solver, LS, GS, Expr) :-
    !,
    mk_expr(A1, TranslationType, Solver, LS, GS, AE1),
    mk_expr(A2, TranslationType, Solver, LS, GS, AE2),
    smt_solver_interface_call(Solver, mk_op_interval(TranslationType, AE1, AE2, Expr)).

mk_expr_aux(direct_product(Arg1,Arg2), Type, TranslationType, Solver, LS, GS, Expr) :-
    !,
    Type = set(CoupleOutType),
    CoupleOutType = couple(_,Couple2Type),
    mk_expr(Arg1, TranslationType, Solver, LS, GS, Arg1E),
    mk_expr(Arg2, TranslationType, Solver, LS, GS, Arg2E),
    Arg1 = b(_,set(CoupleType1),_),
    Arg2 = b(_,set(CoupleType2),_),
    smt_solver_interface_call(Solver, mk_op_direct_product(TranslationType, Arg1E, Arg2E, Couple2Type, CoupleType1, CoupleType2, CoupleOutType, Expr)).

mk_expr_aux(parallel_product(Arg1,Arg2), Type, TranslationType, Solver, LS, GS, Expr) :-
    !,
    Type = set(CoupleOutType),
    mk_expr(Arg1, TranslationType, Solver, LS, GS, Arg1E),
    mk_expr(Arg2, TranslationType, Solver, LS, GS, Arg2E),
    Arg1 = b(_,set(CoupleType1),_),
    Arg2 = b(_,set(CoupleType2),_),
    CoupleOutType = couple(ExistsCoupleType1,ExistsCoupleType2),
    smt_solver_interface_call(Solver, mk_op_parallel_product(TranslationType, Arg1E, Arg2E, CoupleType1, CoupleType2, ExistsCoupleType1, ExistsCoupleType2, CoupleOutType, Expr)).

mk_expr_aux(composition(Arg1,Arg2), Type, TranslationType, Solver, LS, GS, Expr) :-
    !,
    Type = set(CoupleOutType),
    Arg1 = b(_,set(CoupleType1),_),
    CoupleType1 = couple(A,B),
    Arg2 = b(_,set(CoupleType2),_),
    CoupleType2 = couple(B,C),
    CoupleOutType = couple(A,C),
    mk_expr(Arg1, TranslationType, Solver, LS, GS, Arg1E),
    mk_expr(Arg2, TranslationType, Solver, LS, GS, Arg2E),
    smt_solver_interface_call(Solver, mk_op_composition(TranslationType, Arg1E, Arg2E, B, CoupleType1, CoupleType2, CoupleOutType, Expr)).

mk_expr_aux(cartesian_product(A1,A2), Type, TranslationType, Solver, LS, GS, Expr) :-
    !,
    Type = set(CoupleType),
    mk_expr(A1, TranslationType, Solver, LS, GS, AE1),
    mk_expr(A2, TranslationType, Solver, LS, GS, AE2),
    smt_solver_interface_call(Solver, mk_op_cartesian(TranslationType, AE1, AE2, CoupleType, Expr)).

mk_expr_aux(identity(A), Type, TranslationType, Solver, LS, GS, Expr) :-
    !,
    Type = set(CoupleType),
    CoupleType = couple(InnerSetType,_),
    mk_expr(A, TranslationType, Solver, LS, GS, AE),
    smt_solver_interface_call(Solver, mk_op_identity(TranslationType, AE, InnerSetType, CoupleType, Expr)).

mk_expr_aux(reverse(A), Type, TranslationType, Solver, LS, GS, Expr) :-
    !,
    Type = set(CoupleType),
    mk_expr(A, TranslationType, Solver, LS, GS, AE),
    smt_solver_interface_call(Solver, mk_op_reverse(TranslationType, AE, CoupleType, Expr)).

mk_expr_aux(comprehension_set(Args,Body), Type, TranslationType, Solver, LS, GS, Expr) :-
    LambdaId = b(identifier('_lambda_result_'),_,_),
    select(LambdaId, Args, LambdaArgs),
    create_bounded_smt_state(TranslationType, Solver, LambdaArgs, State, ArgsE),
    ArgsE = [Arg],
    append(State, LS, NLS),
    conjunction_to_list(Body, ConjList),
    select(b(equal(LambdaId,BodyExpr),pred,Info), ConjList, RestConjList),
    member(prob_annotation('LAMBDA-EQUALITY'), Info),
    conjunct_predicates(RestConjList, BodyPred),
    Type = set(CoupleType),
    !,
    mk_expr(BodyExpr, TranslationType, Solver, NLS, GS, BodyE),
    mk_expr(BodyPred, TranslationType, Solver, NLS, GS, BodyP),
    smt_solver_interface_call(Solver, mk_op_lambda(TranslationType, Arg, BodyP, BodyE, CoupleType, Expr)).

mk_expr_aux(comprehension_set(Args,Body), _, TranslationType, Solver, LS, GS, Expr) :-
    !,
    create_bounded_smt_state(TranslationType, Solver, Args, State, ArgsE),
    append(State, LS, NLS),
    mk_expr(Body, TranslationType, Solver, NLS, GS, BodyE),
    length(ArgsE, ArgAmount),
    ( ArgAmount == 1
    -> ArgsE = [Arg],
    smt_solver_interface_call(Solver, mk_op_comprehension_set_singleton(TranslationType, Arg, BodyE, Expr))
    ; get_couple_types_comp_args(Args, CoupleTypes),
    smt_solver_interface_call(Solver, mk_op_comprehension_set_multi(TranslationType, ArgsE, CoupleTypes, BodyE, Expr))
).

mk_expr_aux(image(A,B), _, TranslationType, Solver, LS, GS, Expr) :-
    !,
    A = b(_,set(couple(Prj1Type,Prj2Type)),_),
    mk_expr(A, TranslationType, Solver, LS, GS, AE),
    mk_expr(B, TranslationType, Solver, LS, GS, BE),
    smt_solver_interface_call(Solver, mk_op_image(TranslationType, AE,BE,couple(Prj1Type,Prj2Type),Prj1Type,Prj2Type,Expr)).

mk_expr_aux(conjunct(A,B),pred,TranslationType, Solver,LS,GS,Expr) :-
    !,
    conjunction_to_list(b(conjunct(A,B),pred,[]),List),
    maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),List,ExprList), % apply mk_expr on List
    % truth/0 are removed from the conjunction during list / from list
    % the list might be empty now!
    ( ExprList = []
    -> smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr))
    ; ( ExprList = [X]
    -> Expr = X
    ; smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, conjunct,ExprList,Expr))
)
).

mk_expr_aux(disjunct(A,B),pred,TranslationType, Solver,LS,GS,Expr) :-
    !,
    disjunction_to_list(b(disjunct(A,B),pred,[]),List),
    maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),List,ExprList),
    smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, disjunct,ExprList,Expr)).

mk_expr_aux(if_then_else(Pred,A,B),_,TranslationType, Solver,LS,GS,Expr) :-
    !,
    maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),[Pred,A,B],ArgList),
    smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, if_then_else,ArgList,Expr)).

mk_expr_aux(partition(S,Sets),pred,TranslationType, Solver,LS,GS,Expr) :-
    !,
    % definition: sets are disjoint and S is the union
    maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),Sets,SetExprs),
    pairwise_union(TranslationType,SetExprs,Solver,UnionOfSets),
    mk_expr(S,TranslationType, Solver,LS,GS,SExpr),
    smt_solver_interface_call(Solver,mk_op(TranslationType, equal,SExpr,UnionOfSets,EqualToUnion)), % S = Union(Sets)
    % enforce sets pairwise disjoint (= intersection is empty)
    get_texpr_type(S,Type),
    smt_solver_interface_call(Solver,mk_empty_set(TranslationType, Type,EmptySet)),
    pairwise_disjoint(TranslationType,SetExprs,Solver,EmptySet,PWConstraint),
    smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, conjunct,[EqualToUnion,PWConstraint],Expr)).

mk_expr_aux(forall(IDs,b(truth,pred,_),B),pred,TranslationType, Solver,LS,GS,Expr) :-
    !,
    create_bounded_smt_state(TranslationType, Solver,IDs,State,SMTExprs),
    append(State,LS,NLS),
    mk_expr(B,TranslationType, Solver,NLS,GS,BE),
    smt_solver_interface_call(Solver,mk_quantifier(TranslationType, forall,SMTExprs,BE,Expr)).

mk_expr_aux(forall(IDs,A,B),pred,TranslationType, Solver,LS,GS,Expr) :-
    !,
    create_bounded_smt_state(TranslationType, Solver,IDs,State,SMTExprs),
    append(State,LS,NLS),
    mk_expr(A,TranslationType, Solver,NLS,GS,AE), mk_expr(B,TranslationType, Solver,NLS,GS,BE),
    smt_solver_interface_call(Solver,mk_op(TranslationType, implication,AE,BE,InnerExpr)),
    smt_solver_interface_call(Solver,mk_quantifier(TranslationType, forall,SMTExprs,InnerExpr,Expr)).

mk_expr_aux(exists(IDs,B),pred,TranslationType, Solver,LS,GS,Expr) :-
    !,
    create_bounded_smt_state(TranslationType, Solver,IDs,State,SMTExprs),
    append(State,LS,NLS),
    mk_expr(B,TranslationType, Solver,NLS,GS,InnerExpr),
    smt_solver_interface_call(Solver,mk_quantifier(TranslationType, exists,SMTExprs,InnerExpr,Expr)).

mk_expr_aux(equal(A,B),pred,TranslationType, Solver,LS,GS,Expr) :-
    !,
    mk_expr(A,TranslationType, Solver,LS,GS,AE),
    mk_expr(B,TranslationType, Solver,LS,GS,BE),
    get_texpr_type(A,Type),
    ( Type = boolean
    -> smt_solver_interface_call(Solver, mk_op(TranslationType, equivalence, AE, BE, Expr))
    ; smt_solver_interface_call(Solver, mk_op(TranslationType, equal, AE, BE, Expr))
).

mk_expr_aux(convert_int_floor(Real),integer,TranslationType, Solver,LS,GS,Expr) :-
    mk_expr(Real, TranslationType, Solver, LS, GS, RealExpr),
    !,
    number_codes(RealExpr, ECodes),
    append([102,108,111,111,114], ECodes, EECodes),
    atom_codes(EAtom, EECodes),
    ( is_ground_real(Real)
    -> IsGroundArg = 1
    ; IsGroundArg = 0
    ),
    smt_solver_interface_call(Solver,mk_op_floor(TranslationType,IsGroundArg,EAtom,RealExpr,Expr)).

mk_expr_aux(convert_int_ceiling(Real),integer,TranslationType, Solver,LS,GS,Expr) :-
    mk_expr(Real, TranslationType, Solver, LS, GS, RealExpr),
    !,
    number_codes(RealExpr, ECodes),
    append([99,101,105,108,105,110,103], ECodes, EECodes),
    atom_codes(EAtom, EECodes),
    ( is_ground_real(Real)
    -> IsGroundArg = 1
    ; IsGroundArg = 0
    ),
    smt_solver_interface_call(Solver,mk_op_ceiling(TranslationType,IsGroundArg,EAtom,RealExpr,Expr)).

mk_expr_aux(rec(ListOfFields),Type,TranslationType, Solver,LS,GS,Expr) :-
    !,
    findall(FieldExpr, member(field(_,FieldExpr),ListOfFields), FieldExprs),
    maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),FieldExprs,SMTFieldExprs),
    smt_solver_interface_call(Solver,mk_record_const(TranslationType, Type,SMTFieldExprs,Expr)).

mk_expr_aux(record_field(Record,FieldName),Type,TranslationType, Solver,LS,GS,Expr) :-
    !,
    get_texpr_type(Record,record(RFields)),
    nth0(FieldNr,RFields,field(FieldName,Type)),
    % debug_format(9,'Field: ~w Type: ~w~n-> FieldNr: ~w~n',[FieldName,RFields,FieldNr]),
    mk_expr(Record,TranslationType, Solver,LS,GS,SMTRecordExpr),
    smt_solver_interface_call(Solver,mk_record_field(TranslationType, SMTRecordExpr,FieldNr,Expr)).

mk_expr_aux(couple(A,B),Type,TranslationType, Solver,LS,GS,Expr) :-
    !,
    mk_expr(A,TranslationType, Solver,LS,GS,AE),
    mk_expr(B,TranslationType, Solver,LS,GS,BE),
    smt_solver_interface_call(Solver,mk_couple(TranslationType, Type,AE,BE,Expr)).

mk_expr_aux(identifier(Id),_,_,_Solver,LS,GS,Expr) :-
    !,
    lookup(Id,LS,GS,Expr).

mk_expr_aux(real(RealAtom),real,TranslationType, Solver,_LS,_GS,Expr) :-
    !,
    smt_solver_interface_call(Solver,mk_real_const(TranslationType, RealAtom,Expr)).

mk_expr_aux(integer(Int),integer,TranslationType, Solver,_LS,_GS,Expr) :-
    !,
    smt_solver_interface_call(Solver,mk_int_const(TranslationType, Int,Expr)).

mk_expr_aux(min_int,integer,TranslationType, Solver,_LS,_GS,Expr) :-
    !,
    get_preference(minint,MinInt),
    smt_solver_interface_call(Solver,mk_int_const(TranslationType, MinInt,Expr)).

mk_expr_aux(max_int,integer,TranslationType, Solver,_LS,_GS,Expr) :-
    !,
    get_preference(maxint,MaxInt),
    smt_solver_interface_call(Solver,mk_int_const(TranslationType, MaxInt,Expr)).

mk_expr_aux(boolean_true,boolean,_,Solver,_LS,_GS,Expr) :-
    !,
    smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr)).

mk_expr_aux(boolean_false,boolean,_,Solver,_LS,_GS,Expr) :-
    !,
    smt_solver_interface_call(Solver,mk_bool_const(boolean_false,Expr)).

mk_expr_aux(string(S),string,TranslationType,Solver,_LS,_GS,Expr) :-
    !,
    smt_solver_interface_call(Solver,mk_string_const(TranslationType, S,Expr)).

mk_expr_aux(truth,pred,_,Solver,_LS,_GS,Expr) :-
    !,
    smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr)).

mk_expr_aux(falsity,pred,_,Solver,_LS,_GS,Expr) :-
    !,
    smt_solver_interface_call(Solver,mk_bool_const(boolean_false,Expr)).

mk_expr_aux(bool_set,set(boolean),TranslationType, Solver,_LS,_GS,Expr) :-
    !,
    smt_solver_interface_call(Solver,mk_bool_const(boolean_true,True)),
    smt_solver_interface_call(Solver,mk_bool_const(boolean_false,False)),
    smt_solver_interface_call(Solver,mk_set(TranslationType, [True,False],Expr)).

mk_expr_aux(set_extension(List),set(T),TranslationType, Solver,LS,GS,Expr) :-
    !,
    maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),List,SubExprs),
    ( SubExprs = []
    -> smt_solver_interface_call(Solver,mk_empty_set(TranslationType, set(T),Expr))
    ; smt_solver_interface_call(Solver,mk_set(TranslationType, SubExprs,Expr))
).

mk_expr_aux(empty_set,Type,TranslationType, Solver,_LS,_GS,Expr) :-
    !,
    smt_solver_interface_call(Solver,mk_empty_set(TranslationType, Type,Expr)).

mk_expr_aux(value(V),Type,TranslationType, Solver,LS,GS,Expr) :-
    !,
    mk_value(Type,V,TranslationType, Solver,LS,GS,Expr).

mk_expr_aux(convert_bool(P),boolean,TranslationType, Solver,LS,GS,Expr) :-
    !,
    mk_expr(P,TranslationType, Solver,LS,GS,Expr).

mk_expr_aux(let_expression(ListOfIDs,ListOfDefinitions,LetExpression),_Type,TranslationType, Solver,LS,GS,Expr) :-
    create_let_state(ListOfIDs,ListOfDefinitions,TranslationType, Solver,LS,GS,NewLS),
    !,
    mk_expr(LetExpression,TranslationType, Solver,NewLS,GS,Expr).

mk_expr_aux(let_predicate(ListOfIDs,ListOfDefinitions,LetExpression),pred,TranslationType, Solver,LS,GS,Expr) :-
    create_let_state(ListOfIDs,ListOfDefinitions,TranslationType, Solver,LS,GS,NewLS),
    !,
    mk_expr(LetExpression,TranslationType, Solver,NewLS,GS,Expr).

mk_expr_aux(Op, Type, TranslationType, Solver, LS, GS, Expr) :-
    functor(Op, Functor, 1),
    (Functor == pow_subset; Functor == pow1_subset; Functor == fin_subset; Functor == fin1_subset),
    !,
    arg(1, Op, A),
    Type = set(set(InnerSetType)),
    mk_expr(A, TranslationType, Solver, LS, GS, AE),
    ( Functor == pow_subset
    -> smt_solver_interface_call(Solver, mk_op_pow_subset(TranslationType, AE, set(InnerSetType), Expr))
    ; Functor == pow1_subset
    -> smt_solver_interface_call(Solver, mk_op_pow1_subset(TranslationType, AE, set(InnerSetType), InnerSetType, Expr))
    ; Functor == fin_subset
    -> smt_solver_interface_call(Solver, mk_op_fin_subset(TranslationType, AE, set(InnerSetType), Expr))
    ; smt_solver_interface_call(Solver, mk_op_fin1_subset(TranslationType, AE, set(InnerSetType), InnerSetType, Expr))
).

mk_expr_aux(Op, _, TranslationType, Solver, LS, GS, Expr) :-
    functor(Op, Functor, 1),
    (Functor == domain; Functor == range),
    !,
    arg(1, Op, A),
    mk_expr(A, TranslationType, Solver, LS, GS, AE),
    A = b(_,set(CoupleType),_),
    CoupleType = couple(Prj1Type,Prj2Type),
    ( Functor == domain
    -> smt_solver_interface_call(Solver, mk_op_domain(TranslationType, AE, CoupleType, Prj1Type, Prj2Type, Expr))
    ; smt_solver_interface_call(Solver, mk_op_range(TranslationType, AE, CoupleType, Prj1Type, Prj2Type, Expr))
).

mk_expr_aux(Op, Type, TranslationType, Solver, LS, GS, Expr) :-
    functor(Op, Functor, 2),
    (Functor == domain_restriction; Functor == domain_subtraction; Functor == range_restriction; Functor == range_subtraction),
    !,
    Type = set(CoupleType),
    arg(1, Op, A1),
    arg(2, Op, A2),
    mk_expr(A1, TranslationType, Solver, LS, GS, AE1),
    mk_expr(A2, TranslationType, Solver, LS, GS, AE2),
    ( Functor == domain_restriction
    -> smt_solver_interface_call(Solver, mk_op_dom_res(TranslationType, AE1, AE2, CoupleType, Expr))
    ; Functor == domain_subtraction
    -> smt_solver_interface_call(Solver, mk_op_dom_sub(TranslationType, AE1, AE2, CoupleType, Expr))
    ; Functor == range_restriction
    -> smt_solver_interface_call(Solver, mk_op_ran_res(TranslationType, AE1, AE2, CoupleType, Expr))
    ; smt_solver_interface_call(Solver, mk_op_ran_sub(TranslationType, AE1, AE2, CoupleType, Expr))
).

mk_expr_aux(Op,_,TranslationType, Solver,LS,GS,Expr) :-
    functor(Op,Functor,1),
    unary_operator(Functor),
    !,
    arg(1,Op,A),
    mk_expr(A,TranslationType, Solver,LS,GS,AE),
    smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, Functor, [AE], Expr)).

mk_expr_aux(Op, _, TranslationType, Solver, LS, GS, Expr) :-
    functor(Op, Functor, 1),
    ( Functor == general_union; Functor == general_intersection),
    !,
    arg(1, Op, A),
    A = b(_,set(set(InnerType)),_),
    mk_expr(A, TranslationType, Solver, LS, GS, AE),
    ( Functor == general_union
    -> smt_solver_interface_call(Solver, mk_op_general_union(TranslationType, AE, set(InnerType), InnerType, Expr))
    ; store_explicit_set_unique_id(A, UniqueIdName),
    smt_solver_interface_call(Solver, mk_op_general_intersection(TranslationType, UniqueIdName, AE, set(InnerType), InnerType, Expr))
).

mk_expr_aux(Op,_,TranslationType, Solver,LS,GS,Expr) :-
    functor(Op,Functor,2),
    binary_operator(Functor),
    !,
    arg(1,Op,A),
    mk_expr(A,TranslationType, Solver,LS,GS,AE),
    arg(2,Op,B),
    mk_expr(B,TranslationType, Solver,LS,GS,BE),
    smt_solver_interface_call(Solver,mk_op(TranslationType, Functor,AE,BE,Expr)).

mk_expr_aux(Expr,_,_,_,_,_,_) :- !,
    add_error_fail(smt_solvers_interface,'mk_expr failed',Expr).