b_compiler

add_parameters(SortedIds,NewIds,NewSortedIds) :-
    sort(NewIds,SNew),
    ord_union(SortedIds,SNew,NewSortedIds).

b_compile(TExpr,Parameters,NewLS,S,NTExpr) :-
    b_compile(TExpr,Parameters,NewLS,S,NTExpr,no_wf_available). % for unit tests

b_compile(TExpr,Parameters,LS,S,NTExpr,WF) :-
    check_is_id_list(Parameters,Parameters0),
    (get_recursive_identifier_of_closure_body(TExpr,TRID),
    def_get_texpr_id(TRID,RID), nonmember(bind(RID,_),LS)
    -> Parameters1=[RID|Parameters0] % add recursive ID virtually to parameters to avoid error messages
    ; Parameters1=Parameters0),
    % print('compile : '),translate:print_bexpr(TExpr),nl, statistics(runtime,[Start,_]),
    sort(Parameters1,Parameters2),
    if(b_compile1(TExpr,Parameters2,LS,S,NTExpr0,eval,FullyKnown,WF),
    (FullyKnown=true
    -> copy_pos_infos(TExpr,NTExpr0,NTExpr)
    % ensure position info is not deleted if full expression compiled away, see PROB-412 (test 1677)
    ; NTExpr=NTExpr0),
    (add_internal_error_wf(b_compiler,'Compilation failed: ',TExpr,TExpr,WF),
    %b_compile1(TExpr,Parameters1,LS,S,NTExpr0,eval,_FullyKnown,WF),
    NTExpr = TExpr)
).

b_compile1(TExpr,Parameters,LS,S,ResultTExpr,Eval,FullyKnown1,WF) :-
    TExpr = b(Expr,Type,Infos),
    NTExpr = b(NewUntypedExpr,Type,NewInfos),
    %remove_bt(TExpr,Expr,NewUntypedExpr,NTExpr), % remove top-level Type Information
    %hit_profiler:add_profile_hit(Expr),
    %functor(Expr,E1,N1), %print(start_compile(E1/N1,Eval,FullyKnown1)),nl,
    b_compile1_infos(Expr,Type,Infos,Parameters,LS,S,NewUntypedExpr,NewInfos,Eval,FullyKnown,WF),
    %functor(NewUntypedExpr,E2,N2),
    %format(' compiled ~w/~w -> ~w/~w : ',[E1,N1,E2,N2]),translate:print_bexpr_or_subst(NTExpr),nl,
    %format(' fully=~w, eval=~w~n',[FullyKnown,Eval]),
    (NTExpr = b(value(_),_,_)
    -> FullyKnown1=FullyKnown, ResultTExpr=NTExpr
    ; FullyKnown=true, evaluate_this(Eval,NewUntypedExpr,Type,NewInfos)
    -> % print('eval : '),translate:print_bexpr(NTExpr),nl,
    (nonvar(NewUntypedExpr),
    % if( would be more prudent !?, also: we used to call b_compute_expression_nowf
    b_interpreter:b_compute_expression(NTExpr,LS,S,ResultValue,WF)
    -> %print(result(ResultValue)),nl,
    %remove_bt(TExpr,Expr,value(ResultValue),ResultTExpr)
    get_texpr_type(TExpr,TT),ResultTExpr = b(value(ResultValue),TT,[]),
    FullyKnown1 = FullyKnown
    %, print(compiled_value(ResultTExpr)),nl
    ; add_internal_error_wf(b_compiler,'Undefined value marked for evaluation:',NTExpr,Infos,WF),
    %trace, b_interpreter:b_compute_expression(NTExpr,LS,S,ResultValue,WF),
    ResultTExpr=NTExpr, FullyKnown1=false
    )
    ; % ((FullyKnown=true, NTExpr\=b(value(_),_,_)) -> format('not eval: ~w (~w)~n',[NTExpr,Eval]) ; true),
    ResultTExpr=NTExpr, FullyKnown1=false
).

b_compile1_infos(exists(ExistsPara,Pred),_,OldInfos,Parameters,LS,S,NExpr,NewInfos,Eval,FullyKnown,WF) :- !,
    FullyKnown=false, % predicates never automatically evaluated in b_compile1
    get_texpr_ids(ExistsPara,AtomicIds),
    add_parameters(Parameters,AtomicIds,NParameters),
    b_compile1(Pred,NParameters,LS,S,NPred,Eval,_FullyKnown1,WF),
    (is_falsity(NPred) -> NExpr = falsity, NewInfos = OldInfos
    ; is_truth(NPred) -> NExpr = truth, NewInfos = OldInfos
    %; Pred==NPred, write(unchanged(Parameters)),nl, member(used_ids(Old),OldInfos), print(used(Old)),nl,nl,fail
    ; create_exists_or_let_predicate(ExistsPara,NPred,b(NExpr,pred,NI)),
    %print('COMPILED EXISTS: '), translate:print_bexpr(b(NExpr,pred,NI)),nl,
    (delete_first(OldInfos,used_ids(_),I1),
    member(used_ids(NewUsedIds),NI) -> NewInfos = [used_ids(NewUsedIds)|I1]
    ; %nl,print(missing_used_ids(OldInfos,NI)),nl, % can happen when we construt a let_predicate above
    update_infos(NExpr,OldInfos,Parameters,NewInfos))
).

b_compile1_infos(identifier(Id),Type,OldInfos,Parameters,LS,S,NExpr,NewInfos,_Eval,FullyKnown,WF) :- !,
    ( ord_member(Id,Parameters) ->
    NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos
    ; Id=op(_) ->
    NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos
    ; b_interpreter:lookup_value_in_store_and_global_sets_wf(Id,Type,LS,S,Value,OldInfos,WF) ->
    NExpr = value(Value), (known_value(Value) -> FullyKnown=true ; FullyKnown=false),
    NewInfos = [was_identifier(Id)|OldInfos]
    ; add_internal_error_wf(b_compiler,'Compilation of identifier failed: ',Id,OldInfos,WF),
    NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos
).

b_compile1_infos(Expr,_,OldInfos,_Parameters,_LS,_S,NewUntypedExpr,NewInfos,_Eval,FullyKnown,_WF) :-
    b_ast_cleanup:is_integer_set(Expr,_Set),!,
    NewUntypedExpr=Expr, NewInfos=OldInfos,FullyKnown=true.

b_compile1_infos(operation_call_in_expr(Operation,OpCallParas),_Type,OldInfos,Parameters,LS,S,
    Compiled,NewInfos,Eval,FullyKnown,WF) :- !,
    def_get_texpr_id(Operation,op(OperationName)),
    FullyKnown = false,
    b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF),
    b_get_operation_normalized_read_write_info(OperationName,ReadVars,Modified),
    %exclude(operation_identifier,Read,ReadVars), % Read used to contain operations used via operation_call_in_expr; TO DO: check if this is ok in other places of source code of ProB; see test 1957
    (Modified=[] -> true
    ; add_error_wf(b_compiler,'Calling operation that modifies state in expression:',OperationName,OldInfos,WF)),
    % print(compile_call_op(OperationName,ReadVars,Modified,OpCallParaValues)),nl,
    (ReadVars=[]
    -> Compiled = operation_call_in_expr(Operation,OpCallParaValues),
    NewInfos = OldInfos
    ; maplist(create_value_for_read_variable(LS,S,WF),ReadVars,TRead,TValues),
    safe_create_texpr(let_expression_global(TRead,TValues,
    b(operation_call_in_expr(Operation,OpCallParaValues),any,OldInfos)),any,[generated_by_b_compiler],New),
    New = b(Compiled,_,NewInfos)
%NewInfos = [generated_by_b_compiler],
%Compiled = let_expression_global(TRead,TValues,
% b(operation_call_in_expr(Operation,OpCallParaValues),any,OldInfos))
).

b_compile1_infos(kodkod(Id,Identifiers),_,OldInfos,Parameters,LS,S,NExpr,NewInfos,_Eval,FullyKnown,WF) :- !,
    FullyKnown=false, NewInfos=OldInfos,
    exclude(is_parameter(Parameters),Identifiers,IdsToCompile),
    (IdsToCompile=[]
    -> NExpr = kodkod(Id,Identifiers)
    ; maplist(precompile_id(LS,S,WF),IdsToCompile,Values),
    % as we cannot inspect kodkod problem: wrap it into a let with the values stored:
    NExpr = let_predicate(IdsToCompile,Values,b(kodkod(Id,Identifiers),pred,OldInfos))
).

b_compile1_infos(Expr,_,OldInfos,Parameters,LS,S,NewUntypedExpr,NewInfos,Eval,FullyKnown,WF) :-
    b_compile2(Expr,Parameters,LS,S,NewUntypedExpr,Eval,FullyKnown,WF),
    update_infos(NewUntypedExpr,OldInfos,Parameters,NewInfos).

b_compile2(Exp,_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,WF) :- var(Exp), !,
    add_internal_error_wf(b_compiler,'Variable Expression: ',Exp,unknown,WF),
    NExpr=Exp, FullyKnown=false.

b_compile2(truth,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=truth, FullyKnown=false. % predicates never fully known

b_compile2(falsity,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=falsity, FullyKnown=false. % predicates never fully known

b_compile2(empty_set,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value([]), FullyKnown=true.

b_compile2(empty_sequence,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value([]), FullyKnown=true.

b_compile2(boolean_false,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value(pred_false), FullyKnown=true.

b_compile2(boolean_true,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value(pred_true), FullyKnown=true.

b_compile2(value(Val),_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !,
    NExpr=value(Val),
    (known_value(Val) -> % ground(Val) -> known_value ?
    FullyKnown=true ; FullyKnown=false).

b_compile2(integer(Val),_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !,
    NExpr=value(int(Val)), (number(Val) -> FullyKnown=true ; FullyKnown=false).

b_compile2(lazy_lookup_pred(Id),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :- !,
    ( ord_member(Id,Parameters) -> %print(lazy_lookup_pred_id_as_parameter(Id,Parameters)),nl,
    NExpr = lazy_lookup_pred(Id), FullyKnown=false
    ; compute_lazy_lookup(Id,lazy_lookup_pred(Id),LS,S,NExpr,FullyKnown,WF)
).

b_compile2(lazy_lookup_expr(Id),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :- !,
    ( ord_member(Id,Parameters) -> %print(lazy_lookup_expr_id_as_parameter(Id,Parameters)),nl,
    NExpr = lazy_lookup_expr(Id), FullyKnown=false
    ; compute_lazy_lookup(Id,lazy_lookup_expr(Id),LS,S,NExpr,FullyKnown,WF)
).

b_compile2(equal(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    FullyKnown=false, % predicates never evaluated in b_compile1
    b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
    b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
    ( FullyKnownA=true, FullyKnownB=true,
    NExprA = b(value(VA),_,_), NExprB = b(value(VB),_,_)
    -> (equal_object(VA,VB,b_compile2_1) -> NExpr = truth ; NExpr = falsity)
    ; generate_equality(NExprA,NExprB,NExpr)
).

b_compile2(not_equal(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    FullyKnown=false, % predicates never evaluated in b_compile1
    b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
    b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
    ( FullyKnownA=true, FullyKnownB=true,
    NExprA = b(value(VA),_,_), NExprB = b(value(VB),_,_)
    -> %print(computing_neq(VA,VB)),nl,
    (kernel_objects:equal_object(VA,VB,b_compile2_2) -> NExpr = falsity ; NExpr = truth)
    %, print(result(NExpr)),nl
    ; NExpr = not_equal(NExprA,NExprB)
).

b_compile2(member(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    FullyKnown=false, % predicates never evaluated in b_compile1
    b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
    (NExprB = b(value(X),BT,BI)
    -> (X==[], always_well_defined(A) -> NExpr = falsity
    ; b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
    % check if we can decide membership (e.g., 1:{1})
    (quick_test_membership1(NExprA,X,PRes)
    -> convert_pred_res(PRes,NExpr)
    % TO DO: maybe optimize x: {y|P(y)} --> P(x) ; by commenting in code below
    % However, ensure test 273 succeeds and closure equality correctly detected (e.g., for BV16 = {bt|bt : BIT_VECTOR & bv_size(bt) = 16})
    % ; (get_texpr_id(NExprA,IDA),
    % get_comprehension_set(NExprB,IDB,Pred), get_texpr_info(NExprB,Info),
    % print(rename(IDB,IDA,Info)),nl,
    % bsyntaxtree:rename_bt(Pred,[rename(IDB,IDA)],PredA)) -> get_texpr_expr(PredA,NExpr)
    ; custom_explicit_sets:singleton_set(X,El) % replace x:{El} -> x=El
    -> get_texpr_type(NExprA,TA),
    generate_equality_with_value(NExprA,FullyKnownA,El,FullyKnownB,TA,NExpr)
    ; get_template_for_filter_cannot_match(NExprA,VA)
    -> filter_cannot_match(X,VA,NewX,Filtered),
    % (Filtered=false -> true ; print(filtered(NewX,VA,X)),nl),
    (Filtered=false -> NExpr = member(NExprA,NExprB)
    ; (NewX==[], always_well_defined(A)) -> NExpr = falsity
    ; custom_explicit_sets:singleton_set(NewX,El)
    -> get_texpr_type(NExprA,TA),
    %nl,print(create_equal(NExprA,FullyKnownA,El,FullyKnownB,NExprB)),nl,nl,
    generate_equality_with_value(NExprA,FullyKnownA,El,FullyKnownB,TA,NExpr)
    ; NExpr = member(NExprA, b(value(NewX),BT,BI))
    )
    % end fo filtering
    ; NExpr = member(NExprA,NExprB)
    )
    % , print('compile: '),print(NExpr),nl
    )
    ; NExpr = member(NExprA,NExprB),
    b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF)
).

b_compile2(not_member(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    FullyKnown=false, % predicates never evaluated in b_compile1
    b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF),
    (NExprB = b(value(X),_,_)
    -> (X==[], always_well_defined(A) -> NExpr = truth
    ; b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
    (quick_test_membership1(NExprA,X,PRes)
    -> convert_neg_pred_res(PRes,NExpr)
    ; NExpr = not_member(NExprA,NExprB))
    )
    ; NExpr = not_member(NExprA,NExprB),
    b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF)
).

b_compile2(function(Fun,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    (is_lazy_extension_function_for_fun_app(Fun)
    -> Eval1=false % extension function applications treated lazily
    % TO DO: first evaluate B, if known then only evaluate relevant part of extension function
    ; Eval1=Eval),
    b_compile1(Fun,Parameters,LS,S,NExprA,Eval1,FullyKnown1,WF),
    combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown12),
    b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
    %tools_printing:print_term_summary(compiled_function(FullyKnown1,FullyKnown2,NExprA,NExprB)),nl,
    (FullyKnown2=true,
    (NExprA=b(value(_),_,_) -> true % no WD issue can be removed by apply, value already computed
    ; preferences:preference(find_abort_values,false) % in a sequence extension we could remove non-WD elements
    ),
    % check if we have enough information to apply a partially specified function as a list
    % e.g. if the function is [(int(1),A),(int(2),B)] and the argument is int(2): we can apply the function without knowing A or B; can have a dramatic importance when expanding unversal quantifiers !
    can_apply_partially_specified_function(NExprA,NExprB,ResultExpr,WF)
    -> NExpr = ResultExpr,
    (FullyKnown12=true -> FullyKnown=true
    ; ResultExpr=value(ResultValue),known_value(ResultValue) -> FullyKnown=true
    ; FullyKnown = false)
    ; %tools_printing:print_term_summary(cannot_apply_function(FullyKnown2,NExprA,NExprB)),nl,
    %translate:print_bexpr(NExprA),nl, translate:print_bexpr(NExprB),nl,
    NExpr = function(NExprA,NExprB), FullyKnown = FullyKnown12).

b_compile2(conjunct(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    FullyKnown=false, % predicates never automatically evaluated in b_compile1
    b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
    (is_falsity(NExprA) -> NExpr = falsity
    ;
    % TO DO: propagate static information from A to B, e.g. if A :: x=10 -> add x=10 to LS/Parameters
    % also: try and detect unsatisfiable predicates beforehand
    b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF),
    (is_falsity(NExprB) -> NExpr = falsity
    ; is_truth(NExprB) -> get_texpr_expr(NExprA,NExpr)
    ; is_truth(NExprA) -> get_texpr_expr(NExprB,NExpr)
    ; NExpr = conjunct(NExprA,NExprB))
).

b_compile2(disjunct(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    FullyKnown=false, % predicates never automatically evaluated in b_compile1
    b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
    (is_truth(NExprA) -> NExpr = truth
    ; b_compile1(B,Parameters,LS,S,NExprB,false,_,WF), % does not have to be executed in a successful branch: set Eval to false to avoid computing expensive expressions which may not be needed
    (is_truth(NExprB) -> NExpr = truth
    ; is_falsity(NExprA) -> get_texpr_expr(NExprB,NExpr)
    ; is_falsity(NExprB) -> get_texpr_expr(NExprA,NExpr)
    ; NExpr = disjunct(NExprA,NExprB))
).

b_compile2(implication(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    FullyKnown=false, % predicates never automatically evaluated in b_compile1
    b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
    (is_falsity(NExprA) -> NExpr = truth
    ; is_truth(NExprA) -> b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF), get_texpr_expr(NExprB,NExpr)
    ; NExpr = implication(NExprA,NExprB),
    b_compile1(B,Parameters,LS,S,NExprB,false,_,WF) % B does not have to be executed in a successful branch: set Eval to false to avoid computing expensive expressions which may not be needed
% TO DO: add preference to force pre-computation everywhere and pass Eval instead of false to b_compile1; ditto for disjunction
).

b_compile2(negation(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    FullyKnown=false, % predicates never automatically evaluated in b_compile1
    b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
    ( get_negated_operator_expr(NExprA,NegatedA) -> NExpr = NegatedA
    ; NExpr = negation(NExprA)
).

b_compile2(if_then_else(A,B,C),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
    (is_falsity(NExprA) -> b_compile1(C,Parameters,LS,S,NExprC,Eval,FullyKnown,WF), get_texpr_expr(NExprC,NExpr)
    ; is_truth(NExprA) -> b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown,WF), get_texpr_expr(NExprB,NExpr)
    ; NExpr = if_then_else(NExprA,NExprB,NExprC), FullyKnown=false,
    b_compile1(B,Parameters,LS,S,NExprB,false,_,WF), % set Eval to false as we do not know if B will be needed
    b_compile1(C,Parameters,LS,S,NExprC,false,_,WF) % ditto for C
).

b_compile2(forall(ForallPara,A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    FullyKnown=false, % predicates never automatically evaluated in b_compile1
    get_texpr_ids(ForallPara,AtomicIds),
    add_parameters(Parameters,AtomicIds,NParameters),
    b_compile1(A,NParameters,LS,S,NA,Eval,_FullyKnownA,WF),
    (is_falsity(NA) -> NExpr = truth
    ; b_compile1(B,NParameters,LS,S,NB,Eval,_FullyKnownB,WF),
    (is_truth(NB) -> NExpr = truth
    ; NExpr = forall(ForallPara,NA,NB)
% TO DO ??: if we have an equality -> replace Body by value and remove quantifier
%,print('COMPIlED: '),translate:print_bexpr(b(NExpr,pred,[])),nl
)
).

b_compile2(record_field(A,FieldName),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
    % First: we can try compute even if value not fully known !, we just need record field list
    (get_record_field(NExprA,FieldName,NExpr,FullyKnown) -> true
    ; NExpr = record_field(NExprA,FieldName), FullyKnown=FullyKnownA).

b_compile2(couple(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    %NExpr = couple(NExprA,NExprB),
    b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
    combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
    b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
    (FullyKnown \== true, % evaluation will already combine the result
    NExprA=b(value(VA),_,_),NExprB=b(value(VB),_,_)
    -> NExpr = value((VA,VB))
    ; NExpr = couple(NExprA,NExprB)).

b_compile2(image(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
    combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
    b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
    (FullyKnown \= true, NExprA=b(value(VA),BT,BI),
    NExprB=b(value(VB),_,_), nonvar(VB),
    custom_explicit_sets:singleton_set(VB,VBX)
    -> filter_cannot_match(VA,(VBX,_),NewVA,_Filtered), %nl,print(filtered_image(VBX,VA,NewVA)),nl,
    NExpr = image(b(value(NewVA),BT,BI),NExprB)
    % TO DO: add case where VB==[] or VA==[] are the empty set
    ; NExpr = image(NExprA,NExprB)
). %, print('compile image: '),translate:print_bexpr(NExpr),nl.

b_compile2(composition(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
    combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
    NExpr = composition(NExprA,NExprB),
    b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
    (FullyKnown=false, Eval=eval, performance_monitoring_on,
    ( FullyKnown1=true, NExprB=b(value(_),_,Info), large_known_value(NExprA,2)
    -> true %translate:nested_print_bexpr(NExprB),nl
    ; FullyKnown2=true, NExprA=b(value(_),_,Info), large_known_value(NExprB,2)
    -> true %translate:nested_print_bexpr(NExprA),nl
    )
    -> perfmessage(b_compiler,'Cannot compile relational composition (try lift it out of quantification)',Info)
    ; true).

b_compile2(assertion_expression(A,Msg,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
    (is_truth(NExprA) -> % the ASSERT EXPR is redundant
    %print(removed_assert),nl, translate:print_bexpr(B),nl,
    b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown,WF),
    get_texpr_expr(NExprB,NExpr)
    ; b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF),
    FullyKnown=false, % we cannot get rid of WD condition
    NExpr = assertion_expression(NExprA,Msg,NExprB)
).

b_compile2(domain(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
    (FullyKnown1=false,get_texpr_expr(NExprA,NA),evaluate_domain(NA,Domain) % try and compute domain even if not fully known
    -> FullyKnown = true, NExpr = value(Domain)
    ; FullyKnown = FullyKnown1, NExpr = domain(NExprA)).

b_compile2(range(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
    (FullyKnown1=false,evaluate_range(NExprA,Range) % try and compute range even if not fully known
    -> FullyKnown = true, NExpr = value(Range)
    ; FullyKnown = FullyKnown1, NExpr = range(NExprA)).

b_compile2(assign(LHS_List,RHS_List),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
    NExpr = assign(New_LHS_List,NewRHS_List), FullyKnown = false,
    maplist(b_compile_lhs(Parameters,LS,S,Eval,WF),LHS_List,New_LHS_List),
    b_compile_l(RHS_List,Parameters,LS,S,NewRHS_List,Eval,_FullyKnown2,WF).

b_compile2(assign_single_id(ID,B),Parameters,LS,S,assign_single_id(ID,NExprB),Eval,FullyKnown,WF) :- !,
    FullyKnown = false,
    b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF).

b_compile2(operation_call(Operation,OpCallResults,OpCallParas),Parameters,LS,S,InlinedOpCall,Eval,FullyKnown,WF) :-
    % TO DO: evaluate if we should also use the let_expression_global approach used for operation_call_in_expr
    !,
    def_get_texpr_id(Operation,op(OperationName)),
    FullyKnown = false,
    b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF),
    TopLevel=false,
    b_get_machine_operation_for_animation(OperationName,OpResults,OpFormalParameters,Body,_OType,TopLevel),
    bsyntaxtree:replace_ids_by_exprs(Body,OpResults,OpCallResults,Body2),
    get_texpr_ids(OpFormalParameters,OpIds),
    add_parameters(Parameters,OpIds,InnerParas),
    b_compile1(Body2,InnerParas,[],S,NBody,Eval,FullyKnown,WF), % do not pass local state: this may override constants,... from the called machine
    % Note: global state S should be valid for all machines in currently loaded specification
    get_texpr_ids(OpCallResults,OpRIds),
    add_parameters(Parameters,OpRIds,LocalKnownParas),
    simplify_assignment(OpFormalParameters,OpCallParaValues,LHSFormalParas,RHSCallVals),
    split_formal_parameters(LHSFormalParas,RHSCallVals,LocalKnownParas,
    FreshOpParas,FreshCallVals,
    ClashOpParas, ClashCallVals), % only set up VAR for fresh Paras
    % print(split(LHSFormalParas,LocalKnownParas,fresh(FreshOpParas),clash(ClashOpParas))),nl,
    (FreshOpParas=[] -> get_texpr_expr(NBody,Let1)
    ; create_equality_for_let(FreshOpParas,FreshCallVals,Equality1),
    Let1 = let(FreshOpParas,Equality1,NBody)),
    (ClashOpParas = []
    -> InlinedOpCall = Let1
    ; %nl,print(clash(ClashOpParas)),nl,
    maplist(create_fresh_id,ClashOpParas,FreshCopy),
    create_equality_for_let(ClashOpParas,FreshCopy,Equality2), % copy Values from Fresh Ids
    create_equality_for_let(FreshCopy,ClashCallVals,Equality3), % assign Parameter Vals to Fresh Ids
    get_texpr_pos(Body,BodyPos), BodyPosInfo = [nodeid(BodyPos)],
    Let2 = let(ClashOpParas,Equality2,b(Let1,subst,[BodyPosInfo])),
    InlinedOpCall = let(FreshCopy,Equality3,b(Let2,subst,[BodyPosInfo]))
).

b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :-
    functor(Expr,BOP,2),
    binary_boolean_operator(BOP,_,_),!, % from kernel_mappings, slightly more efficient than syntaxtransformation
    arg(1,Expr,A),
    FullyKnown=false, % predicates never evaluated in b_compile1
    b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
    arg(2,Expr,B),
    b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
    (eval_binary_bool(FullyKnownA,NExprA,FullyKnownB,NExprB,BOP,Result)
    -> NExpr = Result
    ; functor(NExpr,BOP,2), arg(1,NExpr,NExprA), arg(2,NExpr,NExprB)
).

b_compile2(external_function_call(ExtFun,Args),_Parameters,LS,_S,NExpr,_Eval,FullyKnown,_WF) :-
    expects_unevaluated_args(ExtFun),
    memberchk(bind('$optimize_do_not_force_lazy_lookups',_),LS), % this is an optimize call
    !,
    debug_format(9,'Not compiling external function call to ~w~n',[ExtFun]),
    NExpr=external_function_call(ExtFun,Args),
    FullyKnown=false.

b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :-
    functor(Expr,BOP,2),
    kernel_mappings:binary_function(BOP,_,_),!, % slightly more efficient than syntaxtransformation
    arg(1,Expr,A),
    b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
    combine_fully_known(FullyKnownA,FullyKnownB,FullyKnown),
    arg(2,Expr,B),
    b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
    functor(NExpr,BOP,2), arg(1,NExpr,NExprA), arg(2,NExpr,NExprB).

b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :-
    functor(Expr,UOP,1),
    kernel_mappings:unary_function(UOP,_,_),!, % slightly more efficient than syntaxtransformation
    arg(1,Expr,A),
    b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown,WF),
    functor(NExpr,UOP,1), arg(1,NExpr,NExprA).

b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- % GENERAL CASE
    %hit_profiler:add_profile_hit(Expr),
    syntaxtransformation(Expr,Subs,Names,NSubs,NExpr),
    get_texpr_ids(Names,Ids),
    add_parameters(Parameters,Ids,NParameters),
    b_compile_l(Subs,NParameters,LS,S,NSubs,Eval,FullyKnown,WF).

b_compile_closure(closure(P,T,Body),Res) :- b_compiler:b_compile(Body,P,[],[],CBody),!, Res=closure(P,T,CBody).

b_compile_closure(C,C).

b_compile_l([],_,_,_,[],_Eval,true,_WF).

b_compile_l([Expr|ExprRest],P,LS,S,[NExpr|NExprRest],Eval,FullyKnown,WF) :-
    b_compile1(Expr,P,LS,S,NExpr,Eval,FullyKnown1,WF),
    combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
    b_compile_l(ExprRest,P,LS,S,NExprRest,Eval,FullyKnown2,WF).

b_compile_lhs(Parameters,LS,S,Eval,WF,TExpr,NewTExpr) :-
    TExpr = b(Expr,Type,Info), NewTExpr = b(NewExpr,Type,Info),
    b_compile_lhs_aux(Expr,Parameters,LS,S,NewExpr,Eval,WF).

b_compile_lhs_aux(function(A,B),Parameters,LS,S,function(NewA,NewB),Eval,WF) :- !,
    b_compile_lhs(Parameters,LS,S,Eval,WF,A,NewA), % we can have nexted function calls f(e)(g) :=
    b_compile1(B,Parameters,LS,S,NewB,Eval,_,WF).

b_compile_lhs_aux(E,_,_,_,E,_,_WF). % other LHS should be identifier -> just copy

b_optimize(TExpr,Parameters,LS,S,NTExpr,WF) :- %print('OPTIMIZE: '),translate:print_bexpr(TExpr),nl, trace,
    append(LS,[bind('$optimize_do_not_force_lazy_lookups',pred_true)],NewLS),
    b_compile(TExpr,Parameters,NewLS,S,NTExpr,WF).

can_apply_aux(value(VAL),TYPE,X,TA,value(ResultValue),WF) :-
    is_set_type(TYPE,couple(TA,_TB)),
    lookup_result(VAL,X,ResultValue,WF).

can_apply_aux(sequence_extension(List),_,X,integer,ResultExpr,_WF) :-
    % important, e.g., for solving test 1551: {b|[a,b,c](2)=333} =res & a : res & b:res
    nonvar(X), X=int(Index), number(Index),
    % this will prevent computing rest of sequence extension: can hide WD issues !
    % print(apply_seq_extension(Index,List)),nl,
    nth1(Index,List,b(ResultExpr,_,_)).

can_apply_partially_specified_function(b(Expr,TYPE,_), b(value(X),TA,_),ResultExpr,WF) :-
    can_apply_aux(Expr,TYPE,X,TA,ResultExpr,WF).

check_is_id_list([],[]).

check_is_id_list([H|T],Res) :-
    (H=b(identifier(_),_,_)
    -> add_internal_error('Typed id list as argument: ',check_is_id_list([H|T],Res)), % use get_texpr_ids or maplist(def_get_texpr_id,P,PIDs)
    maplist(def_get_texpr_id,[H|T],Res)
    ; Res=[H|T]).

check_wd(NTExpr) :- bsyntaxtree:always_well_defined(NTExpr). % ,print(wd(NTExpr)),nl.

combine_fully_known(true,A,A).

combine_fully_known(false,_,false).

compute_lazy_lookup(Id,Expr,LS,S,NExpr,FullyKnown,WF) :-
    lookup_value_for_existing_id_wf(Id,LS,S,(Evaluated,Value),WF),
    % the lazy expression has already been registered, but maybe not yet evaluated
    !,
    known_value(Value,FullyKnown), % compute if value fully known
    (Evaluated==pred_true -> NExpr = value(Value)
    ; FullyKnown==true -> NExpr = value(Value)
    ; memberchk(bind('$optimize_do_not_force_lazy_lookups',_),LS)
    -> NExpr = Expr % we do not force lookup: there could be WD issues !
    % TO DO: examine Infos for wd_condition; we could also return NExpr = lazy_value(Id,Evaluated,Value)
    ; if(Evaluated = pred_true,
    % will force evaluation ! Note: this means shared expression inside a compiled expression must be well-defined
    NExpr = value(Value),
    (add_internal_error_wf(b_compiler,'Compilation failed: ', Id, unknown,WF),
    fail))
).

compute_lazy_lookup(Id,_E,_LS,_S,_LazyValue,_,WF) :-
    add_internal_error_wf(b_compiler,'Compilation failed, illegal lazy_lookup_value: ',Id,unknown,WF),
    fail.

contains_empty_set(pow).

contains_empty_set(fin).

convert_neg_pred_res(pred_true,falsity).

convert_neg_pred_res(pred_false,truth).

convert_pred_res(pred_false,falsity).

convert_pred_res(pred_true,truth).

create_eq(Id,Expr,TPred) :- safe_create_texpr(equal(Id,Expr),pred,TPred).

create_equality_for_let(LHS,RHS,Conj) :-
    maplist(create_eq,LHS,RHS,CL),
    conjunct_predicates(CL,Conj).

create_fresh_id(b(identifier(_),T,I),b(identifier(FRESHID),T,I)) :-
    gensym('__COMPILED_ID__',FRESHID).

create_value_for_read_variable(LS,S,WF,Variable,TVariable,TValue) :-
    b_interpreter:lookup_value_in_store_and_global_sets_wf(Variable,_Type,LS,S,Value,unknown,WF),!,
    % TO DO: try and find type?
    TVariable = b(identifier(Variable),any,[]),
    TValue = b(value(Value),any,[]).

create_value_for_read_variable(_LS,_S,WF,Variable,TVariable,b(value(term(undefined)),any,[])) :-
    TVariable = b(identifier(Variable),any,[]),
    add_internal_error_wf(b_compiler,'Cannot find variable (read) while compiling operation:',Variable,unknown,WF),
    fail.

eval_binary_aux(less,int(A),int(B),Result) :-
    (A < B -> Result = truth ; Result = falsity).

eval_binary_aux(greater,int(A),int(B),Result) :-
    (A > B -> Result = truth ; Result = falsity).

eval_binary_aux(less_equal,int(A),int(B),Result) :-
    (A =< B -> Result = truth ; Result = falsity).

eval_binary_aux(greater_equal,int(A),int(B),Result) :-
    (A >= B -> Result = truth ; Result = falsity).

eval_binary_aux(subset,avl_set(A1),avl_set(A2),Result) :-
    (custom_explicit_sets:check_avl_subset(A1,A2) -> Result = truth ; Result = falsity).

eval_binary_aux(subset,[],_,Result) :- Result=truth.

eval_binary_bool(true,b(value(ValA),_,_),true,b(value(ValB),_,_),BOP,Result) :-
    ground(ValA),
    ground(ValB),
    eval_binary_aux(BOP,ValA,ValB,Result).

evaluate_domain(sequence_extension(L),Domain) :- length(L,Len),
    % this will prevent computing range of sequence extension: can hide WD issues ! TO DO: check wd info and/or preference
    construct_interval_closure(1,Len,Domain).

evaluate_domain(value(L),Domain) :-
    get_domain(L,Domain).

evaluate_range(b(value(L),_T,_),Range) :-
    get_range(L,Range).

evaluate_this(eval,X,Type,Info) :- !, worth_it_type(Type,X,Info).

evaluate_this(_,function(A,B),Type,Info) :- !,
    A=b(value(VA),_,_), nonvar(VA), VA=avl_set(_),
    B=b(value(_),_,_),
    worth_it_type(Type,function(A,B),Info). % will check well-definedness

evaluate_this(_,X,_Type,_Info) :- wd_and_efficient(X).

fast_check_wd(b(E,_,Infos)) :-
    (nonmember(contains_wd_condition,Infos) -> true
    ; nonvar(E), E=value(_)).

fast_lookup_result([(HFrom,HTo)|T],X,Result,WF) :- !,
    equality_can_be_decided_by_unification(HFrom),
    (HFrom=X -> Result = HTo
    ; fast_lookup_result(T,X,Result,WF)
).

fast_lookup_result(List,X,Result,WF) :-
    regular_lookup_result_in_list(List,X,Result,WF).

finite_non_empty_set(b(value(V),set(_),_)) :- nonvar(V), V=avl_set(_).

finite_set(b(value(V),set(_),_)) :- nonvar(V), finite_set_aux(V).

finite_set_aux([]).

finite_set_aux(avl_set(_)).

generate_equality(b(A,_,_),b(B,_,_),Res) :-
    ( generate_equality_aux(A,B,Res) ;
    generate_equality_aux(B,A,Res) ),
    !.

generate_equality(A,B,equal(A,B)).

generate_equality_aux(convert_bool(AA),value(PT),Res) :-
    PT==pred_true,
    get_texpr_expr(AA,TA),
    !,
    Res = TA.

generate_equality_aux(convert_bool(AA),value(PF),Res) :-
    PF==pred_false,!,
    Res = negation(AA).

generate_equality_with_value(b(value(ValA),_,_),true,ValB,true,_TA,NExpr) :-
    % both are FullyKnown
    simple_value(ValA), % we should avoid closures
    !,
    kernel_equality:equality_objects(ValA,ValB,PRes),
    convert_pred_res(PRes,NExpr).

generate_equality_with_value(NExprA,_,Value,_,TA,equal(NExprA,b(value(Value),TA,[]))).

get_domain(V,Dom) :- var(V),!,kfi_domain(V,Dom). % try infer domain from attached co-routines

get_domain([],[]).

get_domain([V|VT],Result) :- nonvar(V), V=(D,_),
    known_value(D),get_list_domain(VT,DT),
    %length(DT,Len),print(got_list_domain(D,Len)),nl,
    (custom_explicit_sets:try_convert_to_avl([D|DT],Res) -> Result=Res
    ; write(could_not_convert_domain_to_avl(D)),nl, Result=[D|DT]). %sort([D|DT],Result)?

get_field_in_range(b(value(OldVal),set(couple(Dom,OldRange)),Info),FieldName,
    b(value(NewVal),set(couple(Dom,NewRange)),Info)) :-
    nonvar(OldVal), OldVal=avl_set(AVL),
    avl_height_less_than(AVL,10),
    OldRange = record(Fields),
    member(field(FieldName,NewRange),Fields),!,
    expand_custom_set_to_list(avl_set(AVL),List,_,get_field_in_range),
    maplist(safe_get_range_field(FieldName),List,NewList),
    convert_to_avl(NewList,NewVal).

get_list_domain(V,_) :- var(V),!,fail.

get_list_domain([],[]).

get_list_domain([V|VT],[D|DT]) :- nonvar(V), V=(D,_),
    known_value(D),get_list_domain(VT,DT).

get_list_range(V,_) :- var(V),!,fail.

get_list_range([],[]).

get_list_range([V|VT],[D|DT]) :-
    nonvar(V), V=(_,D),
    known_value(D),
    get_list_range(VT,DT).

get_range(V,Dom) :- var(V),!,kfi_range(V,Dom). % try infer range from attached co-routines

get_range([],[]).

get_range([V|VT],Result) :- nonvar(V), V=(_,D),
    known_value(D),
    get_list_range(VT,DT),
    sort([D|DT],Result).

get_record_field(b(value(Val),_,_),FieldName,value(Field),FullyKnown) :- !,
    nonvar(Val), Val=rec(Fields),
    safe_get_field(Fields,FieldName,Field),
    known_value(Field,FullyKnown).

get_record_field(b(function(FUN,ARG),_Type,_Info),FieldName,function(ReducedFUN,ARG),false) :-
    % {1|->rec(a:1,b:2),...}(x)'b --> {1|->2,...}(x)
    %nl,print(get_field(FUN,ARG,FieldName)),nl,
    % TO DO: also allow nested functions calls {1|->rec(a:1,b:2),...}(x)(y)'b or other reduction operators
    get_field_in_range(FUN,FieldName,ReducedFUN).