model_translation

any_but_newline --> [C], {C \= 10}, !, any_but_newline.

any_but_newline -->"\n", {inc_linecount},!, ws.

assert_virtual_deferred_set_id(EnumElm, FdVar) :-
    asserta(virtual_deferred_set_id(EnumElm, FdVar)).

atom_to_term(Atom, Term) :-
    atom_concat(Atom, '.', AtomWithStop),
    atom_codes(AtomWithStop, AtomWithStopC),
    read_from_codes(AtomWithStopC, Term).

check_value(_,identifier(A),_,_) :- atom(A),!.

check_value(integer,I,SV,PP) :- \+ (I=int(Nr), number(Nr)),!,
    add_internal_error('Illegal Z3 value, not number computed:', PP:SV:I), fail.

check_value(boolean,B,SV,PP) :- B \= pred_true , B\= pred_false, !,
    add_internal_error('Illegal Z3 value, not boolean computed:', PP:SV:B), fail.

check_value(_,_,_,_).

clear_translation_state :-
    retractall(virtual_deferred_set_id(_,_)),
    retractall(fd_var_of_z3(_,_)),
    retractall(explicit_set_cache(_, _)).

closed_lisp_style_expressions(Res) --> real_ws,!,
    closed_lisp_style_expressions(Res).

closed_lisp_style_expressions([]) --> ")",!.

closed_lisp_style_expressions([E|Es]) -->
    lisp_style_expression(E), !,
    closed_lisp_style_expressions(Es).

compute_bcomp_set(CompSet,ResultOut) :-
    % translate:set_unicode_mode,translate:print_bexpr(CompSet),
    b_compute_expression_nowf(CompSet,[],[],Res,'translating Z3 value',0),
    (try_expand_custom_set_to_list(Res,ResultOut,true,z3_set_to_b_set)
    -> true
    ; ResultOut = Res).

consistent_deferred_set_sizes :-
    findall(DS, (b_global_deferred_set(DS), unfixed_deferred_set(DS)), DeferredSets),
    consistent_deferred_set_sizes(DeferredSets).

consistent_deferred_set_sizes([]).

consistent_deferred_set_sizes([DeferredSet|T]) :-
    findall(FdVarOfZ3, retract(fd_var_of_z3(DeferredSet,FdVarOfZ3)), FdVarsOfZ3),
    FdVarsOfZ3 \== [],
    !,
    max_member(MaxFdVarOfZ3, FdVarsOfZ3),
    ( get_user_defined_scope(DeferredSet,Low,Up,_Span)
    -> DeferredSetSize is 1+Up-Low
    ; get_preference(globalsets_fdrange, DeferredSetSize)
    ),
    % the case for MaxFdVarOfZ3 > DeferredSetSize is already handled in handle_globalsets_fdrange_contradiction
    MaxFdVarOfZ3 == DeferredSetSize,
    consistent_deferred_set_sizes(T).

consistent_deferred_set_sizes([_|T]) :-
    % this deferred set is not part of the solution and can be ignored
    consistent_deferred_set_sizes(T).

create_nested_binary_expr(BOP, Env, Type, TA, TB, [Arg1,Arg2|T], Expr) :-
    translate_z3_expr(Arg1, Env, TA, TArg1),
    get_texpr_type(TArg1, TA),
    translate_z3_expr(Arg2, Env, TB, TArg2),
    get_texpr_type(TArg2, TB),
    TExpr =.. [BOP,TArg1,TArg2],
    Acc = b(TExpr,Type,[]),
    create_nested_binary_expr(BOP, Env, Type, TA, TB, Acc, T, Expr).

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

create_nested_binary_expr(BOP, Env, Type, _, TB, Acc, [Arg], Expr) :-
    !,
    translate_z3_expr(Arg, Env, TB, TArg),
    TExpr =.. [BOP,Acc,TArg],
    Expr = b(TExpr,Type,[]).

create_nested_binary_expr(BOP, Env, Type, TA, TB, Acc, [Arg|T], Expr) :-
    translate_z3_expr(Arg, Env, TA, TArg),
    TExpr =.. [BOP,Acc,TArg],
    NAcc = b(TExpr,Type,[]),
    create_nested_binary_expr(BOP, Env, Type, TA, TB, NAcc, T, Expr).

digit(D) --> [D], {48 =< D, D =< 57}.

expect(L,_) --> L,!.

expect(L,Ctxt,In,_) :- linecount(Line),
    format("lisp-style parser failed on line ~w expecting ~s for ~w on: ~s~n",[Line,L,Ctxt, In]),fail.

get_couple_type_from_atom(CoupleAtom, CoupleType1, CoupleType2) :-
    atom(CoupleAtom),
    atom_codes(CoupleAtom, Codes),
    get_couple_type_from_codes([TT1,TT2], Codes, []),
    atom_codes(T1Atom, TT1),
    atom_to_term(T1Atom, CoupleType1),
    atom_codes(T2Atom, TT2),
    atom_to_term(T2Atom, CoupleType2).

get_couple_type_from_codes([T1,T2]) -->
    "couple(",
    type_symbol(T1),
    ",",
    type_symbol(T2),
    ")".

get_full_model_as_avl(z3,AVL) :- !,
    % get and parse the full model
    smt_solver_interface_call(z3,get_full_model_string(FullModel)),
    %format('z3 full model:~n~w~n',[FullModel]),
    z3_model_to_avl(FullModel,AVL).

get_full_model_as_avl(_,AVL) :- empty_avl(AVL).

get_typing_predicates(BVars, TypingPredList) :-
    get_typing_predicates(BVars, [], [], TypingPredList).

get_typing_predicates([], NotCached, Acc, TypingPredList) :-
    translate:generate_typing_predicates(NotCached, TTypingPredList),
    append(Acc, TTypingPredList, TypingPredList).

get_typing_predicates([BVar|T], NotCached, Acc, TypingPredList) :-
    BVar = b(identifier(IdName),_,_),
    explicit_set_cache(IdName, ExplicitSet),
    !,
    TypingPred = b(member(BVar,ExplicitSet),pred,[]),
    get_typing_predicates(T, NotCached, [TypingPred|Acc], TypingPredList).

get_typing_predicates([BVar|T], NotCached, Acc, TypingPredList) :-
    get_typing_predicates(T, [BVar|NotCached], Acc, TypingPredList).

handle_globalsets_fdrange_contradiction(Z3sResNumber,Set) :-
    get_user_defined_scope(Set,Low,Up,Span),!,
    DeferredSetSize is 1+Up-Low,
    Z3sResNumber > DeferredSetSize,
    add_error(translate_z3_expr_globalsets_fdrange,
    'Z3\'s solution contradicts the size set for the deferred set. Try to increase the set size by adapting the DEFINITION or -card command-line argument.',
    z3:Z3sResNumber:Set:DeferredSetSize,Span),
    fail.

handle_globalsets_fdrange_contradiction(Z3sResNumber,_Set) :-
    get_preference(globalsets_fdrange, DeferredSetSize),
    ( Z3sResNumber > DeferredSetSize
    -> % Z3 does not consider globalsets_fdrange; its solution might contradict ProB's preference
    add_error_fail(translate_z3_expr_globalsets_fdrange,
    'Z3\'s solution contradicts ProB\'s preference DEFAULT_SETSIZE. Try to increase the preference.',
    z3:Z3sResNumber:'DEFAULT_SETSIZE':DeferredSetSize)
    ; % this is any other bug and should not happen
    fail
).

in_couple(Cs1, Cs2) -->
    type_symbol(Cs1), !,
    expect(",", in_couple),
    type_symbol(Cs2).

inc_linecount :- retract(linecount(Nr)), N1 is Nr+1, assertz(linecount(N1)).

is_global_type_variable_name(env(Ids,_), VarName, GlobalType) :-
    member(b(identifier(VarName),GlobalType,_), Ids),
    GlobalType = global(_).

is_global_type_variable_name(_, VarName, global(Set)) :-
    split_atom(VarName, ['!'], [Set,_,_]),
    b_global_set(Set).

linecount(1).

lisp_style_expression(Iteration) --> "((_ |iteration_", rel_type_skip, "| 0)", ws,
    closed_lisp_style_expressions([Arg1,Arg2]), ws, !, {Iteration = [iteration,Arg1,Arg2]}.

lisp_style_expression(A) --> real(Cs), !, {atom_codes(A, Cs)}.

lisp_style_expression(L) --> "!", !, ws, lisp_style_expression(L), ws, ":weight", ws, number(_). % optional term parameter

lisp_style_expression(A) --> "/0", !, {A = '/0'}. % weird special case when using reals, e.g., for ':z3 a:REAL & b/=0.0 & a=1.2/b' a function called '/0' is defined

lisp_style_expression(A) --> z3_op(Cs), !, {atom_codes(A, Cs)}.

lisp_style_expression(A) --> typed_couple_top_level(Cs), !, {atom_codes(A, Cs)}.

lisp_style_expression(A) --> non_empty_symbol(Cs), !, {atom_codes(A, Cs)}.

lisp_style_expression(N) --> number(Cs), !, {number_codes(N, Cs)}.

lisp_style_expression(N) --> "-", number(Cs), !, {number_codes(N2,Cs), N is -N2}.

lisp_style_expression(A) --> string(Codes), !, {atom_codes(A,Codes)}.

lisp_style_expression(List) --> "(", !, closed_lisp_style_expressions(List).

lisp_style_expression(record_type(Fields)) -->
    "[#", !, ws, record_type_fields(Fields),!,
    ws, expect("#]",record_type).

lisp_style_expression(_,In,_) :- In \= [], % not at end of string
    linecount(Line),
    format("lisp-style parser failed on line ~w on: ~s~n",[Line,In]),fail.

lisp_style_expressions(Res) --> real_ws,!,
    lisp_style_expressions(Res).

lisp_style_expressions([E|Es]) -->
    lisp_style_expression(E), !,
    lisp_style_expressions(Es).

lisp_style_expressions([]) --> [].

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

map_translate_z3_expr([Z3Pred|T], Env, Acc, Preds) :-
    translate_z3_expr(Z3Pred, Env, _, Pred),
    map_translate_z3_expr(T, Env, [Pred|Acc], Preds).

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

map_translate_z3_predicate([Z3Pred|T], Env, Acc, Preds) :-
    translate_z3_predicate(Z3Pred, Env, Pred),
    map_translate_z3_predicate(T, Env, [Pred|Acc], Preds).

non_empty_symbol([A|As]) -->
    [A],
    { 65 =< A, A =< 90
    ; 97 =< A, A =< 122
    % ; 48 =< A, A =< 57
    ; 913 =< A, A =< 937 % upper-case greek letters
    ; 945 =< A, A =< 969 % lower-case greek letters
    ; A = 124 % "|"
    ; A = 95 % "_",
    ; A = 45 % "-"
    ; A = 39 % "'"
    ; A = 33 % "!"
    ; 60 =< A, A =< 62 % "<", "=", ">"
    },!,
    symbol(As).

number([D|Ds]) --> digit(D), number(Ds).

number([D]) --> digit(D).

parse_lisp_style_expressions(L) -->
    {reset_line_count},
    lisp_style_expressions(L),!.

parse_uc(Id) -->
    "uc__SORT_TYPE_var_", number(_),
    "__", number(N), {number_codes(Id,N)}.

real(R) -->
    number(I),
    ".",
    number(D),
    ( "?",
    !
    ;
    ),
    {append([I,[46],D],R)}.

real_ws --> "\n", {inc_linecount},!, ws.

real_ws --> [W], {W = 32 ; W = 10 ; W = 13}, !, ws.

real_ws --> ";;", !, any_but_newline.

record_type_field(field(NameA,TypeA)) -->
    non_empty_symbol(Name), ":(TYPE_CONSTANT ", non_empty_symbol(Type), " type)",
    {atom_codes(NameA,Name),atom_codes(TypeA,Type)}.

record_type_fields([F|Fields]) -->
    record_type_field(F), ws, expect(",",record_type_field), !,
    ws, record_type_fields(Fields).

record_type_fields([F]) --> record_type_field(F).

rel_type_skip -->
    "set(couple(", type_symbol(_), ",", type_symbol(_), "))".

reset_line_count :- retractall(linecount(_)), assertz(linecount(1)).

store_explicit_set_unique_id(SetAst, UniqueIdName) :-
    get_texpr_type(SetAst, Type),
    unique_typed_id("inner_set", Type, UniqueId),
    UniqueId = b(identifier(UniqueIdName),_,_),
    asserta(explicit_set_cache(UniqueIdName, SetAst)).

string(Codes) --> "\"", string_symbol(Codes), "\"".

string_symbol([34|As]) -->
    % Z3 escapes double quotes with double quotes while ProB uses \
    [34,34],
    string_symbol(As).

string_symbol([A|As]) -->
    [A],
    { 35 =< A, A =< 126
    ; A = 33 % "!"
    },
    string_symbol(As).

string_symbol([]) --> "".

symbol([A|As]) -->
    [A],
    { 65 =< A, A =< 90
    ; 97 =< A, A =< 122
    ; 48 =< A, A =< 57
    ; 913 =< A, A =< 937 % upper-case greek letters
    ; 945 =< A, A =< 969 % lower-case greek letters
    ; A = 124 % "|"
    ; A = 95 % "_",
    ; A = 45 % "-"
    ; A = 39 % "'"
    ; A = 33 % "!"
    ; 60 =< A, A =< 62 % "<", "=", ">"
    ; A = 8242 % Unicode Prime, should we also allow this as first symbol?
    },!,
    symbol(As).

symbol([]) --> "".

translate_cvc4_record(field(Name,BType),CVCVal,field(Name,BVal)) :-
    translate_cvc4_tree(CVCVal,BType,BVal).

translate_cvc4_tree(['CONST_RATIONAL',Arg],integer,int(Val)) :-
    arg_is_number(Arg,Val).

translate_cvc4_tree(['CONST_BOOLEAN',1],boolean,pred_true).

translate_cvc4_tree(['CONST_BOOLEAN',0],boolean,pred_false).

translate_cvc4_tree(['CONST_STRING',Content],string,string(Content)).

translate_cvc4_tree(['SINGLETON',ValIn],set(X),[ValOut]) :-
    translate_cvc4_tree(ValIn,X,ValOut).

translate_cvc4_tree(['EMPTYSET',emptyset,_Type],set(_),[]).

translate_cvc4_tree(['TUPLE',V1,V2],couple(Type1,Type2),(TV1,TV2)) :-
    translate_cvc4_tree(V1,Type1,TV1),
    translate_cvc4_tree(V2,Type2,TV2).

translate_cvc4_tree(['APPLY_CONSTRUCTOR','__cvc4_tuple_ctor',V1,V2],couple(Type1,Type2),(TV1,TV2)) :-
    translate_cvc4_tree(V1,Type1,TV1),
    translate_cvc4_tree(V2,Type2,TV2).

translate_cvc4_tree(['UNION',V1,V2],set(X),Val) :-
    translate_cvc4_tree(V1,set(X),TV1),
    translate_cvc4_tree(V2,set(X),TV2),
    append(TV1,TV2,Val).

translate_cvc4_tree(['UNINTERPRETED_CONSTANT',C],global(SId),fd(PBCId,SId)) :-
    atom_codes(C,CCodes),
    parse_uc(CId,CCodes,[]),
    PBCId is CId + 1.

translate_cvc4_tree(['RECORD',_CVCRecordType|Fields],record(RFields),rec(FieldsOut)) :-
    maplist(translate_cvc4_record,RFields,Fields,FieldsOut).

translate_smt_model_to_b_value(Solver,State,FullModelAVL,
    b(identifier(Id),Type,_Infos),binding(Id,Value,PPValue)) :-
    member(id(Id,Expr),State),
    smt_solver_interface_call(Solver,get_model_string(Expr,String)), !,
    atom_codes(String,Codes),
    %format('Result of get_model_string:~n~s~n---~n',[Codes]),
    parse_lisp_style_expressions([E],Codes,[]), !,
    (Solver == cvc4 -> translate_cvc4_tree(E,Type,Value) ;
    Solver == z3 -> translate_z3_tree_for_id(Id,E,FullModelAVL,Type,Value) ;
    fail),
   
    (translate_bvalue(Value,PPValue) -> true ; PPValue='**pretty-print failed**').

translate_smt_model_to_b_values(Solver,State,Identifiers,Bindings) :-
    get_full_model_as_avl(Solver,AVL), % parse it only once for all identifiers
    maplist(translate_smt_model_to_b_value(Solver,State,AVL),Identifiers,Bindings).

translate_z3_connective(BOP, T, Env, PredRes) :-
    map_translate_z3_predicate(T, Env, [], NT),
    ( BOP == conjunct
    -> conjunct_predicates(NT, PredRes)
    ; BOP == disjunct
    -> disjunct_predicates(NT, PredRes)
    ; Pred =.. [BOP|NT],
    safe_create_texpr(Pred, pred, PredRes)
).

translate_z3_expr(['-',Number],_,integer,Res) :-
    !,
    Number1 is -Number,
    Res=b(integer(Number1),integer,[]).

translate_z3_expr(Int,_,integer,Res) :- integer(Int),!, Res=b(integer(Int),integer,[]).

translate_z3_expr(true,_,boolean,Res) :- !, Res=b(boolean_true,boolean,[]).

translate_z3_expr(false,_,boolean,Res) :- !, Res=b(boolean_false,boolean,[]).

translate_z3_expr([ZOP|T], Env, boolean, Res) :-
    z3_connective_to_b(ZOP, BOP),
    !,
    translate_z3_connective(BOP, T, Env, PredRes),
    Res = b(convert_bool(PredRes),boolean,[]).

translate_z3_expr(['-',RealAtom], Env, real, Res) :-
    atom(RealAtom),
    atom_concat('-', RealAtom, NRealAtom),
    translate_z3_expr(NRealAtom, Env, real, Res).

translate_z3_expr(Atom, _, Type, Res) :-
    atom(Atom),
    virtual_deferred_set_id(Atom, FdVar),
    FdVar = fd(_,DefSet),
    Type = global(DefSet),
    !,
    Res = b(value(FdVar),Type,[]).

translate_z3_expr(Atom, _, Type, Res) :-
    atom(Atom),
    ( ( split_atom(Atom,['!'],Splitted),
    Splitted = [Set,val,InternalNumber]
    )
    -> Type = global(Set),
    !,
    convert_to_number(InternalNumber,Nr),
    ResNumber is Nr + 1,
    Val = fd(ResNumber,Set),
    asserta(fd_var_of_z3(Set,ResNumber)),
    ( global_type(Val,Set)
    -> true
    ; handle_globalsets_fdrange_contradiction(ResNumber,Set)
    ),
    safe_create_texpr(value(Val), global(Set), Res)
    ; % atom could represent a real number
    Type = real,
    atom_to_number(Atom, Real),
    float(Real), !,
    safe_create_texpr(real(Atom), real, Res)
).

translate_z3_expr(Nr,_,global(GS),Res) :- number(Nr),!, % Z3 represents first element of GS by 0, ...
    Nr1 is Nr+1, Val = fd(Nr1,GS),
    asserta(fd_var_of_z3(GS,Nr1)),
    ( global_type(Val,GS)
    -> true
    ; handle_globalsets_fdrange_contradiction(Nr1,GS)
    ),
    safe_create_texpr(value(Val), global(GS), Res).

translate_z3_expr([Couple,A,B],Env,couple(T1,T2),b(couple(AT,BT),couple(T1,T2),[])) :-
    atom(Couple),
    get_couple_type_from_atom(Couple, T1, T2),
    translate_z3_expr(A, Env, T1, AT),
    translate_z3_expr(B, Env, T2, BT).

translate_z3_expr([CouplePrj,Arg], Env, Type, Res) :-
    atom(CouplePrj),
    translate_z3_expr(Arg, Env, _, RArg),
    get_texpr_type(RArg, CType),
    ( atom_prefix('get_x_couple', CouplePrj),
    PrjNode = first_of_pair(RArg),
    CType = couple(ResType,_)
    ; atom_prefix('get_y_couple', CouplePrj),
    PrjNode = second_of_pair(RArg),
    CType = couple(_,ResType)
    ),
    !,
    Type = ResType,
    safe_create_texpr(PrjNode, ResType, Res).

translate_z3_expr(Id, env(Env,_AVL), Type, Res) :-
    atom(Id),
    TId = b(identifier(Id),Type,_),
    member(TId, Env),
    !,
    Res = TId.

translate_z3_expr(Id, _, Type, Res) :-
    atom(Id),
    Type = global(_),
    % global ids which are not in the environment
    !,
    safe_create_texpr(identifier(Id), Type, Res).

translate_z3_expr(CstFunc,env(Env,AVL),Type,CompSet) :- atom(CstFunc),
    Type = set(couple(PType,RType)),
    avl_fetch(CstFunc,AVL,'z3-define-fun'([[ParamName,ParameterType]],ReturnType,BodyTree)),
    z3_type_to_b_type(ParameterType,PType), % check if type matches
    z3_type_to_b_type(ReturnType,RType), % ditto
    !,
    PID = b(identifier(ParamName),PType,[]),
    %print(translate_body(CstFunc,PID)),nl,
    translate_z3_expr(BodyTree,env([PID|Env],AVL),RType,BodyExpr),
    %print(body(CstFunc)),translate:print_bexpr(BodyExpr),nl,
    unique_typed_id("lambda",RType,LambdaID),
    create_equality(LambdaID,BodyExpr,CPred),
    % {PID,lambda | lambda = BodyExpr}
    safe_create_texpr(comprehension_set([PID,LambdaID],CPred), set(couple(PType,RType)), CompSet).

translate_z3_expr([CstFunc,Arg],env(Env,AVL),Type,Res) :- % function application
    avl_fetch(CstFunc,AVL,'z3-define-fun'([[ParamID,ParameterType]],ReturnType,BodyTree)),
    z3_type_to_b_type(ReturnType,Type), % check if type matches
    !,
    ( ParamID == Arg % special case if argument and parameter identical
    -> translate_z3_expr(BodyTree,env(Env,AVL),Type,Res)
    ; z3_type_to_b_type(ParameterType,PType), % TO DO: couple-> ground type; PType could be not ground !
    translate_z3_expr(CstFunc,env(Env,AVL),set(couple(PType,Type)),TFun),
    translate_z3_expr(Arg,env(Env,AVL),PType,TArg),
    create_texpr(function(TFun,TArg),Type,[contains_wd_condition],Res)
).

translate_z3_expr([let,[[Id,Val]],Function],Env,Type,Res) :- !,
    z3_replace_let_id_by_value(Id,Val,Function,NewFunction),
    translate_z3_expr(NewFunction,Env,Type,Res).

translate_z3_expr([let,[[Id,Val]|T],Function],Env,Type,Res) :-
    T \== [],
    z3_replace_let_id_by_value(Id,Val,Function,NewFunction),
    translate_z3_expr([let,T,NewFunction],Env,Type,Res).

translate_z3_expr([ZOP, Left], Env, Type,Res) :-
    z3_unary_expr_to_b(ZOP, BOP, Type),!,
    translate_z3_expr(Left, Env, Type, TL),
    Expr =.. [BOP,TL],
    safe_create_texpr(Expr, Type, Res).

translate_z3_expr([ZOP|Args], Env, Type, Res) :-
    % operators such as multiplication can have an arbitrary arity like [*,x,x,x]
    z3_binary_expr_to_b(ZOP, BOP, TA, TB, Type), !,
    create_nested_binary_expr(BOP, Env, Type, TA, TB, Args, Res).

translate_z3_expr([ite, Test, Left, Right], Env, Type, Res) :- !,
    translate_z3_predicate(Test,Env, BTest),
    translate_z3_expr(Left, Env, Type, BThen),
    translate_z3_expr(Right,Env, Type, BElse), get_texpr_type(BThen,Type),
    safe_create_texpr(if_then_else(BTest,BThen,BElse),Type,Res).

translate_z3_expr(String,_,string,Res) :-
    atom(String),
    !,
    Res = b(string(String),string,[]).

translate_z3_expr(['_','as-array',AuxFunName],_,set(X),Res) :- !,
    % set is represented by aux function
    translate_z3_expr_using_full_model(AuxFunName,set(couple(X,boolean)),ChFunSet),
    % we computed the characteristic function of the set; now convert it to a set
    % Now we need to compute dom(ChFunSet |> {TRUE}) = ChFunSet~[{TRUE}] = {x|ChFunSet(x)=TRUE}
    unique_typed_id("el!",X,Element),
    create_texpr(function(ChFunSet,Element),boolean,[contains_wd_condition],FCall),
    create_equality(b(boolean_true,boolean,[]),FCall,NewNewPred),
    safe_create_texpr(comprehension_set([Element],NewNewPred),set(X),CompSet),
    % translate:print_bexpr(CompSet),nl,
    compute_bcomp_set(CompSet,Set),
    Res = b(value(Set),set(X),[]).

translate_z3_expr([store,Sub,Entry,TStoreRes],Env,set(Type),Res) :-
    % TStoreRes can be true, false or a predicate which needs to be evaluated first
    translate_z3_expr(Sub,Env,set(Type),S1),
    translate_z3_expr(Entry,Env,Type,El2),
    S2 = b(set_extension([El2]),set(Type),[]),
    ( (TStoreRes = true; TStoreRes = false)
    -> StoreRes = TStoreRes
    ; translate_z3_predicate(TStoreRes, Env, BStoreRes),
    ( b_test_boolean_expression_cs(BStoreRes, [], [],'translating Z3 value',0)
    -> StoreRes = true
    ; StoreRes = false
    )
    ),
    ( StoreRes = true
    -> Expr = union(S1,S2)
    ; StoreRes = false,
    Expr = set_subtraction(S1,S2)
    ),
    !,
    b_compute_expression_nowf(b(Expr,set(Type),[]), [], [], List,'translating Z3 value',0),
    Res = b(value(List),set(Type),[]).

translate_z3_expr([[as,const,['Array',Z3Type,'Bool']],false],_,Type,b(value([]),Type,[])) :-
    ( (Type = set(BType), z3_type_to_b_type(Z3Type,BType))
    -> true
    ; add_error(translate_z3_expr,'Unexpected type in Z3 model: ',types(Z3Type,Type))
    ),
    !.

translate_z3_expr([[as,const,['Array',Z3Type,'Bool']],true],_,Type,b(value(Res),Type,[])) :-
    ( (Type = set(BType), z3_type_to_b_type(Z3Type,BType))
    -> b_type2_set(BType,Res),
    !
    ; add_error(translate_z3_expr,'Unexpected type in Z3 model: ',types(Z3Type,Type)),
    fail
).

translate_z3_expr(['record'|Z3Fields],Env,record(Fields),b(rec(FieldsOut),record(Fields),[])) :-
    maplist(translate_z3_record(Env),Fields,Z3Fields,FieldsOut).

translate_z3_expr([iteration,Rel,Int],Env,set(CoupleType),Res) :-
    translate_z3_expr(Rel,Env,set(CoupleType),TRel),
    translate_z3_expr(Int,Env,integer,BInt),
    Iteration = b(iteration(TRel,BInt),set(CoupleType),[]),
    ( BInt = b(integer(_),_,_)
    -> compute_bcomp_set(Iteration,Set),
    Res = b(value(Set),set(CoupleType),[])
    ; Res = Iteration
).

translate_z3_expr([lambda,[[ClosureVar,ClosureVarType]],Body],Env,SetType,Res) :-
    ( ClosureVar = refl_closure_g_u_var
    -> Functor = reflexive_closure
    ; ClosureVar = closure_g_u_var,
    Functor = closure
    ),
    !,
    z3_type_to_b_type(ClosureVarType,BType),
    TClosureVar = b(identifier(ClosureVar),BType,[]),
    % compute closure with ProB if Z3 does not unfold lambda,
    % the translated model itself (lambda(exists(...))) is too complex so we catch translated closures here
    Env = env(Ids,B),
    translate_z3_predicate(Body, env([TClosureVar|Ids],B), TBody),
    TBody = b(exists(_,ExistsBody),pred,_),
    conjunction_to_list(ExistsBody, ExistsBodyConj),
    member(b(exists(_,ExistsBody2),pred,_), ExistsBodyConj),
    conjunction_to_list(ExistsBody2, ExistsBodyConj2),
    member(b(equal(b(identifier(_),SetType,_),b(iteration(TRel,_),SetType,_)),pred,[]), ExistsBodyConj2),
    !,
    BNode =.. [Functor,TRel],
    TRes = b(BNode,SetType,[]),
    clean_up(TRes, [], Res).

translate_z3_expr([lambda,Args,Body],env(Ids,_),set(BType),Res) :-
    % see for instance ':z3-double-check f = %x.(x : INTEGER|x * x * x) & f(f(x)) = y & y = 512'
    Args = [[ID,Z3Type]],
    z3_type_to_b_type(Z3Type,BType),
    TID = b(identifier(ID),BType,[]),
    Body = [exists|_],
    translate_z3_predicate(Body,env([TID|Ids],empty),TBody),
    TBody = b(exists([LambdaID],ExistsBody),pred,_),
    conjunction_to_list(ExistsBody, ExistsList),
    select(ExistsBody, ExistsList, RestExistsList),
    ExistsBody = b(equal(CoupleCst,ExistCouple),pred,_),
    CoupleCst = b(identifier('_couple_cst'),couple(_,_),_),
    conjunct_predicates(RestExistsList, RestExistsBody),
    !,
    ExistCouple = b(couple(_,ExistsExpr),_,_),
    safe_create_texpr(lambda([LambdaID],RestExistsBody,ExistsExpr), set(BType), BLambda),
    clean_up(BLambda, [], CompSet),
    compute_bcomp_set(CompSet,Set),
    Res = b(value(Set),set(BType),[]).

translate_z3_expr([lambda,Args,Body],env(Ids,B),set(BType),Res) :-
    Args = [[ID,Z3Type]], % TO DO: more than one argument?
    z3_type_to_b_type(Z3Type,BType),
    !,
    TID = b(identifier(ID),BType,[]),
    translate_z3_predicate(Body,env([TID|Ids],B),TBody),
    safe_create_texpr(comprehension_set([TID],TBody),set(BType),CompSet),
    %print('lambda: '),translate:print_bexpr(CompSet),nl, print(CompSet),nl,
    compute_bcomp_set(CompSet,Set),
    Res = b(value(Set),set(BType),[]).

translate_z3_expr([['_',map,AndOrTerm]|T], Env, _, Res) :-
    ( AndOrTerm = [AndOr,['Bool','Bool'],'Bool'] % prior version 4.12.2
    ; AndOrTerm = AndOr % since version 4.12.2
    ),
    ( AndOr == and
    ; AndOr == or
    ),
    !,
    map_translate_z3_expr(T, Env, [], TT),
    TT = [b(_,SetType,_)|_],
    ( AndOr == and
    -> unfold_general_intersection(TT, SetType, Res)
    ; unfold_general_union(TT, SetType, Res)
).

translate_z3_expr([mod,A,B], Env, integer, Res) :-
    !,
    translate_z3_expr(A, Env, integer, BA),
    translate_z3_expr(B, Env, integer, BB),
    BIsZero = b(equal(BB,b(integer(0),integer,[])),pred,[]),
    % return 0 if B is zero, otherwise (= (mod x y) (- x (* y (div x y)))) holds
    ModEq = b(minus(BA,b(multiplication(BB,
    b(floored_div(BA,BB),integer,[contains_wd_condition])),integer,[contains_wd_condition])),
    integer,[contains_wd_condition]),
    safe_create_texpr(if_then_else(BIsZero,b(integer(0),integer,[]),ModEq),integer,TRes),
    clean_up(TRes, [], Res).

translate_z3_expr([rem,A,B], Env, integer, Res) :-
    !,
    translate_z3_expr(A, Env, integer, BA),
    translate_z3_expr(B, Env, integer, BB),
    BIsZero = b(equal(BB,b(integer(0),integer,[])),pred,[]),
    BLowerZero = b(less(BB,b(integer(0),integer,[])),pred,[]),
    % return 0 if B is zero, otherwise (= (rem x y) (ite (< y 0) (* (- x (* y (div x y))) -1) (- x (* y (div x y))))) holds
    ModEq = b(minus(BA,b(multiplication(BB,
    b(floored_div(BA,BB),integer,[contains_wd_condition])),integer,[contains_wd_condition])),
    integer,[contains_wd_condition]),
    safe_create_texpr(if_then_else(BLowerZero,b(unary_minus(ModEq),integer,[]),ModEq),integer,IfExpr),
    safe_create_texpr(if_then_else(BIsZero,b(integer(0),integer,[]),IfExpr),integer,TRes),
    clean_up(TRes, [], Res).

translate_z3_expr(Expr,_,Type,_) :-
    \+ check_error_occured(translate_z3_expr_globalsets_fdrange, _),
    add_error_fail(translate_z3_expr, 'Missing translation for Z3 expression:', Expr:Type).

translate_z3_expr_using_full_model(Expr,Type,Result) :-
    get_full_model_as_avl(z3,AVL),
    translate_z3_expr(Expr,env([],AVL),Type,Result).

translate_z3_predicate([not,Left], Env, Res) :-
    !,
    translate_z3_predicate(Left, Env, TL),
    create_negation(TL,Res).

translate_z3_predicate([ZOP|T], Env, Res) :-
    z3_connective_to_b(ZOP, BOP),
    !,
    translate_z3_connective(BOP, T, Env, Res).

translate_z3_predicate([let,[[Id,Val]],Function], Env, Res) :-
    !,
    z3_replace_let_id_by_value(Id, Val, Function, NewFunction),
    translate_z3_predicate(NewFunction, Env, Res).

translate_z3_predicate([let,[[Id,Val]|T],Function], Env, Res) :-
    !,
    T \== [],
    z3_replace_let_id_by_value(Id, Val, Function, NewFunction),
    translate_z3_predicate([let,T,NewFunction], Env, Res).

translate_z3_predicate([=,Left,Right], Env, Res) :-
    !,
    typecheck_for_global_type(Left, Right, Env, Type),
    translate_z3_expr(Left, Env, Type, TL),
    translate_z3_expr(Right, Env, Type, TR),
    create_equality(TL,TR,Res).

translate_z3_predicate([ZOP,Left,Right], Env, Res) :-
    z3_integer_comparison(ZOP, BOP),
    !,
    translate_z3_expr(Left, Env, IntegerOrReal, TL),
    translate_z3_expr(Right, Env, IntegerOrReal, TR),
    Pred =.. [BOP,TL,TR],
    safe_create_texpr(Pred,pred,Res).

translate_z3_predicate([select,Array,Entry], Env, Res) :-
    !,
    translate_z3_expr(Array, Env, _, BSet),
    translate_z3_expr(Entry, Env, _, BEntry),
    Res = b(member(BEntry,BSet),pred,[]).

translate_z3_predicate([exists,Vars,[Body]], Env, Res) :-
    translate_z3_quantified_vars(Vars, Env, [], BVars),
    Env = env(Ids,AVL),
    append(Ids, BVars, NewIds),
    translate_z3_predicate(Body, env(NewIds,AVL), BBody),
    !,
    find_identifier_uses(BBody, [], UsedIds),
    Res = b(exists(BVars,BBody),pred,[used_ids(UsedIds)]).

translate_z3_predicate([exists,Vars,Body], Env, Res) :-
    translate_z3_quantified_vars(Vars, Env, [], BVars),
    Env = env(Ids,AVL),
    append(Ids, BVars, NewIds),
    translate_z3_predicate(Body, env(NewIds,AVL), BBody),
    !,
    find_identifier_uses(BBody, [], UsedIds),
    Res = b(exists(BVars,BBody),pred,[used_ids(UsedIds)]).

translate_z3_predicate([forall,Vars,[Body]], Env, Res) :-
    translate_z3_quantified_vars(Vars, Env, [], BVars),
    Env = env(Ids,AVL),
    append(Ids, BVars, NewIds),
    translate_z3_predicate(Body, env(NewIds,AVL), BBody),
    !,
    find_identifier_uses(BBody, [], UsedIds),
    get_typing_predicates(BVars, TypingPredList),
    conjunct_predicates(TypingPredList, TypingPred),
    Res = b(forall(BVars,TypingPred,BBody),pred,[used_ids(UsedIds)]).

translate_z3_predicate([forall,Vars,Body], Env, Res) :-
    translate_z3_quantified_vars(Vars, Env, [], BVars),
    Env = env(Ids,AVL),
    append(Ids, BVars, NewIds),
    translate_z3_predicate(Body, env(NewIds,AVL), BBody),
    !,
    find_identifier_uses(BBody, [], UsedIds),
    get_typing_predicates(BVars, TypingPredList),
    conjunct_predicates(TypingPredList, TypingPred),
    Res = b(forall(BVars,TypingPred,BBody),pred,[used_ids(UsedIds)]).

translate_z3_predicate([ite, Test, Left, Right], Env, Res) :- !,
    translate_z3_predicate(Test,Env, BTest),
    translate_z3_predicate(Left, Env, BThen),
    translate_z3_predicate(Right,Env, BElse),
    safe_create_texpr(convert_bool(BThen),boolean,BThenBool),
    safe_create_texpr(convert_bool(BElse),boolean,BElseBool),
    safe_create_texpr(if_then_else(BTest,BThenBool,BElseBool),boolean,TRes),
    Res = b(equal(TRes,b(boolean_true,boolean,[])),pred,[]).

translate_z3_predicate(In, Env, Res) :-
    translate_z3_expr(In, Env, boolean, TRes),
    !,
    % expr to pred
    Res = b(equal(TRes,b(boolean_true,boolean,[])),pred,[]).

translate_z3_predicate(Pred,_,_) :-
    add_error_fail(translate_z3_predicate, 'Missing translation for Z3 predicate:', Pred).

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

translate_z3_quantified_vars([[Name,Type]|T], Env, Acc, Preds) :-
    z3_type_to_b_type(Type,BType),
    Id = b(identifier(Name),BType,[]),
    translate_z3_quantified_vars(T, Env, [Id|Acc], Preds).