eval_strings

add_last_expression_to_unit_tests :- \+ last_expression(_,_Expr),!,
    print_red('Please evaluate an expression or predicate first.'),nl.

add_last_expression_to_unit_tests :- last_expression(Type,Expr,Value),
    open_unit_test_file(S), !, write(S,' & '), nl(S), write(S,' ( '),
    (print_unit_test_assertion(Type,Expr,Value,S) -> true ; print('PRINTING FAILED'),nl),
    write(S,' ) '), datime(datime(Yr,Mon,Day,Hr,Min,_Sec)),
    format(S,'/* ~w/~w/~w ~w:~w */',[Day,Mon,Yr,Hr,Min]),
    nl(S), close(S).

add_last_expression_to_unit_tests :- print('Could not save expression to unit test file ($PROB_EX_DIR/B/Laws/REPL_UNIT_TESTS.def).'),nl.

available_krt_prover(krt,[ml,pp],":krt").

available_krt_prover(ml,[ml],":ml").

available_krt_prover(pp,[pp],":pp").

available_krt_prover(probwd,['prob-wd-prover'(no_double_check)],":prove"). % not a krt prover

available_krt_prover(probwd,['prob-wd-prover'(double_check)],":prove-double-check").

available_smt_solver(cvc4,":cvc ").

available_smt_solver(cvc4,":cvc4 ").

available_smt_solver(nostate(cvc4),":cvc4-free ").

available_smt_solver(z3,":z3 ").

available_smt_solver(z3sat,":z3-sat ").

available_smt_solver(z3axm,":z3-axm ").

available_smt_solver(z3cns,":z3-cns ").

available_smt_solver(nostate(z3),":z3-free ").

available_smt_solver(nostate(z3sat),":z3-sat-free ").

available_smt_solver(nostate(z3axm),":z3-axm-free ").

available_smt_solver(nostate(z3cns),":z3-cns-free ").

available_smt_solver(double_check(z3),":z3-double-check ").

available_smt_solver(double_check(nostate(z3)),":z3-free-double-check ").

available_smt_solver(cdcl_sat,":cdcl-sat ").

available_smt_solver(nostate(cdcl_sat),":cdcl-sat-free ").

available_smt_solver(cdclt,":cdclt ").

available_smt_solver(nostate(cdclt),":cdclt-free ").

available_smt_solver(double_check(cdclt),":cdclt-double-check ").

available_smt_solver(double_check(nostate(cdclt)),":cdclt-free-double-check ").

available_smt_solver(idl,":idl ").

available_smt_solver(setlog,":slog ").

available_smt_solver(double_check(setlog),":slog-double-check ").

available_smt_solver(prob(default),":prob "). % solve with SMT

available_smt_solver(prob(strong),":prob-chr ").

available_smt_solver(prob(eval),":eval "). % solve without SMT option; like default REPL eval

available_smt_solver('prob-unsat-core',":core ").

available_smt_solver('prob-unsat-core-no-chr',":ccore ").

available_smt_solver('prob-unsat-cores',":cores ").

available_smt_solver('prob-fast-unsat-core',":fcore ").

available_smt_solver('prob-fast-unsat-core',":fast-core ").

available_smt_solver('prob-min-core',":mcore ").

available_smt_solver('prob-min-core',":min-core ").

available_smt_solver('smt-unsat-core'(z3),":z3-core ").

available_smt_solver('smt-quick-bup-unsat-core'(z3),":z3-qcore ").

available_smt_solver('smt-quick-bup-unsat-core'(z3cns),":z3-cns-qcore ").

available_smt_solver('smt-quick-bup-unsat-core'(z3axm),":z3-axm-qcore "). % z3axm best for bup-unsat core?

available_smt_solver('smt-unsat-core'(z3cns),":z3-cns-core ").

available_smt_solver('smt-unsat-core'(z3axm),":z3-axm-core ").

available_smt_solver('cdclt-unsat-core',":cdclt-core ").

available_smt_solver('satsolver'(glucose,with_state),":sat ").

available_smt_solver('satsolver'(glucose,nostate),":sat-free ").

available_smt_solver('satsolver'(z3,with_state),":sat-z3 ").

available_smt_solver('satsolver'(z3,nostate),":sat-z3-free ").

available_smt_solver(double_check('satsolver'(glucose,with_state)),":sat-double-check ").

available_smt_solver(double_check('satsolver'(z3,with_state)),":sat-z3-double-check ").

available_smt_solver_for_file(cdclt,":cdclt-file ").

available_smt_solver_for_file(nostate(cdclt),":cdclt-free-file ").

available_smt_solver_for_file(idl,":idl-file ").

available_smt_solver_for_file(z3,":z3-file ").

available_smt_solver_for_file(z3sat,":z3-sat-file ").

available_smt_solver_for_file(z3axm,":z3-axm-file ").

available_smt_solver_for_file(z3cns,":z3-cns-file ").

available_smt_solver_for_file(nostate(z3),":z3-free-file ").

available_smt_solver_for_file('smt-unsat-core'(z3),":z3-core-file ").

available_smt_solver_for_file(cvc4,":cvc4-file ").

available_smt_solver_for_file(nostate(cvc4),":cvc4-free-file ").

available_smt_solver_for_file(prob(default),":prob-file ").

available_smt_solver_for_file(prob(strong),":prob-chr-file ").

available_smt_solver_for_file('prob-unsat-core',":prob-core-file ").

browse_repl_lets :- \+ \+ stored_let_value(_,_,_),
    print('Available let definitions:'),nl,
    stored_let_value(ID,_,Value),
    translate_bvalue_with_limit_and_col(Value,50,VS),
    format(' ~w = ~w~n',[ID,VS]),
    fail.

browse_repl_lets.

check_dc_sol(X,_,X) :- !, print_green('double check ok'),nl.

check_dc_sol(no_solution_found(unfixed_deferred_sets),_,contradiction_found) :-
    % Z3, CDCL(T) do not check for unfixed_deferred sets; see test 2060
    !, print_green('double check of contradiction_found ok'),nl.

check_dc_sol(X,Solver,E) :-
    format_with_colour_nl(user_error,[red,bold],
    'double check unexpected result, ProB reported: ~w,~n ~w reported: ~w',[X,Solver,E]),
    fail.

check_failed(Nr,ExTyped) :-
    nl,print(Nr), print(' >>> '), translate:print_bexpr(ExTyped),nl,
    (eval_predicate_in_cur_state(ExTyped,Res,_,_)
    -> (Res='FALSE' -> true ;
    add_error(must_fail_tests,'Test has not failed deterministically: ',Nr))
    ; add_error(must_fail_tests,'eval_predicate failed: ',Nr)
).

check_residue([]) :- !.

check_residue(Residue) :-
    add_internal_error('Call residue: ',Residue),
    portray_residue(Residue). % or tools_printing:print_goal(Residue)

check_same_ast(Nr,A_New,B_Old) :- % check equivalent to stored AST B, apart from pos
    (compare(A_New,B_Old) -> true
    ; add_error(check_same_ast,'AST not identical: ',Nr),
    print('New AST:'),nl,print(A_New),nl,
    print('Stored AST :'),nl,print(B_Old),nl,
    tools_printing:trace_unify(A_New,B_Old)
).

clash(SIds,TID) :- def_get_texpr_id(TID,ID), ord_member(ID,SIds).

clear_last_expression :-
    retractall(last_expression(_,_)), retractall(last_expression_value(_)).

colour_values(false).

compare(A,B) :- atomic(A),!,B=A.

compare(b(A,TA,IA),b(B,TB,IB)) :- !,
    TA=TB,
    exclude(remove_this,IA,IA1), sort(IA1,SIA1),
    exclude(remove_this,IB,IB1), sort(IB1,SIB1),
    compare_infos(SIA1,SIB1),
    compare(A,B).

compare(A,B) :- A=..[F|As], B=..[F|Bs],
    maplist(compare,As,Bs).

compare_infos([],[]).

compare_infos([H|TA],[H|TB]) :- !, compare_infos(TA,TB).

compare_infos([used_ids(_)|TA],TB) :- TB \= [used_ids(_)|_], % skip additional new used_ids field
    compare_infos(TA,TB).

convert_aux(pred,pred_true,boolean,pred_true).

convert_aux(pred,pred_false,boolean,pred_false).

convert_result(T,V,Type,Value) :-
    (convert_aux(T,V,Type,Value) -> true ; Type=T,Value=V).

digit(X) :- X >= 48, X =< 57.

display_and_set_result(ScopeID,Res,RRes,EnumWarning) :-
    %error_manager:print_error_scopes,
    findall(TE,(specific_event_occurred_at_level(ScopeID,E),translate_error_event(E,TE)), Errors),
    (abort_error_occured_in_error_scope -> WDError=true ; WDError=false),
    (specific_event_occurred_at_level(ScopeID,identifier_not_found) -> IdNotFound=true ; IdNotFound=false),
    exit_error_scope(ScopeID,ErrOcc,display_and_set_result),
    ErrOcc=true, % TO DO: check which kind of error occured: could be CLPFD overflow
    !,
    show_error_pos,
    (WDError=true
    -> format_with_colour(user_output,[red,bold],'NOT-WELL-DEFINED (~w)',[Res]),
    RRes = 'NOT-WELL-DEFINED'
    ; IdNotFound=true -> % should no longer happen; we check requirements first
    format_with_colour(user_output,[red,bold],'IDENTIFIER-NOT-FOUND-ERROR ~w',[Errors]),
    RRes = 'IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST'
    ; format_with_colour(user_output,[red,bold],'UNKNOWN ~w',[Errors]),
    RRes = 'UNKNOWN'
    ),
    print_enum_warning(EnumWarning), nl.

display_and_set_result(_,Res,RRes,EnumWarning) :-
    print_result(Res,EnumWarning), nl,
    (EnumWarning=false -> RRes=Res
    ; Res = 'TRUE' -> RRes=Res % enumeration warning does not matter when solution found
    ; RRes= 'UNKNOWN').

display_dot_expr_result(Expr,Value) :-
    (eval_dot_file(File)
    -> get_dot_expr_state(Expr,Value,NState,[]),
    debug_println(9,writing_dot_file(File)),
    print_cstate_graph(NState,File)
    ; true).

display_dot_solution(NState) :-
    (eval_dot_file(File)
    -> debug_println(9,writing_dot_file(File)),
    print_cstate_graph(NState,File) ; true).

display_smt_result(solution(Bindings),Parameters,ExTyped,Res) :- !,
    set_last_expression(pred,ExTyped,pred_true),
    print_green('TRUE'),nl,
    ( Bindings=[]
    -> set_last_solution(Parameters,[])
    ; silent_mode(off), write('Solution: '),nl,Bindings=[bind(_,_)|_]
    -> print_visible_solution_with_type(Parameters, Bindings),
    set_last_solution(Parameters,Bindings)
    ; Bindings = [bind(_,_)|_] -> set_last_solution(Parameters,Bindings)
    ; findall(bind(ID,Val),member(binding(ID,Val,_),Bindings),LocalState),
    set_last_solution(Parameters,LocalState),
    findall(1,(member(binding(ID2,_,S2),Bindings),print_binding(ID2,S2),nl),_)
    ), Res = 'TRUE'.

display_smt_result(contradiction_found,_,ExTyped,Res) :- !,
    format_with_colour(user_output,[light_red],'FALSE',[]),nl,
    set_last_expression(pred,ExTyped,pred_false),
    Res = 'FALSE'.

display_smt_result(contradiction_found(UnsatCore),_,ExTyped,Res) :- !,
    display_smt_result(contradiction_found,_,ExTyped,'FALSE'),
    translate_bexpression(UnsatCore, PrettyUnsatCore),
    format_with_colour_nl(user_output,[dark_gray],'Unsat Core: ~w',[PrettyUnsatCore]),
    Res = 'FALSE'.

display_smt_result(no_solution_found(no_idl_constraint),_,_,'UNKNOWN') :- !,
    print_red('UNKNOWN: '),nl,
    format_with_colour_nl(user_output,[light_red],'Constraint can not be transformed to integer difference logic.',[]).

display_smt_result(no_solution_found(cvc4_unknown),_,ExTyped,'UNKNOWN') :- !,
    print_red('UNKNOWN'),nl,
    set_last_expression(pred,ExTyped,unknown).

display_smt_result(no_solution_found(Reason),_,ExTyped,'UNKNOWN') :- !,
    print_red('UNKNOWN: '),print(Reason),nl,
    set_last_expression(pred,ExTyped,unknown).

display_smt_result(error,_,ExTyped,'UNKNOWN') :- !,
    print_red('UNKNOWN: '),print('(due to error, possibly well-definedness error)'),nl,
    set_last_expression(pred,ExTyped,unknown).

display_smt_result(Other,_,ExTyped,'UNKNOWN') :- !,
    print_red('*** UNKNOWN SMT RESULT ***: '),print(Other),nl,
    set_last_expression(pred,ExTyped,unknown).

display_sol_required :- silent_mode(off),!.

display_sol_required :- eval_dot_file(_),!.

display_solution(HeaderStr,Parameters,LocalState) :-
    set_last_solution(Parameters,LocalState),
    (display_sol_required
    -> format(HeaderStr,[]),
    display_solution_aux(Parameters,LocalState)
    ; true).

display_solution_aux(Parameters,LocalState) :-
    (eval_det
    -> % copy_term(LocalState,CLS), % avoid triggering co-routines via numbervars
    % tools_meta:safe_numbervars(CLS,0,_),
    print_visible_solution_with_type(Parameters,LocalState)
    ; debug_println(19,normalising_solution(LocalState)),
    normalise_solution(LocalState,NState)
    -> %translate:print_bstate(NState)
    print_visible_solution_with_type(Parameters,NState),
    %visualize_graph:tcltk_print_state_as_graph_for_dot(NState,'~/Desktop/out.dot')
    display_dot_solution(NState)
    ; print_red('Could not normalise value(s):'),nl,
    translate:print_bstate(LocalState)
    ),nl.

double_check_proven_sequent(Typed) :-
    create_negation(Typed,NegTyped),
    member(Solver,[prob(strong),z3]),
    %format_with_colour_nl(user_output,[dark_gray],'Double checking proof using ~w',[Solver]),
    statistics(walltime,[W1,_]),
    %solve_typed_pred_using_smt_solver(Solver,NegTyped,Res,_),
    temporary_set_preference(strict_raise_enum_warnings,false,Chng),
    (solve_using_smt_solver_aux(Solver,[],NegTyped,_,Res) -> true),
    reset_temporary_preference(strict_raise_enum_warnings,Chng),
    statistics(walltime,[W2,_]), W is W2-W1,
    (Res=solution(_) -> Col=[red,bold] ; Col = [dark_gray]),
    format_with_colour_nl(user_output,Col,'Double checking result of ~w after ~w ms: ~w',[Solver,W,Res]),
    (Res=solution(_) ; Res='TRUE'),
    !,
    add_error(double_check_proven_sequent,'Counter example for proven sequent found:',Typed,Typed).

double_check_proven_sequent(_).

double_check_smt_result(Solver,_Parameters,Typed,_LocalState,solution(Bindings)) :- !,
    maplist(get_bind,Bindings,State),
    ( solver_call_should_ignore_state(Solver, Solver2)
    -> find_identifier_uses_top_level(Typed, UsedIds),
    findall(bind(IdName,_), (member(IdName,UsedIds), \+ member(bind(IdName,_),State)), FreeBindings),
    append(State, FreeBindings, FullStore)
    ; Solver2 = Solver,
    get_current_state_full_store(Typed, TFullStore),
    findall(bind(IdName,_), (member(bind(IdName,_),TFullStore), \+ member(bind(IdName,_),State)), TFullStore2),
    append(State, TFullStore2, FullStore)
    ),
    debug_format(19,'Double-checking ~w with ProB solver using solve_predicate~n',[Solver]),
    %print(bindings(Bindings)),nl,
    (solve_predicate(Typed,FullStore,DCResult), %print(DCResult),nl,
    check_dc_sol(DCResult,Solver2,solution(_)) -> true
    ; add_error(double_check_smt_result,'Double checking NOT successful, solution not confirmed: ',Typed,Typed)).

double_check_smt_result(Solver,_Parameters, Typed, _LocalState, Res) :-
    ( solver_call_should_ignore_state(Solver, Solver2)
    -> % FullStore is var
    debug_format(19,'Double checking result of ~w with ProB solver (ignoring current state)~n',[Solver2])
    ; get_current_state_full_store(Typed, FullStore),
    Solver2 = Solver,
    debug_format(19,'Double checking result with of ~w ProB solver (in current state)~n',[Solver2])
    ),
    ( solve_predicate(Typed, FullStore, TDCResult)
    -> DCResult = TDCResult
    ; % solve_predicate did fail if contradiction with current state
    % should no longer happen
    add_warning(double_check_smt_result,'solve_predicate failed: ',Typed, Typed),
    DCResult = contradiction_found
    ),
    ( check_dc_sol(DCResult, Solver2, Res)
    -> true
    ; add_error(double_check_smt_result,'Double checking NOT successful', Typed, Typed)
).

eval_codes(E,Q,Res,EnumWarning,LS,TypeInfo) :-
    call_residue(eval_codes2(E,Q,Res,EnumWarning,LS,TypeInfo),Residue),
    (Residue = [] -> true ;
    eval_det -> print('Call residue in eval_codes: '),print_term_summary(Residue),nl
    ; add_internal_error('Call residue in eval_codes: ',Residue) %,tools_printing:print_goal(Residue)
).

eval_codes2(E,Q,Res,EnumWarning,LS,TypeInfo) :-
    set_error_context(eval_codes),
    reset_repl_lets, % remove invalid lets if required
    catch(
    eval_codes_aux0(E,Q,Res,EnumWarning,LS,TypeInfo),
    enumeration_warning(Cause,ID,_,_,_),
    (get_time_out_message(Cause,ID,CauseStr),
    format_with_colour_nl(user_output,[red,bold],'VIRTUAL TIME-OUT forced by ~w',[CauseStr]),
    EnumWarning = true,
    Res = 'TIME-OUT'
    )),
    clear_error_context.

eval_codes_aux(Expression,_,Res,EnumWarning,LocalState,TypeInfo) :- TypeInfo=expression(_),
    repl_parse_expression(Expression,Typed,Type,Error),
    (Error=none ; Error=type_error),
    !,
    eval_expression_codes2(Typed,Type,Error,Res,EnumWarning,LocalState,TypeInfo,[]).

eval_codes_aux(Expression,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    TypeInfo=predicate(_),
    repl_parse_predicate_for_solving(Expression,OuterQuantifier,Typed,TypeInfo),
    !,
    eval_predicate_in_cur_state(Typed,Res,EnumWarning,LocalState).

eval_codes_aux(_E,_,Res,EnumWarning,LocalState,TypeInfo) :- eval_codes_error(Res,EnumWarning,LocalState,TypeInfo).

eval_codes_aux0("$$",_,Res,false,[],print_last_expression) :- !, Res='',
    print_last_expression.

eval_codes_aux0("$",_,Res,false,[],print_last_info) :- !, Res='',
    print_last_info.

eval_codes_aux0(":col",_,Res,false,[],print_last_expression) :- !, Res='',
    toggle_colouring.

eval_codes_aux0(":recheck",_,Res,EnumWarning,[],recheck_pp_of_last_expression) :- !,
    recheck_pp_of_last_expression(ascii,Res,EnumWarning).

eval_codes_aux0(Codes,_,Res,false,[],set_eval_repeat) :- append("!r",Rest,Codes),
    number_codes(Nr,Rest), !, Res='',
    set_eval_repeat(Nr).

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    append(":repeat ",RestC,Codes),!,
    (eval_repeat(Nr) -> true ; Nr=100), N1 is Nr-1,
    (between(1,N1,Try),
    format('>>> (~w)~n',[Try]),
    (eval_codes_aux0(RestC,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) -> true),
    reset_errors,
    fail
    ;
    format('>>> (~w)~n',[Nr]),
    eval_codes_aux0(RestC,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo)
).

eval_codes_aux0(Codes,_OuterQuantifier,Res,false,LocalState,list) :-
    ( append(":list ",Rest,Codes),
    scan_identifier(Rest,IDCodes,Rest2), atom_codes(ID,IDCodes)
    ;
    Codes = ":list", ID=help, Rest2=[]),
    !,
    (just_whitespace(Rest2) -> true ; add_error(eval_strings,'Ignoring extra argument: ',Rest2)),
    list_information(ID,Res,LocalState).

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    match_command(":print", Codes,PredCodes),
    TypeInfo=predicate(_),
    !, EnumWarning=false,LocalState=[],
    repl_parse_predicate_allow_ws(PredCodes,OuterQuantifier,Typed,TypeInfo),
    nested_print_repl_expression(Typed),
    Res=''.

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    match_command(":sym", Codes,PredCodes),
    TypeInfo=predicate(_),
    !, EnumWarning=false,LocalState=[],
    repl_parse_predicate_allow_ws(PredCodes,OuterQuantifier,ExTyped,TypeInfo),
    (is_existential_quantifier(ExTyped,_,Typed) -> true ; Typed=ExTyped),
    format('Computing symmetry breaking predicate for: ',[]),
    translate:print_bexpr(Typed),nl,
    smt_symmetry_breaking:get_top_level_symmetry_breaking_predicates_decomposed(Typed,TS),
    format('Symmetry breaking: ',[]), translate:print_bexpr(TS),nl,
    Res=''.

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    match_command(":check-ast",Codes,PredCodes),
    TypeInfo=predicate(_),
    !, EnumWarning=false,LocalState=[],
    format('Checking generated AST (Abstract Syntax Tree)~n',[]),
    repl_parse_predicate_allow_ws(PredCodes,OuterQuantifier,Typed,TypeInfo),
    (bsyntaxtree:check_ast(Typed) -> Res='TRUE' ; Res='FALSE').

eval_codes_aux0(Codes,_OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    match_command(":components", Codes,PredCodes),
    TypeInfo=predicate(_),
    !, EnumWarning=false,LocalState=[],
    repl_parse_predicate_allow_ws(PredCodes,no_quantifier,Typed,TypeInfo),
    predicate_components(Typed,Components),
    maplist(print_component,Components),
    Res=''.

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    match_command(":compile",Codes,PredCodes),
    TypeInfo=predicate(_),
    !, EnumWarning=false,LocalState=[],
    repl_parse_predicate_allow_ws(PredCodes,OuterQuantifier,Typed,TypeInfo),
    write('Compiling: '), translate:print_bexpr(Typed),nl,
    get_cur_state_for_repl(Typed,State),
    b_compiler:b_optimize(Typed,[],[],State,NewTyped,no_wf_available),
    nested_print_repl_expression(NewTyped),
    Res=''.

eval_codes_aux0(":wd",_,Res,EnumWarning,LocalState,analyse_wd_for_machine) :- !,
    EnumWarning=false,LocalState=[],
    well_def_analyser:analyse_wd_for_machine(_,_,Res).

eval_codes_aux0(":pinv",_,Res,EnumWarning,LocalState,analyse_wd_for_machine) :- !,
    EnumWarning=false,LocalState=[],
    start_timer(T1,W1),
    well_def_analyser:analyse_invariants_for_machine(UnchangedNr,ProvenNr,UnProvenNr,TotPOsNr,[]),
    stop_timer('% Time to run wd-prover on all invariant POs: ',T1,W1),
    (TotPOsNr>0 -> Perc is (UnchangedNr+ProvenNr)*100/ TotPOsNr ; Perc = 100.0),
    format('Proof summary for ~w POs (~2f % discharged): ~w unchanged, ~w proven, ~w unproven~n',
    [TotPOsNr,Perc,UnchangedNr,ProvenNr,UnProvenNr]), Res=ProvenNr.

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    append(":wd ",PredCodes,Codes),
    !,
    set_current_codes(PredCodes),
    (TypeInfo=predicate(_),repl_parse_predicate_allow_ws(PredCodes,OuterQuantifier,Typed,TypeInfo)
    -> EnumWarning=false,LocalState=[],
    analyse_wd_for_expr(Typed,_ResStr,Discharged,message), Res=Discharged
    ; eval_codes_error(Res,EnumWarning,LocalState,TypeInfo)
).

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    match_command(":wde",Codes,PredCodes), % perform WD analysis and solve transformed predicate
    TypeInfo=predicate(_),
    !,
    repl_parse_predicate_allow_ws(PredCodes,OuterQuantifier,Typed,TypeInfo),
    annotate_wd(Typed,NewTyped),
    eval_predicate_in_cur_state(NewTyped,Res,EnumWarning,LocalState).

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    append(":check ",Rest,Codes),
    TypeInfo=predicate(_),
    !,
    debug_println(20,check_recognised),
    (eval_codes_aux(Rest,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo)
    -> (Res== 'TRUE' -> true ;
    atom_codes(S,Rest), add_error(check,':check predicate not TRUE: ',S)
    )
    ; atom_codes(S,Rest), add_error(check,':check illegal predicate: ',S)
).

eval_codes_aux0(Codes,_OuterQuantifier,RRes,EnumWarning,LocalState,TypeInfo) :-
    append(":exec ",Rest,Codes),
    TypeInfo=subst,
    !,
    debug_println(4,'parsing substitution'),
    repl_parse_substitution(Rest,Statement),
    pp_eval_expr(Statement),
    enter_new_error_scope(ScopeID,eval_codes_aux0),clear_all_errors_in_error_scope(ScopeID),
    (tcltk_interface:tcltk_add_user_executed_statement(Statement,Updates,NewID)
    -> format('Successfully executed statement leading to state: ~w~n',[NewID]),
    Res = 'TRUE',LocalState=Updates
    ; translate:translate_substitution(Statement,Str),
    format_with_colour_nl(user_output,[red],'Could not execute statement: ~w',[Str]),
    Res = 'FALSE',LocalState=[]
    ),
    EnumWarning=false,
    print('Execution result: '),display_and_set_result(ScopeID,Res,RRes,EnumWarning),
    (LocalState=[] -> true
    ; display_solution('Updates:~n',unknown,LocalState)).

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- % let ID = EXPR construct
    (append("let ",Rest,Codes),DotForm=false ; append(":let ",Rest,Codes), DotForm=true),
    scan_identifier(Rest,IDCodes,Rest2),
    atom_codes(ID,IDCodes),
    (scan_to_equal(Rest2,Rest3) -> true
    ; DotForm=false -> debug_println(19,'Missing = sign for let-construction'),
    fail % let mod 2 = 0 is a valid predicate
    ; debug_println(19,'Inserting missing = for :let'), Rest3=Rest2
    ),
    !,
    debug_println(20,let_recognised(ID)),
    eval_codes_aux(Rest3,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo),
    (store_let_id_last_value(ID) -> true ;
    format_with_colour_nl(user_error,[red],'### Could not store let: ~w',[ID])).

eval_codes_aux0(Codes,_,Res,EnumWarning,LocalState,TypeInfo) :- % :s ID : store ID extracted from last predicate
    (append(":s ",Rest,Codes) ; append(":store ",Rest,Codes)),
    scan_identifier(Rest,IDCodes,Rest2),
    atom_codes(ID,IDCodes),
    Rest2=[], % TO DO: allow whitespace
    !,
    (get_last_predicate_value_for_id(ID,T,Val)
    -> store_let_id_last_value(ID), translate_bvalue_with_limit_and_col(Val,50,VS),
    format('Stored ~w = ~w~n',[ID,VS]), Res=Val, TypeInfo = T
    ; format_with_colour_nl(user_error,[red],'### Could not find value for ~w in last predicate',[ID]),
    Res=error, TypeInfo=error),
    EnumWarning=false, LocalState=[].

eval_codes_aux0(Codes,_,Res,EnumWarning,LocalState,TypeInfo) :- % :u ID : remove let for ID
    (append(":u ",Rest,Codes) ; append(":unlet ",Rest,Codes)),
    scan_identifier(Rest,IDCodes,Rest2),
    atom_codes(ID,IDCodes),
    Rest2=[], % TO DO: allow whitespace
    !,
    (retract_stored_let_value(ID,_,_) ->
    format('Undefined let ~w~n',[ID]), Res=ID, TypeInfo = unlet,
    reset_parse_cache % TO DO: maybe remove just all cached expressions using ID
    ; format_with_colour_nl(user_error,[red],'### Could not find let for ~w. Use :b to browse your lets.',[ID]), Res=error, TypeInfo=error),
    EnumWarning=false, LocalState=[].

eval_codes_aux0(":b",_,Res,EnumWarning,LocalState,browsing) :-
    !,EnumWarning=false, LocalState=[],
    get_repl_lets_info(Res), print(repl_lets(Res)),nl.

eval_codes_aux0(Codes,_,Res,EnumWarning,LocalState,typing) :-
    (append(":t ",Expression,Codes) ; append(":type ",Expression,Codes)),
    % :t Expression Haskell like command
    !, EnumWarning=false, LocalState=[],
    repl_typing_scope(TypingScope),
    (b_parse_machine_expression_from_codes(Expression,TypingScope,_Typed,Type,true,Error)
    -> (Error=none
    -> %translate:pretty_type(Type,PrettyType), % will print seq(.)
    create_maximal_type_set(Type,MaxTS), translate_bexpression(MaxTS,PrettyType),
    (max_cardinality(Type,Card) -> true ; Card='??'),
    ajoin([PrettyType,' /* card=',Card,' */'],Res),
    print(Res),nl
    ; (Error=type_error -> get_type_error(Res) ; Res = 'SYNTAX ERROR'),
    print_red('Not a valid expression'),nl)
    ; print_red('Parsing failed'),nl,
    Res = 'SYNTAX ERROR').

eval_codes_aux0(Codes,_,Res,EnumWarning,LocalState,TypeInfo) :-
    append(":find-value ",Codes1,Codes),
    find_value_options(Options,Codes1,ExpressionCodes),
    EnumWarning=false, LocalState=[],
    repl_parse_expression(ExpressionCodes,TExpr,TypeInfo,Error),
    Error=none,
    eval_expression_direct(TExpr,GoalValue),
    get_texpr_type(TExpr,Type),
    (Options = [Opt1|_], GoalValue \= string(_)
    -> add_warning(find_value,':find-value option only useful when using string as target: ',Opt1)
    ; true),
    findall(list([ID,Kind,MatchMsg]),
    (tcltk_interface:find_value_in_cur_state(GoalValue,Type,Options,match(Kind,ID,Path)),
    format_to_codes('~w~n',[Path],MatchMsgC),
    format('* match inside ~w ~w @ path: ~w~n',[Kind,ID,Path]),
    atom_codes(MatchMsg,MatchMsgC)),Res).

eval_codes_aux0(Codes,_OuterQuantifier,OuterRes,false,LocalState,TypeInfo) :- TypeInfo=predicate(_),
    available_krt_prover(_,Provers,CommandStr),
    match_command(CommandStr,Codes,PredCodes), % commands like :pp, :ml, :krt
    !,
    % we ignore OuterQuantifier for proof commands and use forall:
    temporary_set_preference(use_common_subexpression_elimination,false,CHG),
    call_cleanup(repl_parse_predicate_allow_ws(PredCodes,forall,ExTyped,TypeInfo),
    reset_temporary_preference(use_common_subexpression_elimination,CHG)),
    LocalState=[],
    prove_sequent_with_krt_provers(Provers,ExTyped,Res),
    format('Universally quantified predicate is ',[]),
    (Res=proved
    -> print_green('PROVED'),
    OuterRes='TRUE' % for -evalt
    ; print_red(Res),
    OuterRes = 'UNKNOWN' % for -evalu
    ),
    format(' with ~w~n',[Provers]).

eval_codes_aux0(Codes,_OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- TypeInfo=predicate(_),
    append(":forall ",PredCodes,Codes), % like krt, ml, pp command, but using ProB
    !,
    eval_codes_aux(PredCodes,forall,Res,EnumWarning,LocalState,TypeInfo).

eval_codes_aux0(Codes,OuterQuantifier,Res,false,LocalState,TypeInfo) :- TypeInfo=predicate(_),
    available_smt_solver(Solver,CommandStr), % :z3, :cvc4, ...
    append(CommandStr,PredCodes,Codes),
    !,
    solve_using_smt_solver(Solver,PredCodes,no_prolog,OuterQuantifier,Res,LocalState,TypeInfo).

eval_codes_aux0(":z3-version",_,Res,false,LS,TypeInfo) :- LS=[], TypeInfo=string,
    smt_solver_version(z3,Version),
    smt_solver_header_version(z3,HVersion),
    !,
    format('Z3 version is ~w (ProB was compiled against ~w)~n',[Version,HVersion]),
    Res = Version.

eval_codes_aux0(Codes,OuterQuantifier,Res,false,LocalState,TypeInfo) :- TypeInfo=predicate(_),
    available_smt_solver_for_file(Solver,FileCommandStr), % :z3-file, ...
    append(FileCommandStr,FileCodes,Codes),
    !,
    solve_using_smt_solver_from_file(Solver,FileCodes,OuterQuantifier,Res,LocalState,TypeInfo).

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- %TypeInfo=predicate(_),
    append(":kodkod ",PredCodes,Codes), !,
    temporary_set_preference(use_solver_on_load,kodkod,CHG),
    call_cleanup(eval_codes_aux(PredCodes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo),
    reset_temporary_preference(use_solver_on_load,CHG)).

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    append(":chr ",PredCodes,Codes), !,
    temporary_set_preference(use_chr_solver,true,CHG),
    call_cleanup(eval_codes_aux(PredCodes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo),
    reset_temporary_preference(use_chr_solver,CHG)).

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    append(":cse ",PredCodes,Codes), !,
    temporary_set_preference(use_common_subexpression_elimination,true,CHG),
    call_cleanup(eval_codes_aux(PredCodes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo),
    reset_temporary_preference(use_common_subexpression_elimination,CHG)).

eval_codes_aux0(Codes,_OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    get_minmax_command(Codes,OptMode,LambdaExprC), % :min or :max
    repl_parse_expression(LambdaExprC,LambdaExpr,TypeInfo,Error),
    Error=none,
    closures:is_lambda_comprehension_set(LambdaExpr,Parameters,TypedPred,OptExpr),
    format(' ~w lambda expression of type ~w~n',[OptMode,TypeInfo]),
    !,
    get_cur_state_for_repl(LambdaExpr,EState),
    optimizing_solve_predicate(OptMode,EState, Parameters,TypedPred,OptExpr,OptVal,LocalState),
    translate:translate_bvalue(OptVal,OS),
    format('OPTIMAL VALUE = ~w~nFOR SOLUTION:~n',[OS]),
    display_solution('',Parameters,LocalState),
    Res = OS,EnumWarning=false.

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    get_minmax_command(Codes,OptMode,PredCodes),
    !,
    set_eval_mode(optimizing(OptMode)),
    call_cleanup(eval_codes_aux(PredCodes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo),
    unset_eval_mode).

eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
    eval_codes_aux(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo).

eval_codes_error(Res,false,[],TypeInfo) :-
    %findall(S,check_error_occured(S,_),L), print(errs(L)),nl,
    (check_error_occured(type_expression_error,_) -> Res = 'TYPE ERROR', TI = error
    ; Res = 'SYNTAX ERROR', TI = syntax_error
    ),
    show_error_pos,
    ((nonvar(TypeInfo),TypeInfo=predicate(_)) -> print('Not a valid predicate'),nl
    ; (nonvar(TypeInfo),TypeInfo=expression(_)) -> print('Not a valid expression'),nl
    ; print('Not a valid expression or predicate'),nl
    ),
    TypeInfo=TI.

eval_codes_with_time_out(Codes,OuterQuantifier,StringResult,EnumWarning,LocalState,TypeInfo) :-
    %format("Eval: ~s~n",[Codes]),
    get_computed_preference(debug_time_out,DTO),
    %print(debug_time_out(DTO)),nl,
    safe_time_out(eval_codes(Codes,OuterQuantifier,StringResult,EnumWarning,LocalState,TypeInfo),DTO,TimeOutRes),
    (TimeOutRes=time_out ->
    StringResult = '**** TIME-OUT ****', print(StringResult), print(' ('),print(DTO), print('ms)'),nl,
    EnumWarning = time_out
    ; true).

eval_det :- eval_mode(eval_det).

eval_expression(Typed,RRes,Options) :- eval_expression(Typed,RRes,_PrologTerm,Options).

eval_expression(Typed,RRes,NValue,Options) :- %% print('Start Eval Expression: '),nl,flush_output,
    enter_new_error_scope(ScopeID,eval_expression),
    clear_all_errors_in_error_scope(ScopeID),
    replace_expression_by_kodkod_if_enabled(Typed,Typed2),
    set_last_expression(expr,Typed2,exception),
    debug_println(5,'Start Eval Expression'),
    %profile_reset, set_prolog_flag(profiling,on), % comment in to profile individual expression evaluations
    (eval_expression_direct(Typed2,Value)
    -> true
    ; set_last_expression(expr,Typed2,error),fail % probably wd-error
    ),
    !,
    %set_prolog_flag(profiling,off), print_profile, % comment in to profile individual expression evaluations
    debug_println(5,'Normalising Value'),
    normalise_eval_value(Value,NValue),
    set_last_expression(expr,Typed2,NValue),
    (member(silent_no_string_result,Options) -> RRes = '?'
    ;
    debug_println(5,'Translating Value'),
    translate_bvalue_with_col(NValue,Typed2,Result),
    %get_only_critical_enum_warning(EnumWarning),
    start_terminal_colour([dark_gray],user_output),
    format(user_output,'Expression Value = ~n',[]), % TO DO: make output optional, e.g., for json trace replay
    reset_terminal_colour(user_output),
    display_and_set_result(ScopeID,Result,RRes,false),
    display_dot_expr_result(Typed2,NValue) % TO DO: if we have a let with ID: use ID rather than result
).

eval_expression(_,Cause,error,_) :-
    get_fail_error_cause(Cause), % TO DO: refactor and use abort_error_occured_in_error_scope,...
    exit_error_scope(_ScopeID,_,eval_expression).