cdclt_sat_solver

add_heuristic_tuples(_, _, _, []).

add_heuristic_tuples(StateMutable, BoostFactor, VarsFromBinaryClauses, [SatVarName-Score|T]) :-
    ( select(SatVarName, VarsFromBinaryClauses, TVarsFromBinaryClauses)
    -> NScore is Score * BoostFactor
    ; NScore = Score,
    TVarsFromBinaryClauses = VarsFromBinaryClauses
    ),
    fibonacci_heap:push(NScore, SatVarName),
    add_heuristic_tuples(StateMutable, BoostFactor, TVarsFromBinaryClauses, T).

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

all_literals_are_marked([]).

all_literals_are_marked([_-_-_-SatVarName|T]) :-
    part_of_first_uip(SatVarName),
    !,
    all_literals_are_marked(T).

announce_bt_from_smt_solution :-
    asserta(bt_from_smt_solution).

assert_update_pending_theory_propagation(SatVarName, Pol) :-
    retract(pending_theory_prop(SatVarName,_)),
    !,
    asserta(pending_theory_prop(SatVarName,Pol)).

assert_update_pending_theory_propagation(SatVarName, Pol) :-
    asserta(pending_theory_prop(SatVarName,Pol)).

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

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

assignment_count_on_cur_level(0).

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, Res, []),
    !,
    Res = Out.

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

b_to_cnf(b(Expr,_,_Info), State) -->
    !,
    b_to_cnf_aux(Expr, State).

b_to_cnf(In, _, _, _) :-
    add_error_fail(b_to_cnf, 'Not properly wrapped:', In).

b_to_cnf_aux(X, _) -->
    {X == truth}, !,
[].

b_to_cnf_aux(X, _) -->
    {X == falsity}, !,
    [[]].

b_to_cnf_aux(equal(A,B), State) -->
    {get_texpr_expr(B, Expr),
    Expr == boolean_true,
    get_texpr_expr(A, identifier(Name))},
    !,
    {member(bind(Name,Res)-StackInfo, State)},
    [[StackInfo-pred_true-Res-Name]].

b_to_cnf_aux(equal(A,B), State) -->
    {get_texpr_expr(B, Expr),
    Expr == boolean_false,
    get_texpr_expr(A, identifier(Name)),
    member(bind(Name,Res)-StackInfo, State)},
    [[StackInfo-pred_false-Res-Name]].

b_to_cnf_aux(disjunct(D1,D2), State) -->
    b_to_cnf_disj_aux(D1, D2, State).

b_to_cnf_aux(conjunct(A,B), State) -->
    b_to_cnf(A, State),
    b_to_cnf(B, State).

b_to_cnf_disj_aux(D1, D2, State) -->
    {get_texpr_expr(D1, conjunct(A,B))}, !,
    {create_texpr(disjunct(A,D2), pred, [], DJ1),
    create_texpr(disjunct(B,D2), pred, [], DJ2)},
    b_to_cnf_aux(conjunct(DJ1,DJ2), State).

b_to_cnf_disj_aux(D1, D2, State) -->
    {get_texpr_expr(D2, conjunct(A,B))}, !,
    {create_texpr(disjunct(D1,A), pred, [], DJ1),
    create_texpr(disjunct(D1,B), pred, [], DJ2)},
    b_to_cnf_aux(conjunct(DJ1,DJ2), State).

b_to_cnf_disj_aux(D1, D2, State, Res, Acc) :-
    b_to_cnf(D1, State, Res1),
    b_to_cnf(D2, State, Res2),
    !,
    ( Res1 = []
    -> Res = Acc
    ; Res1 = [[]]
    -> append(Res2,Acc,Res)
    ; Res2 = []
    -> Res = Acc
    ; Res2 = [[]]
    -> append(Res1,Acc,Res)
    ; ( Res1 = [ResD1],
    Res2 = [ResD2]
    )
    -> Res = [Res12|Acc],
    append(ResD1, ResD2, Res12)
    ; join_clauses(Res1,Res2,Res,Acc)
    -> true
    ; add_error_fail(b_to_cnf_disj, 'Cannot join clauses: ', Res1:Res2)
).

b_to_cnf_safe(In, State, Out) :-
    b_to_cnf(In, State, TOut),
    !,
    Out = TOut.

b_to_cnf_safe(_, _, _) :-
    add_internal_error('B to CNF conversion failed ', cdclt),
    fail.

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

bt_log_sat_stack(StateMutable, SatVarName, Pol) :-
    increase_stack_size(StateMutable),
    ( true
    ; save_phase(SatVarName, Pol),
    fail
).

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

bump_glue_levels([]).

bump_glue_levels([_-_-_-SatVarName|T]) :-
    ( retract(glue_level(SatVarName, GlueLevel,AlreadyBumped))
    -> NGlueLevel is GlueLevel + 1
    ; NGlueLevel = 1,
    AlreadyBumped = false
    ),
    asserta(glue_level(SatVarName,NGlueLevel,AlreadyBumped)),
    bump_glue_levels(T).

bump_glue_variable_score(Score, SatVarName, GlueLevel, GC) :-
    GlueBump is Score * (GlueLevel/GC),
    NScore is Score + GlueBump,
    fibonacci_heap:update_bt(SatVarName, NScore).

bump_glue_variable_scores(GC, CurLevel) :-
    ( bt_retract(glue_level(GlueVar,GlueLevel,AlreadyBumped))
    -> ( ( \+ AlreadyBumped,
    GlueLevel > CurLevel
    )
    -> fibonacci_heap:get_priority_of(GlueVar, Score),
    bump_glue_variable_score(Score, GlueVar, GlueLevel, GC),
    bump_glue_variable_scores(GC, CurLevel),
    bt_asserta(glue_level(GlueVar,GlueLevel,true))
    ; bump_glue_variable_scores(GC, CurLevel),
    bt_asserta(glue_level(GlueVar,GlueLevel,AlreadyBumped))
    )
    ; true
).

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

bump_heuristic_score_for_type(vmtf, TotalConflicts, _, NewScore) :-
    NewScore is TotalConflicts.

bump_heuristic_score_for_type(acids, TotalConflicts, OldScore, NewScore) :-
    NewScore is (OldScore + TotalConflicts) / 2.

bump_heuristic_score_for_type(evsids, TotalConflicts, OldScore, NewScore) :-
    evsids_f_value(FVal),
    catch(NewScore is OldScore + FVal**(-TotalConflicts), error(evaluation_error(float_overflow),_), NewScore = 1.35743634973696E+308).

checkout_sat_variable(SatVarName, OriginalClause) :-
    delete_from_heuristic(SatVarName),
    retract_if_exists(saved_phase(SatVarName, _)),
    ( allow_partial_model
    -> worsen_scores_for_vars_in_clause(OriginalClause)
    ; true
).

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

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

clean_dynamic_solver_state :-
    retractall(assignment_timeout_occurred),
    retractall(allow_partial_model),
    retractall(unfixed_deferred_set_error),
    retractall(assignment_count_on_cur_level(_)),
    retractall(pending_theory_prop(_,_)),
    retractall(glue_clauses(_)),
    retractall(glue_level(_,_,_)),
    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(_, _, _, _, _, _)).

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_pending_theory_propagations :-
    retractall_once(pending_theory_prop(_,_)).

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, % TODO: adapt to new bj clause handling; yet, forgetting clauses has not shown to be beneficial so far
    debug_format_sat("~nConflict clause is ~w", [strip-ConflictClause]),
    debug_format_sat("~nStart CDCL..", []),
    ( (
    get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause, BjLevel, BjSatVars, UsedVars),
    BjLevel \== -1
    )
    ; 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", [strip-BjClause]),
    debug_format_sat("Backjump level is ~w", [BjLevel]),
    compute_lbd_score(BjClause, LbdScore),
    debug_format_sat("LBD Score is ~w", [LbdScore]),
    ( ( glue_bumping(true),
    LbdScore == 2
    )
    -> retract(glue_clauses(Old)),
    New is Old + 1,
    asserta(glue_clauses(New)),
    bump_glue_levels(BjClause)
    ; true
    ),
    count_found_conflict(NewTotal, NewSinceRestart, _),
    asserta(backjump_clause(BjLevel, BjClause, LbdScore, BjSatVars, UsedVars, NewTotal)),
    asserta(backjump_level(BjLevel)),
    store_recent_stack_size(StackSize),
    count_learned_clause,
    possibly_decay_heuristic_values,
    ( \+ 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(BjClause, LbdScore) :-
    compute_lbd_score(BjClause, [], LbdScore).

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

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

count_found_conflict(Total1, SRes1, SRed1) :-
    log_conflict,
    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_var_occurrences_dict(_, []).

count_var_occurrences_dict(Dict, [Clause|T]) :-
    count_var_occurrences_from_clause_dict(Dict, Clause),
    count_var_occurrences_dict(Dict, T).

count_var_occurrences_from_clause_dict(_, []).

count_var_occurrences_from_clause_dict(Dict, [_-_-Pol-SatVarName|T]) :-
    var(Pol), % skip variables that are already propagated by deterministic unit propagation
    !,
    ( mutdict_get(Dict, SatVarName, Score)
    -> Score1 is Score + 1,
    mutdict_update(Dict, SatVarName, _, Score1)
    ; mutdict_put(Dict, SatVarName, 1)
    ),
    count_var_occurrences_from_clause_dict(Dict, T).

count_var_occurrences_from_clause_dict(Dict, [_|T]) :-
    count_var_occurrences_from_clause_dict(Dict, T).

count_var_occurrences_in_clauses(Clauses, DictItems) :-
    new_mutdict(Dict),
    count_var_occurrences_dict(Dict, Clauses), !,
    mutdict_items(Dict, DictItems), !.

create_solver_state(StateMutable) :-
    State = [cur_level:0,current_stack_size:0],
    create_mutable(solver_state(State), StateMutable).

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

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

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

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

decay_heuristic_values(DecayValue) :-
    Decay is (1/DecayValue),
    fibonacci_heap:mult_priority_of_all(Decay).

delete_from_heuristic(SatVarName) :-
    ( fibonacci_heap:elm_exists(SatVarName)
    -> fibonacci_heap:delete_elm_bt(SatVarName)
    ; % it can be the case that SatVarName has already been removed
    % from the mutable due to coroutines etc.; succeed in this case
    true
).

do_random_restart :-
    log_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_for_phase(SatVarName, StackInfo, SavedPol, Var, SolverEnv, StateMutable, NextLevel) :-
    ( ground(Var)
    -> add_error_fail(elim_var_for_phase, 'Decision variable is already ground: probably an error in the decision heuristic.', [SatVarName])
    ; true
    ),
    update_full_state(StateMutable, cur_level, NextLevel),
    get_next_assignment_count_on_level(ACount),
    ( StackInfo = (branch,(NextLevel,ACount),SavedPol,_OriginalClause),
    bt_log_sat_stack(StateMutable, SatVarName, SavedPol),
    debug_format_sat("Decide variable ~w with polarity ~w on level ~w", [SatVarName,SavedPol,NextLevel]),
    log_boolean_decision,
    Var = SavedPol
    ; \+ backjump_level(_),
    \+ severe_error_occurred,
    negate_polarity(SavedPol, NegSavedPol),
    StackInfo = (branch,(NextLevel,ACount),NegSavedPol,_OriginalClause),
    bt_log_sat_stack(StateMutable, SatVarName, NegSavedPol),
    debug_format_sat("Decide variable ~w with polarity ~w on level ~w", [SatVarName,NegSavedPol,NextLevel]),
    log_boolean_decision,
    Var = NegSavedPol
    ),
    elim_vars(SolverEnv, StateMutable).

elim_vars(SolverEnv, StateMutable) :-
    \+ severe_error_occurred,
    get_full_state(StateMutable, cur_level, CurLevel),
    NextLevel is CurLevel + 1,
    reset_assignment_count_on_level,
    ( % solution found
    fibonacci_heap:is_empty
    -> true
    ; elim_vars_from_asserted_heuristic_rapid_restart(SolverEnv, StateMutable, NextLevel)
).

elim_vars_from_asserted_heuristic_rapid_restart(SolverEnv, StateMutable, NextLevel) :-
    \+ backjump_level(_),
    \+ idl_unsat_core(_),
    get_sat_var_with_max_heuristic(SatVarName, MaxScore),
    get_from_solver_env(SolverEnv, pl_vars, PlVars),
    mutdict_get(PlVars, SatVarName, Var-SatVarName-_-StackInfo), % we need the variable's references
    debug_format_sat("Max heuristic value with score ~w is ~w", [MaxScore,SatVarName]),
    possibly_backjump(SolverEnv, StateMutable, NextLevel),
    ( saved_phase(SatVarName, SavedPol)
    -> % restore phase/polarity from cache for rapid restart
    SelectedPol = SavedPol,
    retract(saved_phase(SatVarName, _)), % don't undo when backtracking
    debug_format_sat("Restore phase of ~w", [SatVarName])
    ; % uninformed phase/polarity selection: start with truth
    SelectedPol = pred_true
    ),
    elim_var_for_phase(SatVarName, StackInfo, SelectedPol, Var, SolverEnv, StateMutable, NextLevel).

explain_theory_propagation(SolverEnv, TheoryPropSatVar, _, _, ExplainingClause) :-
    minimize_theory_explanations(false),
    !,
    debug_format_sat("Use complete lemma for theory explanation of ~w", [TheoryPropSatVar]),
    get_from_solver_env(SolverEnv, sat_bindings, SatBindings),
    get_clause_from_ground_bindings(SatBindings, _, _, [], TExplainingClause),
    get_from_solver_env(SolverEnv, pl_vars, PlVars),
    set_variable_references_in_clause(PlVars, TExplainingClause, ExplainingClause),
    debug_format_sat("finished explanation.", []).

explain_theory_propagation(SolverEnv, TheoryPropSatVar, TheoryPropLevel, TheoryPropPol, ExplainingClause) :-
    debug_format_sat("Explain theory propagation of ~w", [TheoryPropSatVar]),
    get_from_solver_env(SolverEnv, pl_vars, PlVars),
    mutdict_items(PlVars, PlVarsList),
    get_propagated_sat_vars(PlVarsList, 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),
    debug_format_sat("Compute unsat core for explanation: ", [], NegSmt),
    get_explanation_candidate_formula(SatVars, SatVarNameTuples, CandidateFormula),
    ( SatVarNameTuples = [_]
    -> safe_create_texpr(conjunct(CandidateFormula,NegSmt), pred, [], UnsatCore)
    ; temporary_set_preference(time_out, 25, Change1),
    temporary_set_preference(unsat_core_algorithm, linear, Change2),
    call_cleanup(unsat_core_with_fixed_conjuncts(CandidateFormula, NegSmt, TTUnsatCore),
    (reset_temporary_preference(unsat_core_algorithm, Change2),
    reset_temporary_preference(time_out, Change1))),
    safe_create_texpr(conjunct(TTUnsatCore,NegSmt), pred, [], TUnsatCore),
    ( strip_pos_keep_toplevel_conj(TUnsatCore, UnsatCore)
    -> true
    ; add_error_fail(strip_pos_keep_toplevel_conj, 'Removing WD POs for CDCL(T) failed for explaining theory propagation.', [unsat_core_with_wd:TUnsatCore])
    )
    ),
    get_from_solver_env(SolverEnv, t2b_env, T2BEnv),
    debug_format_sat("Computed unsat core for explanation: ", [], UnsatCore),
    (
    (
    predicate_to_sat(only_reuse, [], SatVars, T2BEnv, UnsatCore, _NewEnv, _, UnsatCoreSat, _NewSatVars),
    sat_conj_negate_to_clause(UnsatCoreSat, TExplainingClause)
    )
    -> true
    ; add_error_fail(sat_conj_negate_to_clause, 'Explaining theory propagation failed: Explanation cannot be transformed to SAT.', [unsat_core:UnsatCore])
    ),
    debug_format_sat("finished explanation.", []),
    set_variable_references_in_clause(PlVars, TExplainingClause, TTExplainingClause),
    sort(TTExplainingClause, ExplainingClause).

get_antecedent_assignments(_, _, SatVarName, _, _, ROriginalClause, Antecedent) :-
    is_list(ROriginalClause),
    !,
    select(_-_-_-SatVarName, ROriginalClause, TAntecedent), !,
    Antecedent = TAntecedent.

get_antecedent_assignments(SolverEnv, ConflictDLevel, SatVarName, RPol, theory, ROriginalClause, Antecedent) :-
    \+ is_list(ROriginalClause),
    !,
    explain_theory_propagation(SolverEnv, SatVarName, ConflictDLevel, RPol, OriginalClause),
    ROriginalClause = OriginalClause,
    select(_-_-_-SatVarName, OriginalClause, TAntecedent), !,
    Antecedent = TAntecedent.

get_antecedent_assignments(_, _, SatVarName, _, _, _, _) :-
    add_error_fail(get_antecedent_assignments, 'No antecedent assignments since variable has not been propagated.', SatVarName).

get_backjump_clause_and_level(SolverEnv, ConflictDLevel, ResolvedSoFar, TBjClause, MinBjClause, BjLevel, UsedVars) :-
    get_backjump_clause_and_level_sub(ConflictDLevel, 0, _, TBjClause, Resolver-RPol-RPropType-ROriginalClause, ThisLevelCount),
    ( ThisLevelCount == 1
    -> % break, first UIP
    BjClause = TBjClause,
    clause_minimization(ClauseMinType),
    ( ClauseMinType \== none
    -> ( minimize_clause(SolverEnv, ConflictDLevel, BjClause, ClauseMinType, MinBjClause), !
    ; add_error_fail(minimize_clause, 'Clause minimization failed: ', [BjClause])
    )
    ; MinBjClause = BjClause
    ),
    get_maximum_decision_level_other_than_current(MinBjClause, 0, ConflictDLevel, BjLevel),
    get_variables_used_in_cdcl(ResolvedSoFar, MinBjClause, UsedVars)
    ; ground(Resolver),
    resolve(SolverEnv, TBjClause, ConflictDLevel, Resolver, RPol, RPropType, ROriginalClause, NToExpand),
    mutdict_put(ResolvedSoFar, Resolver, Resolver),
    get_backjump_clause_and_level(SolverEnv, ConflictDLevel, ResolvedSoFar, NToExpand, MinBjClause, BjLevel, UsedVars)
).

get_backjump_clause_and_level_sub(_, ThisLevelCountAcc, ResolverAcc-_-RPol-RPropType-ROriginalClause, [], ResolverAcc-RPol-RPropType-ROriginalClause, ThisLevelCountAcc).

get_backjump_clause_and_level_sub(ConflictDLevel, ThisLevelCountAcc, ResolverAcc-RACount-RPol-RPropType-ROriginalClause, [(PropType,(Level,ACount),_,OriginalClause)-Pol-_-SatVarName|T], Resolver, ThisLevelCount) :-
    ( Level == ConflictDLevel
    -> NThisLevelCountAcc is ThisLevelCountAcc + 1
    ; NThisLevelCountAcc = ThisLevelCountAcc
    ),
    ( (
    Level == ConflictDLevel,
    % unit or theory propagation
    PropType \== branch,
    % use last assigned literal to resolve next
    ( var(ResolverAcc)
    ; ACount > RACount
    )
    )
    -> NResolverAcc = SatVarName-ACount-Pol-PropType-OriginalClause
    ; NResolverAcc = ResolverAcc-RACount-RPol-RPropType-ROriginalClause
    ),
    get_backjump_clause_and_level_sub(ConflictDLevel, NThisLevelCountAcc, NResolverAcc, T, Resolver, ThisLevelCount).

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

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

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

get_bindings_from_ids_acc([b(identifier(Name),IdType,IdInfo)|T], AccStackBindings, AccBindings, AccNames, AccTuples, AccPlVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :-
    NewAccBindings = [bind(Name,PrologVar)|AccBindings],
    % we add Prolog variables for stack infos to each var so that we do not have to maintain a genuine stack
    StackInfo = (_PropType, _Level, _Pol, _OriginalClause),
    NewAccStackBindings = [bind(Name,PrologVar)-StackInfo|AccStackBindings],
    NewAccTuples = [(b(identifier(Name),IdType,IdInfo),PrologVar,StackInfo)|AccTuples],
    !,
    ( member(smt_formula(SmtFormula), IdInfo)
    -> mutdict_put(AccPlVars, Name, PrologVar-Name-SmtFormula-StackInfo)
    ; % 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,[]),
    mutdict_put(AccPlVars, Name, PrologVar-Name-OptEq-StackInfo)
    ),
    get_bindings_from_ids_acc(T, NewAccStackBindings, NewAccBindings, [Name|AccNames], NewAccTuples, AccPlVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple).

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

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

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

get_clause_from_ground_bindings([bind(SatVarName,_)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :-
    % theory propagations during grounding are possibly undone in the stack if finding a contradiction during grounding waitflags
    % we restore such pending theory propagations here
    pending_theory_prop(SatVarName, SatVarPol),
    !,
    get_clause_from_ground_bindings(T, FSatVarName, FSatVarPol, [_-SatVarPol-_-SatVarName|Acc], TheoryLemmaClause).

get_clause_from_ground_bindings([bind(SatVarName,Pol)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :-
    ground(Pol),
    !,
    get_clause_from_ground_bindings(T, FSatVarName, FSatVarPol, [_-Pol-_-SatVarName|Acc], TheoryLemmaClause).

get_clause_from_ground_bindings([_|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :-
    get_clause_from_ground_bindings(T, FSatVarName, FSatVarPol, Acc, TheoryLemmaClause).

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

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

get_clause_from_negated_ground_bindings([bind(SatVarName,_)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :-
    % theory propagations during grounding are possibly undone in the stack if finding a contradiction during grounding waitflags
    % we restore such pending theory propagations here
    pending_theory_prop(SatVarName, SatVarPol),
    !,
    negate_polarity(SatVarPol, NegPol),
    get_clause_from_negated_ground_bindings(T, FSatVarName, FSatVarPol, [_-NegPol-_-SatVarName|Acc], TheoryLemmaClause).

get_clause_from_negated_ground_bindings([bind(SatVarName,_)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :-
    % set fixed polarity
    SatVarName == FSatVarName,
    !,
    negate_polarity(FSatVarPol, NegPol),
    get_clause_from_negated_ground_bindings(T, FSatVarName, FSatVarPol, [_-NegPol-_-SatVarName|Acc], TheoryLemmaClause).

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

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