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