cdclt_solver

add_symmetry_breaking_predicates_cond(Pred, SymPred) :-
    cdclt_settings:static_smt_symmetry_breaking(true),
    !,
    debug_format_cdclt("Start symmetry breaking..", []),
    ( add_symmetry_breaking_predicates(Pred, SymPred),
    get_amount_of_found_sbps(FoundSBPs),
    log_symmetry_breaking_stats(FoundSBPs),
    debug_format_cdclt("done.", [])
    -> true
    ; add_message(smt_symmetry_breaking, 'Symmetry breaking failed for: ',Pred),
    SymPred = Pred
).

add_symmetry_breaking_predicates_cond(Pred, Pred).

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

analyze_binary_clauses(Clauses, VarsFromBinaryClauses) :-
    analyze_binary_clauses(Clauses, 0, 0, [], VarsFromBinaryClauses).

analyze_binary_clauses([], Len, Binary, Acc, Acc) :-
    debug_format_cdclt("Found ~w clauses ~w of which are binary clauses~n", [Len,Binary]).

analyze_binary_clauses([[_-_-_-N1,_-_-_-N2]|T], Len, Binary, Acc, VarsFromBinaryClauses) :-
    !,
    add_element(N1, Acc, NAcc1),
    add_element(N2, NAcc1, NAcc),
    Len1 is Len + 1,
    Binary1 is Binary + 1,
    analyze_binary_clauses(T, Len1, Binary1, NAcc, VarsFromBinaryClauses).

analyze_binary_clauses([_|T], Len, Binary, Acc, VarsFromBinaryClauses) :-
    Len1 is Len + 1,
    analyze_binary_clauses(T, Len1, Binary, Acc, VarsFromBinaryClauses).

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).

cdcl_sat_solve_predicate(BoolFormula, Result) :-
    init,
    get_preference(time_out, Timeout),
    safe_time_out(cdcl_sat_solve_predicate_no_timeout(BoolFormula, TResult),
    Timeout,
    TimeoutResult),
    ( TimeoutResult == time_out
    -> Result = time_out
    ; Result = TResult
).

cdcl_sat_solve_predicate_in_state(BoolFormula, State, Result) :-
    include(ground_state_binding, State, GState),
    get_typed_ids_in_scope_of_pred(BoolFormula, TypedIds),
    set_current_state(BoolFormula, TypedIds, GState, NPred),
    get_equalities_from_bindings(GState, TypedIds, EqConj),
    safe_create_texpr(conjunct(EqConj,NPred), pred, [], Conj),
    cdcl_sat_solve_predicate(Conj, Result).

cdcl_sat_solve_predicate_no_timeout(BoolFormula, Result) :-
    find_typed_identifier_uses(BoolFormula, [], SatVars),
    % rewriting similar to Tseitin
    optimize_clause_size_by_rewriting(BoolFormula, SatVars, TOptBoolFormula, NewSatVars, NewVarConjList),
    conjunct_predicates(NewVarConjList, NewVarConj),
    % add new top-level Boolean variables introduced by Tseitin rewriting
    conjunct_predicates([NewVarConj,TOptBoolFormula], FullBoolFormula),
    get_bindings_from_ids(NewSatVars, StackBindings, SatBindings, SatVarNames, _IdPrologVarTuples, PrologSatVarTriple),
    b_to_cnf_safe(FullBoolFormula, StackBindings, CnfBoolFormula),
    analyze_binary_clauses(CnfBoolFormula, VarsFromBinaryClauses),
    cdclt_sat_solver:create_solver_state(SatStateMutable),
    SolverEnv = [sat_vars:NewSatVars,sat_varnames:SatVarNames,sat_bindings:SatBindings,t2b_env:_,pl_vars:PrologSatVarTriple,binary_clause_vars:VarsFromBinaryClauses],
    ( ( cdclt_sat_solver:unit_propagate_cnf(SolverEnv, SatStateMutable, CnfBoolFormula, TCnfBoolFormula2),
    remove_subsumed_clauses(TCnfBoolFormula2, TCnfBoolFormula3),
    sort(TCnfBoolFormula3, CnfBoolFormula2),
    cdclt_sat_solver:sat(default_sat, SolverEnv, SatStateMutable, CnfBoolFormula2)
    )
    -> Result = solution(SatBindings)
    ; Result = contradiction_found
    ),
    print_stats.

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

cdclt_solve_predicate(SolverName, Pred, SolvedPred, Result) :-
    init,
    cdclt_solve_predicate_timeout(SolverName, Pred, SolvedPred, Result).

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

cdclt_solve_predicate_in_state(SolverName, Pred, State, SolvedPred, Result) :-
    init,
    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),
    asserta(solve_in_state),
    cdclt_solve_predicate_timeout(SolverName, Conj, SolvedPred, Result).

cdclt_solve_predicate_initialized(SolverName, Pred, SolvedPred, Result) :-
    ( check_ast(Pred)
    -> ( (error_occurred_in_error_scope, check_error_occured(check_ast_typing, _))
    -> % input AST is not correctly typed
    SolvedPred = Pred,
    Result = error
    ; cdclt_solve_predicate_initialized_checked(SolverName, Pred, SolvedPred, Result)
    )
    ; add_message(cdclt_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~nFor: ',SolverName),
    cdclt_solve_predicate_initialized_checked(SolverName, Pred, SolvedPred, Result)
).

cdclt_solve_predicate_initialized_checked(SolverName, Pred, SolvedPred, Result) :-
    call_cleanup(catch(cdclt_solve_predicate_no_timeout(SolverName, Pred, SolvedPred, Result),
    Exception, % TO DO: catch specific exception instead of all
    handle_clpfd_overflow(SolverName, Exception, Pred, SolvedPred, Result)
    ),
    reset_preferences
).

cdclt_solve_predicate_no_timeout(SolverName, Pred, SolvedPred, SolverResult) :-
    debug_format_cdclt("Parsed predicate: ", [], Pred),
    debug_format_cdclt("Start preprocessing", []),
    cdclt_solve_predicate_no_timeout_cleanup(SolverName, Pred, NPred),
    debug_format_cdclt("After preprocessing: ", [], NPred),
    cdclt_solve_predicate_no_timeout_clean(SolverName, NPred, SolvedPred, SolverResult).

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

cdclt_solve_predicate_no_timeout_clean(_, b(falsity,pred,Info), SolvedPred, SolverResult) :-
    !,
    SolvedPred = b(falsity,pred,Info),
    SolverResult = contradiction_found.

cdclt_solve_predicate_no_timeout_clean(SolverName, CleanPred, SolvedPred, SolverResult) :-
    cdclt_solve_predicate_no_timeout_setup(SolverName, CleanPred, Env, SmtVars, SatVars, WDPosBoolFormula, AnalysisBoolFormula, SmtBoolFormula),
    cdclt_sat_solver:cnf_to_smt(SmtBoolFormula, SolvedPred),
    start_ms_timer(Timer),
    enter_new_error_scope(ScopeID, cdclt_solve_predicate),
    call_cleanup(conflict_driven_clause_learning_online(SolverName, Env, SmtVars, SatVars, WDPosBoolFormula, AnalysisBoolFormula, SmtBoolFormula, SolverResult),
    exit_error_scope(ScopeID, _, cdclt_solve_predicate)),
    stop_ms_timer_with_debug_msg(Timer, cdclt_solving_success),
    print_stats.

cdclt_solve_predicate_no_timeout_cleanup(SolverName, Pred, NPred) :-
    start_ms_timer(Timer0),
    simplify_negation(Pred, SPred),
    debug_format_cdclt("After simplifying negations: ", [], SPred),
    reset_optimizer_state,
    assert_ground_id_values(0, SPred),
    replace_ids_with_ground_values(SPred, 0, [], AstOpt),
    precompute_values_non_recursive([instantiate_quantifier_limit(0),instantiate_sets_limit(1000)], AstOpt, AstPrecomputed),
    debug_format_cdclt("After precomputing values: ", [], AstOpt),
    stop_ms_timer_with_debug_msg(Timer0, precompute_values_for_cdclt),
    find_identifier_uses(AstPrecomputed, [], UsedIds),
    temporary_set_preference(data_validation_mode, true),
    catch(b_compile(AstPrecomputed, UsedIds, [], [], AstCompiled, no_wf_available),
    enumeration_warning(_,_,_,_,_), % cancel if enumeration warning has occurred
    AstCompiled = AstPrecomputed),
    clear_wd_errors, % b_compile might throw a wd error
    reset_temporary_preference(data_validation_mode),
    debug_format_cdclt("After compiling values (used ids ~w): ", [UsedIds], AstCompiled),
    start_ms_timer(Timer2),
    ( clean_up_pred(AstCompiled, _, NPred)
    -> true
    ; add_internal_error('Clean up failed ',SolverName),
    NPred = AstCompiled
    ),
    stop_ms_timer_with_debug_msg(Timer2, clean_up_pred_for_cdclt).

cdclt_solve_predicate_no_timeout_setup(SolverName, CleanPred, Env, SmtVars, SatVars, WDPosBoolFormula, AnalysisBoolFormula, SmtBoolFormula) :-
    start_ms_timer(Timer),
    cdclt_settings:static_syntax_analysis(PerformStaticAnalysis),
    is_rewrite_to_idl(RewriteToIdl),
    add_symmetry_breaking_predicates_cond(CleanPred, CleanPredSym),
    preprocess_predicate(PerformStaticAnalysis, RewriteToIdl, CleanPredSym, LiftedPred, InferredImplsConj, CandidateImpls),
    log_inferred_implications(InferredImplsConj),
    debug_format_cdclt("Lifted predicate: ", [], LiftedPred),
    predicate_to_sat(normal_make_wd, LiftedPred, Env1, WDPOs1, SmtBoolFormula, SatVars1), !,
    ( PerformStaticAnalysis == true
    -> predicate_to_sat(only_reuse, WDPOs1, SatVars1, Env1, InferredImplsConj, Env3, WDPOsList, ImplBoolFormula, SatVars3),
    debug_format_cdclt("Static analysis inferred: ", [], ImplBoolFormula)
    ; ImplBoolFormula = b(truth,pred,[]),
    SatVars3 = SatVars1, Env3 = Env1, WDPOsList = WDPOs1
    ),
    % well-definedness implication on the top-level to encode well-definedness in the SAT solver
    conjunct_predicates(WDPOsList, WDPOs),
    preprocess_predicate(false, RewriteToIdl, WDPOs, LiftedWDPOs, _, WDCandidateImpls),
    % theory deduction for wd
    get_wd_theory_implications(CandidateImpls, WDCandidateImpls, WDTheoryImpls),
    log_inferred_wd_theory_implications(InferredImplsConj),
    predicate_to_sat(normal_make_wd, [], SatVars3, Env3, WDTheoryImpls, Env4, _, WDTheoryImplsBoolFormula, SatVars4),
    debug_format_cdclt("WD Theory Deduction Implications: ", [], WDTheoryImpls),
    predicate_to_sat(normal_make_wd, [], SatVars4, Env4, LiftedWDPOs, Env5, WDPOsList2, WDPosBoolFormula1, SatVars5),
    % there can be WD POs that also have WD POs
    conjunct_predicates(WDPOsList2, WDPOs2),
    preprocess_predicate(false, RewriteToIdl, WDPOs2, LiftedWDPOs2, _, _),
    predicate_to_sat(normal_make_wd, [], SatVars5, Env5, LiftedWDPOs2, Env, _, WDPosBoolFormula2, SatVars),
    conjunct_predicates([WDPosBoolFormula1,WDPosBoolFormula2], WDPosBoolFormula),
    ( SatVars3 \== SatVars
    -> %set_silent_mode(on),
    %analyse_wd_for_expr(CleanPred, _ResStr, _IsWd), % prints missing WD conditions
    %set_silent_mode(off),
    add_message(cdclt_solve_predicate_no_timeout_setup, 'Input not well-defined: automatically added WD POs for solver ',SolverName)
    ; true
    ),
    debug_format_cdclt("WD Implication: ", [], LiftedWDPOs),
    debug_format_cdclt("WD Implication as Boolean formula: ", [], WDPosBoolFormula),
    !,
    conjunct_predicates([WDTheoryImplsBoolFormula,ImplBoolFormula], AnalysisBoolFormula),
    find_typed_identifier_uses(LiftedPred, SmtVars), % no global sets or constants are considered here
    debug_format_cdclt("Check LiftedPred", []),
    ( check_ast(LiftedPred)
    -> true
    ; add_internal_error('AST is missing well-definedness information for solver ', SolverName)
    ),
    %translate:nested_print_bexpr(LiftedPred),nl,
    stop_ms_timer_with_debug_msg(Timer, preprocessing_for_cdclt),
    debug_format_cdclt("End preprocessing", []),
    !.

cdclt_solve_predicate_no_timeout_setup(_, Pred, _, _, _, _, _, _) :-
    add_error_and_fail(cdclt_solve_predicate, 'Cannot create SAT formula from B predicate:', [Pred]).

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

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) :-
    % rewriting similar to Tseitin
    optimize_clause_size_by_rewriting(BoolFormula, SatVars, TOptBoolFormula, NewSatVars, NewVarConjList),
    conjunct_predicates(NewVarConjList, NewVarConj),
    conjunct_predicates([AnalysisBoolFormula,TOptBoolFormula], TFullBoolFormula),
    % add new top-level Boolean variables introduced by Tseitin rewriting
    ( NewVarConj = b(truth,pred,_)
    -> FullBoolFormula = TFullBoolFormula
    ; safe_create_texpr(conjunct(NewVarConj,TFullBoolFormula), pred, [], FullBoolFormula)
    ),
    get_bindings_from_ids(NewSatVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PlVars),
    b_to_cnf_safe(FullBoolFormula, StackBindings, CnfBoolFormula),
    setup_theory_wf_store(SmtVars, SmtBindings, WfStoreSmt),
    ( get_preference(cdclt_use_idl_theory_solver,true)
    -> difference_logic_solver:init_idl_solver(IdlGraphMut)
    ; true
    ),
    ( WDPosBoolFormula \= b(truth,pred,_)
    -> % add WD PO implications
    b_to_cnf_safe(WDPosBoolFormula, StackBindings, CnfWDPosBoolFormula),
    append(CnfWDPosBoolFormula, CnfBoolFormula, TNCnfBoolFormula)
    ; TNCnfBoolFormula = CnfBoolFormula
    ),
    cdclt_sat_solver:create_solver_state(SatStateMutable),
    SolverEnv = [sat_vars:NewSatVars,sat_varnames:SatVarNames,sat_bindings:SatBindings,t2b_env:Env,pl_vars:PlVars],
    log_unique_predicates(SatVarNames),
    cdclt_sat_solver:unit_propagate_cnf(SolverEnv, SatStateMutable, TNCnfBoolFormula, TNCnfBoolFormula2),
    remove_subsumed_clauses(TNCnfBoolFormula2, TNCnfBoolFormula3),
    sort(TNCnfBoolFormula3, NCnfBoolFormula),
    ( debug_mode(off)
    -> true
    ; cdclt_sat_solver:portray_cnf(NCnfBoolFormula)
    ),
    analyze_binary_clauses(CnfBoolFormula, VarsFromBinaryClauses),
    NSolverEnv = [sat_vars:NewSatVars,sat_varnames:SatVarNames,sat_bindings:SatBindings,t2b_env:Env,pl_vars:PlVars,binary_clause_vars:VarsFromBinaryClauses],
    setup_reification(SatStateMutable, IdlGraphMut, IdPrologVarTuples, SmtBindings, WfStoreSmt),
    cdclt_sat_solver:sat(SolverName, NSolverEnv, SatStateMutable, NCnfBoolFormula, [allow_partial_model]),
    retractall(unfixed_deferred_set_error_after_grounding),
    cdclt_sat_solver:clear_pending_theory_propagations,
    ( severe_error_occurred
    -> % error occurred during SAT solving
    !,
    SolverResult = error
    ; debug_format_cdclt("Ground waitflags", []),
    remove_pending_theory_propagations_on_bt,
    ( conflict_driven_clause_learning_online_grounding(IdlGraphMut, SmtVars, PlVars, SmtBindings, WfStoreSmt, SolverResult)
    -> true
    ; ( unfixed_deferred_set_has_been_propagated
    -> % a contradiction has been found but at least one unfixed deferred set has been propagated
    % we thus do not know if it's a genuine contradiction
    asserta(unfixed_deferred_set_error_after_grounding),
    fail
    ; % this is a genuine contradiction after grounding
    fail
)
)
).

conflict_driven_clause_learning_online(_, _, _, _, _, _, _, Res) :-
    \+ wd_error_occurred_in_error_scope(_),
    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) :-
    severe_error_occurred,
    !,
    Res = error.

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

conflict_driven_clause_learning_online(_, _, _, _, _, _, _, Res) :-
    ( grounding_timeout_occurred
    ; cdclt_sat_solver:assignment_timeout_occurred
    ),
    !,
    Res = no_solution_found(solver_answered_unknown).

conflict_driven_clause_learning_online(_, _, _, _, _, _, _, no_solution_found(unfixed_deferred_sets)) :-
    \+ solve_in_state,
    ( cdclt_sat_solver:unfixed_deferred_set_error_occurred
    ; unfixed_deferred_set_error_after_grounding
    ; unfixed_deferred_set_has_been_propagated
).

conflict_driven_clause_learning_online(_, _, _, _, _, _, _, contradiction_found) :-
    \+ initial_solution,
    ( solve_in_state
    -> true
    ; \+ unfixed_deferred_set_error_after_grounding,
    \+ cdclt_sat_solver:unfixed_deferred_set_error_occurred,
    \+ unfixed_deferred_set_has_been_propagated
    ),
    \+ wd_error_occurred_in_error_scope(_).

conflict_driven_clause_learning_online_grounding(IdlGraphMut, SmtVars, _, SmtBindings, WfStoreSmt, SolverResult) :-
    get_preference(cdclt_use_idl_theory_solver, true),
    !,
    add_typed_ids_in_scope(SmtVars, StateTypedIds),
    propagate_fd_bounds_to_idl_solver(IdlGraphMut, SmtBindings),
    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)
    )
    ),
    finalize_smt_solution(SmtBindings, SolverResult).

conflict_driven_clause_learning_online_grounding(_, _, PlVars, SmtBindings, WfStoreSmt, SolverResult) :-
    grounding_fallback_z3,
    \+ host_platform(windows),
    !,
    ( grounding_timeout_occurred
    -> % use a smaller time limit if a timeout already occurred
    GroundTimeout = 5000
    ; GroundTimeout = 30000
    ),
    safe_time_out(ground_wait_flags(WfStoreSmt),
    GroundTimeout,
    TimeOutRes),
    ( TimeOutRes == time_out
    -> debug_format_cdclt("Timeout when grounding with ProB. Fallback to Z3.", []),
    sat_bindings_to_smt_formula(PlVars, SmtFormula),
    safe_time_out(smt_solve_predicate(z3, [check_sat_skeleton(0)], SmtFormula, _, Result),
    10000,
    TimeOutResZ3),
    ( ( TimeOutResZ3 == time_out
    ; Result = no_solution_found(_)
    )
    -> asserta(grounding_timeout_occurred),
    fail
    ; Result = solution(NSmtBindings),
    debug_format_cdclt("Validating Z3 solution with ProB.", []),
    copy_smt_solution(SmtBindings,NSmtBindings),
    ground_wait_flags(WfStoreSmt) % also avoid Call Residue warnings
    )
    ; NSmtBindings = SmtBindings
    ),
    \+ severe_error_occurred,
    finalize_smt_solution(NSmtBindings, SolverResult).

conflict_driven_clause_learning_online_grounding(_, _, _, SmtBindings, WfStoreSmt, SolverResult) :-
    ground_wait_flags(WfStoreSmt),
    \+ severe_error_occurred,
    finalize_smt_solution(SmtBindings, SolverResult).

copy_smt_solution([],_).

copy_smt_solution([bind(ID,Val)|T],NSmtBindings) :- member(binding(ID,Z3Val,_),NSmtBindings),!,
    equal_object(Val,Z3Val,copy_smt_solution),
    copy_smt_solution(T,NSmtBindings).

copy_smt_solution([H|T],NSmtBindings) :- add_internal_error('No SMT solution for:',H),
    copy_smt_solution(T,NSmtBindings).

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

debug_format_cdclt(Msg, Vars) :-
    append(Msg, " (CDCL(T) Solver)~n", NCodes),
    format(NCodes, Vars), !.

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

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

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),
    safe_create_texpr(negation(EQ), pred, [], Neg),
    safe_create_texpr(disjunct(Neg,Acc), pred, [], NAcc),
    exclude_solution(T, NAcc, StateTypedIds, Exclusion).

finalize_smt_solution(SmtBindings, SolverResult) :-
    SolverResult = solution(SmtBindings),
    log_solution,
    announce_bt_from_smt_solution.

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),
    (clean_up_pred(AstPrecomputed, _, CleanPred) -> true
    ; add_internal_error('Clean up failed ', cdclt), CleanPred=AstPrecomputed),
    ( CleanPred = b(truth,pred,_)
    -> AmountOfSatVars = 1
    ; CleanPred = b(falsity,pred,_)
    -> AmountOfSatVars = 1
    ; preprocess_predicate(false, false, CleanPred, LiftedPred, _, _),
    predicate_to_sat(normal_make_wd, 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),
    !,
    Zero = b(identifier('_zero'),integer,[]),
    % Var = Int but represented as Var - _zero <= Int & _zero - Var <= -Int
    Conj1 = b(less_equal(b(minus(b(identifier(Var),integer,[]),Zero),integer,[]),b(integer(Int),integer,[])),pred,[]),
    Conj2 = b(less_equal(b(minus(Zero,b(identifier(Var),integer,[])),integer,[]),b(unary_minus(b(integer(Int),integer,[])),integer,[])),pred,[]),
    get_constraints_from_fd_bounds(SmtBindings, T, [Conj1,Conj2|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 = [MinBound,MaxBound|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),
    safe_create_texpr(conjunct(Eq,EqAcc), pred, [], Conj),
    get_equalities_from_bindings(T, TypedIds, Conj, 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).

grounding_fallback_z3.

handle_clpfd_overflow(SolverName, Exception, Pred, SolvedPred, Result) :-
    Exception = error(representation_error(Err),_),
    memberchk(Err, ['CLPFD integer overflow','max_clpfd_integer','min_clpfd_integer']),
    !,
    debug_format_cdclt("Handle CLP(FD) overflow error and restart CDCL(T) without CLP(FD).", []),
    temporary_set_preference(use_clpfd_solver, false),
    cdclt_solve_predicate_initialized(SolverName, Pred, SolvedPred, Result).

handle_clpfd_overflow(SolverName, Exception, Pred, SolvedPred, unknown) :-
    ajoin(['Exception occured during solving with ',SolverName,':'],Msg),
    add_error(cdclt,Msg,Exception),
    SolvedPred = Pred.

idl_solver_interface(IdlGraphMut, SatPrologVar, [DLConstraint]) :-
    SatPrologVar == pred_true,
    difference_logic_solver:remove_unsat_core,
    cdclt_sat_solver:remove_idl_unsat_core,
    ( difference_logic_solver:register_constraint(IdlGraphMut, DLConstraint)
    ; \+ cdclt_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,
    cdclt_sat_solver:remove_idl_unsat_core,
    ( difference_logic_solver:register_constraint(IdlGraphMut, b(negation(DLConstraint),pred,[]))
    ; \+ cdclt_sat_solver:is_backjumping,
    propagate_idl_unsat_core_to_sat_solver(IdlGraphMut),
    fail
).

init :-
    % enumeration has to be linear for symmetry breaking but also set to false by default
    temporary_set_preference(randomise_enumeration_order, false),
    cdclt_pred_to_sat:reset_sat_var_id,
    cdclt_preprocessing:reset_artificial_id_counter,
    reset_stats,
    ( additional_z3_reification
    -> smt_solvers_interface:reset_smt_supported_interpreter
    ; true
    ),
    welldef:filter_typing_pos(true),
    welldef:preprocess_pos_for_cdclt(true),
    retractall(initial_solution),
    retractall(grounding_timeout_occurred),
    retractall(unfixed_deferred_set_error_after_grounding),
    retractall(unfixed_deferred_set_has_been_propagated),
    retractall(solve_in_state),
    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(allow_improving_wd_mode, true),
    %temporary_set_preference(solver_strength, 20000),
    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(add_wd_pos_for_z3, false),
    temporary_set_preference(normalize_ast_sort_commutative, false),
    temporary_set_preference(normalize_ast, false).

is_rewrite_to_idl(Res) :-
    get_preference(cdclt_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_and_unfixed_deferred_sets(SatStateMutable, SatVarName, StackInfo, ContainsUnfixed, DetUnfixedProp, SatPrologVar) :-
    ground(SatPrologVar),
    ( ContainsUnfixed
    -> % log unfixed deferred set propagation but undo when backtracking if not deterministic unit propagation
    asserta(unfixed_deferred_set_has_been_propagated),
    ( DetUnfixedProp
    -> true
    ; (true; (retract(unfixed_deferred_set_has_been_propagated), !, fail))
    )
    ; true
    ),
    StackInfo = (PropType,_,_,_),
    ( ( PropType == unit; PropType == branch) % has been propagated by the SAT solver
    -> true
    ; cdclt_sat_solver:log_theory_propagation_sat_stack(SatStateMutable, SatVarName, SatPrologVar, StackInfo)
).

propagate_fd_bounds_to_idl_solver(IdlGraphMut, SmtBindings) :-
    get_preference(cdclt_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(cdclt_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,
    cdclt_sat_solver:store_idl_unsat_core(IdlCore), !.

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

remove_pending_theory_propagations_on_bt :-
    ( true
    ; cdclt_sat_solver:clear_pending_theory_propagations,
    debug_format_cdclt("backtrack after grounding waitflags", []),
    fail
).