dpllt_solver

add_typed_ids_in_scope(PTypedIds, TypedIds) :-
    b_get_machine_variables(MachineVars),
    b_get_machine_constants(MachineConstants),
    append([PTypedIds,MachineVars,MachineConstants], TypedIds).

arithmetic_expr(minus(Lhs,Rhs), Lhs, Rhs).

arithmetic_expr(add(Lhs,Rhs), Lhs, Rhs).

arithmetic_expr(div(Lhs,Rhs), Lhs, Rhs).

arithmetic_expr(floored_div(Lhs,Rhs), Lhs, Rhs).

arithmetic_expr(power_of(Lhs,Rhs), Lhs, Rhs).

arithmetic_expr(multiplication(Lhs,Rhs), Lhs, Rhs).

arithmetic_expr(modulo(Lhs,Rhs), Lhs, Rhs).

assert_idl_candidates([], _).

assert_idl_candidates([Id|T], IntConstants) :-
    retract(idl_candidate_constants(Id, Candidates)),
    !,
    subtract(IntConstants, Candidates, New),
    append(Candidates, New, NewCandidates),
    asserta(idl_candidate_constants(Id, NewCandidates)),
    assert_idl_candidates(T, IntConstants).

assert_idl_candidates([Id|T], IntConstants) :-
    asserta(idl_candidate_constants(Id, IntConstants)),
    assert_idl_candidates(T, IntConstants).

comparison_op(less(Lhs,Rhs), Lhs, Rhs).

comparison_op(less_equal(Lhs,Rhs), Lhs, Rhs).

comparison_op(equal(Lhs,Rhs), Lhs, Rhs).

comparison_op(not_equal(Lhs,Rhs), Lhs, Rhs).

conflict_driven_clause_learning_online(_, _, _, _, _, _, b(truth,pred,_), SolverResult) :-
    !,
    SolverResult = solution([]).

conflict_driven_clause_learning_online(_, _, _, _, _, _, b(falsity,pred,_), SolverResult) :-
    !,
    SolverResult = contradiction_found.

conflict_driven_clause_learning_online(SolverName, Env, SmtVars, SatVars, WDPosBoolFormula, AnalysisBoolFormula, BoolFormula, SolverResult) :-
    add_typed_ids_in_scope(SmtVars, StateTypedIds),
    % rewriting similar to Tseitin
    optimize_clause_size_by_rewriting(BoolFormula, SatVars, TOptBoolFormula, NewSatVars, NewVarConjList),
    conjunct_predicates([AnalysisBoolFormula,TOptBoolFormula], TFullBoolFormula),
    conjunct_predicates(NewVarConjList, NewVarConj),
    ( NewVarConj = b(truth,pred,_)
    -> FullBoolFormula = TFullBoolFormula
    ; % add new top-level Boolean variables introduced by Tseitin rewriting
    FullBoolFormula = b(conjunct(NewVarConj,TFullBoolFormula),pred,[])
    ),
    %bool_formula_to_smt(FullBoolFormula, SmtFullBoolFormula),
    %nl,nl,translate:nested_print_bexpr(SmtFullBoolFormula), nl,nl,
    get_bindings_from_ids(NewSatVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple),
    ( b_to_cnf(FullBoolFormula, SatBindings, CnfBoolFormula)
    -> true
    ; add_internal_error('B to CNF conversion failed ', dpllt)
    ),
    setup_theory_wf_store(SmtVars, SmtBindings, WfStoreSmt),
    ( get_preference(dpllt_use_idl_theory_solver,true)
    -> difference_logic_solver:init_idl_solver(IdlGraphMut)
    ; true
    ),
    ( WDPosBoolFormula \= b(truth,pred,_)
    -> % add WD PO implications
    b_to_cnf(WDPosBoolFormula, SatBindings, CnfWDPosBoolFormula),
    append(CnfWDPosBoolFormula, CnfBoolFormula, TNCnfBoolFormula)
    ; TNCnfBoolFormula = CnfBoolFormula
    ),
    dpllt_sat_solver:create_solver_state(SatStateMutable),
    SolverEnv = [sat_vars:NewSatVars,sat_varnames:SatVarNames,sat_bindings:SatBindings,t2b_env:Env,pl_vars:PrologSatVarTriple,smt_bindings:SmtBindings],
    dpllt_sat_solver:unit_propagate_cnf(SolverEnv, SatStateMutable, TNCnfBoolFormula, TNCnfBoolFormula2),
    sort(TNCnfBoolFormula2, NCnfBoolFormula),
    ( debug_mode(off)
    -> true
    ; dpllt_sat_solver:portray_cnf(NCnfBoolFormula)
    ),
    setup_reification(SatStateMutable, IdlGraphMut, IdPrologVarTuples, SmtBindings, WfStoreSmt),
    %format("Initial Smt Bindings after deterministic unit propagation:~n~w~n", [SmtBindings]),
    dpllt_sat_solver:sat(SolverName, SolverEnv, SatStateMutable, NCnfBoolFormula),
    %nl,nl,format("Exit sat solver, ground waitflags~n", []),
    %dpllt_sat_solver:portray_sat_stack(SatStateMutable),
    %\+ error_manager:check_error_occured(_, _),
    debug_format_dpllt("Ground waitflags", []),
    ( get_preference(dpllt_use_idl_theory_solver,true)
    -> propagate_fd_bounds_to_idl_solver(IdlGraphMut, SmtBindings),% TO DO: propagate from ProB to IDL solver earlier?
    get_idl_solution_bindings(IdlGraphMut, IdlBindings),
    ( % try one idl solution first since ProB could timeout, but do not enumerate idl solutions here
    set_bindings(IdlBindings, SmtBindings),
    ground_wait_flags(WfStoreSmt)
    ; exclude_idl_solution(IdlBindings, SmtBindings, StateTypedIds, WfStoreSmt),
    ( ground_wait_flags(WfStoreSmt)
    ; % fallback to idl solver and possibly enumerate all solutions
    critical_enumeration_warning_occured_in_error_scope(_, _, _, _),
    clear_enumeration_warnings,
    propagate_idl_solution_to_bindings_bt(IdlGraphMut, SmtBindings),
    ground_wait_flags(WfStoreSmt)
    )
    )
    ; ground_wait_flags(WfStoreSmt)
    ),
    ( check_error_occured(ErrorName, _),
    ErrorName \== warning(smt_symmetry_breaking),
    ErrorName \== smt_symmetry_breaking,
    fail
    ; true
    ),
    SolverResult = solution(SmtBindings),
    log_solution,
    announce_bt_from_smt_solution.

conflict_driven_clause_learning_online(_, _, _, _, _, _, _, Res) :-
    \+ check_error_occured(well_definedness_error, _),
    critical_enumeration_warning_occured_in_error_scope(A, B, C, D),
    !,
    clear_enumeration_warnings,
    Res = no_solution_found(enumeration_warning(A,B,C,D,critical)).

conflict_driven_clause_learning_online(_, _, _, _, _, _, _, Res) :-
    check_error_occured(ErrorName, _),
    ErrorName \== smt_symmetry_breaking,
    ErrorName \== warning(smt_symmetry_breaking),
    ErrorName \== well_definedness_error,
    ErrorName \== internal_error(b_compiler),
    !,
    Res = error.

conflict_driven_clause_learning_online(_, _, _, _, _, _, _, error) :-
    \+ initial_solution,
    check_error_occured(well_definedness_error, Reason),
    add_error(well_definedness_error, Reason, 'conflict_driven_clause_learning_online').

conflict_driven_clause_learning_online(_, _, _, _, _, _, _, contradiction_found) :-
    \+ initial_solution,
    \+ check_error_occured(well_definedness_error, _).

debug_format_dpllt(_, _) :-
    print_logs(false),
    !.

debug_format_dpllt(Msg, Vars) :-
    append(Msg, " (DPLL(T) Solver)~n", NCodes),
    atom_codes(NMsg, NCodes),
    format(NMsg, Vars), !.

debug_format_dpllt(_, _, _) :-
    print_logs(false),
    !.

debug_format_dpllt(Msg, Vars, Pred) :-
    format(Msg, Vars),
    translate:print_bexpr(Pred), nl, !.

dpllt_solve_predicate(Pred, SolvedPred, Result) :-
    dpllt_solve_predicate(default, Pred, SolvedPred, Result).

dpllt_solve_predicate(SolverName, Pred, SolvedPred, Result) :-
    init,
    get_preference(time_out, Timeout),
    safe_time_out(dpllt_solve_predicate_initialized(SolverName, Pred, TSolvedPred, SolverResult),
    Timeout,
    TimeoutResult),
    ( TimeoutResult == time_out
    -> Result = time_out,
    SolvedPred = Pred
    ; ground(SolverResult),
    Result = SolverResult,
    SolvedPred = TSolvedPred
).

dpllt_solve_predicate_in_state(Pred, State, SolvedPred, Result) :-
    dpllt_solve_predicate_in_state(default, Pred, State, SolvedPred, Result).

dpllt_solve_predicate_in_state(SolverName, Pred, State, SolvedPred, Result) :-
    include(ground_state_binding, State, GState),
    get_typed_ids_in_scope_of_pred(Pred, TypedIds),
    set_current_state(Pred, TypedIds, GState, NPred),
    get_equalities_from_bindings(GState, TypedIds, EqConj),
    safe_create_texpr(conjunct(EqConj,NPred), pred, [], Conj),
    dpllt_solve_predicate(SolverName, Conj, SolvedPred, Result).

dpllt_solve_predicate_initialized(SolverName, Pred, SolvedPred, Result) :-
    ( check_ast(Pred)
    -> ( check_error_occured(check_ast_typing, _)
    -> % input AST is not correctly typed
    SolvedPred = Pred,
    Result = error
    ; dpllt_solve_predicate_initialized_checked(SolverName, Pred, SolvedPred, Result)
    )
    ; add_message(dpllt_solve_predicate_no_timeout, 'Input predicate is not well-defined~nProB\'s SMT solver transforms the input to a well-defined predicate before constraint solving~n'),
    dpllt_solve_predicate_initialized_checked(SolverName, Pred, SolvedPred, Result)
).

dpllt_solve_predicate_initialized_checked(SolverName, Pred, SolvedPred, Result) :-
    call_cleanup(catch(dpllt_solve_predicate_no_timeout(SolverName, Pred, SolvedPred, Result),
    Exception, % TODO: catch specific exception instead of all
    handle_clpfd_overflow(SolverName, Exception, Pred, SolvedPred, Result)
    ),
    reset_preferences
).

dpllt_solve_predicate_no_timeout(SolverName, Pred, SolvedPred, SolverResult) :-
    debug_format_dpllt("After parsing: ", [], Pred),
    debug_format_dpllt("~nStart preprocessing", []),
    start_ms_timer(T0),
    simplify_negation(Pred, SPred),
    debug_format_dpllt("After simplifying negations: ", [], SPred),
    reset_optimizer_state,
    assert_ground_id_values(0, SPred),
    replace_ids_with_ground_values(SPred, 0, [], AstOpt),
    precompute_values(AstOpt, [instantiate_quantifier_limit(2)], AstPrecomputed),
    debug_format_dpllt("After precomputing values: ", [], AstOpt),
    stop_ms_timer_with_debug_msg(T0,precompute_values_for_dpllt),
    find_identifier_uses(AstPrecomputed, [], UsedIds),
    temporary_set_preference(data_validation_mode, true),
    b_compile(AstPrecomputed, UsedIds, [], [], AstCompiled, no_wf_available),
    clear_wd_errors, % b_compile might throw a wd error
    reset_temporary_preference(data_validation_mode),
    debug_format_dpllt("After compiling values: ", [], AstCompiled),
    start_ms_timer(T1),
    (clean_up_pred(AstCompiled, _, CleanPred) -> true
    ; add_internal_error('Clean up failed ',SolverName), CleanPred=AstCompiled),
    stop_ms_timer_with_debug_msg(T1,clean_up_pred_for_dpllt),
    start_ms_timer(T2),
    debug_format_dpllt("After AST cleanup: ", [], CleanPred),
    ( CleanPred = b(truth,pred,_)
    -> SolverResult = solution([]),
    SolvedPred = b(truth,pred,[])
    ; CleanPred = b(falsity,pred,_)
    -> SolverResult = contradiction_found,
    SolvedPred = b(falsity,pred,[])
    ; is_rewrite_to_idl(RewriteToIdl),
    ( dpllt_settings:static_smt_symmetry_breaking(true)
    -> debug_format_dpllt("Start symmetry breaking..", []),
    ( get_symmetry_breaking_predicates_decomposed(CleanPred, SymPred)
    ; add_message(smt_symmetry_breaking, 'Symmetry breaking failed on the top-level.'),
    SymPred = b(truth,pred,[])
    )
    ; SymPred = b(truth,pred,[])
    ),
    debug_format_dpllt("done.", []),
    dpllt_settings:static_syntax_analysis(PerformStaticAnalysis),
    preprocess_predicate(PerformStaticAnalysis, RewriteToIdl, CleanPred, LiftedPred, FilteredCandidateImplsConj, CandidateImpls),
    debug_format_dpllt("Lifted predicate: ", [], LiftedPred),
    predicate_to_sat(normal, LiftedPred, Env1, WDPOs1, SmtBoolFormula, SatVars1),
    preprocess_predicate(false, RewriteToIdl, SymPred, LiftedSymPred, _, _),
    predicate_to_sat(normal, WDPOs1, SatVars1, Env1, LiftedSymPred, Env2, WDPOs2, SymBoolFormula, SatVars2),
    ( PerformStaticAnalysis=true
    -> predicate_to_sat(only_reuse, WDPOs2, SatVars2, Env2, FilteredCandidateImplsConj, Env3, WDPOsList, ImplBoolFormula, SatVars3),
    debug_format_dpllt("Static analysis inferred: ", [], ImplBoolFormula)
    ; ImplBoolFormula = b(truth,pred,[]),
    SatVars3 = SatVars2, Env3 = Env2, WDPOsList = WDPOs2
    ),
    % well-definedness implication on the top-level to encode well-definedness in the SAT solver
    dpllt_sat_solver:init_dynamic_solver_state(SolverName), % TODO: check if this can be moved inside the SAT solver again
    conjunct_predicates(WDPOsList, WDPOs),
    preprocess_predicate(false, RewriteToIdl, WDPOs, _, _, WDCandidateImpls),
    % theory deduction for wd
    get_wd_theory_implications(CandidateImpls, WDCandidateImpls, WDTheoryImpls),
    predicate_to_sat(normal, WDTheoryImpls, SatVars3, Env3, WDPOs, Env4, _, WDTheoryImplsBoolFormula, SatVars4),
    debug_format_dpllt("WD Theory Deduction Implications: ", [], WDTheoryImpls),
    predicate_to_sat(normal, WDPOs, SatVars4, Env4, WDPOs, NewEnv, _, WDPosBoolFormula, SatVars),
    debug_format_dpllt("WD Implication: ", [], WDPOs),
    debug_format_dpllt("WD Implication as Boolean formula: ", [], WDPosBoolFormula),
    !,
    conjunct_predicates([SymBoolFormula,WDTheoryImplsBoolFormula,ImplBoolFormula], AnalysisBoolFormula),
    find_typed_identifier_uses(LiftedPred, SmtVars), % TO DO: improve
    debug_format_dpllt("Check LiftedPred", []),
    ( check_ast(LiftedPred)
    -> true
    ; add_internal_error('AST is missing well-definedness information for solver ', SolverName)
    ),
    dpllt_sat_solver:cnf_to_smt(SmtBoolFormula, SolvedPred),
    stop_ms_timer_with_debug_msg(T2,preprocessing_for_dpllt),
    debug_format_dpllt("End preprocessing", []),
    start_ms_timer(T3),
    enter_new_error_scope(ScopeID, dpllt_solve_predicate),
    %nl, write('smtBoolFormula: '), nl, translate:print_bexpr(SmtBoolFormula), nl,
    %nl, write('Analysis Bool formula: '), nl, translate:print_bexpr(AnalysisBoolFormula), nl,
    call_cleanup(conflict_driven_clause_learning_online(SolverName, NewEnv, SmtVars, SatVars, WDPosBoolFormula, AnalysisBoolFormula, SmtBoolFormula, SolverResult),
    exit_error_scope(ScopeID, _, dpllt_solve_predicate)),
    stop_ms_timer_with_debug_msg(T3,dpllt_solving_success)
).

dpllt_solve_predicate_no_timeout(_, Pred, _, _) :-
    add_error(dpllt_solve_predicate, 'Cannot create SAT formula from B predicate:', [Pred]).

exclude_idl_solution(IdlBindings, SmtBindings, StateTypedIds, WfStoreSmt) :-
    initial_solution,
    exclude_solution(IdlBindings, StateTypedIds, Exclusion),
    b_test_boolean_expression(Exclusion, SmtBindings, [], WfStoreSmt).

exclude_idl_solution(_, _, _, _) :-
    \+ initial_solution.

exclude_solution([], _, b(truth,pred,[])).

exclude_solution([Binding|T], StateTypedIds, Exclusion) :-
    get_equality_from_binding(Binding, StateTypedIds, EQ),
    exclude_solution(T, EQ, StateTypedIds, Exclusion).

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

exclude_solution([Binding|T], Acc, StateTypedIds, Exclusion) :-
    get_equality_from_binding(Binding, StateTypedIds, EQ),
    NAcc = b(disjunct(b(negation(EQ),pred,[]),Acc),pred,[]),
    exclude_solution(T, NAcc, StateTypedIds, Exclusion).

get_amount_of_sat_variables(Pred, AmountOfSatVars) :-
    simplify_negation(Pred, SPred),
    reset_optimizer_state,
    assert_ground_id_values(0, SPred),
    replace_ids_with_ground_values(SPred, 0, [], AstCardOpt),
    precompute_values(AstCardOpt, [instantiate_quantifier_limit(0)], AstPrecomputed),
    %writeq(AstCompiled),nl,
    (clean_up_pred(AstPrecomputed, _, CleanPred) -> true
    ; add_internal_error('Clean up failed ', dpllt), CleanPred=AstPrecomputed),
    ( CleanPred = b(truth,pred,_)
    -> AmountOfSatVars = 1
    ; CleanPred = b(falsity,pred,_)
    -> AmountOfSatVars = 1
    ; preprocess_predicate(false, false, CleanPred, LiftedPred, _, _),
    predicate_to_sat(normal, LiftedPred, _, _, _, SatVars1)
    ),
    length(SatVars1, AmountOfSatVars).

get_candidate_bounds_from_non_idl_constraints(CandidateTuples) :-
    findall((VarName,Candidates), idl_candidate_constants(VarName, Candidates), CandidateTuples).

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

get_constraints_from_fd_bounds(SmtBindings, [Var|T], Acc, ConjList) :-
    memberchk(bind(Var, int(Int)), SmtBindings),
    integer(Int),
    !,
    Equality = b(equal(b(identifier(Var),integer,[]),b(integer(Int),integer,[])),pred,[]),
    get_constraints_from_fd_bounds(SmtBindings, T, [Equality|Acc], ConjList).

get_constraints_from_fd_bounds(SmtBindings, [Var|T], Acc, ConjList) :-
    memberchk(bind(Var, int(FDVar)), SmtBindings),
    fd_var(FDVar),
    fd_min(FDVar, Min),
    fd_max(FDVar, Max),
    !,
    ( var_geq_min(Var, Min, MinBound)
    -> ( var_leq_max(Var, Max, MaxBound)
    -> NAcc = [b(conjunct(MinBound,MaxBound),pred,[])|Acc]
    ; NAcc = [MinBound|Acc]
    )
    ; ( var_leq_max(Var, Max, MaxBound)
    -> NAcc = [MaxBound|Acc]
    ; NAcc = Acc
    )
    ),
    get_constraints_from_fd_bounds(SmtBindings, T, NAcc, ConjList).

get_constraints_from_fd_bounds(SmtBindings, [_|T], Acc, ConjList) :-
    get_constraints_from_fd_bounds(SmtBindings, T, Acc, ConjList).

get_equalities_from_bindings([], _, b(truth,pred,[])).

get_equalities_from_bindings([bind(Id,Val)|T], TypedIds, EqConj) :-
    get_equality_from_binding(bind(Id,Val), TypedIds, Eq),
    get_equalities_from_bindings(T, TypedIds, Eq, EqConj).

get_equalities_from_bindings([], _, EqConj, EqConj).

get_equalities_from_bindings([bind(Id,Val)|T], TypedIds, EqAcc, EqConj) :-
    get_equality_from_binding(bind(Id,Val), TypedIds, Eq),
    get_equalities_from_bindings(T, TypedIds, b(conjunct(Eq,EqAcc),pred,[]), EqConj).

get_equality_from_binding(Binding, TypedIds, EQ) :-
    ( Binding = bind(VarName,Val)
    ; Binding = binding(VarName,Val,_)
    ),
    ( member(b(identifier(VarName),TType,_), TypedIds)
    -> Type = TType
    ; infer_value_type(Val, Type)
    ),
    ( contains_any(Type)
    -> add_error_and_fail(get_equality_from_binding, 'Cannot infer type of identifier to setup state for ', VarName)
    ; EQ = b(equal(b(identifier(VarName),Type,[]),b(value(Val),Type,[])),pred,[])
).

get_idl_solution_bindings(IdlGraphMut, Bindings) :-
    get_solver_result(IdlGraphMut, SolverResult),
    SolverResult = solution(Bindings).

get_ids_and_int_constants(b(Node,pred,_), Ids, IntConstants) :-
    comparison_op(Node, Lhs, Rhs),
    get_ids_and_int_constants_expr(Lhs, [], [], IdsAcc, IntConstantsAcc),
    get_ids_and_int_constants_expr(Rhs, IdsAcc, IntConstantsAcc, Ids, IntConstants).

get_ids_and_int_constants_expr(Id, IdsAcc, IntConstantsAcc, [Name|IdsAcc], IntConstantsAcc) :-
    Id = b(identifier(Name),integer,_).

get_ids_and_int_constants_expr(Int, IdsAcc, IntConstantsAcc, IdsAcc, [Value,Value1|IntConstantsAcc]) :-
    ( Int = b(integer(Value),integer,_)
    ; Int = b(unary_minus(b(integer(Value),integer,_)),integer,_)
    ),
    % select positive and negative value
    Value1 is Value * -1.

get_ids_and_int_constants_expr(b(Node,integer,_), IdsAcc, IntConstantsAcc, Ids, IntConstants) :-
    arithmetic_expr(Node, Lhs, Rhs),
    get_ids_and_int_constants_expr(Lhs, IdsAcc, IntConstantsAcc, NIdsAcc, NIntConstantsAcc),
    get_ids_and_int_constants_expr(Rhs, NIdsAcc, NIntConstantsAcc, Ids, IntConstants).

get_typed_ids_in_scope_of_pred(Pred, TypedIds) :-
    find_typed_identifier_uses(Pred, PTypedIds),
    add_typed_ids_in_scope(PTypedIds, TypedIds).

ground_state_binding(Binding) :-
    Binding = bind(_,_),
    ground(Binding).

handle_clpfd_overflow(SolverName, Exception, Pred, SolvedPred, Result) :-
    Exception = error(representation_error(Err),_),
    memberchk(Err, ['CLPFD integer overflow','max_clpfd_integer','min_clpfd_integer']),
    !,
    temporary_set_preference(use_clpfd_solver, false),
    dpllt_solve_predicate_initialized(SolverName, Pred, SolvedPred, Result).

handle_clpfd_overflow(_, Exception, _, _, unknown) :-
    add_error(dpllt,'Exception occurred during solving:',Exception).

idl_solver_interface(IdlGraphMut, SatPrologVar, [DLConstraint]) :-
    SatPrologVar == pred_true,
    difference_logic_solver:remove_unsat_core,
    dpllt_sat_solver:remove_idl_unsat_core,
    ( difference_logic_solver:register_constraint(IdlGraphMut, DLConstraint)
    ; \+ dpllt_sat_solver:is_backjumping,
    propagate_idl_unsat_core_to_sat_solver(IdlGraphMut),
    fail
).

idl_solver_interface(IdlGraphMut, SatPrologVar, [DLConstraint]) :-
    SatPrologVar == pred_false,
    difference_logic_solver:remove_unsat_core,
    dpllt_sat_solver:remove_idl_unsat_core,
    ( difference_logic_solver:register_constraint(IdlGraphMut, b(negation(DLConstraint),pred,[]))
    ; \+ dpllt_sat_solver:is_backjumping,
    propagate_idl_unsat_core_to_sat_solver(IdlGraphMut),
    fail
).

init :-
    %retract(debug:debug_mode(_)),
    %asserta(debug:debug_mode(on)),
    % enumeration has to be linear for symmetry breaking but also set to false by default
    temporary_set_preference(randomise_enumeration_order, false),
    dpllt_pred_to_sat:reset_sat_var_id,
    retractall(initial_solution),
    retractall(idl_candidate_constants(_,_)),
    %temporary_set_preference(use_chr_solver, true),
    temporary_set_preference(unsat_core_algorithm, divide_and_conquer), % default is linear_greedy
    temporary_set_preference(use_smt_mode, false),
    temporary_set_preference(use_clpfd_solver, true),
    temporary_set_preference(optimize_ast, true),
    temporary_set_preference(use_common_subexpression_elimination, false),
    temporary_set_preference(normalize_ast_sort_commutative, false),
    temporary_set_preference(normalize_ast, false).

is_rewrite_to_idl(Res) :-
    get_preference(dpllt_use_idl_theory_solver,true),
    !,
    Res = true.

is_rewrite_to_idl(false).

log_idl_candidates_from_constraint(Constraint) :-
    get_ids_and_int_constants(Constraint, Ids, IntConstants),
    Ids \== [],
    IntConstants \== [],
    !,
    assert_idl_candidates(Ids, IntConstants).

log_idl_candidates_from_constraint(_).

log_solution :-
    \+ initial_solution,
    !,
    asserta(initial_solution).

log_solution.

log_theory_propagation(SatStateMutable, SatVarName, SatPrologVar) :-
    ground(SatPrologVar),
    ( is_last_propagated_sat_var(SatStateMutable, SatVarName)
    -> true
    ; dpllt_sat_solver:log_theory_propagation_sat_stack(SatStateMutable, SatVarName, SatPrologVar)
).

propagate_fd_bounds_to_idl_solver(IdlGraphMut, SmtBindings) :-
    get_preference(dpllt_use_idl_theory_solver,true),
    !,
    difference_logic_solver:get_registered_vars(IdlGraphMut, Vars),
    get_constraints_from_fd_bounds(SmtBindings, Vars, [], ConjList),
    difference_logic_solver:register_constraints(IdlGraphMut, ConjList).

propagate_fd_bounds_to_idl_solver(_, _).

propagate_idl_solution_to_bindings_bt(IdlGraphMut, SmtBindings) :-
    get_preference(dpllt_use_idl_theory_solver,true),
    !,
    % TO DO: try the current solution first
    ( get_candidate_bounds_from_non_idl_constraints(CandidateTuples),
    difference_logic_solver:try_candidate_bounds(IdlGraphMut, CandidateTuples, Result)
    ; difference_logic_solver:get_all_solutions_on_bt(IdlGraphMut, Result)
    ),
    Result = solution(Bindings),
    set_bindings(Bindings, SmtBindings).

propagate_idl_solution_to_bindings_bt(_, _).

propagate_idl_unsat_core_to_sat_solver(IdlGraphMut) :-
    difference_logic_solver:get_solver_result(IdlGraphMut, Res),
    Res == contradiction_found,
    difference_logic_solver:get_unsat_core(IdlCore),
    difference_logic_solver:remove_unsat_core,
    dpllt_sat_solver:store_idl_unsat_core(IdlCore).

propagate_non_idl_to_idl(IdlGraphMut, SatPrologVar, SmtFormula) :-
    ( SatPrologVar == pred_true % TO DO: pred_false?
    % e.g., x:NAT -> x>=0
    -> ( infer_constraints_for_idl_solver(SmtFormula, ConjList)
    -> register_constraints(IdlGraphMut, ConjList)
    ; true
    )
    ; true
).

reset_preferences :-
    reset_temporary_preference(randomise_enumeration_order),
    reset_temporary_preference(unsat_core_algorithm),
    reset_temporary_preference(use_smt_mode),
    reset_temporary_preference(use_clpfd_solver),
    reset_temporary_preference(optimize_ast),
    reset_temporary_preference(use_common_subexpression_elimination),
    reset_temporary_preference(normalize_ast_sort_commutative),
    reset_temporary_preference(normalize_ast).

sat_debug_msg(SatVarName,SmtFormula,SatPrologVar) :-
    (debug_mode(off) -> true
    ; format('% SAT variable ~w (~w) for ProB pred: ',[SatVarName,SatPrologVar]),
    print_bexpr(SmtFormula),nl).

set_bindings([], _).

set_bindings([binding(VarName,Val,_)|T], SmtBindings) :-
    member(bind(VarName,Val), SmtBindings),
    set_bindings(T, SmtBindings).

set_current_state(Pred, TypedIds, State, NPred) :-
    reset_optimizer_state,
    assert_state_id_values(TypedIds, State),
    replace_ids_with_ground_values(Pred, 0, [], NPred),
    reset_optimizer_state, !.

setup_reification(_, _, [], _, _).

setup_reification(SatStateMutable, IdlGraphMut, [(SatId,SatPrologVar)|T], SmtBindings, WfStoreSmt) :-
    get_texpr_info(SatId, Info),
    memberchk(smt_formula(SmtFormula), Info),
    !,
    SatId = b(identifier(SatVarName),_,_),
    setup_reification_for_solver(SatStateMutable, IdlGraphMut, SmtFormula, SmtBindings, WfStoreSmt, SatVarName, SatPrologVar),
    %sat_smt_reification(SatId, SatPrologVar, SmtBindings, WfStoreSmt)
    setup_reification(SatStateMutable, IdlGraphMut, T, SmtBindings, WfStoreSmt).

setup_reification(SatStateMutable, IdlGraphMut, [_|T], SmtBindings, WfStoreSmt) :-
    % plain SAT variable which is not reified with a theory solver, e.g., introduced by CNF optimization rewriting
    setup_reification(SatStateMutable, IdlGraphMut, T, SmtBindings, WfStoreSmt).

setup_reification_for_solver(SatStateMutable, IdlGraphMut, SmtFormula, SmtBindings, WfStoreSmt, SatVarName, SatPrologVar) :-
    log_theory_propagation(SatStateMutable, SatVarName, SatPrologVar),
    ( get_preference(dpllt_use_idl_theory_solver,true)
    % TO DO: Problem beide Solver aufzusetzen: was ist wenn idl solver lösung findet aber prob timeout?
    -> ( ast_to_difference_logic:rewrite_to_idl(SmtFormula, [DLConstraint])
    -> debug_format_dpllt("Constraint for IDL: ", [], SmtFormula),
    idl_solver_interface(IdlGraphMut, SatPrologVar, [DLConstraint])
    ; log_idl_candidates_from_constraint(SmtFormula),
    propagate_non_idl_to_idl(IdlGraphMut, SatPrologVar, SmtFormula)
    ),
    sat_debug_msg(SatVarName,SmtFormula,SatPrologVar),
    b_convert_bool(SmtFormula, SmtBindings, [], WfStoreSmt, SatPrologVar)
    ; sat_debug_msg(SatVarName,SmtFormula,SatPrologVar),
    b_convert_bool(SmtFormula, SmtBindings, [], WfStoreSmt, SatPrologVar)
).

setup_theory_wf_store(SmtVars, SmtBindings, WFStoreSMT) :-
    set_up_typed_localstate(SmtVars, _, SmtTypedVals, [], SmtBindings, positive),
    init_wait_flags(WFStoreSMT, [wf_smt_cdcl]),
    b_tighter_enumerate_all_values(SmtTypedVals, WFStoreSMT),!.

var_geq_min(Var, Min, MinBound) :-
    % -v <= -min
    integer(Min),
    Min1 is Min * -1,
    MinBound = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),b(identifier(Var),integer,[])),integer,[]),b(integer(Min1),integer,[])),pred,[]).

var_leq_max(Var, Max, MaxBound) :-
    % v <= Max
    integer(Max),
    MaxBound = b(less_equal(b(identifier(Var),integer,[]),b(integer(Max),integer,[])),pred,[]).