dpllt_sat_solver

add_heuristic_tuples(_, []).

add_heuristic_tuples(StateMutable, [(SatVarName,Score)|T]) :-
    add_state_instance(StateMutable, heuristic_avl, (SatVarName,Score)),
    add_heuristic_tuples(StateMutable, T).

add_state_instance(StateMutable, Key, Datum) :-
    get_mutable(solver_state(SolverState), StateMutable),
    memberchk(Key:Data, SolverState),
    ( Key == heuristic_avl
    -> Datum = (SatVarName,Score),
    Value = Score
    ; Key == sat_stack,
    Datum = (SatVarName,A,B,C,D),
    Value = (A,B,C,D)
    ), !,
    mutdict_put(Data, SatVarName, Value).

add_used_vars_to_mutdict([], _).

add_used_vars_to_mutdict([_-_-SatVarName|T], VarNamesDict) :-
    \+ mutdict_get(VarNamesDict, SatVarName, _),
    !,
    mutdict_put(VarNamesDict, SatVarName, SatVarName),
    add_used_vars_to_mutdict(T, VarNamesDict).

add_used_vars_to_mutdict([_|T], VarNamesDict) :-
    add_used_vars_to_mutdict(T, VarNamesDict).

announce_bt_from_smt_solution :-
    asserta(bt_from_smt_solution).

assert_count_occurrences([]).

assert_count_occurrences([Clause|T]) :-
    assert_count_occurrences_from_clause(Clause),
    assert_count_occurrences(T).

assert_count_occurrences_from_clause([]).

assert_count_occurrences_from_clause([_-_-SatVarName|T]) :-
    ( retract(occurrences(SatVarName, Score))
    -> Score1 is Score + 1,
    asserta(occurrences(SatVarName, Score1))
    ; asserta(occurrences(SatVarName, 1))
    ),
    assert_count_occurrences_from_clause(T).

assert_memoized_clauses(SolverName, SolverEnv, NewSolverEnv) :-
    findall(C-LbdScore, memoize_backjump_clause(SolverName, C, LbdScore), SmtClauses),
    SmtClauses \== [],
    !,
    % learned clauses can be applied to all variables which are equal to new ids (see id_equality/3)
    %findall(CPrime-LbdScore, (memoize_backjump_clause(SolverName, C, LbdScore), replace_ids_with_eq_ids_top_level(C, CPrime)), PrimedSmtClauses),
    %append(SmtClauses, PrimedSmtClauses, FullClauses),
    get_from_solver_env(SolverEnv, sat_vars, SatVars),
    get_from_solver_env(SolverEnv, t2b_env, T2BEnv),
    clauses_to_sat_assert(SmtClauses, SatVars, T2BEnv, NewSatVars, NewT2BEnv, _SatClauses),
    get_bindings_from_ids(NewSatVars, NewSatBindings, NewSatVarNames, _, PrologSatVarTriple),
    NewSolverEnv = [sat_vars:NewSatVars,sat_varnames:NewSatVarNames,sat_bindings:NewSatBindings,t2b_env:NewT2BEnv,pl_vars:PrologSatVarTriple].

asserta_once(Assertion) :-
    call(dpllt_sat_solver:Assertion),
    !.

asserta_once(Assertion) :-
    asserta(dpllt_sat_solver:Assertion).

b_pred_or_bool_false(X) :- X == falsity; X == boolean_false; X == value(pred_false).

b_pred_or_bool_true(X) :- X == truth; X == boolean_true; X == value(pred_true).

b_to_cnf(In, State, Out) :-
    get_texpr_expr(In, Expr),
    b_to_cnf_aux(Expr, State, Out),
    !.

b_to_cnf(In, _, _) :-
    translate_bexpression(In, PPIn),
    !,
    add_error_fail(b_to_cnf, 'CNF conversion failed', PPIn).

b_to_cnf_aux(identifier(Name), State, [[pred_true-Res-Name]]) :- !,
    member(bind(Name,Res), State).

b_to_cnf_aux(X, _, [Out]) :-
    ( b_pred_or_bool_true(X)
    -> Out = [pred_true-pred_true-nonvar]
    ; b_pred_or_bool_false(X)
    -> Out = []
    ; fail
    ), !.

b_to_cnf_aux(equal(A,B), State, CNF) :-
    ground(B),
    get_texpr_expr(B, Expr),
    ( b_pred_or_bool_true(Expr)
    -> b_to_cnf(A, State, CNF)
    ; %b_pred_or_bool_false(Expr),
    safe_create_texpr(value(pred_true), boolean, [], True),
    safe_create_texpr(equal(A,True), pred, [], EqualTrue),
    b_to_cnf_aux(negation(EqualTrue), State, CNF)
).

b_to_cnf_aux(negation(A), State, [[Res]]) :-
    b_to_cnf(A, State, [[Pol-Var-Name]]),
    ( Pol == pred_true
    -> Res = pred_false-Var-Name
    ; Pol == pred_false,
    Res = pred_true-Var-Name
).

b_to_cnf_aux(disjunct(D1,D2), State, Res) :-
    get_texpr_expr(D1, conjunct(A,B)),
    !,
    b_to_cnf(b(disjunct(A,D2),pred,[]), State, RDJ1),
    b_to_cnf(b(disjunct(B,D2),pred,[]), State, RDJ2),
    append(RDJ1, RDJ2, Res).

b_to_cnf_aux(disjunct(D1,D2), State, Res) :-
    get_texpr_expr(D2, conjunct(A,B)),
    !,
    b_to_cnf(b(disjunct(D1,A),pred,[]), State, RDJ1),
    b_to_cnf(b(disjunct(D1,B),pred,[]), State, RDJ2),
    append(RDJ1, RDJ2, Res).

b_to_cnf_aux(disjunct(D1,D2),State,Res) :-
    b_to_cnf(D1, State, TResD1),
    b_to_cnf(D2, State, TResD2),
    ( TResD1 = [ResD1],
    TResD2 = [ResD2]
    -> append(ResD1, ResD2, DRes),
    Res = [DRes]
    ; TResD1 = [ClauseResD1],
    TResD2 \= [_]
    -> maplist(append(ClauseResD1), TResD2, Res)
    ; TResD2 = [ClauseResD2],
    TResD1 \= [_]
    -> maplist(append(ClauseResD2), TResD1, Res)
    ; disjunct_non_singleton_cnfs(TResD1, TResD2, Res)
).

b_to_cnf_aux(conjunct(A,B), State, Res) :-
    b_to_cnf(A, State, RA),
    b_to_cnf(B, State, RB),
    append(RA, RB, Res).

bt_asserta(Assertion) :-
    asserta(Assertion); (retract(Assertion), fail).

bt_log_sat_stack(StateMutable, SatVarName, PropType, CurLevel, Pol, OriginalClause) :-
    add_state_instance(StateMutable, sat_stack, (SatVarName, PropType, CurLevel, Pol, OriginalClause)),
    ( increase_stack_size(StateMutable)
    ; is_restart,
    asserta_once(saved_phase(SatVarName, Pol)),
    fail
).

bt_retract(Assertion) :-
    ( retract(Assertion)
    -> ( true
    ; asserta(Assertion),
    fail
    )
    ; fail
).

bt_retract_if_exists(Assertion) :-
    ( dpllt_sat_solver:Assertion
    -> bt_retract(dpllt_sat_solver:Assertion)
    ; true
).

bump_heuristic_score_for_type(vsids, _, OldScore, NewScore) :-
    NewScore is OldScore + 1.

bump_heuristic_score_for_type(evsids, TotalConflicts, OldScore, NewScore) :-
    evsids_f_value(FVal),
    NewScore is ceiling(OldScore + FVal**(-TotalConflicts)).

clause_order(_-_-A3, _-_-B3) :- A3 @< B3.

clause_setup(SolverEnv, StateMutable, Clause) :-
    Clause = [Pol-Var-SatVarName|Triples],
    set_watch(SolverEnv, StateMutable, Clause, Triples, Var, Pol, SatVarName).

clause_to_smt(PlVars, Clause, SmtFormula) :-
    clause_to_smt(PlVars, Clause, [], SmtFormula).

clause_to_smt(_, [], Acc, SmtFormula) :-
    disjunct_predicates(Acc, SmtFormula).

clause_to_smt(PlVars, [Pol-_-SatVarName|T], Acc, SmtClause) :-
    member(_-SatVarName-TSmtFormula, PlVars),
    get_smt_formula_for_sat_pol(TSmtFormula, Pol, SmtFormula),
    clause_to_smt(PlVars, T, [SmtFormula|Acc], SmtClause).

clauses_to_sat_assert([], SatVars, T2BEnv, SatVars, T2BEnv, []).

clauses_to_sat_assert([SmtClause-LbdScore|T], SatVars, T2BEnv, NewSatVars, NewT2BEnv, [SatClause|NT]) :-
    predicate_to_sat(normal, [], SatVars, T2BEnv, SmtClause, TT2BEnv, _, SatClause, TSatVars),
    !,
    asserta(backjump_clause(0, SatClause, LbdScore, [])),
    debug_format_sat("Learn clause from prior run ~w~n", [SatClause]),
    clauses_to_sat_assert(T, TSatVars, TT2BEnv, NewSatVars, NewT2BEnv, NT).

clauses_to_sat_assert([_|T], SatVars, T2BEnv, NewSatVars, NewT2BEnv, NT) :-
    clauses_to_sat_assert(T, SatVars, T2BEnv, NewSatVars, NewT2BEnv, NT).

clean_dynamic_solver_state :-
    retractall(solver_name(_)),
    retractall(restarts(_)),
    retractall(is_restart),
    retractall(bt_from_smt_solution),
    retractall(recent_lbds_dl(_, _)),
    retractall(recent_stack_sizes_dl(_, _)),
    retractall(saved_phase(_, _)),
    retractall(amount_clause_reductions(_)),
    retractall(amount_learned_clauses(_)),
    retractall(luby_counter(_)),
    retractall(exclude_sat_solution_clause(_)),
    retractall(total_lbd_sum(_)),
    retractall(conflict_stats(_, _, _)),
    retractall(idl_unsat_core(_)),
    retractall(backjump_level(_)),
    retractall(backjump_clause(_, _, _, _)),
    ( incremental_mode
    -> true
    ; retractall(memoize_backjump_clause(_, _, _))
).

clear_lbd_values_or_fail(StateMutable) :-
    glucose_restart_trail_threshold(TrailThresh),
    glucose_restart_stack_avg_factor(StackSizeFactor),
    recent_stack_sizes_dl(StackSizes-[], AmountStackSizes),
    AmountStackSizes == TrailThresh, % queue of recent stack sizes on conflict is full
    get_full_state(StateMutable, current_stack_size, StackSize),
    sumlist(StackSizes, SSum),
    StackSizesAvg is SSum / AmountStackSizes,
    StackSize > StackSizeFactor * StackSizesAvg,
    clear_recent_lbds_state.

clear_recent_lbds_state :-
    retract(recent_lbds_dl(_, _)),
    asserta(recent_lbds_dl(Diff-Diff, 0)).

cnf_to_smt(BoolPred, Smt) :-
    BoolPred = b(Expr,_,_),
    cnf_to_smt_e(Expr, Smt).

cnf_to_smt_e(falsity, b(falsity,pred,[])).

cnf_to_smt_e(truth, b(truth,pred,[])).

cnf_to_smt_e(conjunct(A,B), Smt) :-
    cnf_to_smt(A, NA),
    cnf_to_smt(B, NB),
    safe_create_texpr(conjunct(NA,NB), pred, [], Smt).

cnf_to_smt_e(disjunct(A,B), Smt) :-
    cnf_to_smt(A, NA),
    cnf_to_smt(B, NB),
    safe_create_texpr(disjunct(NA,NB), pred, [], Smt).

cnf_to_smt_e(equal(b(identifier(_),_,Info),b(BoolExpr,boolean,_)), Smt) :-
    member(smt_formula(TSmt), Info),
    ( BoolExpr == boolean_true
    -> Smt = TSmt
    ; safe_create_texpr(negation(TSmt), pred, [], Smt)
).

compute_and_assert_backjump_clause(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause) :-
    compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, _).

compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, BjLevel) :-
    get_last_decision_level(StateMutable, _),
    possibly_discard_learned_clauses,
    debug_format_sat("~nConflict clause is ~w", [ConflictClause]),
    debug_format_sat("~nStart CDCL..", []),
    ( (get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause, BjLevel, UsedVars), BjLevel \== -1)
    ; %trace,nl,get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause2, BjLevel2, UsedVars2),
    add_error_fail(compute_and_assert_backjump_clause_get_level, 'SMT solver\'s conflict resolution failed', [])
    ),
    debug_format_sat("done.", []),
    debug_format_sat("Backjump clause is ~w", [BjClause]),
    debug_format_sat("Backjump level is ~w", [BjLevel]),
    get_full_state(StateMutable, sat_stack, SatStack),
    compute_lbd_score(SatStack, BjClause, LbdScore),
    asserta(backjump_clause(BjLevel, BjClause, LbdScore, UsedVars)),
    asserta(backjump_level(BjLevel)),
    ( incremental_mode,
    get_from_solver_env(SolverEnv, pl_vars, PlVars),
    clause_to_smt(PlVars, BjClause, SmtFormula),
    SmtFormula \= b(negation(b(truth,pred,_)),pred,_),
    SmtFormula \= b(truth,pred,_) % uses _cnf_opt variable, don't store those
    -> solver_name(SolverName),
    asserta(memoize_backjump_clause(SolverName, SmtFormula, LbdScore))
    ; true
    ),
    count_found_conflict(NewTotal, NewSinceRestart, _),
    store_recent_stack_size(StackSize),
    count_learned_clause,
    ( \+ clear_lbd_values_or_fail(StateMutable),
    BjLevel \== 0
    -> store_recent_lbd_score(LbdScore),
    update_total_lbd_sum(LbdScore),
    (random_restart(NewTotal, NewSinceRestart), !; true)
    ; true
    ), !.

compute_lbd_score(SatStack, BjClause, LbdScore) :-
    compute_lbd_score(SatStack, BjClause, [], LbdScore).

compute_lbd_score(_, [], Acc, LbdScore) :-
    length(Acc, LbdScore).

compute_lbd_score(SatStack, [_-_-SatVarName|T], Acc, LbdScore) :-
    mutdict_get(SatStack, SatVarName, (_,Level,_,_)),
    !,
    ord_add_element(Acc, Level, NewAcc),
    compute_lbd_score(SatStack, T, NewAcc, LbdScore).

compute_lbd_score(SatStack, [_|T], Acc, LbdScore) :- % TO DO: check this, happens when using idl solver unsat core?
    compute_lbd_score(SatStack, T, Acc, LbdScore).

count_found_conflict(Total1, SRes1, SRed1) :-
    retract(conflict_stats(total(Total), since_restart(SRes), since_reduction(SRed))),
    Total1 is Total + 1,
    SRes1 is SRes + 1,
    SRed1 is SRed + 1,
    asserta(conflict_stats(total(Total1), since_restart(SRes1), since_reduction(SRed1))).

count_learned_clause :-
    retract(amount_learned_clauses(Old)),
    New is Old + 1,
    asserta(amount_learned_clauses(New)).

count_occurrences_in_clauses(Clauses, VarScoreTuples) :-
    retractall(occurrences(_, _)),
    assert_count_occurrences(Clauses),
    findall((SatVarName,Score), retract(occurrences(SatVarName, Score)), VarScoreTuples), !.

create_solver_state(StateMutable) :-
    new_mutdict(EmptySatStack),
    new_mutdict(EmptyHeuristic),
    State = [sat_stack:EmptySatStack,cur_level:0,':'(decision_level,-1),current_stack_size:0,heuristic_avl:EmptyHeuristic],
    create_mutable(solver_state(State), StateMutable).

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

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

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

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

delete_state_instance(StateMutable, Key, Datum) :-
    get_mutable(solver_state(SolverState), StateMutable),
    memberchk(Key:Data, SolverState),
    ( Key == heuristic_avl
    ; Key == sat_stack
    ),
    Datum = (SatVarName,_), !,
    ( mutdict_get(Data, SatVarName, _)
    -> mutdict_delete(Data, SatVarName)
    ; % it can be the case that SatVarName has already been removed
    % from the mutable due to coroutines etc.; succeed in this case
    true
).

discard_half_of_learned_clauses_greater_lbd(C, Half, LbdLimit, Removed) :-
    C =< Half,
    backjump_clause(BjLevel, BjClause, LbdScore, UsedVars),
    !,
    retract(backjump_clause(BjLevel, BjClause, LbdScore, UsedVars)),
    ( LbdScore > LbdLimit
    -> C1 is C + 1,
    discard_half_of_learned_clauses_greater_lbd(C1, Half, LbdLimit, Removed)
    ; discard_half_of_learned_clauses_greater_lbd(C, Half, LbdLimit, Removed),
    asserta(backjump_clause(BjLevel, BjClause, LbdScore, UsedVars))
).

discard_half_of_learned_clauses_greater_lbd(C, _, _, C).

disjunct_non_singleton_cnfs([], Cnf, Cnf).

disjunct_non_singleton_cnfs([Clause|T], Cnf2, Cnf) :-
    maplist(append(Clause), Cnf2, NCnf2),
    disjunct_non_singleton_cnfs(T, NCnf2, Cnf).

do_random_restart :-
    retract(restarts(OldR)),
    NewR is OldR + 1,
    asserta(restarts(NewR)),
    retract(backjump_level(_)),
    asserta(backjump_level(0)),
    retract(conflict_stats(total(Total), _, since_reduction(SRed))),
    asserta(conflict_stats(total(Total), since_restart(0), since_reduction(SRed))),
    asserta_once(is_restart),
    debug_format_sat("~nRandom restart", []).

elim_var_from_saved_phase(SatVarName, SavedPol, Var, SolverEnv, StateMutable, CurLevel, PlVars) :-
    get_pl_var_for_sat_id(SatVarName, PlVars, Var),
    NextLevel is CurLevel + 1,
    ( bt_log_sat_stack(StateMutable, SatVarName, branch, CurLevel, SavedPol, _OriginalClause),
    debug_format_sat("Phase Restore: Decide variable ~w with polarity ~w on level ~w", [SatVarName,SavedPol,CurLevel]),
    Var = SavedPol,
    update_full_state(StateMutable, cur_level, NextLevel),
    bt_retract_if_exists(saved_phase(SatVarName, _)),
    elim_vars(SolverEnv, StateMutable, PlVars)
    ; \+ backjump_level(_),
    %( learn_idl_core(StateMutable, CurLevel, SolverEnv)
    %; true
    %),
    ( ground(Var)
    -> true
    ; negate_polarity(SavedPol, NegSavedPol),
    bt_log_sat_stack(StateMutable, SatVarName, branch, CurLevel, NegSavedPol, _OriginalClause),
    debug_format_sat("Phase Restore Failed: Decide variable ~w with polarity ~w on level ~w", [SatVarName,NegSavedPol,CurLevel]),
    Var = NegSavedPol
    ),
    update_full_state(StateMutable, cur_level, NextLevel),
    elim_vars(SolverEnv, StateMutable, PlVars)
).

elim_vars(SolverEnv, StateMutable, PlVars) :-
    get_full_state(StateMutable, cur_level, CurLevel),
    ( % solution found
    get_full_state(StateMutable, heuristic_avl, Heuristic),
    mutdict_empty(Heuristic)
    ; update_full_state(StateMutable, decision_level, CurLevel),
    %possibly_decay_heuristic_values, % only for vsids; remove for now
    ( elim_vars_from_asserted_heuristic_rapid_restart(SolverEnv, StateMutable, CurLevel, PlVars)
    ; % backjumping
    backjump_level(C),
    debug_format_sat("Current level is ~w", [CurLevel]),
    C == CurLevel,
    retract(backjump_level(C)),
    debug_format_sat("~nbackjump branch prop level ~w", [CurLevel]),
    get_clauses_to_learn_bump_scores(StateMutable, C, SolverEnv, ClausesToLearn),
    problem_setup(SolverEnv, StateMutable, ClausesToLearn),
    elim_vars(SolverEnv, StateMutable, PlVars)
)
).

elim_vars_from_asserted_heuristic_rapid_restart(SolverEnv, StateMutable, CurLevel, PlVars) :-
    \+ backjump_level(_),
    \+ idl_unsat_core(_),
    get_sat_vars_with_max_heuristic(StateMutable, MaxScore, TSatVarNames),
    % we set a deterministic order on variable selection using sort/2
    % the solver gets nondeterministic if this is removed and mutdicts are enabled since mutdict_items/2 does not impose an order
    sort(TSatVarNames, SatVarNames),
    debug_format_sat("Max heuristic values with score ~w are ~w", [MaxScore,SatVarNames]),
    get_decision_variable_from_list(SatVarNames, SatVarName),
    delete_state_instance(StateMutable, heuristic_avl, (SatVarName, MaxScore)),
    get_pl_var_for_sat_id(SatVarName, PlVars, Var),
    NextLevel is CurLevel + 1,
    ( saved_phase(SatVarName, SavedPol)
    -> elim_var_from_saved_phase(SatVarName, SavedPol, Var, SolverEnv, StateMutable, CurLevel, PlVars)
    ; % uninformed phase/polarity selection
    ( bt_log_sat_stack(StateMutable, SatVarName, branch, CurLevel, pred_true, _OriginalClause),
    debug_format_sat("Decide variable ~w with polarity ~w on level ~w", [SatVarName,pred_true,CurLevel]),
    %get_theory_formula_for_satvar(SolverEnv, SatVarName, TheoryFormula),
    %translate:print_bexpr(TheoryFormula),nl,
    Var = pred_true,
    update_full_state(StateMutable, cur_level, NextLevel),
    elim_vars(SolverEnv, StateMutable, PlVars)
    ; \+ backjump_level(_),
    %( learn_idl_core(StateMutable, CurLevel, SolverEnv)
    %; true
    %),
    ( ground(Var)
    -> true
    ; bt_log_sat_stack(StateMutable, SatVarName, branch, CurLevel, pred_false, _OriginalClause),
    debug_format_sat("Decide variable ~w with polarity ~w on level ~w", [SatVarName,pred_false,CurLevel]),
    %get_theory_formula_for_satvar(SolverEnv, SatVarName, TheoryFormula),
    %translate:print_bexpr(TheoryFormula),nl,
    Var = pred_false
    ),
    update_full_state(StateMutable, cur_level, NextLevel),
    elim_vars(SolverEnv, StateMutable, PlVars)
)
).

explain_theory_propagation(SolverEnv, SatStack, TheoryPropSatVar, TheoryPropLevel, TheoryPropPol, ExplainingClause) :-
    debug_format_sat("Explain theory propagation", []),
    mutdict_items(SatStack, SatStackList),
    findall((SatVarName-Pol), (member(SatVarName-(_,Level,Pol,_), SatStackList), Level<TheoryPropLevel), SatVarNameTuples),
    get_from_solver_env(SolverEnv, sat_vars, SatVars),
    get_smt_formula_from_vars_for_sat_pol(SatVars, TheoryPropSatVar, TheoryPropPol, SmtFormula),
    negate_smt_formula(SmtFormula, NegSmt),
    get_explanation_candidate_formula(SatVars, SatVarNameTuples, CandidateFormula),
    ( SatVarNameTuples = [_]
    -> UnsatCore = b(conjunct(CandidateFormula,NegSmt),pred,[])
    ; temporary_set_unsat_core_timeout,
    unsat_core_with_fixed_conjuncts(CandidateFormula, NegSmt, TUnsatCore),
    UnsatCore = b(conjunct(TUnsatCore,NegSmt),pred,[]),
    preferences:reset_temporary_preference(time_out)
    ),
    get_from_solver_env(SolverEnv, t2b_env, T2BEnv),
    predicate_to_sat(only_reuse, [], SatVars, T2BEnv, UnsatCore, _NewEnv, _, UnsatCoreSat, _NewSatVars),
    sat_conj_negate_to_clause(UnsatCoreSat, TExplainingClause),
    get_from_solver_env(SolverEnv, pl_vars, PlVars),
    set_variable_references_in_clause(PlVars, TExplainingClause, ExplainingClause).% TO DO: learn theory lemma?

get_antecedent_assignments(SatStack, SatVarName, Antecedent) :-
    mutdict_get(SatStack, SatVarName, (_,_,_,OriginalClause)),
    !,
    select(_-_-SatVarName, OriginalClause, TAntecedent),
    negate_polarities(TAntecedent, Antecedent), !.

get_antecedent_assignments(_, _, []). % wd po not necessarily assigned, e.g., if the predicate containing the wd condition is false

get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, BjClauses, UsedVars) :-
    get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, [], BjClauses, [], UsedVars).

get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, BAcc, BjClauses, UAcc, UsedVars) :-
    ( backjump_clause(BjLevel, BjClause, _, _)
    -> bt_retract(backjump_clause(BjLevel, BjClause, _, BUsedVars)),
    ( BjLevel >= CurrentBjLevel
    -> append(BUsedVars, UAcc, NUAcc),
    get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, [BjClause|BAcc], BjClauses, NUAcc, UsedVars)
    ; get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, BAcc, BjClauses, UAcc, UsedVars),
    bt_asserta(backjump_clause(BjLevel, BjClause, _, BUsedVars))
    )
    ; BjClauses = BAcc,
    UsedVars = UAcc
    ), !.

get_backjump_clause_and_level(SolverEnv, StateMutable, ConflictDLevel, ResolvedSoFar, TBjClause, BjClause, BjLevel, UsedVars) :-
    get_backjump_clause_and_level_sub(SolverEnv, StateMutable, ConflictDLevel, 0, _, TBjClause, Resolver, ThisLevelCount),
    get_full_state(StateMutable, sat_stack, SatStack),
    ( ThisLevelCount == 1
    -> % break, first UIP
    negate_assignments_to_polarities(TBjClause, BjClause),
    get_maximum_decision_level_other_than_current(BjClause, SatStack, 0, ConflictDLevel, BjLevel),
    get_variables_used_in_cdcl(ResolvedSoFar, BjClause, UsedVars)
    ; ground(Resolver),
    resolve(SatStack, TBjClause, Resolver, NToExpand),
    mutdict_put(ResolvedSoFar, Resolver, Resolver),
    get_backjump_clause_and_level(SolverEnv, StateMutable, ConflictDLevel, ResolvedSoFar, NToExpand, BjClause, BjLevel, UsedVars)
).

get_backjump_clause_and_level_sub(_, _, _, ThisLevelCountAcc, ResolverAcc, [], ResolverAcc, ThisLevelCountAcc).

get_backjump_clause_and_level_sub(SolverEnv, StateMutable, ConflictDLevel, ThisLevelCountAcc, ResolverAcc, [_-_-SatVarName|T], Resolver, ThisLevelCount) :-
    get_from_sat_stack_or_explain_theory_propagation(SolverEnv, StateMutable, SatVarName, PropType, Level, _, _),
    ( Level == ConflictDLevel
    -> NThisLevelCountAcc is ThisLevelCountAcc + 1
    ; NThisLevelCountAcc = ThisLevelCountAcc
    ),
    ( (
    Level == ConflictDLevel,
    PropType == unit
    )
    -> NResolverAcc = SatVarName
    ; NResolverAcc = ResolverAcc
    ),
    get_backjump_clause_and_level_sub(SolverEnv, StateMutable, ConflictDLevel, NThisLevelCountAcc, NResolverAcc, T, Resolver, ThisLevelCount).

get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause, BjLevel, UsedVars) :-
    get_last_decision_level(StateMutable, _),
    new_mutdict(ResolvedSoFar),
    get_backjump_clause_and_level(SolverEnv, StateMutable, ConflictLevel, ResolvedSoFar, ConflictClause, BjClause, BjLevel, UsedVars).

get_bindings_from_ids(SatVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :-
    get_bindings_from_ids_acc(SatVars, [], [], [], [], SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple), !.

get_bindings_from_ids_acc([], AccBindings, AccNames, AccTuples, AccPlVars, AccBindings, AccNames, AccTuples, AccPlVars).

get_bindings_from_ids_acc([b(identifier(Name),IdType,IdInfo)|T], AccBindings, AccNames, AccTuples, AccPlVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :-
    NewAccBindings = [bind(Name,PrologVar)|AccBindings],
    NewAccTuples = [(b(identifier(Name),IdType,IdInfo),PrologVar)|AccTuples],
    !,
    ( member(smt_formula(SmtFormula), IdInfo)
    -> NewAccPlVars = [PrologVar-Name-SmtFormula|AccPlVars]
    ; % plain SAT variable which is not reified with a theory solver, e.g., introduced by CNF optimization rewriting
    OptEq = b(equal(b(identifier(Name),boolean,[]),b(boolean_true,boolean,[])),pred,[]),
    NewAccPlVars = [PrologVar-Name-OptEq|AccPlVars]
    ),
    get_bindings_from_ids_acc(T, NewAccBindings, [Name|AccNames], NewAccTuples, NewAccPlVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple).

get_bindings_from_ids_acc([_|T], AccBindings, AccNames, AccTuples, AccPlVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :-
    get_bindings_from_ids_acc(T, AccBindings, AccNames, AccTuples, AccPlVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple).

get_clause_from_negated_ground_bindings(SatBindings, TheoryLemmaClause) :-
    get_clause_from_negated_ground_bindings(SatBindings, [], TheoryLemmaClause).

get_clause_from_negated_ground_bindings([], Acc, Acc).

get_clause_from_negated_ground_bindings([bind(SatVarName,Pol)|T], Acc, TheoryLemmaClause) :-
    ground(Pol),
    !,
    negate_polarity(Pol, NegPol),
    get_clause_from_negated_ground_bindings(T, [NegPol-_-SatVarName|Acc], TheoryLemmaClause).

get_clause_from_negated_ground_bindings([_|T], Acc, TheoryLemmaClause) :-
    get_clause_from_negated_ground_bindings(T, Acc, TheoryLemmaClause).

get_clauses_to_learn_bump_scores(StateMutable, CurrentBjLevel, SolverEnv, ClausesToLearn) :-
    get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, TempBjClauses, UsedVars),
    %length(TempBjClauses, Len),
    %debug_format_sat("Learn ~w clauses", [Len]),
    get_sat_solution_exclusion_clauses(ExclClauses),
    append(ExclClauses, TempBjClauses, BjClausesNoRef),
    set_references_and_bump_scores(BjClausesNoRef, UsedVars, StateMutable, SolverEnv, ClausesToLearn).

get_complete_theory_lemma(SolverEnv, TheoryLemmaClause) :-
    get_from_solver_env(SolverEnv, pl_vars, PlVars),
    get_from_solver_env(SolverEnv, sat_bindings, SatBindings),
    get_clause_from_negated_ground_bindings(SatBindings, TTheoryLemmaClause),
    set_variable_references_in_clause(PlVars, TTheoryLemmaClause, TheoryLemmaClause), !.

get_conflict_clause_for_theory_conflict(LastVarName, LastVarValue, SolverEnv, ConflictClause) :-
    ( retract(idl_unsat_core(UnsatCore))
    -> true
    ; get_from_solver_env(SolverEnv, sat_bindings, SatBindingsNoLast),
    get_from_solver_env(SolverEnv, sat_vars, SatVars),
    temporary_set_unsat_core_timeout,
    sat_to_predicate_from_solution(SatBindingsNoLast, SatVars, SmtFormulaNoLast),
    sat_to_predicate_from_solution([bind(LastVarName,LastVarValue)], SatVars, FixedConj),
    debug_format_sat("Compute unsat core for : ", [], b(conjunct(FixedConj,SmtFormulaNoLast),pred,[])),
    tools:start_ms_timer(TT),
    conjunct_predicates([FixedConj,SmtFormulaNoLast],FullFormula),
    time_out(unsat_chr_core_list_with_auto_time_limit(FullFormula, 30000,
    [auto_time_out_factor(180), % we add 80
    no_warning_if_sol_found], GlobalRes, CoreList),
    30000, TimeoutResult),
    tools:stop_ms_timer_with_msg(TT,'unsat_chr_core_list_with_auto_time_limit'),
    ( GlobalRes = solution(_)
    -> % just to make sure that this never happens
    add_internal_error('Unsat core is satisfiable. This is probably a bug in this SMT solver.', get_conflict_clause_for_theory_conflict(FullFormula)),
    fail
    ; GlobalRes == time_out
    -> % ignore core if global result is timeout
    TUnsatCore = FullFormula
    ; TimeoutResult == time_out
    -> % don't waste too much time in unsat core computation
    debug_format_sat("Canceled unsat core computation due to exceeding a timeout" ,[]),
    TUnsatCore = FullFormula
    ; (CoreList == []
    -> add_internal_error('Conflict clause in SMT solving is not a conflict.',
    get_conflict_clause_for_theory_conflict(LastVarName)),
    fail
    ; conjunct_predicates(CoreList, TUnsatCore)
    )
    ),
    debug_format_sat("Computed unsat core with added WD POs: ", [], TUnsatCore),
    ( remove_wd_pos_introduced_for_dpllt_keep_toplevel(TUnsatCore, UnsatCore)
    -> true
    ; add_internal_error('Removing WD POs for DPLL(T) failed.', remove_wd_pos_introduced_for_dpllt_keep_toplevel(TUnsatCore, UnsatCore))
    ),
    debug_format_sat("Computed unsat core: ", [], UnsatCore),
    preferences:reset_temporary_preference(time_out)
    ), !,
    get_conflict_clause_from_unsat_core(UnsatCore, SolverEnv, TConflictClause),
    sort(TConflictClause, ConflictClause), % there can be duplicates due to added top-level WD POs; important to remove
    !.