solver_interface

apply_kodkod_or_other_optimisations(Identifiers,Predicate,NewPredicate) :-
    get_preference(use_solver_on_load,kodkod),
    !,
    (replace_by_kodkod(Identifiers,Predicate,NewPredicate) -> true
    ; get_texpr_ids(Identifiers,Ids),
    add_warning(kodkod_fail,'Could not use KODKOD to translate predicate to SAT, identifiers = ', Ids, Predicate),
    (get_preference(kodkod_for_components,full)
    -> throw(enumeration_warning(translating_for_kodkod,Ids,[],kodkod,critical))
    ; true),
    NewPredicate = Predicate
).

apply_kodkod_or_other_optimisations(Identifiers,Predicate,NewPredicate) :-
    Span=Predicate,
    perform_do_not_enumerate_analysis(Identifiers,Predicate,'EXISTS',Span,NewPredicate).

apply_kodkod_or_other_optimisations(Ids,Types,Predicate,NewPredicate) :-
    get_preference(use_solver_on_load,kodkod),
    maplist(create_id,Ids,Types,Identifiers),
    !,
    apply_kodkod_or_other_optimisations(Identifiers,Predicate,NewPredicate).

apply_kodkod_or_other_optimisations(_Identifiers,_Types,Predicate,Predicate).

call_with_smt_mode_enabled(Call) :-
    temporary_set_preference(use_smt_mode,true,SMT),
    temporary_set_preference(use_clpfd_solver,true,CLPFD), % we also enable CLPFD
    % TO DO: also enable CHR
    call_cleanup( (Call,!),
    (reset_temporary_preference(use_smt_mode,SMT),
    reset_temporary_preference(use_clpfd_solver,CLPFD)
)).

clean_solver_predicate(Pred,Options,CleanedPred) :-
    (nonmember(repair_used_ids,Options) -> Pred0=Pred
    ; repair_used_ids(solve_predicate,Pred,Pred0)), % ideally we should not need this; some BMC monolithic predicates are faulty and this allows a repair
    (nonmember(clean_up_pred,Options) -> CleanedPred=Pred0
    ; clean_up_pred(Pred0, [], CleanedPred)
    -> (debug_mode(off) -> true ; print(cleaned),nl, translate:print_bexpr(CleanedPred),nl)
    ; add_internal_error('Clean up failed ', solve_predicate_aux3), CleanedPred=Pred0
).

create_id(Id,Type,b(identifier(Id),Type,[])).

exit_err_scope(ScopeID,Options,Res) :-
    (member(ignore_wd_errors,Options),wd_error_occured
    -> debug_format(19,'Ignoring WD-Error(s) in solve_predicate (scope: ~w, result: ~w)~n',[ScopeID,Res]),
    clear_wd_errors
    ; true),
    exit_error_scope(ScopeID,_,solve_predicate_aux).

fallback_to_smt_if_requested(solution(S),_,_,Res) :- !, Res=solution(S).

fallback_to_smt_if_requested(contradiction_found,_,_,Res) :- !,Res=contradiction_found.

fallback_to_smt_if_requested(S,_,_,Res) :-
    \+ preferences:get_preference(smt_supported_interpreter,true), ! , Res = S.

fallback_to_smt_if_requested(_,Pred,State,Res) :-
    smt_solve_predicate(z3,Pred,State,Res), !.

get_full_machine_state_typed_identifiers(TIds) :-
    b_get_machine_variables(Variables),
    b_get_machine_constants(Constants), append(Constants,Variables,TIds).

initialise_localstate(FullStore,bind(Var,Val)) :-
    (member(bind(Var,VarVal),FullStore)
    -> Val=VarVal ; true).

link_bindings([],[]).

link_bindings([],[bind(ID,_)|_T]) :- add_error(solve_predicate,'Provided state has no entry for identifier: ',ID),fail.

link_bindings([bind(ID,Val)|T1],[bind(ID,Val)|T2]) :- !,link_bindings(T1,T2).

link_bindings([bind(_,_)|T],S2) :- % ignore ID in state provided to solver
    link_bindings(T,S2).

normalise_solver_store(yes,Store,NormStore) :- !, normalise_solver_store2(Store,NormStore).

normalise_solver_store(_,S,Res) :- !,
    Res=S. % for error, time_out, ... Store irrelevant; just copy to avoid call_residues

normalise_solver_store2(no_state,R) :- !, R=no_state.

normalise_solver_store2(CState,State) :- normalise_store(CState,State),!.

normalise_solver_store2(CState,Res) :-
    add_internal_error('Normalising store failed:',normalise_solver_store2(CState,Res)),
    Res=CState.

predicate_uses_unfixed_deferred_set(TExpr) :- predicate_uses_unfixed_deferred_set(TExpr,_).

predicate_uses_unfixed_deferred_set(TExpr,CType) :-
    unfixed_deferred_set_exists, % check first if some unfixed deferred set exists
    map_over_typed_bexpr(solver_interface:uses_unfixed_ds_aux,TExpr,CType).

problematic_id(DeferredSets,TID) :- get_texpr_type(TID,Type),
    uses_def_set(Type,DeferredSets).

set_no_state(State) :- var(State),!,State=no_state.

set_no_state(_).

set_up_typed_localstate_for_pred(CV,Pred,TypedVals,State) :-
    (preference(use_static_ordering,true)
    -> sort_ids_by_usage(CV,Pred,SortedVarlist,no_warnings) ,
    set_up_typed_localstate(SortedVarlist,_FreshVars,TypedVals,[],SortedState,positive),
    reorder_state(CV,SortedState,State) % SortedState can have issues with pack_state skeleton
    ; set_up_typed_localstate(CV,_FreshVars,TypedVals,[],State,positive)).

solve_components(Pred2,State,TypedVals) :-
    call_residue(
    b_interpreter_components:b_trace_test_components(Pred2,State,TypedVals),
    Residue),
    (Residue=[] -> true
    ; add_internal_error('Call residue in solve_predicate: ',Residue)
%add_message(solver_interface,'Call residue in solve_predicate: ',Residue)
).

solve_predicate(Pred,State,Res) :- solve_predicate(Pred,State,1,Res).

solve_predicate(Pred,State,TimeoutFactor,Res) :-
    solve_predicate(Pred,State,TimeoutFactor,[use_smt_mode/true,use_clpfd_solver/true],Res).

solve_predicate(Pred,State,TimeoutFactor,Options,RealRes) :-
    solve_predicate_with_options(Options,[],Pred,State,TimeoutFactor,Res), !,
    if(solver_result(Res,Pred,State,Options,RealResBeforeFallback),true,
    (add_internal_error('Unknown solver_result: ',Res),RealResBeforeFallback=error)),
    fallback_to_smt_if_requested(RealResBeforeFallback,Pred,State,RealRes).

solve_predicate_aux(Pred,State,TimeoutFactor,Options,Res) :-
    enter_new_error_scope(ScopeID,solve_predicate), %print(enter_scope(ScopeID)),nl,
    call_cleanup(solve_predicate_aux0(Pred,State,TimeoutFactor,Options,Res),
    exit_err_scope(ScopeID,Options,Res)).

solve_predicate_aux0(Pred,State,TimeoutFactor,Options,Res) :-
    clean_solver_predicate(Pred,Options,CleanedPred),
    (solve_predicate_aux1(CleanedPred,State,TimeoutFactor,Options,SRes)
    -> (SRes = time_out
    -> fail % fail if we have a time_out to avoid pending co-routines and return time_out in clause below
    ; !, Res=SRes
    )
    ; !,
    add_warning(solver_interface,'solve_predicate failed:',CleanedPred), % this should normally not happen
    fail % the above can fail when state is provided
).

solve_predicate_aux0(_,_,_,_,time_out).

solve_predicate_aux1(Pred,State,TimeoutFactor,Options,Res) :- var(State),
    solve_predicate_aux2(Pred,CState,TimeoutFactor,Options,Res),
    !, % we only look for one solution
    normalise_solver_store(Res,CState,State),
    clear_enumeration_warnings. % avoid propagating them higher up

solve_predicate_aux1(Pred,State,TimeoutFactor,Options,Res) :- nonvar(State),
    solve_predicate_aux2(Pred,State,TimeoutFactor,Options,Res),
    !, % we only look for one solution
    clear_enumeration_warnings. % avoid propagating them higher up

solve_predicate_aux1(_Pred,State,_TimeoutFactor,_Options,Res) :-
    critical_enumeration_warning_occured_in_error_scope(A,B,C,D), % we did not find a solution: check for enum warnings
    !,
    clear_enumeration_warnings,
    set_no_state(State),
    Res = virtual_time_out(enumeration_warning(A,B,C,D,critical)).

solve_predicate_aux1(Pred,State,_TimeoutFactor,_Options,Res) :- var(State),!,
    % a variable state means we are in a disprover context; check if deferred sets are involved
    set_no_state(State),
    % print('Checking for use of deferred sets in: '), translate:print_bexpr(Pred),nl,
    (predicate_uses_unfixed_deferred_set(Pred,CType)
    -> debug_println(10,solver_predicate_contains_unfixed_deferred_set(CType)),
    Res=unfixed_deferred_sets
    % if no unfixed global sets involved -> real contradiction found
    ; Res=no
).

solve_predicate_aux1(_Pred,_State,_TimeoutFactor,_Options,Res) :-
    % if state is set: we are looking for a solution in the context of the current state
    % which implicitly includes the valuation of the unfixed deferred sets, hence
    % we can return no rather than unfixed_deferred_sets
    %set_no_state(State),
    Res = no.

solve_predicate_aux2(Pred,State,TimeoutFactor,Options,Res) :-
    %predicate_level_optimizations(Pred,OptPred),
    % is now done in b_interpreter_components; to avoid that CSE disrupts partitioning
    catch_clpfd_overflow_call2(
    solve_predicate_aux3(Pred,State,TimeoutFactor,Options,Res),
    ( debug_println(19,overflow_in_solve_predicate),
    %clpfd_interface:clpfd_overflow_warning_message, % message is already printed by catch_clpfd_overflow_call2
    % we could try and solve without CLPFD ?!!
    Res=overflow,State=no_state)).

solve_predicate_aux3(Pred,State,TimeoutFactor,Options,Res) :-
    % find all identifiers used in the predicate and create a state
    % was done by the caller, leading to code duplication
    (member(full_machine_state,Options) -> get_full_machine_state_typed_identifiers(FilteredIdentifiers)
    ; find_typed_identifier_uses(Pred,FilteredIdentifiers)),
    !,
    % global constants should not appear in the state
    % otherwise they treated are as variables by the solver
    % -> we now call find_typed_identifier_uses; we used to call filter_global_identifiers(Identifiers,FilteredIdentifiers),
    % state may be predefined / partially set up
    apply_kodkod_or_other_optimisations(FilteredIdentifiers,Pred,Pred2),
    (member(solve_in_visited_state(StateID),Options)
    -> set_up_typed_localstate_for_pred(FilteredIdentifiers,Pred2,TypedVals,State),
    (visited_expression(StateID,StateExpr),
    state_corresponds_to_set_up_constants(StateExpr,FullStore)
    -> maplist(initialise_localstate(FullStore),State)
    ; StateID=root -> true
    ; add_internal_error('Illegal State:',use_visited_state(StateID))
    )
    ; var(State)
    -> set_up_typed_localstate_for_pred(FilteredIdentifiers,Pred2,TypedVals,State)
    % TypedVals contains typedval(Val,Type,Var,TriggersEnumWarning)
    % TO DO: add static_symmetry detection b_global_sets:static_symmetry_reduction_for_global_sets(State),
    ;
    set_up_typed_localstate_for_pred(FilteredIdentifiers,Pred2,TypedVals,State2),
    sort(State,S1),sort(State2,S2),
    link_bindings(S1,S2)
    ),
    %tools_printing:print_term_summary(b_trace_test_components(Pred2,State,TypedVals)),nl,
    b_interpreter_components:reset_component_info(false),
    time_out_with_factor_call(
    solver_interface:solve_components(Pred2,State,TypedVals),
    TimeoutFactor, [silent],
    TO='time_out'),
    (TO==time_out -> Res = TO ; Res = yes).

solve_predicate_direct(Pred,State,TimeoutFactor,Options,Res) :-
    %temporary_set_preference(randomise_enumeration_order,true),
    %temporary_set_preference(find_abort_values,true), % I am not sure we should do this; we want to find counter-examples quickly, we are less worried with finding WD-problems ?!
   
    %temporary_set_preference(minint,-2147483648), % disabled to pass tests 1004,1015,..
    %temporary_set_preference(maxint,2147483647),
    get_total_number_of_errors(Errs),
   
    announce_event(start_solving),
    solve_predicate_aux(Pred,State,TimeoutFactor,Options,InnerRes),
    announce_event(end_solving),
   
    get_total_number_of_errors(ErrsAfter),
    (InnerRes = overflow -> Res = overflow ; ErrsAfter>Errs -> Res = error; Res = InnerRes).

solve_predicate_with_options([],RestOptions,Pred,State,TimeoutFactor,Res) :-
    solve_predicate_direct(Pred,State,TimeoutFactor,RestOptions,Res).

solve_predicate_with_options([Option|T],RestOptions,Pred,State,TimeoutFactor,Res) :-
    solve_with_option(Option,T,RestOptions,Pred,State,TimeoutFactor,Res).

solve_with_option('CHR',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
    solve_with_option(use_chr_solver/true,T,Rest,Pred,State,TimeoutFactor,Res).

solve_with_option('SMT',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
    solve_with_option(use_smt_mode/true,T,Rest,Pred,State,TimeoutFactor,Res).

solve_with_option('KODKOD',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
    solve_with_option(use_solver_on_load/kodkod,T,Rest,Pred,State,TimeoutFactor,Res).

solve_with_option('SMT_SUPPORTED_INTERPRETER',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
    solve_with_option(smt_supported_interpreter/true,T,Rest,Pred,State,TimeoutFactor,Res).

solve_with_option('CLPFD',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
    solve_with_option(use_clpfd_solver/true,T,Rest,Pred,State,TimeoutFactor,Res).

solve_with_option(Pref/Val,T,Rest,Pred,State,TimeoutFactor,Res) :- !,
    call_with_preference(solve_predicate_with_options(T,Rest,Pred,State,TimeoutFactor,Res),Pref,Val).

solve_with_option(Opt,T,Rest,Pred,State,TimeoutFactor,Res) :-
    valid_solver_option(Opt),!,
    solve_predicate_with_options(T,[Opt|Rest],Pred,State,TimeoutFactor,Res).

solve_with_option(Opt,T,Rest,Pred,State,TimeoutFactor,Res) :-
    add_warning(solve_with_option,'Unrecognised option: ',Opt),
    solve_predicate_with_options(T,Rest,Pred,State,TimeoutFactor,Res).

solver_pp_bvalue(Value,Options,EValue,PPValue) :- member(force_evaluation,Options),!,
    EXPAND=force,
    normalise_value_for_var(solver_result,EXPAND,Value,EValue), % will suspend if timeout occurs!
    solver_pp_bvalue2(EValue,Options,PPValue).

solver_pp_bvalue(Value,Options,Value,PPValue) :- solver_pp_bvalue2(Value,Options,PPValue).

solver_pp_bvalue2(Value,Options,PPValue) :- member(truncate(Limit),Options),!,
    translate_bvalue_with_limit(Value,Limit,PPValue). % should we also control expand_avl_upto ??

solver_pp_bvalue2(Value,Options,PPValue) :- member(truncate,Options),!,
    translate_bvalue_with_limit(Value,10000,PPValue).

solver_pp_bvalue2(Value,_,PPValue) :- translate_bvalue(Value,PPValue).

solver_result(time_out,_P,_State,_,Res) :- !,Res=time_out.

solver_result(error,_P,_State,_,Res) :- !,Res=error.

solver_result(no,_P,_State,_,Res) :- !, Res=contradiction_found.

solver_result(unfixed_deferred_sets,_,_,_,Res) :- !,
    Res=no_solution_found(unfixed_deferred_sets).

solver_result(virtual_time_out(Reason),_P,_State,_,Res) :- !,
    Res=no_solution_found(Reason).

solver_result(overflow,_P,_State,_,Res) :- !, Res=no_solution_found(clpfd_overflow).

solver_result(yes,_P,State,Options,Res) :- !,Res=solution(Solution),
    findall(binding(Id,EValue,PPValue),
    (member(bind(Id,Value),State),
    (solver_pp_bvalue(Value,Options,EValue,PPValue) -> true
    ; EValue=Value, PPValue='**pretty-print failed**')),
    Solution).

solver_result(OTHER,_P,_State,_,no_solution_found(OTHER)) :-
    add_internal_error('Unknown solver_result:',OTHER).

strip_outer_exists(b(exists(Paras,Pred),pred,_),Res) :-
    debug_println(9,stripping_exists(Paras)),
    strip_outer_exists(Pred,Res).

strip_outer_exists(b(let_predicate(Paras,Exprs,Pred),pred,_),R) :- !,
    debug_println(9,stripping_let(Paras,Exprs)),
    maplist(create_equality,Paras,Exprs,Equals),
    append(Equals,[Pred],List),
    conjunct_predicates(List,NewPred),
    strip_outer_exists(NewPred,R).

strip_outer_exists(R,R).

type_check_in_machine_context(Predicates, TPredicates) :-
    % create an empty type environment
    % and store the known types of variables / constants
    % otherwise, we might be unable to type variables from
    % machines somewhere in the refinement hierarchy
    % (their typing predicate might not be in the hypothesis)
    % Definitions are also added to the environment since the typechecker
    % inlines definitions.
    env_empty(E),
    b_get_machine_variables(V), b_get_machine_constants(C),
    % add theory operators
    full_b_machine(Machine),
    get_section(operators,Machine,Operators),
    keys_and_values(Operators,Ids,Ops),
    foldl(env_store_operator,Ids,Ops,E,EWithTheories),
    get_section(definitions, Machine, Definitions),
    foldl(env_store_definition, Definitions, EWithTheories, EWithDefinitions),
    % constants and variables
    findall(b(identifier(Name),global(GlobalSet),[enumerated_set_element]),is_b_global_constant(GlobalSet,_Nr,Name),GC),
    findall(b(identifier(Set),set(global(Set)),[given_set]),b_global_set(Set),GS),
    add_identifiers_to_environment(V,EWithDefinitions,EV),
    add_identifiers_to_environment(C,EV,EVC),
    add_identifiers_to_environment(GC,EVC,EVCGC),
    add_identifiers_to_environment(GS,EVCGC,EOut),
    opentype(Predicates, EOut, Identifiers, DeferredSets, TPredicates),
    % DeferredSets should be empty? I.e. should this be allowed to create new types?
    % currently this would not work as these types have not been added/registered in b_global_sets ! kernel_objects:basic_type would fail
    (DeferredSets = [] -> true
    ; include(problematic_id(DeferredSets),Identifiers,TErrIds),
    maplist(get_texpr_id,TErrIds,ErrIds),
    add_warning(solver_interface,'The types of some variables could not be determined: ',ErrIds),
    fail).

unfixed_typed_id_in_list(TID,CType,Constants) :-
    unfixed_deferred_set_exists, % check first if some unfixed deferred set exists
    member(TID,Constants), get_texpr_type(TID,CType),
    contains_unfixed_deferred_set(CType).

uses_def_set(global(T),DeferredSets) :- member(T,DeferredSets).

uses_def_set(set(A),DeferredSets) :- uses_def_set(A,DeferredSets).

uses_def_set(seq(A),DeferredSets) :- uses_def_set(A,DeferredSets).

uses_def_set(couple(A,_),DeferredSets) :- uses_def_set(A,DeferredSets).

uses_def_set(couple(_,A),DeferredSets) :- uses_def_set(A,DeferredSets).

uses_def_set(record(F),DS) :- member(field(_,T),F), uses_def_set(T,DS).

uses_unfixed_ds_aux(TExpr,DSType) :- get_texpr_type(TExpr,Type),
    contains_unfixed_deferred_set(Type,DSType).

valid_solver_option(full_machine_state).

valid_solver_option(ignore_wd_errors).

valid_solver_option(clean_up_pred).

valid_solver_option(allow_improving_wd_mode/_). % enable left-propagation of falsity/truth in clean_up

valid_solver_option(repair_used_ids).

valid_solver_option(solve_in_visited_state(S)) :- atomic(S).

valid_solver_option(truncate(Limit)) :- number(Limit). % truncate pretty printing

valid_solver_option(truncate). % 10000

valid_solver_option(force_evaluation). % force evaluation of symbolic results

valid_solver_option(use_smt_mode/_).

valid_solver_option(use_clpfd_solver/_).

valid_solver_option(use_chr_solver/_).

valid_solver_option(use_solver_on_load/_).

valid_solver_option(smt_supported_interpreter/_).

valid_solver_option(solver_strength/_).