1		% (c) 2019-2022 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(dpllt_sat_solver, [b_to_cnf/3,
6		create_solver_state/1,
7		sat/3,
8		sat/4,
9		restarts/1,
10		is_backjumping/0,
11		is_last_propagated_sat_var/2,
12		announce_bt_from_smt_solution/0,
13		store_idl_unsat_core/1,
14		log_theory_propagation_sat_stack/3,
15		set_variable_references_in_clauses/3,
16		remove_idl_unsat_core/0,
17		exhaustive_unit_propagate_cnf/4,
18		unit_propagate_cnf/4,
19		init_dynamic_solver_state/1,
20		get_bindings_from_ids/5,
21		portray_cnf/1,
22		portray_sat_stack/1,
23		cnf_to_smt/2]).
24
25		:- meta_predicate(asserta_once(0)).
26		:- meta_predicate(bt_retract_if_exists(0)).
27
28		:- use_module(library(lists)).
29		:- use_module(library(avl)).
30		:- use_module(library(heaps)).
31		:- use_module(library(ordsets)).
32		:- use_module(library(timeout)).
33		:- use_module(library(samsort)).
34		:- use_module(library(aggregate),[forall/2]).
35
36		:- use_module(smt_solvers_interface(ast_optimizer_for_smt)).
37		:- use_module(dpllt_solver('dpllt_pred_to_sat')).
38		:- use_module(dpllt_solver('dpllt_settings')).
39		:- use_module(dpllt_solver('symmetry_check/sat_symmetry_breaking')).
40		:- use_module(wdsrc(well_def_hyps), [empty_hyps/1]).
41		:- use_module(wdsrc(well_def_analyser), [compute_wd/4]).
42		:- use_module(probsrc(tools_portability), [exists_source/1]).
43		:- use_module(probsrc(bsyntaxtree),[get_texpr_expr/2,
44		safe_create_texpr/4,
45		disjunct_predicates/2,
46		conjunct_predicates/2,
47		conjunction_to_list/2]).
48		:- use_module(probsrc(debug)).
49		:- use_module(probsrc(error_manager), [add_error_fail/3,add_internal_error/2]).
50		:- use_module(probsrc(translate), [translate_bexpression/2]).
51		:- use_module(extrasrc(unsat_cores), [unsat_core_with_fixed_conjuncts/3,unsat_chr_core_list_with_auto_time_limit/5]).
52		:- use_module(probsrc(module_information), [module_info/2]).
53
54		:- module_info(group, dpllt).
55		:- module_info(description,'This module provides the SAT solver for DPLL(T) implementing CDCL with backjumping.').
56
57		:- dynamic backjump_wd_level/1, backjump_wd_clause/3, solver_name/1, incremental_mode/0, memoize_backjump_clause/3, backjump_clause/4, backjump_level/1, conflict_stats/3, saved_phase/2, bt_from_smt_solution/0, is_restart/0, exclude_sat_solution_clause/1, total_lbd_sum/1, recent_lbds_dl/2, recent_stack_sizes_dl/2, amount_clause_reductions/1, amount_learned_clauses/1, idl_unsat_core/1.
58		:- volatile backjump_wd_level/1, backjump_wd_clause/3, solver_name/1, incremental_mode/0, memoize_backjump_clause/3, backjump_clause/4, backjump_level/1, conflict_stats/3, saved_phase/2, bt_from_smt_solution/0, is_restart/0, exclude_sat_solution_clause/1, total_lbd_sum/1, recent_lbds_dl/2, recent_stack_sizes_dl/2, amount_clause_reductions/1, amount_learned_clauses/1, idl_unsat_core/1.
59
60		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
61		% A sat solver utilising delay declaration to implement watched literals.
62		% Authors: Jacob Howe and Andy King
63		%
64		% Extended for DPLL(T) with first UIP conflict-driven clause learning,
65		% theory propagation, branching heuristics, phase saving for rapid restarts,
66		% learned clause reduction, random restarts, and static SMT symmetry breaking.
67		% We implement a variant of VSIDS as follows:
68		% - one score for each variable initialized with the number of occurrences in all clauses
69		% - increase score by one for each variable occuring in a learned clause
70		% - divide all scores by 2 after each dpllt_settings:vsids_decay_frequency/1 conflict (favor recently learned clauses)
71		% Random restarts:
72		% restarts using either the Luby sequence or Glucose restarts
73		% Phase saving:
74		% - if backjump level is 0 because of learning a unit clause or a random restart,
75		% cache phases/polarities of variable assignments (see saved_phase/2)
76		% - when the decision heuristic decides to branch on a variable, pick the cached phase first if one exists
77		% Reducing learned clauses:
78		% - remove half of the learned clauses every "frequency_constant + constant_factor * x" conflicts, where x is the amount of clause reductions so far
79		% - keep clauses with small LBD (dpllt_settings:discard_clause_greater_lbd/1) forever
80		% incremental_mode/0 memoizes learned clauses and reuses them for the following calls.
81		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
82
83		% TO DO:
84		% [] ANRFA, VMTF, (ACIDS) branching heuristics
85		% -> empirical results by Biere and Fröhlich in "Evaluating CDCL Variable Scoring Schemes" have shown that EVSIDS is as good as the other heuristics
86		% [] polarity for heuristic scores (no branching when selecting max heuristic value?)
87		% -> first tests inidicated that this is slower
88		% (- FirstNewCutscheme (cf. https://www.aaai.org/Papers/JAIR/Vol22/JAIR-2210.pdf))
89		% [] improve implying constraint detection (e.g., :dpllt x > y & gt : {x+1} & y > gt)
90		% [] clause minimization (cf. Definition 9, "Towards Understanding and Harnessing the Potential of Clause Learning")
91		% [] use profiler
92		% [] check out "Advances in Symmetry Breaking for SAT Modulo Theories" by Dinliwal et al. for static SMT symmetry breaking
93
94		:- if(exists_source(library(mutdict))).
95		:- use_module(library(mutdict)).
96		:- else.
97		new_mutdict(Dict) :-
98		empty_avl(Avl),
99		create_mutable(Avl, Dict).
100
101		mutdict_put(Dict, Key, Value) :-
102		get_mutable(Avl, Dict),
103		avl_store(Key, Avl, Value, NewAvl),
104		update_mutable(NewAvl, Dict).
105
106		mutdict_get(Dict, Key, Value) :-
107		get_mutable(Avl, Dict),
108		avl_fetch(Key, Avl, Value).
109
110		mutdict_keys(Dict, Keys) :-
111		get_mutable(Avl, Dict),
112		avl_domain(Avl, Keys).
113
114		:- endif.
115
116		debug_format_sat(_, _) :-
117		debug_mode(off),
118		!.
119		debug_format_sat(Msg, Vars) :-
120		append(Msg, " (DPLL(T) SAT Solver)~n", NCodes),
121		atom_codes(NMsg, NCodes),
122		format(NMsg, Vars), !.
123
124		debug_format_sat(_, _, _) :-
125		debug_mode(off),
126		!.
127		debug_format_sat(Msg, Vars, Pred) :-
128		format(Msg, Vars),
129		translate:print_bexpr(Pred), nl, !.
130
131		%log_propagated_wd_pred(SatId) :-
132		% bt_asserta(propagated_wd_pred(SatId)).
133
134		clauses_to_sat_assert([], SatVars, T2BEnv, SatVars, T2BEnv, []).
135		clauses_to_sat_assert([SmtClause-LbdScore|T], SatVars, T2BEnv, NewSatVars, NewT2BEnv, [SatClause|NT]) :-
136		predicate_to_sat(normal, [], SatVars, T2BEnv, SmtClause, TT2BEnv, _, SatClause, TSatVars),
137		!,
138		asserta(backjump_clause(0, SatClause, LbdScore, [])),
139		debug_format_sat("Learn clause from prior run ~w~n", [SatClause]),
140		clauses_to_sat_assert(T, TSatVars, TT2BEnv, NewSatVars, NewT2BEnv, NT).
141		clauses_to_sat_assert([_|T], SatVars, T2BEnv, NewSatVars, NewT2BEnv, NT) :-
142		clauses_to_sat_assert(T, SatVars, T2BEnv, NewSatVars, NewT2BEnv, NT).
143
144		assert_memoized_clauses(SolverName, SolverEnv, NewSolverEnv) :-
145		findall(C-LbdScore, memoize_backjump_clause(SolverName, C, LbdScore), SmtClauses),
146		SmtClauses \== [],
147		!,
148		% learned clauses can be applied to all variables which are equal to new ids (see id_equality/3)
149		%findall(CPrime-LbdScore, (memoize_backjump_clause(SolverName, C, LbdScore), replace_ids_with_eq_ids_top_level(C, CPrime)), PrimedSmtClauses),
150		%append(SmtClauses, PrimedSmtClauses, FullClauses),
151		get_from_solver_env(SolverEnv, sat_vars, SatVars),
152		get_from_solver_env(SolverEnv, t2b_env, T2BEnv),
153		clauses_to_sat_assert(SmtClauses, SatVars, T2BEnv, NewSatVars, NewT2BEnv, _SatClauses),
154		get_bindings_from_ids(NewSatVars, NewSatBindings, NewSatVarNames, _, PrologSatVarTriple),
155		NewSolverEnv = [sat_vars:NewSatVars,sat_varnames:NewSatVarNames,sat_bindings:NewSatBindings,t2b_env:NewT2BEnv,pl_vars:PrologSatVarTriple].
156
157		learn_clauses_if_incremental(SolverName, StateMutable, SolverEnv, Clauses, NewSolverEnv, NewClauses) :-
158		incremental_mode,
159		format("INCREMENTAL MODE: Learn clauses from prior run", []),
160		assert_memoized_clauses(SolverName, SolverEnv, NewSolverEnv),
161		learn_asserted_clauses(StateMutable, 0, SolverEnv, Clauses, NewClauses), !.
162		learn_clauses_if_incremental(_, _, SolverEnv, Clauses, SolverEnv, Clauses).
163
164		% Given a set of boolean B identifiers. Create a list of bindings containing terms bind/2
165		% and a list of tuples of B identifier and corresponding Prolog variable used for sat solving.
166		get_bindings_from_ids(SatVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :-
167		get_bindings_from_ids_acc(SatVars, [], [], [], [], SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple), !.
168
169		get_bindings_from_ids_acc([], AccBindings, AccNames, AccTuples, AccPlVars, AccBindings, AccNames, AccTuples, AccPlVars).
170		get_bindings_from_ids_acc([b(identifier(Name),IdType,IdInfo)|T], AccBindings, AccNames, AccTuples, AccPlVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :-
171		NewAccBindings = [bind(Name,PrologVar)|AccBindings],
172		NewAccTuples = [(b(identifier(Name),IdType,IdInfo),PrologVar)|AccTuples],
173		!,
174		( member(smt_formula(SmtFormula), IdInfo)
175		-> NewAccPlVars = [PrologVar-Name-SmtFormula|AccPlVars]
176		; % plain SAT variable which is not reified with a theory solver, e.g., introduced by CNF optimization rewriting
177		OptEq = b(equal(b(identifier(Name),boolean,[]),b(boolean_true,boolean,[])),pred,[]),
178		NewAccPlVars = [PrologVar-Name-OptEq|AccPlVars]
179		),
180		get_bindings_from_ids_acc(T, NewAccBindings, [Name|AccNames], NewAccTuples, NewAccPlVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple).
181		get_bindings_from_ids_acc([_|T], AccBindings, AccNames, AccTuples, AccPlVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :-
182		get_bindings_from_ids_acc(T, AccBindings, AccNames, AccTuples, AccPlVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple).
183
184		%% sat(+SolverName, +SolverEnv, +Clauses).
185		% SolverEnv is a list [sat_vars:_, sat_bindings:_, t2b_env:_, pl_vars:_].
186		% sat_vars are boolean b/3 identifier ASTs for corresponding SAT variables in Clauses.
187		% sat_bindings is a list of terms bind/2 as used by the ProB constraint solver.
188		% t2b_env is the environment mapping SAT variable names and theory formulae used to
189		% translate B predicates to SAT.
190		% pl_vars is a list of triples PrologVar-SatVarName-SmtFormula.
191		% Note: init_dynamic_solver_state/1 has to be called before the call to sat/3
192		sat(SolverName, SolverEnv, Clauses) :-
193		debug_format_sat("Start SAT solving with solver ~w ", [SolverName]),
194		create_solver_state(StateMutable),
195		learn_clauses_if_incremental(SolverName, StateMutable, SolverEnv, Clauses, NewSolverEnv, NewClauses),
196		%init_heuristic(SolverEnv),
197		init_decision_heuristic(StateMutable, NewClauses),
198		sat_stateful_pre(NewSolverEnv, StateMutable, NewClauses).
199
200		%% sat(+SolverName, +SolverEnv, +StateMutable, +Clauses).
201		% Note: init_dynamic_solver_state/1 has to be called before the call to sat/4
202		sat(SolverName, SolverEnv, StateMutable, Clauses) :-
203		debug_format_sat("Start SAT solving with solver ~w ", [SolverName]),
204		learn_clauses_if_incremental(SolverName, StateMutable, SolverEnv, Clauses, NewSolverEnv, NewClauses),
205		init_decision_heuristic(StateMutable, NewClauses),
206		sat_stateful_pre(NewSolverEnv, StateMutable, NewClauses).
207
208		% Wrapper for sat_stateful_restart_cp/3 to enable backjumping to level 0 several times.
209		sat_stateful_pre(SolverEnv, StateMutable, Clauses) :-
210		sat_stateful_restart_cp(SolverEnv, StateMutable, Clauses).
211
212		sat_stateful_restart_cp(SolverEnv, StateMutable, Clauses) :-
213		( sat_stateful(SolverEnv, StateMutable, Clauses)
214		; % we either learned a unit-clause from conflict analysis or randomly restart
215		% in both cases, we learn all asserted backjump clauses
216		retract(backjump_level(0)),
217		( retract(is_restart)
218		-> debug_format_sat("backjump to level 0 random restart", [])
219		; debug_format_sat("backjump to level 0", [])
220		),
221		learn_asserted_clauses(StateMutable, 0, SolverEnv, Clauses, NewClauses),
222		sat_stateful_pre(SolverEnv, StateMutable, NewClauses)
223		).
224
225		%% sat_stateful(+Clauses, +StateMutable, +Clauses).
226		% DPLL with first UIP conflict-driven clause learning, two-watched literals, VSIDS branching heuristic,
227		% random restarts (Luby sequence with unit length 32), and phase saving for rapid restarts.
228		% See create_solver_state/1 for variable StateMutable.
229		sat_stateful(SolverEnv, StateMutable, Clauses) :-
230		problem_setup(SolverEnv, StateMutable, Clauses),
231		update_full_state(StateMutable, cur_level, 1),
232		get_from_solver_env(SolverEnv, pl_vars, PlVars), % TO DO: enable constant access by assuming an order of SolverEnv
233		%static_sat_symmetry_breaking(Clauses, SolverEnv, CurLevelMut, NewSolverEnv),
234		elim_vars(SolverEnv, StateMutable, PlVars).
235
236		%% elim_vars(+SolverEnv, +StateMutable, +PlVars).
237		elim_vars(SolverEnv, StateMutable, PlVars) :-
238		get_full_state(StateMutable, cur_level, CurLevel),
239		( % solution found
240		get_full_state(StateMutable, heuristic_avl, AVL),
241		empty_avl(AVL)
242		; update_full_state(StateMutable, decision_level, CurLevel),
243		%possibly_decay_heuristic_values, % only for vsids; remove for now
244		( elim_vars_from_asserted_heuristic_rapid_restart(SolverEnv, StateMutable, CurLevel, PlVars)
245		; % backjumping
246		backjump_level(C),
247		debug_format_sat("Current level is ~w", [CurLevel]),
248		C == CurLevel,
249		retract(backjump_level(C)),
250		debug_format_sat("~nbackjump branch prop level ~w", [CurLevel]),
251		get_clauses_to_learn_bump_scores(StateMutable, C, SolverEnv, ClausesToLearn),
252		problem_setup(SolverEnv, StateMutable, ClausesToLearn),
253		elim_vars(SolverEnv, StateMutable, PlVars)
254		)
255		).
256
257		%% handle_backjump_wd_clauses(+BjClausesNoRef, +LbdScore, +CurLevel, +StateMutable, +SolverEnv).
258		% Learn and convert to common backjump clause.
259		handle_backjump_wd_clauses(BjClausesNoRef, LbdScore, CurLevel, StateMutable, SolverEnv) :-
260		set_references_and_bump_scores(BjClausesNoRef, [], StateMutable, SolverEnv, ClausesToLearn),
261		!,
262		problem_setup(SolverEnv, StateMutable, ClausesToLearn),
263		bt_asserta(backjump_clause(CurLevel, BjClausesNoRef, LbdScore, [])).
264
265		%% elim_vars_from_asserted_heuristic_rapid_restart(+SolverEnv, +StateMutable, +CurLevel, +PlVars).
266		% Variable State Independent Decaying Sum (VSIDS) branching heuristic.
267		% Initially, each variable is assigned the number of its occurrences in all clauses as its score.
268		% Afterwards, for each conflict clause, the scores of the variables occuring in the clause are increased by bump_heuristic_score_for_type.
269		% Periodically divides all scores by a constant for vsids (see possibly_decay_heuristic_values/0).
270		% Possibly choose the polarity to assign first using saved_phase/2 for rapid restarts.
271		% Note: Assert state before propagation because Var is bound to coroutines.
272		% OriginalClause not necessary for decision variables in the stack because
273		% they are not expanded during conflict analysis.
274		elim_vars_from_asserted_heuristic_rapid_restart(SolverEnv, StateMutable, CurLevel, PlVars) :-
275		\+ backjump_level(_),
276		\+ backjump_wd_level(_),
277		\+ idl_unsat_core(_),
278		max_heuristic_values(StateMutable, MaxScore, SatVarNames),
279		debug_format_sat("Max heuristic values with score ~w are ~w", [MaxScore,SatVarNames]),
280		get_decision_variable_from_list(SatVarNames, SatVarName),
281		delete_state_instance(StateMutable, heuristic_avl, (SatVarName, MaxScore)),
282		get_pl_var_for_sat_id(SatVarName, PlVars, Var),
283		NextLevel is CurLevel + 1,
284		( saved_phase(SatVarName, SavedPol)
285		-> elim_var_from_saved_phase(SatVarName, SavedPol, Var, SolverEnv, StateMutable, CurLevel, PlVars)
286		; % uninformed phase/polarity selection
287		( bt_log_sat_stack(StateMutable, SatVarName, branch, CurLevel, pred_true, _OriginalClause),
288		debug_format_sat("Decide variable ~w with polarity ~w on level ~w", [SatVarName,pred_true,CurLevel]),
289		%get_theory_formula_for_satvar(SolverEnv, SatVarName, TheoryFormula),
290		%translate:print_bexpr(TheoryFormula),nl,
291		Var = pred_true,
292		update_full_state(StateMutable, cur_level, NextLevel),
293		elim_vars(SolverEnv, StateMutable, PlVars)
294		; ( \+ backjump_level(_),
295		\+ backjump_wd_level(_)
296		; retract(backjump_wd_level(CurLevel)), % backjump to wd decision without CDCL (custom backjumping)
297		retract(backjump_wd_clause(_, BjClauseNoRef, LbdScore)),
298		handle_backjump_wd_clauses([BjClauseNoRef], LbdScore, CurLevel, StateMutable, SolverEnv)
299		),
300		%( learn_idl_core(StateMutable, CurLevel, SolverEnv)
301		%; true
302		%),
303		( ground(Var)
304		-> true
305		; bt_log_sat_stack(StateMutable, SatVarName, branch, CurLevel, pred_false, _OriginalClause),
306		debug_format_sat("Decide variable ~w with polarity ~w on level ~w", [SatVarName,pred_false,CurLevel]),
307		%get_theory_formula_for_satvar(SolverEnv, SatVarName, TheoryFormula),
308		%translate:print_bexpr(TheoryFormula),nl,
309		Var = pred_false
310		),
311		update_full_state(StateMutable, cur_level, NextLevel),
312		elim_vars(SolverEnv, StateMutable, PlVars)
313		)
314		).
315
316		%% elim_var_from_saved_phase(+SatVarName, +SavedPol, +Var, +SolverEnv, +StateMutable, +CurLevel, +PlVars).
317		% Restore phase/polarity for +SatVarName from cache for rapid restart.
318		elim_var_from_saved_phase(SatVarName, SavedPol, Var, SolverEnv, StateMutable, CurLevel, PlVars) :-
319		get_pl_var_for_sat_id(SatVarName, PlVars, Var),
320		NextLevel is CurLevel + 1,
321		( bt_log_sat_stack(StateMutable, SatVarName, branch, CurLevel, SavedPol, _OriginalClause),
322		debug_format_sat("Phase Restore: Decide variable ~w with polarity ~w on level ~w", [SatVarName,SavedPol,CurLevel]),
323		Var = SavedPol,
324		update_full_state(StateMutable, cur_level, NextLevel),
325		bt_retract(saved_phase(SatVarName, SavedPol)),
326		elim_vars(SolverEnv, StateMutable, PlVars)
327		; ( \+ backjump_level(_),
328		\+ backjump_wd_level(_)
329		; retract(backjump_wd_level(CurLevel)), % backjump to wd decision without CDCL (custom backjumping)
330		retract(backjump_wd_clause(_, BjClauseNoRef, LbdScore)),
331		handle_backjump_wd_clauses([BjClauseNoRef], LbdScore, CurLevel, StateMutable, SolverEnv)
332		),
333		%( learn_idl_core(StateMutable, CurLevel, SolverEnv)
334		%; true
335		%),
336		( ground(Var)
337		-> true
338		; negate_polarity(SavedPol, NegSavedPol),
339		bt_log_sat_stack(StateMutable, SatVarName, branch, CurLevel, NegSavedPol, _OriginalClause),
340		debug_format_sat("Phase Restore Failed: Decide variable ~w with polarity ~w on level ~w", [SatVarName,NegSavedPol,CurLevel]),
341		% remove saved phase permanently once it has failed to evaluate to true
342		%retract(saved_phase(SatVarName, SavedPol)),
343		Var = NegSavedPol
344		),
345		update_full_state(StateMutable, cur_level, NextLevel),
346		elim_vars(SolverEnv, StateMutable, PlVars)
347		).
348
349		problem_setup(_, _, []).
350		problem_setup(SolverEnv, StateMutable, [Clause|Clauses]) :-
351		clause_setup(SolverEnv, StateMutable, Clause),
352		problem_setup(SolverEnv, StateMutable, Clauses).
353
354		clause_setup(SolverEnv, StateMutable, Clause) :-
355		Clause = [Pol-Var-SatVarName|Triples],
356		set_watch(SolverEnv, StateMutable, Clause, Triples, Var, Pol, SatVarName).
357
358		% Enforce well-definedness before cdcl if unit propagation of predicate that entails the well-definedness condition caused a theory conflict.
359		/*enforce_well_definedness(SolverEnv, StateMutable, SatVarName, Var) :-
360		get_top_level_wd_condition(SolverEnv, SatVarName, TopLevelWdPred, PredWithWdCondition),
361		!,
362		debug_format_sat("Enforce well-definedness for ~w ", [SatVarName]),
363		get_from_solver_env(SolverEnv, t2b_env, T2BEnv),
364		get_from_solver_env(SolverEnv, sat_vars, SatVars),
365		debug_format_sat("Top level wd pred ", [], TopLevelWdPred),
366		debug_format_sat("Pred with wd condition ", [], PredWithWdCondition),
367		predicate_to_sat(only_reuse, [], SatVars, T2BEnv, TopLevelWdPred, _NewEnv1, _, TopLevelWdBool, _NewSatVars1),
368		predicate_to_sat(only_reuse, [], SatVars, T2BEnv, PredWithWdCondition, _NewEnv2, _, PredWithWdConditionBool, _NewSatVars2),
369		TopLevelWdBool = b(equal(b(identifier(WdSatVarName),_,_),_),pred,[]),
370		PredWithWdConditionBool = b(equal(b(identifier(PredWithWdSatVarName),_,_),_),pred,[]),
371		get_from_solver_env(SolverEnv, pl_vars, PlVars),
372		memberchk(Var-WdSatVarName-_, PlVars),
373		get_full_state(StateMutable, cur_level, CurLevel),
374		set_variable_references_in_clause(PlVars, [pred_false-_-PredWithWdSatVarName,pred_true-_-WdSatVarName], OriginalClause),
375		debug_format_sat("OriginalClause for well-definedness is ~w ", [OriginalClause]),
376		worsen_scores_for_vars_in_clause(StateMutable, OriginalClause),
377		bt_log_sat_stack(StateMutable, WdSatVarName, branch, CurLevel, pred_true, OriginalClause),
378		Var = pred_true.
379		%; bt_log_sat_stack(StateMutable, WdSatVarName, branch, CurLevel, pred_false, OriginalClause),
380		% Var = pred_false
381		%).
382		enforce_well_definedness(_, _, _, _).*/
383
384		clause_contains_decided_pred(_, _, [], _, Acc, Acc).
385		clause_contains_decided_pred(SolverEnv, StateMutable, [_-_-SatVarName|T], SatStack, Acc, WdDecisionLevels) :-
386		get_from_sat_stack_or_explain_theory_propagation(SolverEnv, StateMutable, SatVarName, PropType, Level, AssignedPol, _),
387		AssignedPol == pred_true, % assuming that we first assign true when deciding for a polarity
388		PropType == branch,
389		!,
390		clause_contains_decided_pred(SolverEnv, StateMutable, T, SatStack, [Level|Acc], WdDecisionLevels).
391		clause_contains_decided_pred(SolverEnv, StateMutable, [_|T], SatStack, Acc, WdDecisionLevels) :-
392		clause_contains_decided_pred(SolverEnv, StateMutable, T, SatStack, Acc, WdDecisionLevels).
393
394		assert_backjump_wd_clause(SatStack, BjLevel, BjClause) :-
395		compute_lbd_score(SatStack, BjClause, LbdScore),
396		asserta(backjump_wd_clause(BjLevel, BjClause, LbdScore)).
397
398		set_polarity_of_var_explicitly(_, _, [], []).
399		set_polarity_of_var_explicitly(SatVarName, Pol, [CPol-CVar-CName|T], ConflictClause) :-
400		var(CVar),
401		SatVarName == CName,
402		!,
403		ConflictClause = [CPol-Pol-CName|T].
404		set_polarity_of_var_explicitly(SatVarName, Pol, [Triple|T], [Triple|NT]) :-
405		set_polarity_of_var_explicitly(SatVarName, Pol, T, NT).
406
407
408		set_watch(_, StateMutable, OriginalClause, [], Var, Pol, SatVarName) :-
409		Var == Pol,
410		delete_state_instance(StateMutable, heuristic_avl, (SatVarName, _)),
411		bt_retract_if_exists(saved_phase(SatVarName, _)),
412		worsen_scores_for_vars_in_clause(StateMutable, OriginalClause).
413		set_watch(SolverEnv, StateMutable, OriginalClause, [], Var, Pol, _) :-
414		ground(Var),
415		Var \== Pol,
416		debug_format_sat("sat conflict", []),
417		get_complete_theory_lemma(SolverEnv, TheoryLemmaClause),
418		possibly_bt_from_smt_solution(StateMutable, TheoryLemmaClause),
419		get_full_state(StateMutable, current_stack_size, StackSize),
420		get_full_state(StateMutable, cur_level, CurLevel),
421		compute_and_assert_backjump_clause(SolverEnv, StateMutable, StackSize, CurLevel, OriginalClause),
422		fail.
423		set_watch(SolverEnv, StateMutable, OriginalClause, [], Var, Pol, SatVarName) :-
424		var(Var),
425		get_full_state(StateMutable, cur_level, CurLevel),
426		debug_format_sat("unit propagation of ~w with polarity ~w on level ~w due to clause ~w", [SatVarName,Pol,CurLevel,OriginalClause]),
427		%translate:print_bexpr(TheoryFormula),nl,
428		bt_log_sat_stack(StateMutable, SatVarName, unit, CurLevel, Pol, OriginalClause),
429		( Var = Pol,
430		%( Pol == pred_true
431		%-> enforce_well_definedness(SolverEnv, StateMutable, SatVarName, Var)
432		%; true
433		%),
434		delete_state_instance(StateMutable, heuristic_avl, (SatVarName, _)),
435		bt_retract_if_exists(saved_phase(SatVarName, _)),
436		worsen_scores_for_vars_in_clause(StateMutable, OriginalClause),
437		( true
438		; % remove idl unsat core from higher decision level on backtracking
439		remove_idl_unsat_core,
440		fail
441		)
442		; % theory conflict: if Var = Pol triggered a SAT conflict instead,
443		% a backjump clause has been computed and backjump_level/1 is asserted
444		\+ backjump_level(_), % skip when backjumping
445		\+ backjump_wd_level(_),
446		get_last_decision_level(StateMutable, LastDLevel), % skip if no decision so far
447		LastDLevel \== 1, % just backtrack if last decision level is 1
448		get_complete_theory_lemma(SolverEnv, TheoryLemmaClause),
449		possibly_bt_from_smt_solution(StateMutable, TheoryLemmaClause),
450		( learn_idl_core(StateMutable, CurLevel, SolverEnv)
451		-> true
452		; debug_format_sat("theory conflict on level ~w", [CurLevel]),
453		get_conflict_clause_for_theory_conflict(SatVarName, Pol, SolverEnv, TConflictClause),
454		get_full_state(StateMutable, sat_stack, SatStack),
455		% explicitly set the polarity which failed to be assigned above in line 414 for conflict analysis (possibly part of the unsat core)
456		set_polarity_of_var_explicitly(SatVarName, Pol, TConflictClause, ConflictClause),
457		get_maximum_decision_level_other_than_current(ConflictClause, SatStack, 0, 0, ConflictLevel),
458		% it can be the case that ProB first recognizes unsatisfiable after grounding waitflags; the last decision level is then not necessarily the conflict level
459		( ConflictLevel =< CurLevel,
460		clause_contains_decided_pred(SolverEnv, StateMutable, ConflictClause, SatStack, [], WdDecisionLevels),
461		WdDecisionLevels \== []
462		-> min_member(BjLevel, WdDecisionLevels),
463		negate_polarities(ConflictClause, BjClause),
464		asserta(backjump_wd_level(BjLevel)),
465		assert_backjump_wd_clause(SatStack, BjLevel, BjClause),
466		debug_format_sat("theory conflict on level ~w due to pred with wd", [BjLevel])
467		; debug_format_sat("theory conflict on level ~w after unsat core computation", [ConflictLevel]),
468		%ConflictLevel \== 0,
469		get_full_state(StateMutable, current_stack_size, StackSize),
470		%portray_sat_stack(StateMutable),
471		compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, _BjLevel)
472		)
473		),
474		fail
475		).
476		set_watch(SolverEnv, StateMutable, OriginalClause, [Pol2-Var2-Name2|Triples], Var1, Pol1, Name1):-
477		watch(SolverEnv, StateMutable, OriginalClause, Var1, Pol1, Name1, Var2, Pol2, Name2, Triples).
478
479		:- block watch(?, ?, ?, -, ?, ?, -, ?, ?, ?).
480		watch(SolverEnv, StateMutable, OriginalClause, Var1, Pol1, Name1, Var2, Pol2, Name2, Triples) :-
481		( nonvar(Var1)
482		-> update_watch(SolverEnv, StateMutable, OriginalClause, Var1, Pol1, Name1, Var2, Pol2, Name2, Triples)
483		; update_watch(SolverEnv, StateMutable, OriginalClause, Var2, Pol2, Name2, Var1, Pol1, Name1, Triples)
484		).
485
486		update_watch(SolverEnv, StateMutable, OriginalClause, Var1, Pol1, Name1, Var2, Pol2, Name2, Triples) :-
487		( Var1 == Pol1
488		-> delete_state_instance(StateMutable, heuristic_avl, (Name1, _)),
489		bt_retract_if_exists(saved_phase(Name1, _)),
490		worsen_scores_for_vars_in_clause(StateMutable, OriginalClause)
491		; set_watch(SolverEnv, StateMutable, OriginalClause, Triples, Var2, Pol2, Name2)
492		).
493
494		retract_once(Assertion) :-
495		retract(Assertion),
496		!.
497
498		/*get_top_level_wd_condition(SolverEnv, SatVarName, TopLevelWdPred, PredWithWdCondition) :-
499		get_from_solver_env(SolverEnv, sat_vars, SatVars),
500		member(b(identifier(SatVarName),_,Info), SatVars),
501		member(contains_top_level_wd_condition(TopLevelWdPred,PredWithWdCondition), Info).*/
502
503		%% is_backjumping.
504		is_backjumping :-
505		backjump_level(_).
506		is_backjumping :-
507		backjump_wd_level(_).
508
509		%% is_last_propagated_sat_var(+StateMutable, +SatVarName).
510		is_last_propagated_sat_var(StateMutable, SatVarName) :-
511		get_full_state(StateMutable, sat_stack, Stack),
512		% TO DO: improve, can be mutable dict
513		avl_fetch(SatVarName, Stack, _).
514
515		log_theory_propagation_sat_stack(StateMutable, SatVarName, SatPrologVar) :-
516		get_full_state(StateMutable, cur_level, CurLevel),
517		!,
518		debug_format_sat("Theory propagation of ~w with polarity ~w", [SatVarName,SatPrologVar]),
519		% explanation (OriginalClause) is computed lazily for conflict analysis if necessary, see explain_theory_propagation/5
520		bt_log_sat_stack(StateMutable, SatVarName, theory, CurLevel, SatPrologVar, _).
521
522		% Calculating the unsat core in the idl solver is no overhead so it might be worthwhile to learn
523		% unsat cores on the decision level as well.
524		learn_idl_core(StateMutable, _CurLevel, SolverEnv) :-
525		retract(idl_unsat_core(Core)),
526		remove_idl_unsat_core,
527		!,
528		get_conflict_clause_from_unsat_core(Core, SolverEnv, ConflictClause),
529		get_full_state(StateMutable, current_stack_size, StackSize),
530		get_full_state(StateMutable, cur_level, CurLevel),
531		compute_and_assert_backjump_clause(SolverEnv, StateMutable, StackSize, CurLevel, ConflictClause).
532
533		% Log variable assignments.
534		% Effect is undone on backtracking. If backjump level is zero on backtracking, i.e.,
535		% a random restart occured or a unit-clause has been learned, save the phase to restore
536		% assignments afterwards for a rapid restart.
537		bt_log_sat_stack(StateMutable, SatVarName, PropType, CurLevel, Pol, OriginalClause) :-
538		add_state_instance(StateMutable, sat_stack, (SatVarName, PropType, CurLevel, Pol, OriginalClause)),
539		( increase_stack_size(StateMutable)
540		; is_restart,
541		asserta_once(saved_phase(SatVarName, Pol)),
542		fail
543		).
544
545		increase_stack_size(StateMutable) :-
546		get_full_state(StateMutable, current_stack_size, Old),
547		New is Old + 1, !,
548		update_full_state(StateMutable, current_stack_size, New).
549
550		%% possibly_bt_from_smt_solution(+StateMutable, +TheoryLemmaClause).
551		% Backtracking from an SMT solution which should not be handled as a theory conflict.
552		possibly_bt_from_smt_solution(StateMutable, TheoryLemmaClause) :-
553		retract(bt_from_smt_solution),
554		!,
555		% backjump to the last decision level without computing a conflict clause
556		% but excluding the last SAT solution when backtracking after finding an SMT solution
557		get_last_decision_level(StateMutable, Level),
558		asserta(exclude_sat_solution_clause(TheoryLemmaClause)),
559		asserta(backjump_level(Level)),
560		fail.
561		possibly_bt_from_smt_solution(_, _).
562
563		negate_smt_formula(b(negation(Smt),pred,[]), NegSmt) :-
564		!,
565		NegSmt = Smt.
566		negate_smt_formula(Smt, b(negation(Smt),pred,[])).
567
568		%% explain_theory_propagation(+SolverEnv, +SatStack, +TheoryPropSatVar, +TheoryPropLevel, +TheoryPropPol, -ExplainingClause).
569		explain_theory_propagation(SolverEnv, SatStack, TheoryPropSatVar, TheoryPropLevel, TheoryPropPol, ExplainingClause) :-
570		debug_format_sat("Explain theory propagation", []),
571		avl_to_list(SatStack, SatStackList),
572		findall((SatVarName-Pol), (member(SatVarName-(_,Level,Pol,_), SatStackList), Level<TheoryPropLevel), SatVarNameTuples),
573		get_from_solver_env(SolverEnv, sat_vars, SatVars),
574		get_smt_formula_from_vars_for_sat_pol(SatVars, TheoryPropSatVar, TheoryPropPol, SmtFormula),
575		negate_smt_formula(SmtFormula, NegSmt),
576		get_explanation_candidate_formula(SatVars, SatVarNameTuples, CandidateFormula),
577		( SatVarNameTuples = [_]
578		-> UnsatCore = b(conjunct(CandidateFormula,NegSmt),pred,[])
579		; temporary_set_unsat_core_timeout,
580		unsat_core_with_fixed_conjuncts(CandidateFormula, NegSmt, TUnsatCore),
581		UnsatCore = b(conjunct(TUnsatCore,NegSmt),pred,[]),
582		preferences:reset_temporary_preference(time_out)
583		),
584		%nl, write('Explanation Core: '), nl,translate:print_bexpr(UnsatCore),nl,
585		get_from_solver_env(SolverEnv, t2b_env, T2BEnv),
586		predicate_to_sat(only_reuse, [], SatVars, T2BEnv, UnsatCore, _NewEnv, _, UnsatCoreSat, _NewSatVars),
587		sat_conj_negate_to_clause(UnsatCoreSat, TExplainingClause),
588		get_from_solver_env(SolverEnv, pl_vars, PlVars),
589		set_variable_references_in_clause(PlVars, TExplainingClause, ExplainingClause).% TO DO: learn theory lemma?
590
591		get_explanation_candidate_formula(SatVars, [SatVarName-Pol|T], CandidateFormula) :-
592		get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula),
593		!,
594		get_explanation_candidate_formula_acc(SatVars, T, SmtFormula, CandidateFormula).
595		get_explanation_candidate_formula(SatVars, [_|T], CandidateFormula) :-
596		% can be artificial SAT variable introduced by cnf rewriting
597		get_explanation_candidate_formula(SatVars, T, CandidateFormula).
598
599		get_explanation_candidate_formula_acc(_, [], Acc, Acc).
600		get_explanation_candidate_formula_acc(SatVars, [SatVarName-Pol|T], Acc, CandidateFormula) :-
601		get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula),
602		!,
603		NAcc = b(conjunct(SmtFormula,Acc),pred,[]),
604		get_explanation_candidate_formula_acc(SatVars, T, NAcc, CandidateFormula).
605		get_explanation_candidate_formula_acc(SatVars, [_|T], Acc, CandidateFormula) :-
606		get_explanation_candidate_formula_acc(SatVars, T, Acc, CandidateFormula).
607
608		get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula) :-
609		memberchk(b(identifier(SatVarName),_,Info), SatVars),
610		member(smt_formula(TSmtFormula), Info),
611		get_smt_formula_for_sat_pol(TSmtFormula, Pol, SmtFormula).
612
613		get_smt_formula_for_sat_pol(TSmtFormula, Pol, SmtFormula) :-
614		( Pol == pred_true
615		-> SmtFormula = TSmtFormula
616		; TSmtFormula = b(negation(SmtFormula),pred,[])
617		-> true
618		; TSmtFormula = b(_,_,Info),
619		SmtFormula = b(negation(TSmtFormula),pred,Info)
620		).
621
622		%% max_heuristic_values(+StateMutable, -MaxScore, -SatVarNames).
623		% Fails if there are no heuristic scores.
624		max_heuristic_values(StateMutable, MaxScore, SatVarNames) :-
625		get_full_state(StateMutable, heuristic_avl, AVL),
626		avl_range(AVL, Range), % TO DO: improve datastructure, e.g. max heap
627		max_member(MaxScore, Range),
628		!,
629		findall(SatVarName, (avl_member(SatVarName, AVL, S), S == MaxScore), SatVarNames).
630
631		%get_heuristic_values_for_score(Heap, Score, [SatVarName|NT]) :-
632		% get_from_heap(Heap, MinScore, SatVarName, NewHeap),
633		% MinScore == Score,
634		% !,
635		% get_heuristic_values_for_score(NewHeap, Score, NT).
636		%get_heuristic_values_for_score(_, _, []).
637
638		% Skip on backjumping.
639		get_decision_variable_from_list(SatVarNames, SatVarName) :-
640		memberchk(SatVarName, SatVarNames), % important for performance to get only one member
641		\+ backjump_level(_),
642		\+ backjump_wd_level(_),
643		\+ idl_unsat_core(_).
644
645		bt_retract_if_exists(Assertion) :-
646		( dpllt_sat_solver:Assertion
647		-> bt_retract(Assertion)
648		; true
649		).
650
651		% Not undone on backtracking.
652		/*
653		If this is used we need to store the mutable since operations are undone on backtracking.
654		possibly_decay_heuristic_values(StateMutable) :-
655		decision_heuristic(Heuristic),
656		Heuristic == vsids,
657		conflict_stats(total(AC), _, _),
658		AC \== 0,
659		vsids_decay_frequency(I),
660		C is AC mod I,
661		C == 0,
662		debug_format_sat("~nDecay heuristic scores", []),
663		!,
664		vsids_decay_value(Val),
665		decay_heuristic_values(StateMutable, Val).
666		possibly_decay_heuristic_values(_).
667
668		% Not undone on backtracking.
669		decay_heuristic_values(StateMutable, DecayValue) :-
670		retract(heuristic_tuple(SatVarName, Score)),
671		!,
672		NewScore is Score / DecayValue,
673		decay_heuristic_values(DecayValue),
674		asserta(heuristic_tuple(SatVarName, NewScore)).
675		decay_heuristic_values(_, _).*/
676
677		% Each variable in each polarity has a counter, initialized to 0.
678		/*init_heuristic(SolverEnv) :-
679		get_from_solver_env(SolverEnv, sat_varnames, SatVarNames),
680		init_heuristic_tuples_from_vars(SatVarNames).
681
682		init_heuristic_tuples_from_vars([]).
683		init_heuristic_tuples_from_vars([SatVarName|T]) :-
684		asserta(heuristic_tuple(SatVarName, 0)),
685		%asserta(heuristic_tuple(SatVarName, pred_true, 0)),
686		%asserta(heuristic_tuple(SatVarName, pred_false, 0)),
687		init_heuristic_tuples_from_vars(T).*/
688
689		% Each variable is initially assigned the number of its occurrences in all clauses as its score.
690		% Variable scores are not split for polarities.
691		init_decision_heuristic(StateMutable, Clauses) :-
692		count_occurrences_in_clauses(Clauses, VarScoreTuples),
693		add_heuristic_tuples(StateMutable, VarScoreTuples).
694
695		add_heuristic_tuples(_, []).
696		add_heuristic_tuples(StateMutable, [(SatVarName,Score)|T]) :-
697		add_state_instance(StateMutable, heuristic_avl, (SatVarName,Score)),
698		add_heuristic_tuples(StateMutable, T).
699
700		:- dynamic occurrences/2.
701		:- volatile occurrences/2.
702
703		count_occurrences_in_clauses(Clauses, VarScoreTuples) :-
704		retractall(occurrences(_, _)),
705		assert_count_occurrences(Clauses),
706		findall((SatVarName,Score), retract(occurrences(SatVarName, Score)), VarScoreTuples), !.
707
708		assert_count_occurrences([]).
709		assert_count_occurrences([Clause|T]) :-
710		assert_count_occurrences_from_clause(Clause),
711		assert_count_occurrences(T).
712
713		% TO DO: use avl tree instead of assert
714		assert_count_occurrences_from_clause([]).
715		assert_count_occurrences_from_clause([_-_-SatVarName|T]) :-
716		( retract(occurrences(SatVarName, Score))
717		-> Score1 is Score + 1,
718		asserta(occurrences(SatVarName, Score1))
719		; asserta(occurrences(SatVarName, 1))
720		),
721		assert_count_occurrences_from_clause(T).
722
723		get_unassigned_vars([], _, []).
724		get_unassigned_vars([SatVarName|T], PlVars, UnassignedVars) :-
725		get_pl_var_for_sat_id(SatVarName, PlVars, PlVar),
726		var(PlVar),
727		!,
728		get_unassigned_vars(T, PlVars, NT),
729		UnassignedVars = [SatVarName|NT].
730		get_unassigned_vars([_|T], PlVars, UnassignedVars) :-
731		get_unassigned_vars(T, PlVars, UnassignedVars).
732
733		update_heuristic_scores_for_vars(StateMutable, UsedVars, PlVars) :-
734		get_unassigned_vars(UsedVars, PlVars, UnassignedVars),
735		decision_heuristic(Type),
736		update_heuristic_scores(StateMutable, Type, UnassignedVars).
737
738		% Update heuristic scores from learned clauses for VSIDS branching heuristic.
739		update_heuristic_scores_for_clauses(StateMutable, ClausesToLearn) :-
740		% we don't want to bump scores for already assigned variables, i.e., don't add them to the heuristic again
741		get_non_ground_varnames_occurring_in_clauses(ClausesToLearn, SatVarNames),
742		decision_heuristic(Type),
743		update_heuristic_scores(StateMutable, Type, SatVarNames).
744
745		get_non_ground_varnames_occurring_in_clauses(ClausesToLearn, SatVarNames) :-
746		get_non_ground_varnames_occurring_in_clauses(ClausesToLearn, [], SatVarNames).
747
748		get_non_ground_varnames_occurring_in_clauses([], Acc, Acc).
749		get_non_ground_varnames_occurring_in_clauses([Clause|T], Acc, SatVarNames) :-
750		get_non_ground_varnames_occurring_in_clause(Clause, Acc, NewAcc),
751		get_non_ground_varnames_occurring_in_clauses(T, NewAcc, SatVarNames).
752
753		get_non_ground_varnames_occurring_in_clause([], Acc, Acc).
754		get_non_ground_varnames_occurring_in_clause([_-Var-SatVarName|T], Acc, SatVarNames) :-
755		var(Var),
756		!,
757		ord_add_element(Acc, SatVarName, NewAcc),
758		get_non_ground_varnames_occurring_in_clause(T, NewAcc, SatVarNames).
759		get_non_ground_varnames_occurring_in_clause([_|T], Acc, SatVarNames) :-
760		get_non_ground_varnames_occurring_in_clause(T, Acc, SatVarNames).
761
762		%% update_heuristic_scores(+StateMutable, +Type, +SatVarNames).
763		% Type is either vsids or evsids.
764		% SatVarNames are the variable names occurring in learned clauses.
765		% Effect is undone on backtracking.
766		update_heuristic_scores(StateMutable, Type, SatVarNames) :-
767		conflict_stats(total(TotalConflicts), _, _),
768		get_full_state(StateMutable, heuristic_avl, Avl),
769		update_heuristic_scores(Avl, TotalConflicts, Type, NAvl, SatVarNames),
770		update_full_state(StateMutable, heuristic_avl, NAvl).
771
772		update_heuristic_scores(AvlAcc, _, _, AvlAcc, []).
773		update_heuristic_scores(AvlAcc, TotalConflicts, Type, NAvl, [SatVarName|T]) :-
774		avl_fetch(SatVarName, AvlAcc, OldScore),
775		!,
776		bump_heuristic_score_for_type(Type, TotalConflicts, OldScore, NewScore),
777		avl_change(SatVarName, AvlAcc, _, NAvlAcc, NewScore),
778		update_heuristic_scores(NAvlAcc, TotalConflicts, Type, NAvl, T).
779		update_heuristic_scores(AvlAcc, TotalConflicts, Type, NAvl, [_|T]) :-
780		% guided backjump to decision due to wd, not all vars necessarily propagated
781		update_heuristic_scores(AvlAcc, TotalConflicts, Type, NAvl, T).
782
783		% v_s + 1
784		bump_heuristic_score_for_type(vsids, _, OldScore, NewScore) :-
785		NewScore is OldScore + 1.
786		% v_s + f^(-k), where f is evsids_f_value/1 and it is the k-th conflict
787		bump_heuristic_score_for_type(evsids, TotalConflicts, OldScore, NewScore) :-
788		evsids_f_value(FVal),
789		NewScore is ceiling(OldScore + FVal**(-TotalConflicts)).
790
791		get_pl_var_for_sat_id(SatVarName, PlVars, Var) :-
792		member((Var-SatVarName-_), PlVars), !. % TO DO: improve?
793
794		% We have positive scores, maximum value is best. Remove if zero.
795		% Effect is undone on backtracking.
796		worsen_scores_for_vars_in_clause(_, []).
797		worsen_scores_for_vars_in_clause(StateMutable, [_-_-SatVarName|T]) :-
798		get_full_state(StateMutable, heuristic_avl, Avl),
799		( avl_fetch(SatVarName, Avl, Score)
800		-> ( Score \== 1,
801		NScore is Score - 1,
802		avl_change(SatVarName, Avl, _, NAvl, NScore),
803		update_full_state(StateMutable, heuristic_avl, NAvl)
804		; Score == 1,
805		delete_state_instance(StateMutable, heuristic_avl, (SatVarName, Score))
806		),
807		worsen_scores_for_vars_in_clause(StateMutable, T)
808		; worsen_scores_for_vars_in_clause(StateMutable, T)
809		).
810
811		% Literal Block Distance (LBD) as defined in "Predicting Learnt Clauses Quality in Modern SAT Solvers",
812		% i.e., the amount of different decision levels in a clause.
813		compute_lbd_score(SatStack, BjClause, LbdScore) :-
814		compute_lbd_score(SatStack, BjClause, [], LbdScore).
815
816		compute_lbd_score(_, [], Acc, LbdScore) :-
817		length(Acc, LbdScore).
818		compute_lbd_score(SatStack, [_-_-SatVarName|T], Acc, LbdScore) :-
819		avl_fetch(SatVarName, SatStack, (_,Level,_,_)),
820		!,
821		ord_add_element(Acc, Level, NewAcc),
822		compute_lbd_score(SatStack, T, NewAcc, LbdScore).
823		compute_lbd_score(SatStack, [_|T], Acc, LbdScore) :- % TO DO: check this, happens when using idl solver unsat core?
824		compute_lbd_score(SatStack, T, Acc, LbdScore).
825
826		% Remove half of the clauses every "frequency_constant + constant_factor * x" conflicts,
827		% where x is the amount of clause reductions so far. We keep clauses with a small LBD forever.
828		possibly_discard_learned_clauses :-
829		conflict_stats(_, _, since_reduction(SRed)),
830		dpllt_settings:discard_learned_clauses_frequency_constant(Frequency),
831		SRed >= Frequency, % first check to improve performance
832		amount_clause_reductions(Reductions),
833		dpllt_settings:discard_learned_clauses_constant_factor(Factor),
834		Threshold is Frequency + Factor * Reductions,
835		SRed == Threshold,
836		!,
837		debug_format_sat("~nDiscard half of learned clauses..", []),
838		dpllt_settings:discard_clause_greater_lbd(LbdLimit),
839		amount_learned_clauses(ALC),
840		Half is ALC // 2,
841		discard_half_of_learned_clauses_greater_lbd(0, Half, LbdLimit, Removed),
842		retract(amount_learned_clauses(Old)),
843		New is Old - Removed,
844		asserta(amount_learned_clauses(New)),
845		retract(conflict_stats(total(Total), since_restart(SRed), _)),
846		asserta(conflict_stats(total(Total), since_restart(SRed), since_reduction(0))), !.
847		possibly_discard_learned_clauses.
848
849		% Remove half of the clauses learned so far.
850		% We keep clauses with an LBD smaller than dpllt_settings:discard_clause_greater_lbd/1
851		% forever. Thus it is not guaranteed that exactly half of the clauses are deleted if
852		% a lot of high quality clauses have been learned.
853		discard_half_of_learned_clauses_greater_lbd(C, Half, LbdLimit, Removed) :-
854		C =< Half,
855		backjump_clause(BjLevel, BjClause, LbdScore, UsedVars),
856		!,
857		retract(backjump_clause(BjLevel, BjClause, LbdScore, UsedVars)),
858		( LbdScore > LbdLimit
859		-> C1 is C + 1,
860		discard_half_of_learned_clauses_greater_lbd(C1, Half, LbdLimit, Removed)
861		; discard_half_of_learned_clauses_greater_lbd(C, Half, LbdLimit, Removed),
862		asserta(backjump_clause(BjLevel, BjClause, LbdScore, UsedVars))
863		).
864		discard_half_of_learned_clauses_greater_lbd(C, _, _, C).
865
866		%% count_found_conflict(-NewTotal, -NewSinceRestart, -NewSinceReduction).
867		count_found_conflict(Total1, SRes1, SRed1) :-
868		retract(conflict_stats(total(Total), since_restart(SRes), since_reduction(SRed))),
869		Total1 is Total + 1,
870		SRes1 is SRes + 1,
871		SRed1 is SRed + 1,
872		asserta(conflict_stats(total(Total1), since_restart(SRes1), since_reduction(SRed1))).
873
874		%% compute_and_assert_backjump_clause(+SolverEnv, +StateMutable, +StackSize, +ConflictClause).
875		compute_and_assert_backjump_clause(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause) :-
876		compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, _).
877
878		cnf_to_smt(BoolPred, Smt) :-
879		BoolPred = b(Expr,_,_),
880		cnf_to_smt_e(Expr, Smt).
881
882		cnf_to_smt_e(falsity, b(falsity,pred,[])).
883		cnf_to_smt_e(truth, b(truth,pred,[])).
884		cnf_to_smt_e(conjunct(A,B), Smt) :-
885		cnf_to_smt(A, NA),
886		cnf_to_smt(B, NB),
887		safe_create_texpr(conjunct(NA,NB), pred, [], Smt).
888		cnf_to_smt_e(disjunct(A,B), Smt) :-
889		cnf_to_smt(A, NA),
890		cnf_to_smt(B, NB),
891		safe_create_texpr(disjunct(NA,NB), pred, [], Smt).
892		cnf_to_smt_e(equal(b(identifier(_),_,Info),b(BoolExpr,boolean,_)), Smt) :-
893		member(smt_formula(TSmt), Info),
894		( BoolExpr == boolean_true
895		-> Smt = TSmt
896		; safe_create_texpr(negation(TSmt), pred, [], Smt)
897		).
898
899		/*cnf_to_smt([], _, Acc, SmtFromCnf) :-
900		conjunct_predicates(Acc, SmtFromCnf).
901		cnf_to_smt([Clause|T], PrologSatVarTriple, Acc, SmtFromCnf) :-
902		clause_to_smt(PrologSatVarTriple, Clause, SmtClause),
903		cnf_to_smt(T, PrologSatVarTriple, [SmtClause|Acc], SmtFromCnf).*/
904
905		clause_to_smt(PlVars, Clause, SmtFormula) :-
906		clause_to_smt(PlVars, Clause, [], SmtFormula).
907
908		clause_to_smt(_, [], Acc, SmtFormula) :-
909		disjunct_predicates(Acc, SmtFormula).
910		clause_to_smt(PlVars, [Pol-_-SatVarName|T], Acc, SmtClause) :-
911		member(_-SatVarName-TSmtFormula, PlVars),
912		get_smt_formula_for_sat_pol(TSmtFormula, Pol, SmtFormula),
913		clause_to_smt(PlVars, T, [SmtFormula|Acc], SmtClause).
914
915		%% compute_and_assert_backjump_clause_get_level(+SolverEnv, +StateMutable, +StackSize, +ConflictLevel, +ConflictClause, -BjLevel).
916		/*compute_and_assert_backjump_clause_get_level(_SolverEnv, StateMutable, _StackSize, ConflictLevel, ConflictClause, BjLevel) :-
917		% Theory conflict in unsat core can be on level zero while the SMT actually found the contradiction on a higher level
918		% after the grounding phase of ProB's constraint solver.
919		% In this case, we learn the negated unsat core and backjump to level 0.
920		get_last_decision_level(StateMutable, _),
921		ConflictLevel == 0,
922		!,
923		BjLevel = 0,
924		negate_assignments_to_polarities(ConflictClause, BjClause),
925		debug_format_sat("Found theory conflict in unsat core on level 0.", []),
926		debug_format_sat("Backjump clause is ~w", [BjClause]),
927		debug_format_sat("Backjump level is ~w", [BjLevel]),
928		get_full_state(StateMutable, sat_stack, SatStack),
929		compute_lbd_score(SatStack, BjClause, LbdScore),
930		asserta(backjump_clause(BjLevel, BjClause, LbdScore, [])),
931		asserta(backjump_level(BjLevel)).*/
932		compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, BjLevel) :-
933		get_last_decision_level(StateMutable, _),
934		possibly_discard_learned_clauses,
935		debug_format_sat("~nConflict clause is ~w", [ConflictClause]),
936		debug_format_sat("~nStart CDCL..", []),
937		( (get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause, BjLevel, UsedVars), BjLevel \== -1)
938		; add_error_fail(compute_and_assert_backjump_clause_get_level, 'SMT solver\'s conflict resolution failed', [])
939		),%trace,get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause, BjLevel, UsedVars)),
940		debug_format_sat("done.", []),
941		debug_format_sat("Backjump clause is ~w", [BjClause]),
942		debug_format_sat("Backjump level is ~w", [BjLevel]),
943		get_full_state(StateMutable, sat_stack, SatStack),
944		compute_lbd_score(SatStack, BjClause, LbdScore),
945		asserta(backjump_clause(BjLevel, BjClause, LbdScore, UsedVars)),
946		asserta(backjump_level(BjLevel)),
947		( incremental_mode,
948		get_from_solver_env(SolverEnv, pl_vars, PlVars),
949		clause_to_smt(PlVars, BjClause, SmtFormula),
950		SmtFormula \= b(negation(b(truth,pred,_)),pred,_),
951		SmtFormula \= b(truth,pred,_) % uses _cnf_opt variable, don't store those
952		-> solver_name(SolverName),
953		asserta(memoize_backjump_clause(SolverName, SmtFormula, LbdScore))
954		; true
955		),
956		count_found_conflict(NewTotal, NewSinceRestart, _),
957		store_recent_stack_size(StackSize),
958		count_learned_clause,
959		( \+ clear_lbd_values_or_fail(StateMutable),
960		BjLevel \== 0
961		-> store_recent_lbd_score(LbdScore),
962		update_total_lbd_sum(LbdScore),
963		(random_restart(NewTotal, NewSinceRestart), !; true)
964		; true
965		), !.
966
967		count_learned_clause :-
968		retract(amount_learned_clauses(Old)),
969		New is Old + 1,
970		asserta(amount_learned_clauses(New)).
971
972		%% store_recent_lbd_score(+LbdScore).
973		% The stored list of recent LBDs is a difference list and we insert at the end of list.
974		% The first LBD is thus the oldest one and removed when exceeding the maximum size
975		% defined by recent_lbd_threshold/1.
976		store_recent_lbd_score(LbdScore) :-
977		retract(recent_lbds_dl(Lbds-Diff, Amount)),
978		glucose_restart_recent_lbds_threshold(Thresh),
979		Diff = [LbdScore|NDiff],
980		( Amount < Thresh
981		-> Amount1 is Amount + 1,
982		asserta(recent_lbds_dl(Lbds-NDiff, Amount1))
983		; Lbds = [_|RLbds],
984		asserta(recent_lbds_dl(RLbds-NDiff, Amount))
985		).
986
987		store_recent_stack_size(StackSize) :-
988		retract(recent_stack_sizes_dl(StackSizes-Diff, Amount)),
989		glucose_restart_trail_threshold(Thresh),
990		Diff = [StackSize|NDiff],
991		( Amount < Thresh
992		-> Amount1 is Amount + 1,
993		asserta(recent_stack_sizes_dl(StackSizes-NDiff, Amount1))
994		; StackSizes = [_|RStackSizes],
995		asserta(recent_stack_sizes_dl(RStackSizes-NDiff, Amount))
996		).
997
998		%% update_total_lbd_sum(+LbdScore).
999		update_total_lbd_sum(LbdScore) :-
1000		retract(total_lbd_sum(Old)),
1001		New is Old + LbdScore,
1002		asserta(total_lbd_sum(New)).
1003
1004		%% random_restart(+AmountOfConflicts, +AmountOfConflictsSinceRestart).
1005		% "Randomly" restart after an amount of conflicts since the last restart.
1006		random_restart(_AC, ACR) :-
1007		restart_policy(luby),
1008		random_luby_restart(ACR), !.
1009		random_restart(AC, _ACR) :-
1010		restart_policy(glucose),
1011		random_glucose_restart(AC), !.
1012
1013		:- dynamic restarts/1.
1014
1015		do_random_restart :-
1016		retract(restarts(OldR)),
1017		NewR is OldR + 1,
1018		asserta(restarts(NewR)),
1019		retract(backjump_level(_)),
1020		asserta(backjump_level(0)),
1021		retract(conflict_stats(total(Total), _, since_reduction(SRed))),
1022		asserta(conflict_stats(total(Total), since_restart(0), since_reduction(SRed))),
1023		asserta_once(is_restart),
1024		debug_format_sat("~nRandom restart", []).
1025
1026		%% random_glucose_restart(+AmountOfConflicts).
1027		% Restart search if recent_lbds_dl/2 contains exactly glucose_restart_recent_lbds_threshold/1 amount
1028		% of most recent LBDs and RecentAvg * Proportion > TotalAvg is satisfied, i.e., the recently learned clauses'
1029		% LBDs got too large.
1030		random_glucose_restart(AC) :-
1031		total_lbd_sum(TotalLbdSum), % TO DO: reset the sum at any time?
1032		TotalAvg is TotalLbdSum / AC,
1033		recent_lbds_dl(RLbds-[], LbdAmount),
1034		glucose_restart_recent_lbds_threshold(LbdThresh),
1035		LbdAmount == LbdThresh, % queue of recent LBDs is full
1036		sumlist(RLbds, RSum),
1037		RecentAvg is RSum / LbdAmount,
1038		glucose_restart_margin_ratio(Proportion),
1039		debug_format_sat("~nTotalAvg: ~w~nRecentAvg: ~w", [TotalAvg,RecentAvg]),
1040		( RecentAvg * Proportion > TotalAvg
1041		-> do_random_restart,
1042		clear_recent_lbds_state
1043		; true
1044		).
1045
1046		% Favor SAT instances too by possibly clearing the recent LBD queue.
1047		% Assumption: The queue of recent LBDs is full.
1048		clear_lbd_values_or_fail(StateMutable) :-
1049		glucose_restart_trail_threshold(TrailThresh),
1050		glucose_restart_stack_avg_factor(StackSizeFactor),
1051		recent_stack_sizes_dl(StackSizes-[], AmountStackSizes),
1052		AmountStackSizes == TrailThresh, % queue of recent stack sizes on conflict is full
1053		get_full_state(StateMutable, current_stack_size, StackSize),
1054		sumlist(StackSizes, SSum),
1055		StackSizesAvg is SSum / AmountStackSizes,
1056		StackSize > StackSizeFactor * StackSizesAvg,
1057		clear_recent_lbds_state.
1058
1059		clear_recent_lbds_state :-
1060		retract(recent_lbds_dl(_, _)),
1061		asserta(recent_lbds_dl(Diff-Diff, 0)).
1062
1063		%% random_luby_restart(+AmountOfConflictsSinceRestart).
1064		% The amount of conflicts when to restart is defined by the Luby sequence,
1065		% i.e., 1,1,2,1,1,2,4,1,1,2,1,1,2,4,8,.. etc., (cf. "Optimal speedup of Las Vegas algorithms")
1066		% using a unit length of 32 (see luby_counter/1).
1067		random_luby_restart(ACR) :-
1068		restart_policy(luby),
1069		get_next_luby_value(Luby),
1070		!,
1071		( ACR == Luby
1072		-> retract_once(luby_counter(_)),
1073		do_random_restart
1074		; true
1075		).
1076		random_luby_restart(_) :-
1077		add_error_fail(random_restart, 'No more values in predefined Luby sequence', []).
1078
1079		get_next_luby_value(LubyValue) :-
1080		luby_counter(Luby),
1081		luby_restart_unit_length(UnitLength),
1082		LubyValue is UnitLength * Luby, % TO DO: faster to precompute once a unit length is fixed
1083		!.
1084
1085		%% learn_asserted_clauses(+CurrentBjLevel, +SolverEnv, +Clauses, -NewClauses).
1086		learn_asserted_clauses(StateMutable, CurrentBjLevel, SolverEnv, Clauses, NewClauses) :-
1087		get_clauses_to_learn_bump_scores(StateMutable, CurrentBjLevel, SolverEnv, ClausesToLearn),
1088		append(ClausesToLearn, Clauses, NewClauses), !.
1089
1090		%% get_sat_solution_exclusion_clauses(-ExclClausesNoRef).
1091		% We exclude SAT solutions when backtracking from finding an SMT solution to find a different assignment.
1092		get_sat_solution_exclusion_clauses(ExclClausesNoRef) :-
1093		findall(ExclClause, exclude_sat_solution_clause(ExclClause), ExclClausesNoRef), !.
1094
1095		%% get_clauses_to_learn_bump_scores(+StateMutable, +CurrentBjLevel, +SolverEnv, -ClausesToLearn).
1096		% Note that the Prolog variable references are set correctly in here.
1097		% We thus do not have to take care for correct references when analyzing a conflict
1098		% and creating a backjump clause beforehand.
1099		% We learn all backjump clauses which have been learned on a decision level higher or equal to CurrentBjLevel.
1100		% Note that the clauses learned on a lower level are already included in the set of clauses.
1101		% Yet, when backjumping, we do not want to forget clauses learned on a decision level between the current backjump
1102		% level and the last conflict level.
1103		% -UsedVars are the SAT variables used during all conlict analyses of clauses to learn.
1104		get_clauses_to_learn_bump_scores(StateMutable, CurrentBjLevel, SolverEnv, ClausesToLearn) :-
1105		get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, TempBjClauses, UsedVars),
1106		%length(TempBjClauses, Len),
1107		%debug_format_sat("Learn ~w clauses", [Len]),
1108		get_sat_solution_exclusion_clauses(ExclClauses),
1109		append(ExclClauses, TempBjClauses, BjClausesNoRef),
1110		set_references_and_bump_scores(BjClausesNoRef, UsedVars, StateMutable, SolverEnv, ClausesToLearn).
1111
1112		set_references_and_bump_scores(BjClausesNoRef, UsedVars, StateMutable, SolverEnv, ClausesToLearn) :-
1113		get_from_solver_env(SolverEnv, pl_vars, PlVars),
1114		set_variable_references_in_clauses(PlVars, BjClausesNoRef, ClausesToLearn),
1115		update_heuristic_scores_for_clauses(StateMutable, ClausesToLearn),
1116		( bump_scores_for_bj_clause_only(true)
1117		; % additionally bump scores for all variables used during conflict analysis
1118		bump_scores_for_bj_clause_only(false),
1119		update_heuristic_scores_for_vars(StateMutable, UsedVars, PlVars)
1120		).
1121
1122		%% get_asserted_backjump_clauses_greater_eq_level(+CurrentBjLevel, -BjClauses).
1123		% Get and remove, but undo on backtracking.
1124		get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, BjClauses, UsedVars) :-
1125		get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, [], BjClauses, [], UsedVars).
1126
1127		get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, BAcc, BjClauses, UAcc, UsedVars) :-
1128		( backjump_clause(BjLevel, BjClause, _, _)
1129		-> bt_retract(backjump_clause(BjLevel, BjClause, _, BUsedVars)),
1130		( BjLevel >= CurrentBjLevel
1131		-> append(BUsedVars, UAcc, NUAcc),
1132		get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, [BjClause|BAcc], BjClauses, NUAcc, UsedVars)
1133		; get_asserted_backjump_clauses_greater_eq_level(CurrentBjLevel, BAcc, BjClauses, UAcc, UsedVars),
1134		bt_asserta(backjump_clause(BjLevel, BjClause, _, BUsedVars))
1135		)
1136		; BjClauses = BAcc,
1137		UsedVars = UAcc
1138		), !.
1139
1140		%% set_variable_references_in_clauses(+PlVars, +Clauses, -RefClauses).
1141		set_variable_references_in_clauses(_, [], []).
1142		set_variable_references_in_clauses(PlVars, [Clause|T], [RefClause|NT]) :-
1143		set_variable_references_in_clause(PlVars, Clause, RefClause),
1144		set_variable_references_in_clauses(PlVars, T, NT).
1145
1146		%% set_variable_references_in_clause(+PlVars, +Clause, -RefClauses).
1147		% We need to set the correct variable references in a new learned clause
1148		% to trigger co-routines etc.
1149		set_variable_references_in_clause(_, [], []).
1150		set_variable_references_in_clause(PlVars, [Pol-_-Name|T], [Pol-Var-Name|NT]) :-
1151		member(Var-Name-_, PlVars),
1152		!,
1153		set_variable_references_in_clause(PlVars, T, NT).
1154		set_variable_references_in_clause(PlVars, [_|T], NT) :-
1155		% symmetry breaking might introduce new SAT variables which are not connected to any SMT variable
1156		set_variable_references_in_clause(PlVars, T, NT).
1157
1158		get_from_solver_env(SolverEnv, Key, OutValue) :-
1159		member(Key:Value, SolverEnv),
1160		!,
1161		OutValue = Value.
1162		get_from_solver_env(SolverEnv, Key, _) :-
1163		add_error_fail(get_from_solver_env,
1164		'Wrong key or corrupt solver environment in DPLL(T) SAT solver',
1165		[env:SolverEnv,key:Key]).
1166
1167		bt_asserta(Assertion) :-
1168		asserta(Assertion); (retract(Assertion), fail).
1169
1170		bt_retract(Assertion) :-
1171		( retract(Assertion)
1172		-> ( true
1173		; asserta(Assertion),
1174		fail
1175		)
1176		; fail
1177		).
1178
1179		%% Assert all list elements as wd_condition/1.
1180		/*register_wd_conditions([]).
1181		register_wd_conditions([WDImpl|T]) :-
1182		WDImpl = b(disjunct(_,Pred),_,_),
1183		norm_pred_check(Pred,NPred),
1184		asserta(wd_condition(NPred)),
1185		register_wd_conditions(T).
1186
1187		contains_pred_with_wd_or_for_wd(Conj) :-
1188		ground(Conj),
1189		conjunction_to_list(Conj, L),
1190		contains_pred_with_wd_or_for_wd_l(L).
1191
1192		contains_pred_with_wd_or_for_wd_l([Pred|_]) :-
1193		Pred = b(_,_,I),
1194		( member(contains_wd_condition, I)
1195		; member(discharged_wd_po, I)
1196		; member(discharged(_,_), I)
1197		),
1198		!.
1199		contains_pred_with_wd_or_for_wd_l([Pred|_]) :-
1200		norm_pred_check(Pred,NPred),
1201		wd_condition(NPred),
1202		!.
1203		contains_pred_with_wd_or_for_wd_l([_|T]) :-
1204		contains_pred_with_wd_or_for_wd_l(T).*/
1205
1206		has_wd_condition(_, Pred) :-
1207		empty_hyps(Hyps),
1208		compute_wd(Pred, Hyps, [], _WDPo), !.
1209		%has_wd_condition(_, Pred) :-
1210		% contains_pred_with_wd_or_for_wd(Pred), !.
1211		%has_wd_condition(PredList, _) :-
1212		% member(b(member(_,b(domain(_),_,_)),pred,_), PredList), !. % TO DO: add more
1213
1214		get_core_for_cdcl(Cores, UnsatCore, RestCores) :-
1215		get_core_for_cdcl_aux(Cores, _, TUnsatCore, TRestCores),
1216		( ground(TUnsatCore)
1217		-> UnsatCore = TUnsatCore,
1218		RestCores = TRestCores
1219		; TRestCores = [UnsatCore|RestCores]
1220		).
1221
1222		get_core_for_cdcl_aux([], CoreAcc, CoreAcc, []).
1223		get_core_for_cdcl_aux([CoreList|T], CoreAcc, UnsatCore, RestCores) :-
1224		conjunct_predicates(CoreList, Core),
1225		( var(CoreAcc),
1226		has_wd_condition(CoreList, Core),
1227		CoreList \= [_] % not a single WD condition, can't learn from that
1228		-> get_core_for_cdcl_aux(T, Core, UnsatCore, RestCores)
1229		; get_core_for_cdcl_aux(T, CoreAcc, UnsatCore, TRestCores),
1230		RestCores = [Core|TRestCores]
1231		).
1232
1233		%% get_conflict_clause_for_theory_conflict(+LastVarName, +LastVarValue, +SolverEnv, -ConflictClause).
1234		% Translate current sat solution, which is a theory conflict, to the theory and compute
1235		% the (minimum) unsat core. Return the negated unsat core as a conflict clause.
1236		% Note that an SMT formula passed to the theory solver is always a conjunction and
1237		% thus the negated unsat core is a disjunction (clause).
1238		% Assumption: unsat core computation only removes constraints and does not deduce new ones.
1239		get_conflict_clause_for_theory_conflict(LastVarName, LastVarValue, SolverEnv, ConflictClause) :-
1240		( retract(idl_unsat_core(UnsatCore))
1241		-> true
1242		; get_from_solver_env(SolverEnv, sat_bindings, SatBindingsNoLast),
1243		get_from_solver_env(SolverEnv, sat_vars, SatVars),
1244		temporary_set_unsat_core_timeout,
1245		sat_to_predicate_from_solution(SatBindingsNoLast, SatVars, SmtFormulaNoLast),
1246		sat_to_predicate_from_solution([bind(LastVarName,LastVarValue)], SatVars, FixedConj),
1247		debug_format_sat("Compute unsat core for : ", [], b(conjunct(FixedConj,SmtFormulaNoLast),pred,[])),
1248		tools:start_ms_timer(TT),
1249		conjunct_predicates([FixedConj,SmtFormulaNoLast],FullFormula),
1250		time_out(unsat_chr_core_list_with_auto_time_limit(FullFormula, 30000,
1251		[auto_time_out_factor(180), % we add 80 %
1252		ignore_if_sol_found], _Result, CoreList),
1253		30000, TimeoutResult),
1254		tools:stop_ms_timer_with_msg(TT,'unsat_chr_core_list_with_auto_time_limit'),
1255		( TimeoutResult == time_out
1256		-> % don't waste too much time in unsat core computation
1257		debug_format_sat("Canceled unsat core computation due to exceeding a timeout" ,[]),
1258		TUnsatCore = FullFormula
1259		; (CoreList == []
1260		-> add_internal_error('Conflict clause in SMT solving is not a conflict.',
1261		get_conflict_clause_for_theory_conflict(LastVarName)),
1262		fail
1263		; conjunct_predicates(CoreList, TUnsatCore)
1264		)
1265		),
1266		remove_wd_pos_introduced_for_dpllt_keep_toplevel(TUnsatCore, UnsatCore),
1267		debug_format_sat("Computed unsat core: ", [], UnsatCore),
1268		preferences:reset_temporary_preference(time_out)
1269		), !,
1270		get_conflict_clause_from_unsat_core(UnsatCore, SolverEnv, ConflictClause),
1271		!.
1272
1273		get_conflict_clause_from_unsat_core_map(SolverEnv, UnsatCore, ConflictClause) :-
1274		get_conflict_clause_from_unsat_core(UnsatCore, SolverEnv, ConflictClause).
1275
1276		%% get_conflict_clause_from_unsat_core(+UnsatCore, +SolverEnv, -ConflictClause).
1277		get_conflict_clause_from_unsat_core(UnsatCore, SolverEnv, ConflictClause) :-
1278		get_from_solver_env(SolverEnv, sat_vars, SatVars),
1279		get_from_solver_env(SolverEnv, t2b_env, T2BEnv),
1280		get_from_solver_env(SolverEnv, pl_vars, PlVars),
1281		predicate_to_sat(only_reuse, [], SatVars, T2BEnv, UnsatCore, _NewEnv, _, UnsatCoreSat, _NewSatVars),
1282		%nl, write('Core: '),
1283		%translate:print_bexpr(UnsatCore),nl,
1284		%translate:print_bexpr(UnsatCoreSat),nl,
1285		sat_conj_negate_to_clause(UnsatCoreSat, TConflictClause),
1286		set_variable_references_in_clause(PlVars, TConflictClause, ConflictClause),
1287		!.
1288		get_conflict_clause_from_unsat_core(_, _, _) :-
1289		add_internal_error('Unsat core to conflict clause failed.', get_conflict_clause_from_unsat_core),
1290		fail.
1291
1292		%% get_complete_theory_lemma(+SolverEnv, -TheoryLemmaClause) :-
1293		% Return the complete unsatisfiable SMT formula as a conflict clause.
1294		get_complete_theory_lemma(SolverEnv, TheoryLemmaClause) :-
1295		get_from_solver_env(SolverEnv, pl_vars, PlVars),
1296		get_from_solver_env(SolverEnv, sat_bindings, SatBindings),
1297		get_clause_from_negated_ground_bindings(SatBindings, TTheoryLemmaClause),
1298		set_variable_references_in_clause(PlVars, TTheoryLemmaClause, TheoryLemmaClause), !.
1299
1300		%% get_clause_from_negated_ground_bindings(+SatBindings, -TheoryLemmaClause) :-
1301		get_clause_from_negated_ground_bindings(SatBindings, TheoryLemmaClause) :-
1302		get_clause_from_negated_ground_bindings(SatBindings, [], TheoryLemmaClause).
1303
1304		get_clause_from_negated_ground_bindings([], Acc, Acc).
1305		get_clause_from_negated_ground_bindings([bind(SatVarName,Pol)|T], Acc, TheoryLemmaClause) :-
1306		ground(Pol),
1307		!,
1308		negate_polarity(Pol, NegPol),
1309		get_clause_from_negated_ground_bindings(T, [NegPol-_-SatVarName|Acc], TheoryLemmaClause).
1310		get_clause_from_negated_ground_bindings([_|T], Acc, TheoryLemmaClause) :-
1311		get_clause_from_negated_ground_bindings(T, Acc, TheoryLemmaClause).
1312
1313		temporary_set_unsat_core_timeout :-
1314		preferences:temporary_set_preference(time_out, 25).
1315		temporary_set_unsat_core_timeout :-
1316		preferences:reset_temporary_preference(time_out),
1317		fail.
1318
1319		% In the conflict graph each node corresponds to a variable assignment.
1320		% The predecessors of node x are the antecedent assignments A^w(x) corresponding
1321		% to the unit clause w (in its original form) that led to the propagation of x (logical implications).
1322		% The directed edges from the nodes in A^w(x) to node x are all labeled with w.
1323		% Nodes that have no predecessor correspond to decision/branching assignments
1324		% (cf. GRASP: A Search Algorithm for Propositional Satisfiability, by Marques-Silva and Sakallah).
1325		% As an improvement, we apply first UIP clause learning (cf. Efficient Conflict Driven Learning in a Boolean Satisfiability Solver, Zhang et al.).
1326		%% get_backjump_clause_conflict_resolution(+SolverEnv, +StateMutable, +ConflictLevel, +ConflictClause, -BjClause, -BjLevel, -UsedVars).
1327		% Compute the conflict graph for a conflicting unit-propagation of a variable
1328		% and extract a backjump clause.
1329		% -UsedVars are the SAT variables used during conflict analysis (can be necessary for branching heuristic).
1330		% Notes:
1331		% - the variable references in the returned clause are not yet set (cf. get_clauses_to_learn_bump_scores/4)
1332		% - we do not create an actual graph
1333		get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause, BjLevel, UsedVars) :-
1334		get_last_decision_level(StateMutable, _),
1335		get_full_state(StateMutable, sat_stack, SatStack),
1336		get_antecedent_assignments_for_clause(ConflictClause, SatStack, Antecedent),
1337		new_mutdict(ResolvedSoFar),
1338		( Antecedent == []
1339		-> % special case if there are no antecedents of the conflict clause: occurs if
1340		% antecedent assignments are all deterministic unit propagations (unit clauses in original formula)
1341		% or all decision variables
1342		negate_assignments_to_polarities(ConflictClause, BjClause),
1343		get_variables_used_in_cdcl(ResolvedSoFar, BjClause, UsedVars),
1344		% highest level other than conflict level or 0
1345		get_maximum_decision_level_other_than_current(BjClause, SatStack, 0, ConflictLevel, BjLevel)
1346		; get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, ConflictClause, DecisionVars),
1347		add_used_vars_to_mutdict(DecisionVars, ResolvedSoFar),
1348		get_backjump_clause_and_level(SolverEnv, StateMutable, ConflictLevel, ResolvedSoFar, Antecedent, BjClause, BjLevel, UsedVars)
1349		).
1350
1351		%% get_wo_antecedent_from_conflict_clause(+SolverEnv, +StateMutable, +Clause, -VarsNoAnt).
1352		% Get variables without antecedent assignments from conflict clause.
1353		get_wo_antecedent_from_conflict_clause(_, _, [], []).
1354		get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, [Pol-Var-N|T], VarsNoAnt) :-
1355		get_from_sat_stack_or_explain_theory_propagation(SolverEnv, StateMutable, N, PropType, _, _, _),
1356		PropType == branch,
1357		!,
1358		get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, T, NT),
1359		VarsNoAnt = [Pol-Var-N|NT].
1360		get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, [Pol-Var-N|T], VarsNoAnt) :-
1361		get_from_sat_stack_or_explain_theory_propagation(SolverEnv, StateMutable, N, _, _, _, OriginalClause),
1362		get_full_state(StateMutable, sat_stack, SatStack),
1363		get_antecedent_assignments_for_clause(OriginalClause, SatStack, Antecedent),
1364		Antecedent == [],
1365		!,
1366		get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, T, NT),
1367		VarsNoAnt = [Pol-Var-N|NT].
1368		get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, [_|T], NT) :-
1369		get_wo_antecedent_from_conflict_clause(SolverEnv, StateMutable, T, NT).
1370
1371		negate_assignments_to_polarities([], Out) :-
1372		!,
1373		Out = [].
1374		negate_assignments_to_polarities([_-AssignedPol-SatVarName|T], [Pol-_-SatVarName|NT]) :-
1375		ground(AssignedPol),
1376		!,
1377		negate_polarity(AssignedPol, Pol),
1378		negate_assignments_to_polarities(T, NT).
1379		/*negate_assignments_to_polarities([Pol-AssignedPol-SatVarName|T], [NPol-_-SatVarName|NT]) :-
1380		var(AssignedPol),
1381		!,
1382		negate_polarity(Pol, NPol),
1383		negate_assignments_to_polarities(T, NT).*/
1384		negate_assignments_to_polarities(In, _) :-
1385		add_internal_error('Expected ground polarity.', negate_assignments_to_polarities(In)),
1386		fail.
1387
1388		% Fail if no decision has been made so far, i.e., the decision level is set to -1.
1389		get_last_decision_level(StateMutable, Level) :-
1390		get_full_state(StateMutable, decision_level, TLevel),
1391		TLevel \== -1,
1392		!,
1393		Level = TLevel.
1394
1395		negate_polarities([], []).
1396		negate_polarities([Pol-Var-Name|T], [NPol-Var-Name|NT]) :-
1397		negate_polarity(Pol, NPol),
1398		negate_polarities(T, NT).
1399
1400		get_maximum_decision_level_other_than_current([_], _, _, _, BjLevel) :-
1401		% zero if learning a unit clause
1402		!,
1403		BjLevel = 0.
1404		get_maximum_decision_level_other_than_current(BjClause, SatStack, BjLevelAcc, CurLevel, BjLevel) :-
1405		get_maximum_decision_level_other_than_current_not_unit(BjClause, SatStack, BjLevelAcc, CurLevel, BjLevel).
1406
1407		get_maximum_decision_level_other_than_current_not_unit([], _, BjLevelAcc, _, BjLevelAcc).
1408		get_maximum_decision_level_other_than_current_not_unit([_-_-Name|T], SatStack, BjLevelAcc, CurLevel, BjLevel) :-
1409		avl_fetch(Name, SatStack, (_,Level,_,_)),
1410		( (Level \== CurLevel,
1411		Level > BjLevelAcc
1412		)
1413		-> NBjLevelAcc = Level
1414		; NBjLevelAcc = BjLevelAcc
1415		),
1416		get_maximum_decision_level_other_than_current_not_unit(T, SatStack, NBjLevelAcc, CurLevel, BjLevel).
1417
1418		%% get_antecedent_assignments_for_clause(+ConflictClause, +SatStack, -Antecedent).
1419		% It is important that the resulting list does not contain any duplicates
1420		% to identify the first UIP.
1421		get_antecedent_assignments_for_clause(ConflictClause, SatStack, Antecedent) :-
1422		get_antecedent_assignments_for_clause(ConflictClause, SatStack, [], TAntecedent),
1423		sort(TAntecedent, Antecedent),
1424		!.
1425
1426		get_antecedent_assignments_for_clause([], _, Acc, Acc).
1427		get_antecedent_assignments_for_clause([_-_-SatVarName|T], SatStack, Acc, Antecedent) :-
1428		get_antecedent_assignments(SatStack, SatVarName, TAntecedent),
1429		append(Acc, TAntecedent, NAcc),
1430		get_antecedent_assignments_for_clause(T, SatStack, NAcc, Antecedent).
1431
1432		%% get_antecedent_assignments(+SatStack, +SatVarName, -Antecedent).
1433		get_antecedent_assignments(SatStack, SatVarName, Antecedent) :-
1434		avl_fetch(SatVarName, SatStack, (_,_,_,OriginalClause)),
1435		!,
1436		select(_-_-SatVarName, OriginalClause, TAntecedent),
1437		negate_polarities(TAntecedent, Antecedent), !.
1438		get_antecedent_assignments(_, _, []). % wd po not necessarily assigned, e.g., if the predicate containing the wd condition is false
1439
1440		%% join_assignments(+A1, +A2, -Joined).
1441		join_assignments([], A, _, A).
1442		join_assignments([Pol-Var-Name|T], A2, ResolvedSoFar, A) :-
1443		( ( \+ member(Pol-Var-Name, A2),
1444		\+ mutdict_get(ResolvedSoFar, Name, _)
1445		)
1446		-> join_assignments(T, [Pol-Var-Name|A2], ResolvedSoFar, A)
1447		; join_assignments(T, A2, ResolvedSoFar, A)
1448		).
1449
1450		%% resolve(+SatStack, +TBjClause, +ResolvedSoFar, +Resolver, -New).
1451		% +Resolver is a SAT variable name to resolve next (i.e., expand its antecedent assignments).
1452		resolve(SatStack, TBjClause, ResolvedSoFar, Resolver, New) :-
1453		get_antecedent_assignments(SatStack, Resolver, Antecedent),
1454		join_assignments(Antecedent, TBjClause, ResolvedSoFar, TNTBjClause),
1455		select(_-_-Resolver, TNTBjClause, NTBjClause),
1456		sort(NTBjClause, New).
1457
1458		add_used_vars_to_mutdict([], _).
1459		add_used_vars_to_mutdict([_-_-SatVarName|T], VarNamesDict) :-
1460		\+ mutdict_get(VarNamesDict, SatVarName, _),
1461		!,
1462		mutdict_put(VarNamesDict, SatVarName, SatVarName),
1463		add_used_vars_to_mutdict(T, VarNamesDict).
1464		add_used_vars_to_mutdict([_|T], VarNamesDict) :-
1465		add_used_vars_to_mutdict(T, VarNamesDict).
1466
1467		get_variables_used_in_cdcl(ResolvedSoFar, BjClause, UsedVars) :-
1468		add_used_vars_to_mutdict(BjClause, ResolvedSoFar),
1469		mutdict_keys(ResolvedSoFar, UsedVars).
1470
1471		%% get_backjump_clause_and_level(+SolverEnv, +StateMutable, +ConflictDLevel, +ResolvedSoFar, +TBjClause, -BjClause, -BjLevel, -UsedVars).
1472		get_backjump_clause_and_level(SolverEnv, StateMutable, ConflictDLevel, ResolvedSoFar, TBjClause, BjClause, BjLevel, UsedVars) :-
1473		get_backjump_clause_and_level_sub(SolverEnv, StateMutable, ConflictDLevel, 0, _, TBjClause, Resolver, ThisLevelCount),
1474		get_full_state(StateMutable, sat_stack, SatStack),
1475		( ThisLevelCount == 1
1476		-> % break, first UIP
1477		negate_polarities(TBjClause, BjClause),
1478		get_maximum_decision_level_other_than_current(BjClause, SatStack, -1, ConflictDLevel, BjLevel),
1479		get_variables_used_in_cdcl(ResolvedSoFar, BjClause, UsedVars)
1480		; ( var(Resolver)
1481		-> % nothing to resolve and decision on conflict level not part of temporary backjump clause,
1482		% all sources are backjump clause
1483		negate_polarities(TBjClause, BjClause),
1484		get_maximum_decision_level_other_than_current(BjClause, SatStack, -1, ConflictDLevel, BjLevel),
1485		get_variables_used_in_cdcl(ResolvedSoFar, BjClause, UsedVars)
1486		; resolve(SatStack, TBjClause, ResolvedSoFar, Resolver, NToExpand),
1487		mutdict_put(ResolvedSoFar, Resolver, Resolver),
1488		get_backjump_clause_and_level(SolverEnv, StateMutable, ConflictDLevel, ResolvedSoFar, NToExpand, BjClause, BjLevel, UsedVars)
1489		)
1490		).
1491
1492		get_backjump_clause_and_level_sub(_, _, _, ThisLevelCountAcc, ResolverAcc, [], ResolverAcc, ThisLevelCountAcc).
1493		get_backjump_clause_and_level_sub(SolverEnv, StateMutable, ConflictDLevel, ThisLevelCountAcc, ResolverAcc, [_-_-SatVarName|T], Resolver, ThisLevelCount) :-
1494		get_from_sat_stack_or_explain_theory_propagation(SolverEnv, StateMutable, SatVarName, PropType, Level, _, OriginalClause),
1495		( Level == ConflictDLevel
1496		-> NThisLevelCountAcc is ThisLevelCountAcc + 1
1497		; NThisLevelCountAcc = ThisLevelCountAcc
1498		),
1499		( (Level == ConflictDLevel,
1500		PropType == unit,
1501		OriginalClause \= [_] % not a deterministic unit propagation
1502		)
1503		-> NResolverAcc = SatVarName
1504		; NResolverAcc = ResolverAcc
1505		),
1506		get_backjump_clause_and_level_sub(SolverEnv, StateMutable, ConflictDLevel, NThisLevelCountAcc, NResolverAcc, T, Resolver, ThisLevelCount).
1507
1508		%% get_from_sat_stack_or_explain_theory_propagation(+SolverEnv, +StateMutable, +SatVarName, -PropType, -Level, -Pol, -OriginalClause).
1509		get_from_sat_stack_or_explain_theory_propagation(SolverEnv, StateMutable, SatVarName, PropType, Level, Pol, OriginalClause) :-
1510		get_full_state(StateMutable, sat_stack, SatStack),
1511		avl_fetch(SatVarName, SatStack, (PropType,Level,Pol,TOriginalClause)),
1512		( (PropType == theory, var(TOriginalClause))
1513		-> explain_theory_propagation(SolverEnv, SatStack, SatVarName, Level, Pol, OriginalClause),
1514		avl_change(SatVarName, SatStack, _, NStack, (PropType,Level,Pol,OriginalClause)),
1515		update_full_state(StateMutable, sat_stack, NStack)
1516		; OriginalClause = TOriginalClause
1517		).
1518
1519		negate_polarity(pred_true, pred_false).
1520		negate_polarity(pred_false, pred_true).
1521
1522		asserta_once(Assertion) :-
1523		call(dpllt_sat_solver:Assertion),
1524		!.
1525		asserta_once(Assertion) :-
1526		asserta(dpllt_sat_solver:Assertion).
1527
1528		b_pred_or_bool_true(X) :- X == truth; X == boolean_true; X == value(pred_true).
1529		b_pred_or_bool_false(X) :- X == falsity; X == boolean_false; X == value(pred_false).
1530
1531		sat_conj_negate_to_clause(Pred, Clause) :-
1532		conjunction_to_list(Pred, List),
1533		maplist(sat_equality_negate_to_literal, List, Clause).
1534
1535		sat_equality_negate_to_literal(b(equal(ID,Pol),pred,_), NegPol-_-Name) :-
1536		ID = b(identifier(Name),_,_),
1537		Pol = b(Value,boolean,_),
1538		( b_pred_or_bool_true(Value)
1539		-> NegPol = pred_false
1540		; NegPol = pred_true
1541		).
1542
1543		%%%%% Solver State
1544		create_solver_state(StateMutable) :-
1545		empty_avl(EmptyAvl),
1546		State = [sat_stack:EmptyAvl,cur_level:0,':'(decision_level,-1),current_stack_size:0,heuristic_avl:EmptyAvl],
1547		create_mutable(solver_state(State), StateMutable).
1548
1549		%% get_full_state(+StateMutable, +Key, -Datum).
1550		get_full_state(StateMutable, Key, Datum) :-
1551		get_mutable(solver_state(SolverState), StateMutable),
1552		member(Key:Datum, SolverState), !.
1553
1554		%% add_state_instance(+StateMutable, +Key, +Datum).
1555		% Add an instance to iterable data.
1556		add_state_instance(StateMutable, Key, Datum) :-
1557		get_mutable(solver_state(SolverState), StateMutable),
1558		select(Key:Data, SolverState, Rest),
1559		( Key == heuristic_avl
1560		-> Datum = (SatVarName,Score),
1561		avl_store(SatVarName, Data, Score, NewData)
1562		; Key == sat_stack,
1563		Datum = (SatVarName,A,B,C,D),
1564		avl_store(SatVarName, Data, (A,B,C,D), NewData)
1565		), !,
1566		update_mutable(solver_state([Key:NewData|Rest]), StateMutable).
1567
1568		%% delete_state_instance(+StateMutable, +Key, ?Datum).
1569		delete_state_instance(StateMutable, Key, Datum) :-
1570		get_mutable(solver_state(SolverState), StateMutable),
1571		select(Key:Data, SolverState, Rest),
1572		( Key == heuristic_avl
1573		-> Datum = (SatVarName,Score),
1574		( avl_delete(SatVarName, Data, Score, NewData)
1575		; NewData = Data
1576		)
1577		; Key == sat_stack,
1578		Datum = (SatVarName,A,B,C,D),
1579		( avl_delete(SatVarName, Data, (A,B,C,D), NewData)
1580		; NewData = Data
1581		)
1582		),
1583		!,
1584		update_mutable(solver_state([Key:NewData|Rest]), StateMutable).
1585
1586		%% update_full_state(+StateMutable, +Key, +Datum).
1587		update_full_state(StateMutable, Key, Datum) :-
1588		get_mutable(solver_state(SolverState), StateMutable),
1589		select(Key:_, SolverState, Rest), !,
1590		update_mutable(solver_state([Key:Datum|Rest]), StateMutable).
1591
1592		%% Initialize the dynamic solver state for a specific solver.
1593		init_dynamic_solver_state(SolverName) :-
1594		clean_dynamic_solver_state,
1595		asserta(solver_name(SolverName)),
1596		asserta(restarts(0)),
1597		asserta(amount_clause_reductions(0)),
1598		asserta(amount_learned_clauses(0)),
1599		asserta(conflict_stats(total(0), since_restart(0), since_reduction(0))),
1600		asserta(recent_lbds_dl(Diff1-Diff1, 0)),
1601		asserta(recent_stack_sizes_dl(Diff2-Diff2, 0)),
1602		asserta(total_lbd_sum(0)),
1603		init_luby_sequence.
1604
1605		clean_dynamic_solver_state :-
1606		retractall(solver_name(_)),
1607		retractall(restarts(_)),
1608		retractall(is_restart),
1609		retractall(bt_from_smt_solution),
1610		retractall(recent_lbds_dl(_, _)),
1611		retractall(recent_stack_sizes_dl(_, _)),
1612		retractall(saved_phase(_, _)),
1613		retractall(amount_clause_reductions(_)),
1614		retractall(amount_learned_clauses(_)),
1615		retractall(luby_counter(_)),
1616		retractall(exclude_sat_solution_clause(_)),
1617		retractall(total_lbd_sum(_)),
1618		retractall(conflict_stats(_, _, _)),
1619		retractall(idl_unsat_core(_)),
1620		retractall(backjump_wd_level(_)),
1621		retractall(backjump_wd_clause(_,_,_)),
1622		retractall(backjump_level(_)),
1623		retractall(backjump_clause(_, _, _, _)),
1624		( incremental_mode
1625		-> true
1626		; retractall(memoize_backjump_clause(_, _, _))
1627		).
1628
1629		%% Remove dynamically stored unsat core found by the IDL solver.
1630		remove_idl_unsat_core :-
1631		retractall(idl_unsat_core(_)).
1632
1633		%% Store an unsat core found by the IDL solver in the SMT solvers dynamic state.
1634		store_idl_unsat_core(Core) :-
1635		retractall(idl_unsat_core(_)),
1636		asserta(idl_unsat_core(Core)).
1637
1638		%% Announce backtracking after a solution has been found in order to backtrack to search for another solution.
1639		%% We have to be able to distinguish between backtracking due to not finding a solution or backtracking
1640		%% triggered by the user to find another solution.
1641		announce_bt_from_smt_solution :-
1642		asserta(bt_from_smt_solution).
1643		%%%%%
1644
1645		%% b_to_cnf(+In, +State, -Out).
1646		% Accepts predicates with conjunction and disjunction.
1647		b_to_cnf(In, State, Out) :-
1648		get_texpr_expr(In, Expr),
1649		b_to_cnf_aux(Expr, State, Out),
1650		!.
1651		b_to_cnf(In, _, _) :-
1652		translate_bexpression(In, PPIn),
1653		!,
1654		add_error_fail(b_to_cnf, 'CNF conversion failed', PPIn).
1655
1656		b_to_cnf_aux(identifier(Name), State, [[pred_true-Res-Name]]) :- !,
1657		member(bind(Name,Res), State).
1658		b_to_cnf_aux(X, _, [Out]) :-
1659		( b_pred_or_bool_true(X)
1660		-> Out = [pred_true-pred_true-nonvar]
1661		; b_pred_or_bool_false(X)
1662		-> Out = []
1663		; fail
1664		), !.
1665
1666		b_to_cnf_aux(equal(A,B), State, CNF) :-
1667		ground(B),
1668		get_texpr_expr(B, Expr),
1669		( b_pred_or_bool_true(Expr)
1670		-> b_to_cnf(A, State, CNF)
1671		; %b_pred_or_bool_false(Expr),
1672		safe_create_texpr(value(pred_true), boolean, [], True),
1673		safe_create_texpr(equal(A,True), pred, [], EqualTrue),
1674		b_to_cnf_aux(negation(EqualTrue), State, CNF)
1675		).
1676		b_to_cnf_aux(negation(A), State, [[Res]]) :-
1677		b_to_cnf(A, State, [[Pol-Var-Name]]),
1678		( Pol == pred_true
1679		-> Res = pred_false-Var-Name
1680		; Pol == pred_false,
1681		Res = pred_true-Var-Name
1682		).
1683		b_to_cnf_aux(disjunct(D1,D2), State, Res) :-
1684		get_texpr_expr(D1, conjunct(A,B)),
1685		!,
1686		b_to_cnf(b(disjunct(A,D2),pred,[]), State, RDJ1),
1687		b_to_cnf(b(disjunct(B,D2),pred,[]), State, RDJ2),
1688		append(RDJ1, RDJ2, Res).
1689		b_to_cnf_aux(disjunct(D1,D2), State, Res) :-
1690		get_texpr_expr(D2, conjunct(A,B)),
1691		!,
1692		b_to_cnf(b(disjunct(D1,A),pred,[]), State, RDJ1),
1693		b_to_cnf(b(disjunct(D1,B),pred,[]), State, RDJ2),
1694		append(RDJ1, RDJ2, Res).
1695		b_to_cnf_aux(disjunct(D1,D2),State,Res) :-
1696		b_to_cnf(D1, State, TResD1),
1697		b_to_cnf(D2, State, TResD2),
1698		( TResD1 = [ResD1],
1699		TResD2 = [ResD2]
1700		-> append(ResD1, ResD2, DRes),
1701		Res = [DRes]
1702		; TResD1 = [ClauseResD1],
1703		TResD2 \= [_]
1704		-> maplist(append(ClauseResD1), TResD2, Res)
1705		; TResD2 = [ClauseResD2],
1706		TResD1 \= [_]
1707		-> maplist(append(ClauseResD2), TResD1, Res)
1708		; disjunct_non_singleton_cnfs(TResD1, TResD2, Res)
1709		).
1710		b_to_cnf_aux(conjunct(A,B), State, Res) :-
1711		b_to_cnf(A, State, RA),
1712		b_to_cnf(B, State, RB),
1713		append(RA, RB, Res).
1714
1715		%% disjunct_non_singleton_cnfs(+Cnf1, +Cnf2, -Cnf).
1716		disjunct_non_singleton_cnfs([], Cnf, Cnf).
1717		disjunct_non_singleton_cnfs([Clause|T], Cnf2, Cnf) :-
1718		maplist(append(Clause), Cnf2, NCnf2),
1719		disjunct_non_singleton_cnfs(T, NCnf2, Cnf).
1720
1721		:- dynamic luby_counter/1.
1722		:- volatile luby_counter/1.
1723
1724		% Used for random restarts.
1725		% First restart is after 32nd conflict, second after additional 32 conflicts,
1726		% third after additional 64 conflicts etc.
1727		init_luby_sequence :-
1728		retractall(luby_counter(_)),
1729		% unit length of 32
1730		% 1,1,2,1,1,2,4,1,1,2,1,1,2,4,8,..
1731		assertz(luby_counter(1)),
1732		assertz(luby_counter(1)),
1733		assertz(luby_counter(2)),
1734		assertz(luby_counter(1)),
1735		assertz(luby_counter(1)),
1736		assertz(luby_counter(2)),
1737		assertz(luby_counter(4)),
1738		assertz(luby_counter(1)),
1739		assertz(luby_counter(1)),
1740		assertz(luby_counter(2)),
1741		assertz(luby_counter(1)),
1742		assertz(luby_counter(1)),
1743		assertz(luby_counter(2)),
1744		assertz(luby_counter(4)),
1745		assertz(luby_counter(8)),
1746		assertz(luby_counter(1)),
1747		assertz(luby_counter(1)),
1748		assertz(luby_counter(2)),
1749		assertz(luby_counter(1)),
1750		assertz(luby_counter(1)),
1751		assertz(luby_counter(2)),
1752		assertz(luby_counter(4)),
1753		assertz(luby_counter(8)),
1754		assertz(luby_counter(16)),
1755		assertz(luby_counter(1)),
1756		assertz(luby_counter(1)),
1757		assertz(luby_counter(2)),
1758		assertz(luby_counter(1)),
1759		assertz(luby_counter(1)),
1760		assertz(luby_counter(2)),
1761		assertz(luby_counter(4)),
1762		assertz(luby_counter(8)),
1763		assertz(luby_counter(16)),
1764		assertz(luby_counter(32)),
1765		assertz(luby_counter(1)),
1766		assertz(luby_counter(1)),
1767		assertz(luby_counter(2)),
1768		assertz(luby_counter(1)),
1769		assertz(luby_counter(1)),
1770		assertz(luby_counter(2)),
1771		assertz(luby_counter(4)),
1772		assertz(luby_counter(8)),
1773		assertz(luby_counter(16)),
1774		assertz(luby_counter(32)),
1775		assertz(luby_counter(64)),
1776		assertz(luby_counter(1)),
1777		assertz(luby_counter(1)),
1778		assertz(luby_counter(2)),
1779		assertz(luby_counter(1)),
1780		assertz(luby_counter(1)),
1781		assertz(luby_counter(2)),
1782		assertz(luby_counter(4)),
1783		assertz(luby_counter(8)),
1784		assertz(luby_counter(16)),
1785		assertz(luby_counter(32)),
1786		assertz(luby_counter(64)),
1787		assertz(luby_counter(128)).
1788
1789		% ----------------
1790
1791		%% simplify_cnf(+CNF, -Simplified).
1792		% Boolean resolution.
1793		simplify_cnf([], []).
1794		simplify_cnf([Clause|T], NewCnf) :-
1795		simplify_clause(Clause, _, Simplified, IsTrue), !,
1796		Simplified \== [], % contradiction if a clause is empty
1797		( IsTrue == true
1798		-> NewCnf = NT % remove true clauses
1799		; NewCnf = [Simplified|NT]
1800		),
1801		simplify_cnf(T, NT).
1802
1803		simplify_clause([], IsTrue, [], IsTrue).
1804		simplify_clause([Pol-Var-_|T], IsTrueAcc, NT, IsTrue) :-
1805		ground(Var),
1806		Pol \== Var,
1807		!,
1808		simplify_clause(T, IsTrueAcc, NT, IsTrue).
1809		simplify_clause([Pol-Var-SatVarName|T], IsTrueAcc, [Pol-Var-SatVarName|NT], IsTrue) :-
1810		( Pol == Var
1811		-> IsTrueAcc = true
1812		; true
1813		),
1814		simplify_clause(T, IsTrueAcc, NT, IsTrue).
1815
1816		clause_order(_-_-A3, _-_-B3) :- A3 @< B3.
1817
1818		%% unit_propagate_cnf(+StateMutable, +Clauses, -NewClauses).
1819		% A simple unit propagation, useful to run before reification.
1820		% Removes duplicates from each clause.
1821		% Important to identify all unit clauses, b_to_cnf does not check for unique sat variables in clauses.
1822		unit_propagate_cnf(SolverEnv, StateMutable, Clauses, NewClauses) :-
1823		unit_prop_clause_sort(true, SolverEnv, StateMutable, Clauses, _, _, TNewClauses),
1824		simplify_cnf(TNewClauses, NewClauses).
1825
1826		%% exhaustive_unit_propagate_cnf(+SolverEnv, +StateMutable, +Clauses, -NewClauses).
1827		% Exhaustive unit propagation until no more unit clause is present.
1828		% Simplifies CNF after unit propagation and checks for unit clauses again.
1829		% Removes duplicates from each clause once.
1830		exhaustive_unit_propagate_cnf(SolverEnv, StateMutable, Clauses, NewClauses) :-
1831		unit_prop_clause_sort(true, SolverEnv, StateMutable, Clauses, _, Resolved, TNewClauses),
1832		exhaustive_unit_propagate_cnf_loop(SolverEnv, StateMutable, Resolved, TNewClauses, NewClauses).
1833
1834		exhaustive_unit_propagate_cnf_loop(_, _, false, CAcc, NewClauses) :-
1835		!,
1836		NewClauses = CAcc.
1837		exhaustive_unit_propagate_cnf_loop(SolverEnv, StateMutable, true, Cnf, NewCnf) :-
1838		simplify_cnf(Cnf, SimplifiedCnf),
1839		unit_prop_clause_sort(false, SolverEnv, StateMutable, SimplifiedCnf, _, Resolved, TNewCnf),
1840		exhaustive_unit_propagate_cnf_loop(SolverEnv, StateMutable, Resolved, TNewCnf, NewCnf).
1841
1842		%% unit_prop_clause_sort(+Sort, +StateMutable, +CNF, +RAcc, -Resolved, -NewClauses).
1843		% Removes duplicates from each clause if +Sort is true.
1844		% Logs if a variable has been unit propagated in -Resolved using +RAcc.
1845		unit_prop_clause_sort(_, _, _, [], RAcc, RAcc, []).
1846		unit_prop_clause_sort(Sort, SolverEnv, StateMutable, [Clause|T], RAcc, Resolved, NewClauses) :-
1847		( Sort = true
1848		-> sort(Clause, TNewClause),
1849		samsort(clause_order, TNewClause, NewClause)
1850		; NewClause = Clause
1851		),
1852		( NewClause = [pred_false-pred_false-nonvar]
1853		-> % false on the top level conjunction
1854		fail
1855		; NewClause = [pred_true-pred_true-nonvar]
1856		-> % true on the top level conjunction; remove clause
1857		NewClauses = NT
1858		; NewClause = [Pol-PrologVar-SatVarName]
1859		-> PrologVar = Pol,
1860		RAcc = true,
1861		debug_format_sat("deterministic unit propagation of ~w with polarity ~w before reification", [SatVarName,Pol]),
1862		bt_log_sat_stack(StateMutable, SatVarName, unit, 0, Pol, [Pol-PrologVar-SatVarName]),
1863		NewClauses = NT
1864		; NewClauses = [NewClause|NT]
1865		),
1866		unit_prop_clause_sort(Sort, SolverEnv, StateMutable, T, RAcc, Resolved, NT).
1867
1868		% ----------------
1869
1870		portray_sat_stack(StateMutable) :-
1871		get_full_state(StateMutable, sat_stack, SatStack),
1872		forall(avl_member(Key, SatStack, Val), format("~w,~w~n", [Key,Val])).
1873
1874		portray_cnf(Clauses) :- length(Clauses,Len), format('CNF with ~w clauses:~n',[Len]),
1875		maplist(portray_sat_clause,Clauses).
1876
1877		portray_sat_clause(Clause) :- write(' '),maplist(portray_literal,Clause),nl.
1878
1879		portray_literal(pred_false-PrologVar-ID) :- !, format('- ~w(~w) ',[ID,PrologVar]).
1880		portray_literal(pred_true-PrologVar-ID) :- !, format(' ~w(~w) ',[ID,PrologVar]).
1881		portray_literal(Lit) :- format(' *** UNKNOWN: ~w ',[Lit]).
1882
1883		% ----------------
1884
1885
1886
1887		/*
1888		%% static_sat_symmetry_breaking(+Clauses, +SolverEnv, +CurLevelMut, -NewSolverEnv).
1889		% Static SAT symmetry breaking after unit propagation of problem_setup/3 but only once, e.g., not after a restart or bj to level 0
1890		% Can only be used for pure SAT solving.
1891		static_sat_symmetry_breaking(_, SolverEnv, _, NewSolverEnv) :-
1892		static_sat_symmetry_breaking(false),
1893		!,
1894		NewSolverEnv = SolverEnv.
1895		static_sat_symmetry_breaking(Clauses, SolverEnv, CurLevelMut, NewSolverEnv) :-
1896		\+ symmetry_breaking_pred(_, _),
1897		!,
1898		get_symmetry_breaking_predicates(Clauses, SBPsConjNoRef, NewSatVars),
1899		asserta(symmetry_breaking_pred(SBPsConjNoRef,NewSatVars)),
1900		static_sat_symmetry_breaking(Clauses, SolverEnv, CurLevelMut, NewSolverEnv).
1901		static_sat_symmetry_breaking(_, SolverEnv, CurLevelMut, NewSolverEnv) :-
1902		get_asserted_symmetry_breaking_pred(SolverEnv, SBPsConj, NewSolverEnv),
1903		problem_setup(NewSolverEnv, CurLevelMut, SBPsConj).
1904
1905		get_asserted_symmetry_breaking_pred(SolverEnv, SBPsConj, NewSolverEnv) :-
1906		symmetry_breaking_pred(SBPsConjNoRef, NewSatVars),
1907		add_symmetry_breaking_eqs_to_solver_env(NewSatVars, SolverEnv, NewSolverEnv),
1908		get_from_solver_env(NewSolverEnv, pl_vars, PlVars),
1909		set_variable_references_in_clauses(PlVars, SBPsConjNoRef, SBPsConj),
1910		findall(Var, (member(Var, NewSatVars), bt_asserta(heuristic_tuple(Var,1))), _).
1911
1912		%% add_symmetry_breaking_eqs_to_solver_env(+NewSatVars, +SolverEnv, -NewSolverEnv).
1913		% Symmetry breaking might introduce new SAT variables for equalities inbetween cycles of permutations.
1914		% We update the solver environment and create the corresponding SMT formulas for equalities here.
1915		% This is necessary, e.g., if a SAT variable corresponding to an equality introduced
1916		% from symmetry breaking is involved in a conflict.
1917		add_symmetry_breaking_eqs_to_solver_env(NewSatVars, SolverEnv, NewSolverEnv) :-
1918		SolverEnv = [sat_vars:SatVars,sat_varnames:SatVarNames,sat_bindings:SatBindings,t2b_env:Env,pl_vars:PrologSatVarTriple],
1919		add_symmetry_breaking_eqs_to_solver_env(NewSatVars, SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple, NSatVars, NSatVarNames, NSatBindings, NEnv, NPrologSatVarTriple),
1920		NewSolverEnv = [sat_vars:NSatVars,sat_varnames:NSatVarNames,sat_bindings:NSatBindings,t2b_env:NEnv,pl_vars:NPrologSatVarTriple].
1921
1922		add_symmetry_breaking_eqs_to_solver_env([], SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple, SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple).
1923		add_symmetry_breaking_eqs_to_solver_env([NewSatVarName-EqClauses|T], SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple, NSatVars, NSatVarNames, NSatBindings, NEnv, NPrologSatVarTriple) :-
1924		maplist(clause_to_smt_disjunction(SatVars), EqClauses, EqSmtClauses),
1925		conjunct_predicates(EqSmtClauses, EqSmt1), % all true
1926		maplist(negate_smt_formula, EqSmtClauses, NegEqSmtClauses),
1927		conjunct_predicates(NegEqSmtClauses, EqSmt2), % or all false
1928		EqSmt = b(disjunct(EqSmt1,EqSmt2),pred,[]),
1929		SatVars1 = [b(identifier(NewSatVarName),boolean,[smt_formula(EqSmt),eq_symmetry_break])|SatVars],
1930		SatVarNames1 = [NewSatVarName|SatVarNames],
1931		SatBindings1 = [bind(NewSatVarName,Var)|SatBindings],
1932		PrologSatVarTriple1 = [Var-NewSatVarName-EqSmt|PrologSatVarTriple],
1933		Env1 = [(EqSmt,b(identifier(NewSatVarName),boolean,[]))|Env],
1934		add_symmetry_breaking_eqs_to_solver_env(T, SatVars1, SatVarNames1, SatBindings1, Env1, PrologSatVarTriple1, NSatVars, NSatVarNames, NSatBindings, NEnv, NPrologSatVarTriple).
1935
1936		%clause_to_smt_disjunction(_, [], b(truth,pred,[])).
1937		clause_to_smt_disjunction(SatVars, [Pol-_-SatVarName|T], SmtDisj) :-
1938		get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula),
1939		clause_to_smt_disjunction(SatVars, T, SmtFormula, SmtDisj).
1940
1941		clause_to_smt_disjunction(_, [], Acc, Acc).
1942		clause_to_smt_disjunction(SatVars, [Pol-_-SatVarName|T], Acc, SmtDisj) :-
1943		get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula),
1944		NAcc = b(disjunct(SmtFormula,Acc),pred,[]),
1945		clause_to_smt_disjunction(SatVars, T, NAcc, SmtDisj).
1946		*/