1		% (c) 2019-2024 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_solver, [cdcl_sat_solve_predicate/2,
6		cdcl_sat_solve_predicate_in_state/3,
7		cdclt_solve_predicate/3,
8		cdclt_solve_predicate/4,
9		cdclt_solve_predicate_in_state/4,
10		cdclt_solve_predicate_in_state/5,
11		get_amount_of_sat_variables/2]).
12
13		:- use_module(library(lists)).
14		:- use_module(library(timeout)).
15		:- use_module(library(sets), [subtract/3,add_element/3]).
16		:- use_module(library(clpfd), [fd_var/1, fd_min/2, fd_max/2]).
17
18		:- use_module(smt_solvers_interface(ast_optimizer_for_smt)).
19
20		:- use_module(cdclt_solver('symmetry_check/smt_symmetry_breaking')).
21		:- use_module(cdclt_solver('cdclt_stats')).
22		:- use_module(cdclt_solver('cdclt_preprocessing')).
23		:- use_module(cdclt_solver('cdclt_pred_to_sat')).
24		:- use_module(cdclt_solver('cdclt_sat_solver')).
25		:- use_module(cdclt_solver('difference_logic/difference_logic_solver')).
26		:- use_module(cdclt_solver('difference_logic/ast_to_difference_logic')).
27		:- use_module(cdclt_solver('cdclt_settings')).
28
29		:- use_module(probsrc(debug)).
30		:- use_module(probsrc(tools), [ajoin/2]).
31		:- use_module(probsrc(b_ast_cleanup), [clean_up_pred/3]).
32		:- use_module(probsrc(preferences), [get_preference/2,
33		temporary_set_preference/2,
34		reset_temporary_preference/1]).
35		:- use_module(probsrc(bmachine), [b_get_machine_variables/1,b_get_machine_constants/1]).
36		:- use_module(probsrc(b_global_sets), [list_contains_unfixed_deferred_set_id/1]).
37		:- use_module(probsrc(b_compiler), [b_compile/6]).
38		:- use_module(probsrc(b_enumerate), [b_tighter_enumerate_all_values/2]).
39		:- use_module(probsrc(tools_meta), [safe_time_out/3]).
40		:- use_module(probsrc(translate), [print_bexpr/1]).
41		:- use_module(probsrc(tools), [start_ms_timer/1,stop_ms_timer_with_debug_msg/2]).
42		:- use_module(probsrc(kernel_waitflags), [init_wait_flags/2,ground_wait_flags/1]).
43		:- use_module(probsrc(kernel_objects), [infer_value_type/2,contains_any/1]).
44		:- use_module(probsrc(b_interpreter), [set_up_typed_localstate/6,
45		b_test_boolean_expression/4,
46		b_convert_bool_timeout/7]).
47		:- use_module(probsrc(error_manager), [error_occurred_in_error_scope/0,
48		add_error/3,
49		add_error_and_fail/3,
50		add_internal_error/2,
51		add_message/3,
52		add_message/4,
53		check_error_occured/2,
54		enter_new_error_scope/2,
55		exit_error_scope/3,
56		clear_enumeration_warnings/0,
57		clear_wd_errors/0,
58		critical_enumeration_warning_occured_in_error_scope/4]).
59		:- use_module(probsrc(bsyntaxtree), [find_typed_identifier_uses/2,
60		find_typed_identifier_uses/3,
61		find_identifier_uses/3,
62		check_ast/1,
63		get_texpr_info/2,
64		conjunct_predicates/2,
65		safe_create_texpr/4]).
66		%:- use_module(probsrc('well_def/well_def_analyser'), [analyse_wd_for_expr/3]).
67		%:- use_module(probsrc('debug'), [set_silent_mode/1]).
68		:- use_module(probsrc(module_information), [module_info/2]).
69
70		:- module_info(group, cdclt).
71		:- module_info(description,'This module provides a CDCL(T) based solver for B.').
72
73		:- dynamic initial_solution/0, unfixed_deferred_set_error_after_grounding/0, unfixed_deferred_set_has_been_propagated/0, solve_in_state/0, idl_candidate_constants/2, grounding_timeout_occurred/0, grounding_fallback_z3/0, additional_z3_reification/0.
74
75		%% Use a small timeout for grounding with ProB and fall back to Z3 if time limit exceeded.
76		grounding_fallback_z3.
77		% Additionally reify constraints with Z3 using the incremental solver.
78		%additional_z3_reification.
79
80		debug_format_cdclt(_, _) :-
81		print_logs(false),
82		!.
83		debug_format_cdclt(Msg, Vars) :-
84		append(Msg, " (CDCL(T) Solver)~n", NCodes),
85		format(NCodes, Vars), !.
86
87		debug_format_cdclt(_, _, _) :-
88		print_logs(false),
89		!.
90		debug_format_cdclt(Msg, Vars, Pred) :-
91		format(Msg, Vars),
92		translate:print_bexpr(Pred), nl, !.
93
94		init :-
95		% enumeration has to be linear for symmetry breaking but also set to false by default
96		temporary_set_preference(randomise_enumeration_order, false),
97		cdclt_pred_to_sat:reset_sat_var_id,
98		cdclt_preprocessing:reset_artificial_id_counter,
99		reset_stats,
100		( additional_z3_reification
101		-> smt_solvers_interface:reset_smt_supported_interpreter
102		; true
103		),
104		retractall(initial_solution),
105		retractall(grounding_timeout_occurred),
106		retractall(unfixed_deferred_set_error_after_grounding),
107		retractall(unfixed_deferred_set_has_been_propagated),
108		retractall(solve_in_state),
109		retractall(idl_candidate_constants(_,_)),
110		%temporary_set_preference(use_chr_solver, true),
111		temporary_set_preference(unsat_core_algorithm, divide_and_conquer), % default is linear_greedy
112		temporary_set_preference(allow_improving_wd_mode, true),
113		%temporary_set_preference(solver_strength, 20000),
114		temporary_set_preference(use_smt_mode, false),
115		temporary_set_preference(use_clpfd_solver, true),
116		temporary_set_preference(optimize_ast, true),
117		temporary_set_preference(use_common_subexpression_elimination, false),
118		temporary_set_preference(add_wd_pos_for_z3, false),
119		temporary_set_preference(normalize_ast_sort_commutative, false),
120		temporary_set_preference(normalize_ast, false).
121
122		reset_preferences :-
123		reset_temporary_preference(randomise_enumeration_order),
124		%reset_temporary_preference(solver_strength),
125		reset_temporary_preference(unsat_core_algorithm),
126		reset_temporary_preference(allow_improving_wd_mode),
127		reset_temporary_preference(use_smt_mode),
128		reset_temporary_preference(use_clpfd_solver),
129		reset_temporary_preference(optimize_ast),
130		reset_temporary_preference(use_common_subexpression_elimination),
131		reset_temporary_preference(add_wd_pos_for_z3),
132		reset_temporary_preference(normalize_ast_sort_commutative),
133		reset_temporary_preference(normalize_ast).
134
135		set_current_state(Pred, TypedIds, State, NPred) :-
136		reset_optimizer_state,
137		assert_state_id_values(TypedIds, State),
138		replace_ids_with_ground_values(Pred, 0, [], NPred),
139		reset_optimizer_state, !.
140
141		%% cdcl_sat_solve_predicate_in_state(+BoolFormula, +State, -Result).
142		cdcl_sat_solve_predicate_in_state(BoolFormula, State, Result) :-
143		include(ground_state_binding, State, GState),
144		get_typed_ids_in_scope_of_pred(BoolFormula, TypedIds),
145		set_current_state(BoolFormula, TypedIds, GState, NPred),
146		get_equalities_from_bindings(GState, TypedIds, EqConj),
147		safe_create_texpr(conjunct(EqConj,NPred), pred, [], Conj),
148		cdcl_sat_solve_predicate(Conj, Result).
149
150		%% cdcl_sat_solve_predicate(+BoolFormula, -Result).
151		% Pure SAT solving without theories.
152		cdcl_sat_solve_predicate(BoolFormula, Result) :-
153		init,
154		get_preference(time_out, Timeout),
155		safe_time_out(cdcl_sat_solve_predicate_no_timeout(BoolFormula, TResult),
156		Timeout,
157		TimeoutResult),
158		( TimeoutResult == time_out
159		-> Result = time_out
160		; Result = TResult
161		).
162
163		analyze_binary_clauses(Clauses, VarsFromBinaryClauses) :-
164		analyze_binary_clauses(Clauses, 0, 0, [], VarsFromBinaryClauses).
165
166		analyze_binary_clauses([], Len, Binary, Acc, Acc) :-
167		debug_format_cdclt("Found ~w clauses ~w of which are binary clauses~n", [Len,Binary]).
168		analyze_binary_clauses([[_-_-_-N1,_-_-_-N2]|T], Len, Binary, Acc, VarsFromBinaryClauses) :-
169		!,
170		add_element(N1, Acc, NAcc1),
171		add_element(N2, NAcc1, NAcc),
172		Len1 is Len + 1,
173		Binary1 is Binary + 1,
174		analyze_binary_clauses(T, Len1, Binary1, NAcc, VarsFromBinaryClauses).
175		analyze_binary_clauses([_|T], Len, Binary, Acc, VarsFromBinaryClauses) :-
176		Len1 is Len + 1,
177		analyze_binary_clauses(T, Len1, Binary, Acc, VarsFromBinaryClauses).
178
179		cdcl_sat_solve_predicate_no_timeout(BoolFormula, Result) :-
180		find_typed_identifier_uses(BoolFormula, [], SatVars),
181		% rewriting similar to Tseitin
182		optimize_clause_size_by_rewriting(BoolFormula, SatVars, TOptBoolFormula, NewSatVars, NewVarConjList),
183		conjunct_predicates(NewVarConjList, NewVarConj),
184		% add new top-level Boolean variables introduced by Tseitin rewriting
185		conjunct_predicates([NewVarConj,TOptBoolFormula], FullBoolFormula),
186		get_bindings_from_ids(NewSatVars, StackBindings, SatBindings, SatVarNames, _IdPrologVarTuples, PrologSatVarTriple),
187		b_to_cnf_safe(FullBoolFormula, StackBindings, CnfBoolFormula),
188		analyze_binary_clauses(CnfBoolFormula, VarsFromBinaryClauses),
189		cdclt_sat_solver:create_solver_state(SatStateMutable),
190		SolverEnv = [sat_vars:NewSatVars,sat_varnames:SatVarNames,sat_bindings:SatBindings,t2b_env:_,pl_vars:PrologSatVarTriple,binary_clause_vars:VarsFromBinaryClauses],
191		( ( cdclt_sat_solver:unit_propagate_cnf(SolverEnv, SatStateMutable, CnfBoolFormula, TCnfBoolFormula2),
192		remove_subsumed_clauses(TCnfBoolFormula2, TCnfBoolFormula3),
193		sort(TCnfBoolFormula3, CnfBoolFormula2),
194		cdclt_sat_solver:sat(default_sat, SolverEnv, SatStateMutable, CnfBoolFormula2)
195		)
196		-> Result = solution(SatBindings)
197		; Result = contradiction_found
198		),
199		print_stats.
200
201		%% cdclt_solve_predicate(+Pred, -SolvedPred, -Result).
202		% Main interface predicate for CDCL(T) based solver which times out
203		% with respect to ProB's time_out preference.
204		cdclt_solve_predicate(Pred, SolvedPred, Result) :-
205		cdclt_solve_predicate(default, Pred, SolvedPred, Result).
206
207		%% cdclt_solve_predicate(+SolverName, +Pred, -SolvedPred, -Result).
208		cdclt_solve_predicate(SolverName, Pred, SolvedPred, Result) :-
209		init,
210		cdclt_solve_predicate_timeout(SolverName, Pred, SolvedPred, Result).
211
212		%% cdclt_solve_predicate_in_state(+Pred, +Pred, -Result).
213		cdclt_solve_predicate_in_state(Pred, State, SolvedPred, Result) :-
214		cdclt_solve_predicate_in_state(default, Pred, State, SolvedPred, Result).
215
216		%% cdclt_solve_predicate_in_state(+SolverName, +Pred, +Pred, -Result).
217		cdclt_solve_predicate_in_state(SolverName, Pred, State, SolvedPred, Result) :-
218		init,
219		include(ground_state_binding, State, GState),
220		get_typed_ids_in_scope_of_pred(Pred, TypedIds),
221		set_current_state(Pred, TypedIds, GState, NPred),
222		get_equalities_from_bindings(GState, TypedIds, EqConj),
223		safe_create_texpr(conjunct(EqConj,NPred), pred, [], Conj),
224		asserta(solve_in_state),
225		cdclt_solve_predicate_timeout(SolverName, Conj, SolvedPred, Result).
226
227		cdclt_solve_predicate_timeout(SolverName, Pred, SolvedPred, Result) :-
228		get_preference(time_out, Timeout),
229		safe_time_out(cdclt_solve_predicate_initialized(SolverName, Pred, TSolvedPred, SolverResult),
230		Timeout,
231		TimeoutResult),
232		( TimeoutResult == time_out
233		-> Result = time_out,
234		SolvedPred = Pred
235		; ground(SolverResult),
236		Result = SolverResult,
237		SolvedPred = TSolvedPred
238		).
239
240		cdclt_solve_predicate_initialized(SolverName, Pred, SolvedPred, Result) :-
241		( check_ast(Pred)
242		-> ( (error_occurred_in_error_scope, check_error_occured(check_ast_typing, _))
243		-> % input AST is not correctly typed
244		SolvedPred = Pred,
245		Result = error
246		; cdclt_solve_predicate_initialized_checked(SolverName, Pred, SolvedPred, Result)
247		)
248		; add_message(cdclt_solve_predicate_no_timeout, 'Input predicate is not well-defined~nProB\'s SMT solver transforms the input to a well-defined predicate before constraint solving~nFor: ',SolverName),
249		cdclt_solve_predicate_initialized_checked(SolverName, Pred, SolvedPred, Result)
250		).
251
252		cdclt_solve_predicate_initialized_checked(SolverName, Pred, SolvedPred, Result) :-
253		call_cleanup(catch(cdclt_solve_predicate_no_timeout(SolverName, Pred, SolvedPred, Result),
254		Exception, % TO DO: catch specific exception instead of all
255		handle_clpfd_overflow(SolverName, Exception, Pred, SolvedPred, Result)
256		),
257		reset_preferences
258		).
259
260		%% handle_clpfd_overflow(+SolverName, +Exception, +Pred, -SolvedPred, -Result).
261		% Disable CLP(FD) interface and restart CDCL(T) if an overflow occurred.
262		handle_clpfd_overflow(SolverName, Exception, Pred, SolvedPred, Result) :-
263		Exception = error(representation_error(Err),_),
264		memberchk(Err, ['CLPFD integer overflow','max_clpfd_integer','min_clpfd_integer']),
265		!,
266		debug_format_cdclt("Handle CLP(FD) overflow error and restart CDCL(T) without CLP(FD).", []),
267		temporary_set_preference(use_clpfd_solver, false),
268		cdclt_solve_predicate_initialized(SolverName, Pred, SolvedPred, Result).
269		handle_clpfd_overflow(SolverName, Exception, Pred, SolvedPred, unknown) :-
270		ajoin(['Exception occured during solving with ',SolverName,':'],Msg),
271		add_error(cdclt,Msg,Exception),
272		SolvedPred = Pred.
273
274		%% cdclt_solve_predicate(+SolverName, +Pred, -SolvedPred, -SolverResult).
275		% Interface predicate for CDCL(T) based solver without a timeout.
276		cdclt_solve_predicate_no_timeout(SolverName, Pred, SolvedPred, SolverResult) :-
277		debug_format_cdclt("Parsed predicate: ", [], Pred),
278		debug_format_cdclt("Start preprocessing", []),
279		cdclt_solve_predicate_no_timeout_cleanup(SolverName, Pred, NPred),
280		debug_format_cdclt("After preprocessing: ", [], NPred),
281		cdclt_solve_predicate_no_timeout_clean(SolverName, NPred, SolvedPred, SolverResult).
282
283		cdclt_solve_predicate_no_timeout_clean(_, b(truth,pred,Info), SolvedPred, SolverResult) :-
284		!,
285		SolvedPred = b(truth,pred,Info),
286		SolverResult = solution([]).
287		cdclt_solve_predicate_no_timeout_clean(_, b(falsity,pred,Info), SolvedPred, SolverResult) :-
288		!,
289		SolvedPred = b(falsity,pred,Info),
290		SolverResult = contradiction_found.
291		cdclt_solve_predicate_no_timeout_clean(SolverName, CleanPred, SolvedPred, SolverResult) :-
292		cdclt_solve_predicate_no_timeout_setup(SolverName, CleanPred, Env, SmtVars, SatVars, WDPosBoolFormula, AnalysisBoolFormula, SmtBoolFormula),
293		cdclt_sat_solver:cnf_to_smt(SmtBoolFormula, SolvedPred),
294		start_ms_timer(Timer),
295		enter_new_error_scope(ScopeID, cdclt_solve_predicate),
296		call_cleanup(conflict_driven_clause_learning_online(SolverName, Env, SmtVars, SatVars, WDPosBoolFormula, AnalysisBoolFormula, SmtBoolFormula, SolverResult),
297		exit_error_scope(ScopeID, _, cdclt_solve_predicate)),
298		stop_ms_timer_with_debug_msg(Timer, cdclt_solving_success),
299		print_stats.
300
301		%% cdclt_solve_predicate_no_timeout_cleanup(+SolverName, +Pred, -NPred).
302		% Some rewriting and cleanup for CDCL(T).
303		cdclt_solve_predicate_no_timeout_cleanup(SolverName, Pred, NPred) :-
304		start_ms_timer(Timer0),
305		simplify_negation(Pred, SPred),
306		debug_format_cdclt("After simplifying negations: ", [], SPred),
307		reset_optimizer_state,
308		assert_ground_id_values(0, SPred),
309		replace_ids_with_ground_values(SPred, 0, [], AstOpt),
310		precompute_values_non_recursive([instantiate_quantifier_limit(0),instantiate_sets_limit(1000)], AstOpt, AstPrecomputed),
311		debug_format_cdclt("After precomputing values: ", [], AstOpt),
312		stop_ms_timer_with_debug_msg(Timer0, precompute_values_for_cdclt),
313		find_identifier_uses(AstPrecomputed, [], UsedIds),
314		temporary_set_preference(data_validation_mode, true),
315		catch(b_compile(AstPrecomputed, UsedIds, [], [], AstCompiled, no_wf_available),
316		enumeration_warning(_,_,_,_,_), % cancel if enumeration warning has occurred
317		AstCompiled = AstPrecomputed),
318		clear_wd_errors, % b_compile might throw a wd error
319		reset_temporary_preference(data_validation_mode),
320		debug_format_cdclt("After compiling values (used ids ~w): ", [UsedIds], AstCompiled),
321		start_ms_timer(Timer2),
322		( clean_up_pred(AstCompiled, _, NPred)
323		-> true
324		; add_internal_error('Clean up failed ',SolverName),
325		NPred = AstCompiled
326		),
327		stop_ms_timer_with_debug_msg(Timer2, clean_up_pred_for_cdclt).
328
329		%% cdclt_solve_predicate_no_timeout_setup(+SolverName, +CleanPred, -Env, -SmtVars, -SatVars, -WDPosBoolFormula, -AnalysisBoolFormula, -SmtBoolFormula).
330		cdclt_solve_predicate_no_timeout_setup(SolverName, CleanPred, Env, SmtVars, SatVars, WDPosBoolFormula, AnalysisBoolFormula, SmtBoolFormula) :-
331		start_ms_timer(Timer),
332		cdclt_settings:static_syntax_analysis(PerformStaticAnalysis),
333		is_rewrite_to_idl(RewriteToIdl),
334		add_symmetry_breaking_predicates_cond(CleanPred, CleanPredSym),
335		preprocess_predicate(PerformStaticAnalysis, RewriteToIdl, CleanPredSym, LiftedPred, InferredImplsConj, CandidateImpls),
336		log_inferred_implications(InferredImplsConj),
337		debug_format_cdclt("Lifted predicate: ", [], LiftedPred),
338		predicate_to_sat(normal, LiftedPred, Env1, WDPOs1, SmtBoolFormula, SatVars1), !,
339		( PerformStaticAnalysis == true
340		-> predicate_to_sat(only_reuse, WDPOs1, SatVars1, Env1, InferredImplsConj, Env3, WDPOsList, ImplBoolFormula, SatVars3),
341		debug_format_cdclt("Static analysis inferred: ", [], ImplBoolFormula)
342		; ImplBoolFormula = b(truth,pred,[]),
343		SatVars3 = SatVars1, Env3 = Env1, WDPOsList = WDPOs1
344		),
345		% well-definedness implication on the top-level to encode well-definedness in the SAT solver
346		conjunct_predicates(WDPOsList, WDPOs),
347		preprocess_predicate(false, RewriteToIdl, WDPOs, LiftedWDPOs, _, WDCandidateImpls),
348		% theory deduction for wd
349		get_wd_theory_implications(CandidateImpls, WDCandidateImpls, WDTheoryImpls),
350		log_inferred_wd_theory_implications(InferredImplsConj),
351		predicate_to_sat(normal, [], SatVars3, Env3, WDTheoryImpls, Env4, _, WDTheoryImplsBoolFormula, SatVars4),
352		debug_format_cdclt("WD Theory Deduction Implications: ", [], WDTheoryImpls),
353		predicate_to_sat(normal, [], SatVars4, Env4, LiftedWDPOs, Env5, WDPOsList2, WDPosBoolFormula1, SatVars5),
354		% there can be WD POs that also have WD POs
355		conjunct_predicates(WDPOsList2, WDPOs2),
356		preprocess_predicate(false, RewriteToIdl, WDPOs2, LiftedWDPOs2, _, _),
357		predicate_to_sat(normal, [], SatVars5, Env5, LiftedWDPOs2, Env, _, WDPosBoolFormula2, SatVars),
358		conjunct_predicates([WDPosBoolFormula1,WDPosBoolFormula2], WDPosBoolFormula),
359		( SatVars3 \== SatVars
360		-> %set_silent_mode(on),
361		%analyse_wd_for_expr(CleanPred, _ResStr, _IsWd), % prints missing WD conditions
362		%set_silent_mode(off),
363		add_message(cdclt_solve_predicate_no_timeout_setup, 'Input not well-defined: automatically added WD POs for solver ',SolverName)
364		; true
365		),
366		debug_format_cdclt("WD Implication: ", [], LiftedWDPOs),
367		debug_format_cdclt("WD Implication as Boolean formula: ", [], WDPosBoolFormula),
368		!,
369		conjunct_predicates([WDTheoryImplsBoolFormula,ImplBoolFormula], AnalysisBoolFormula),
370		find_typed_identifier_uses(LiftedPred, SmtVars), % no global sets or constants are considered here
371		debug_format_cdclt("Check LiftedPred", []),
372		( check_ast(LiftedPred)
373		-> true
374		; add_internal_error('AST is missing well-definedness information for solver ', SolverName)
375		),
376		%translate:nested_print_bexpr(LiftedPred),nl,
377		stop_ms_timer_with_debug_msg(Timer, preprocessing_for_cdclt),
378		debug_format_cdclt("End preprocessing", []),
379		!.
380		cdclt_solve_predicate_no_timeout_setup(_, Pred, _, _, _, _, _, _) :-
381		add_error_and_fail(cdclt_solve_predicate, 'Cannot create SAT formula from B predicate:', [Pred]).
382
383		%% add_symmetry_breaking_predicates_cond(+Pred, -SymPred).
384		add_symmetry_breaking_predicates_cond(Pred, SymPred) :-
385		cdclt_settings:static_smt_symmetry_breaking(true),
386		!,
387		debug_format_cdclt("Start symmetry breaking..", []),
388		( add_symmetry_breaking_predicates(Pred, SymPred),
389		get_amount_of_found_sbps(FoundSBPs),
390		log_symmetry_breaking_stats(FoundSBPs),
391		debug_format_cdclt("done.", [])
392		-> true
393		; add_message(smt_symmetry_breaking, 'Symmetry breaking failed for: ',Pred),
394		SymPred = Pred
395		).
396		add_symmetry_breaking_predicates_cond(Pred, Pred).
397
398		is_rewrite_to_idl(Res) :-
399		get_preference(cdclt_use_idl_theory_solver,true),
400		!,
401		Res = true.
402		is_rewrite_to_idl(false).
403
404		%% conflict_driven_clause_learning_online(+SolverName, +Env, +SmtVars, +SatVars, +WDPosBoolFormula, +AnalysisBoolFormula, +BoolFormula, -SolverResult).
405		% Conflict-driven clause learning from incomplete assignments of the boolean formula by setting up reification constraints (b_interpreter:b_convert_bool_timeout/7)
406		% connecting the SAT and theory solver. IDL constraint solver uses custom coroutines for the reification (cdclt_solver:idl_solver_interface/3).
407		conflict_driven_clause_learning_online(_, _, _, _, _, _, b(truth,pred,_), SolverResult) :-
408		!,
409		SolverResult = solution([]).
410		conflict_driven_clause_learning_online(_, _, _, _, _, _, b(falsity,pred,_), SolverResult) :-
411		!,
412		SolverResult = contradiction_found.
413		conflict_driven_clause_learning_online(SolverName, Env, SmtVars, SatVars, WDPosBoolFormula, AnalysisBoolFormula, BoolFormula, SolverResult) :-
414		% rewriting similar to Tseitin
415		optimize_clause_size_by_rewriting(BoolFormula, SatVars, TOptBoolFormula, NewSatVars, NewVarConjList),
416		conjunct_predicates(NewVarConjList, NewVarConj),
417		conjunct_predicates([AnalysisBoolFormula,TOptBoolFormula], TFullBoolFormula),
418		% add new top-level Boolean variables introduced by Tseitin rewriting
419		( NewVarConj = b(truth,pred,_)
420		-> FullBoolFormula = TFullBoolFormula
421		; safe_create_texpr(conjunct(NewVarConj,TFullBoolFormula), pred, [], FullBoolFormula)
422		),
423		get_bindings_from_ids(NewSatVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PlVars),
424		b_to_cnf_safe(FullBoolFormula, StackBindings, CnfBoolFormula),
425		setup_theory_wf_store(SmtVars, SmtBindings, WfStoreSmt),
426		( get_preference(cdclt_use_idl_theory_solver,true)
427		-> difference_logic_solver:init_idl_solver(IdlGraphMut)
428		; true
429		),
430		( WDPosBoolFormula \= b(truth,pred,_)
431		-> % add WD PO implications
432		b_to_cnf_safe(WDPosBoolFormula, StackBindings, CnfWDPosBoolFormula),
433		append(CnfWDPosBoolFormula, CnfBoolFormula, TNCnfBoolFormula)
434		; TNCnfBoolFormula = CnfBoolFormula
435		),
436		cdclt_sat_solver:create_solver_state(SatStateMutable),
437		SolverEnv = [sat_vars:NewSatVars,sat_varnames:SatVarNames,sat_bindings:SatBindings,t2b_env:Env,pl_vars:PlVars],
438		log_unique_predicates(SatVarNames),
439		cdclt_sat_solver:unit_propagate_cnf(SolverEnv, SatStateMutable, TNCnfBoolFormula, TNCnfBoolFormula2),
440		remove_subsumed_clauses(TNCnfBoolFormula2, TNCnfBoolFormula3),
441		sort(TNCnfBoolFormula3, NCnfBoolFormula),
442		( debug_mode(off)
443		-> true
444		; cdclt_sat_solver:portray_cnf(NCnfBoolFormula)
445		),
446		analyze_binary_clauses(CnfBoolFormula, VarsFromBinaryClauses),
447		NSolverEnv = [sat_vars:NewSatVars,sat_varnames:SatVarNames,sat_bindings:SatBindings,t2b_env:Env,pl_vars:PlVars,binary_clause_vars:VarsFromBinaryClauses],
448		setup_reification(SatStateMutable, IdlGraphMut, IdPrologVarTuples, SmtBindings, WfStoreSmt),
449		cdclt_sat_solver:sat(SolverName, NSolverEnv, SatStateMutable, NCnfBoolFormula, [allow_partial_model]),
450		retractall(unfixed_deferred_set_error_after_grounding),
451		cdclt_sat_solver:clear_pending_theory_propagations,
452		( severe_error_occurred
453		-> % error occurred during SAT solving
454		!,
455		SolverResult = error
456		; debug_format_cdclt("Ground waitflags", []),
457		remove_pending_theory_propagations_on_bt,
458		( conflict_driven_clause_learning_online_grounding(IdlGraphMut, SmtVars, PlVars, SmtBindings, WfStoreSmt, SolverResult)
459		-> true
460		; ( unfixed_deferred_set_has_been_propagated
461		-> % a contradiction has been found but at least one unfixed deferred set has been propagated
462		% we thus do not know if it's a genuine contradiction
463		asserta(unfixed_deferred_set_error_after_grounding),
464		fail
465		; % this is a genuine contradiction after grounding
466		fail
467		)
468		)
469		).
470		conflict_driven_clause_learning_online(_, _, _, _, _, _, _, Res) :-
471		\+ wd_error_occurred_in_error_scope(_),
472		critical_enumeration_warning_occured_in_error_scope(A, B, C, D),
473		!,
474		clear_enumeration_warnings,
475		Res = no_solution_found(enumeration_warning(A,B,C,D,critical)).
476		conflict_driven_clause_learning_online(_, _, _, _, _, _, _, Res) :-
477		severe_error_occurred,
478		!,
479		Res = error.
480		conflict_driven_clause_learning_online(_, _, _, _, _, _, _, error) :-
481		\+ initial_solution,
482		wd_error_occurred_in_error_scope(Reason),
483		add_error(well_definedness_error, Reason, 'conflict_driven_clause_learning_online').
484		conflict_driven_clause_learning_online(_, _, _, _, _, _, _, Res) :-
485		( grounding_timeout_occurred
486		; cdclt_sat_solver:assignment_timeout_occurred
487		),
488		!,
489		Res = no_solution_found(solver_answered_unknown).
490		conflict_driven_clause_learning_online(_, _, _, _, _, _, _, no_solution_found(unfixed_deferred_sets)) :-
491		\+ solve_in_state,
492		( cdclt_sat_solver:unfixed_deferred_set_error_occurred
493		; unfixed_deferred_set_error_after_grounding
494		; unfixed_deferred_set_has_been_propagated
495		).
496		conflict_driven_clause_learning_online(_, _, _, _, _, _, _, contradiction_found) :-
497		\+ initial_solution,
498		( solve_in_state
499		-> true
500		; \+ unfixed_deferred_set_error_after_grounding,
501		\+ cdclt_sat_solver:unfixed_deferred_set_error_occurred,
502		\+ unfixed_deferred_set_has_been_propagated
503		),
504		\+ wd_error_occurred_in_error_scope(_).
505
506		% Backtracking after grounding: We have either found a solution or a conflict.
507		% If a conflict has been found, it can be a theory conflict in the SAT solver
508		% (pending props have already been used for CDCL) or we just backtrack to the last decision.
509		% In all cases, remove all pending theory propagations now.
510		remove_pending_theory_propagations_on_bt :-
511		( true
512		; cdclt_sat_solver:clear_pending_theory_propagations,
513		debug_format_cdclt("backtrack after grounding waitflags", []),
514		fail
515		).
516
517		:- use_module(smt_solvers_interface(smt_solvers_interface)).
518
519		%% conflict_driven_clause_learning_online_grounding(+IdlGraphMut, +SmtVars, +PlVars, +SmtBindings, +WfStoreSmt, -SolverResult).
520		% Use IDL theory solver if option is set and enter ProB's grounding phase.
521		conflict_driven_clause_learning_online_grounding(IdlGraphMut, SmtVars, _, SmtBindings, WfStoreSmt, SolverResult) :-
522		get_preference(cdclt_use_idl_theory_solver, true),
523		!,
524		add_typed_ids_in_scope(SmtVars, StateTypedIds),
525		propagate_fd_bounds_to_idl_solver(IdlGraphMut, SmtBindings),
526		get_idl_solution_bindings(IdlGraphMut, IdlBindings),
527		( % try one idl solution first since ProB could timeout, but do not enumerate idl solutions here
528		set_bindings(IdlBindings, SmtBindings),
529		ground_wait_flags(WfStoreSmt)
530		; exclude_idl_solution(IdlBindings, SmtBindings, StateTypedIds, WfStoreSmt),
531		( ground_wait_flags(WfStoreSmt)
532		; % fallback to idl solver and possibly enumerate all solutions
533		critical_enumeration_warning_occured_in_error_scope(_, _, _, _),
534		clear_enumeration_warnings,
535		propagate_idl_solution_to_bindings_bt(IdlGraphMut, SmtBindings),
536		ground_wait_flags(WfStoreSmt)
537		)
538		),
539		finalize_smt_solution(SmtBindings, SolverResult).
540		conflict_driven_clause_learning_online_grounding(_, _, PlVars, SmtBindings, WfStoreSmt, SolverResult) :-
541		grounding_fallback_z3,
542		!,
543		( grounding_timeout_occurred
544		-> % use a smaller time limit if a timeout already occurred
545		GroundTimeout = 5000
546		; GroundTimeout = 30000
547		),
548		safe_time_out(ground_wait_flags(WfStoreSmt),
549		GroundTimeout,
550		TimeOutRes),
551		( TimeOutRes == time_out
552		-> debug_format_cdclt("Timeout when grounding with ProB. Fallback to Z3.", []),
553		sat_bindings_to_smt_formula(PlVars, SmtFormula),
554		safe_time_out(smt_solve_predicate(z3, [check_sat_skeleton(0)], SmtFormula, _, Result),
555		10000,
556		TimeOutResZ3),
557		( ( TimeOutResZ3 == time_out
558		; Result = no_solution_found(_)
559		)
560		-> asserta(grounding_timeout_occurred),
561		fail
562		; Result = solution(NSmtBindings),
563		debug_format_cdclt("Validating Z3 solution with ProB.", []),
564		copy_smt_solution(SmtBindings,NSmtBindings),
565		ground_wait_flags(WfStoreSmt) % also avoid Call Residue warnings
566		)
567		; NSmtBindings = SmtBindings
568		),
569		\+ severe_error_occurred,
570		finalize_smt_solution(NSmtBindings, SolverResult).
571		conflict_driven_clause_learning_online_grounding(_, _, _, SmtBindings, WfStoreSmt, SolverResult) :-
572		ground_wait_flags(WfStoreSmt),
573		\+ severe_error_occurred,
574		finalize_smt_solution(SmtBindings, SolverResult).
575
576		:- use_module(probsrc(kernel_objects),[equal_object/3]).
577		copy_smt_solution([],_).
578		copy_smt_solution([bind(ID,Val)|T],NSmtBindings) :- member(binding(ID,Z3Val,_),NSmtBindings),!,
579		equal_object(Val,Z3Val,copy_smt_solution),
580		copy_smt_solution(T,NSmtBindings).
581		copy_smt_solution([H|T],NSmtBindings) :- add_internal_error('No SMT solution for:',H),
582		copy_smt_solution(T,NSmtBindings).
583
584		finalize_smt_solution(SmtBindings, SolverResult) :-
585		SolverResult = solution(SmtBindings),
586		log_solution,
587		announce_bt_from_smt_solution.
588
589		wd_error_occurred_in_error_scope(Reason) :-
590		error_occurred_in_error_scope,
591		check_error_occured(well_definedness_error, Reason).
592
593		%% setup_reification(+SatStateMutable, +IdlGraphMut, +IdPrologVarTuples, +SmtBindings, +WfStoreSmt).
594		% Set up reification constraints to connect SAT and SMT solver.
595		% Propagates in both directions (b_convert_bool_timeout/7 implements theory propagation).
596		setup_reification(_, _, [], _, _).
597		setup_reification(SatStateMutable, IdlGraphMut, [(SatId,SatPrologVar,StackInfo)|T], SmtBindings, WfStoreSmt) :-
598		get_texpr_info(SatId, Info),
599		memberchk(smt_formula(SmtFormula), Info),
600		!,
601		SatId = b(identifier(SatVarName),_,_),
602		setup_reification_for_solver(SatStateMutable, StackInfo, IdlGraphMut, SmtFormula, SmtBindings, WfStoreSmt, SatVarName, SatPrologVar),
603		%sat_smt_reification(SatId, SatPrologVar, SmtBindings, WfStoreSmt)
604		setup_reification(SatStateMutable, IdlGraphMut, T, SmtBindings, WfStoreSmt).
605		setup_reification(SatStateMutable, IdlGraphMut, [_|T], SmtBindings, WfStoreSmt) :-
606		% plain SAT variable which is not reified with a theory solver, e.g., introduced by CNF optimization rewriting
607		setup_reification(SatStateMutable, IdlGraphMut, T, SmtBindings, WfStoreSmt).
608
609		/*:- block sat_smt_reification(?, -, ?, ?).
610		% without theory propagation
611		sat_smt_reification(SatId, SatPrologVar, SmtBindings, WfStoreSmt) :-
612		get_texpr_info(SatId, Info),
613		memberchk(smt_formula(TSmtFormula), Info),
614		( SatPrologVar == pred_true
615		-> SmtFormula = TSmtFormula
616		; SmtFormula = b(negation(TSmtFormula),pred,[])
617		),
618		b_test_boolean_expression(SmtFormula, SmtBindings, [], WfStoreSmt).*/
619
620		setup_reification_for_solver(SatStateMutable, StackInfo, IdlGraphMut, SmtFormula, SmtBindings, WfStoreSmt, SatVarName, SatPrologVar) :-
621		find_typed_identifier_uses(SmtFormula, [], UsedIds),
622		( list_contains_unfixed_deferred_set_id(UsedIds)
623		-> ContainsUnfixed = true,
624		( ground(SatPrologVar)
625		-> DetUnfixedProp = true
626		; DetUnfixedProp = false
627		)
628		; ContainsUnfixed = false,
629		DetUnfixedProp = false
630		),
631		log_theory_propagation_and_unfixed_deferred_sets(SatStateMutable, SatVarName, StackInfo, ContainsUnfixed, DetUnfixedProp, SatPrologVar),
632		sat_var_assignment_timeout(ATO),
633		( get_preference(cdclt_use_idl_theory_solver,true)
634		-> ( ast_to_difference_logic:rewrite_to_idl(SmtFormula, [DLConstraint])
635		-> debug_format_cdclt("Constraint for IDL: ", [], SmtFormula),
636		idl_solver_interface(IdlGraphMut, SatPrologVar, [DLConstraint])
637		; log_idl_candidates_from_constraint(SmtFormula)
638		-> propagate_non_idl_to_idl(IdlGraphMut, SatPrologVar, SmtFormula)
639		; true
640		),
641		sat_debug_msg(SatVarName,SmtFormula,SatPrologVar),
642		b_convert_bool_timeout(SmtFormula, SmtBindings, [], WfStoreSmt, SatPrologVar, ATO, TORes),
643		cdclt_sat_solver:log_det_theory_timeout(TORes)
644		; sat_debug_msg(SatVarName,SmtFormula,SatPrologVar),
645		b_convert_bool_timeout(SmtFormula, SmtBindings, [], WfStoreSmt, SatPrologVar, ATO, TORes),
646		cdclt_sat_solver:log_det_theory_timeout(TORes),
647		( additional_z3_reification
648		-> kernel_waitflags:get_wait_flag1(smt_call, WfStoreSmt, BeforeEnumWF),
649		gensym:gensym(smt_assertion_name, Symbol),
650		z3_coroutine(SatPrologVar, BeforeEnumWF, Symbol, SmtBindings, SmtFormula)
651		; true
652		)
653		).
654
655		:- block z3_coroutine(-, ?, ?, ?, ?).
656		z3_coroutine(SatPrologVar, BeforeEnumWF, Symbol, SmtBindings, SmtFormula) :-
657		SatPrologVar == pred_true,
658		smt_add_predicate(BeforeEnumWF, SmtFormula, SmtBindings, SmtBindings, Symbol).
659		z3_coroutine(SatPrologVar, BeforeEnumWF, Symbol, SmtBindings, SmtFormula) :-
660		SatPrologVar == pred_false,
661		safe_create_texpr(negation(SmtFormula), pred, [], NSmtFormula),
662		smt_add_predicate(BeforeEnumWF, NSmtFormula, SmtBindings, SmtBindings, Symbol).
663
664		sat_debug_msg(SatVarName, SmtFormula, SatPrologVar) :-
665		( debug_mode(off)
666		-> true
667		; format('% SAT variable ~w (~w) for ProB pred: ',[SatVarName,SatPrologVar]),
668		print_bexpr(SmtFormula), nl
669		).
670
671		:- block log_theory_propagation_and_unfixed_deferred_sets(?, ?, ?, ?, ?, -).
672		log_theory_propagation_and_unfixed_deferred_sets(SatStateMutable, SatVarName, StackInfo, ContainsUnfixed, DetUnfixedProp, SatPrologVar) :-
673		ground(SatPrologVar),
674		( ContainsUnfixed
675		-> % log unfixed deferred set propagation but undo when backtracking if not deterministic unit propagation
676		asserta(unfixed_deferred_set_has_been_propagated),
677		( DetUnfixedProp
678		-> true
679		; (true; (retract(unfixed_deferred_set_has_been_propagated), !, fail))
680		)
681		; true
682		),
683		StackInfo = (PropType,_,_,_),
684		( ( PropType == unit; PropType == branch) % has been propagated by the SAT solver
685		-> true
686		; cdclt_sat_solver:log_theory_propagation_sat_stack(SatStateMutable, SatVarName, SatPrologVar, StackInfo)
687		).
688
689		log_idl_candidates_from_constraint(Constraint) :-
690		get_ids_and_int_constants(Constraint, Ids, IntConstants),
691		Ids \== [],
692		IntConstants \== [],
693		!,
694		assert_idl_candidates(Ids, IntConstants).
695		log_idl_candidates_from_constraint(_).
696
697		assert_idl_candidates([], _).
698		assert_idl_candidates([Id|T], IntConstants) :-
699		retract(idl_candidate_constants(Id, Candidates)),
700		!,
701		subtract(IntConstants, Candidates, New),
702		append(Candidates, New, NewCandidates),
703		asserta(idl_candidate_constants(Id, NewCandidates)),
704		assert_idl_candidates(T, IntConstants).
705		assert_idl_candidates([Id|T], IntConstants) :-
706		asserta(idl_candidate_constants(Id, IntConstants)),
707		assert_idl_candidates(T, IntConstants).
708
709		get_ids_and_int_constants(b(Node,pred,_), Ids, IntConstants) :-
710		comparison_op(Node, Lhs, Rhs),
711		get_ids_and_int_constants_expr(Lhs, [], [], IdsAcc, IntConstantsAcc),
712		get_ids_and_int_constants_expr(Rhs, IdsAcc, IntConstantsAcc, Ids, IntConstants).
713
714		get_ids_and_int_constants_expr(Id, IdsAcc, IntConstantsAcc, [Name|IdsAcc], IntConstantsAcc) :-
715		Id = b(identifier(Name),integer,_).
716		get_ids_and_int_constants_expr(Int, IdsAcc, IntConstantsAcc, IdsAcc, [Value,Value1|IntConstantsAcc]) :-
717		( Int = b(integer(Value),integer,_)
718		; Int = b(unary_minus(b(integer(Value),integer,_)),integer,_)
719		),
720		% select positive and negative value
721		Value1 is Value * -1.
722		get_ids_and_int_constants_expr(b(Node,integer,_), IdsAcc, IntConstantsAcc, Ids, IntConstants) :-
723		arithmetic_expr(Node, Lhs, Rhs),
724		get_ids_and_int_constants_expr(Lhs, IdsAcc, IntConstantsAcc, NIdsAcc, NIntConstantsAcc),
725		get_ids_and_int_constants_expr(Rhs, NIdsAcc, NIntConstantsAcc, Ids, IntConstants).
726
727		comparison_op(less(Lhs,Rhs), Lhs, Rhs).
728		comparison_op(less_equal(Lhs,Rhs), Lhs, Rhs).
729		comparison_op(equal(Lhs,Rhs), Lhs, Rhs).
730		comparison_op(not_equal(Lhs,Rhs), Lhs, Rhs).
731
732		arithmetic_expr(minus(Lhs,Rhs), Lhs, Rhs).
733		arithmetic_expr(add(Lhs,Rhs), Lhs, Rhs).
734		arithmetic_expr(div(Lhs,Rhs), Lhs, Rhs).
735		arithmetic_expr(floored_div(Lhs,Rhs), Lhs, Rhs).
736		arithmetic_expr(power_of(Lhs,Rhs), Lhs, Rhs).
737		arithmetic_expr(multiplication(Lhs,Rhs), Lhs, Rhs).
738		arithmetic_expr(modulo(Lhs,Rhs), Lhs, Rhs).
739
740		:- block propagate_non_idl_to_idl(?, -, ?).
741		propagate_non_idl_to_idl(IdlGraphMut, SatPrologVar, SmtFormula) :-
742		( SatPrologVar == pred_true
743		% e.g., x:NAT -> x>=0
744		-> ( infer_constraints_for_idl_solver(SmtFormula, ConjList)
745		-> register_constraints(IdlGraphMut, ConjList)
746		; true
747		)
748		; true % TO DO: also propagate pred_false? probably not beneficial
749		).
750
751		%% idl_solver_interface(+IdlGraphMut, +SatPrologVar, +Constraint).
752		:- block idl_solver_interface(?, -, ?).
753		idl_solver_interface(IdlGraphMut, SatPrologVar, [DLConstraint]) :-
754		SatPrologVar == pred_true,
755		difference_logic_solver:remove_unsat_core,
756		cdclt_sat_solver:remove_idl_unsat_core,
757		( difference_logic_solver:register_constraint(IdlGraphMut, DLConstraint)
758		; \+ cdclt_sat_solver:is_backjumping,
759		propagate_idl_unsat_core_to_sat_solver(IdlGraphMut),
760		fail
761		).
762		idl_solver_interface(IdlGraphMut, SatPrologVar, [DLConstraint]) :-
763		SatPrologVar == pred_false,
764		difference_logic_solver:remove_unsat_core,
765		cdclt_sat_solver:remove_idl_unsat_core,
766		( difference_logic_solver:register_constraint(IdlGraphMut, b(negation(DLConstraint),pred,[]))
767		; \+ cdclt_sat_solver:is_backjumping,
768		propagate_idl_unsat_core_to_sat_solver(IdlGraphMut),
769		fail
770		).
771
772		propagate_idl_unsat_core_to_sat_solver(IdlGraphMut) :-
773		difference_logic_solver:get_solver_result(IdlGraphMut, Res),
774		Res == contradiction_found,
775		difference_logic_solver:get_unsat_core(IdlCore),
776		difference_logic_solver:remove_unsat_core,
777		cdclt_sat_solver:store_idl_unsat_core(IdlCore), !.
778
779		%% get_idl_solution_bindings(+IdlGraphMut, -Bindings).
780		get_idl_solution_bindings(IdlGraphMut, Bindings) :-
781		get_solver_result(IdlGraphMut, SolverResult),
782		SolverResult = solution(Bindings).
783
784		%% propagate_idl_solution_to_bindings_bt(+IdlGraphMut, +SmtBindings).
785		propagate_idl_solution_to_bindings_bt(IdlGraphMut, SmtBindings) :-
786		get_preference(cdclt_use_idl_theory_solver,true),
787		!,
788		% TO DO: try the current solution first
789		( get_candidate_bounds_from_non_idl_constraints(CandidateTuples),
790		difference_logic_solver:try_candidate_bounds(IdlGraphMut, CandidateTuples, Result)
791		; difference_logic_solver:get_all_solutions_on_bt(IdlGraphMut, Result)
792		),
793		Result = solution(Bindings),
794		set_bindings(Bindings, SmtBindings).
795		propagate_idl_solution_to_bindings_bt(_, _).
796
797		%% propagate_fd_bounds_to_idl_solver(+IdlGraphMut, +SmtBindings).
798		propagate_fd_bounds_to_idl_solver(IdlGraphMut, SmtBindings) :-
799		get_preference(cdclt_use_idl_theory_solver,true),
800		!,
801		difference_logic_solver:get_registered_vars(IdlGraphMut, Vars),
802		get_constraints_from_fd_bounds(SmtBindings, Vars, [], ConjList),
803		difference_logic_solver:register_constraints(IdlGraphMut, ConjList).
804		propagate_fd_bounds_to_idl_solver(_, _).
805
806		get_constraints_from_fd_bounds(_, [], Acc, Acc).
807		get_constraints_from_fd_bounds(SmtBindings, [Var|T], Acc, ConjList) :-
808		memberchk(bind(Var, int(Int)), SmtBindings),
809		integer(Int),
810		!,
811		Zero = b(identifier('_zero'),integer,[]),
812		% Var = Int but represented as Var - _zero <= Int & _zero - Var <= -Int
813		Conj1 = b(less_equal(b(minus(b(identifier(Var),integer,[]),Zero),integer,[]),b(integer(Int),integer,[])),pred,[]),
814		Conj2 = b(less_equal(b(minus(Zero,b(identifier(Var),integer,[])),integer,[]),b(unary_minus(b(integer(Int),integer,[])),integer,[])),pred,[]),
815		get_constraints_from_fd_bounds(SmtBindings, T, [Conj1,Conj2|Acc], ConjList).
816		get_constraints_from_fd_bounds(SmtBindings, [Var|T], Acc, ConjList) :-
817		memberchk(bind(Var, int(FDVar)), SmtBindings),
818		fd_var(FDVar),
819		fd_min(FDVar, Min),
820		fd_max(FDVar, Max),
821		!,
822		( var_geq_min(Var, Min, MinBound)
823		-> ( var_leq_max(Var, Max, MaxBound)
824		-> NAcc = [MinBound,MaxBound|Acc]
825		; NAcc = [MinBound|Acc]
826		)
827		; ( var_leq_max(Var, Max, MaxBound)
828		-> NAcc = [MaxBound|Acc]
829		; NAcc = Acc
830		)
831		),
832		get_constraints_from_fd_bounds(SmtBindings, T, NAcc, ConjList).
833		get_constraints_from_fd_bounds(SmtBindings, [_|T], Acc, ConjList) :-
834		get_constraints_from_fd_bounds(SmtBindings, T, Acc, ConjList).
835
836		var_geq_min(Var, Min, MinBound) :-
837		% -v <= -min
838		integer(Min),
839		Min1 is Min * -1,
840		Minus = b(minus(b(identifier('_zero'),integer,[]),b(identifier(Var),integer,[])),integer,[]),
841		MinBound = b(less_equal(Minus,b(integer(Min1),integer,[])),pred,[]).
842
843		var_leq_max(Var, Max, MaxBound) :-
844		% v <= Max
845		integer(Max),
846		MaxBound = b(less_equal(b(identifier(Var),integer,[]),b(integer(Max),integer,[])),pred,[]).
847
848		get_candidate_bounds_from_non_idl_constraints(CandidateTuples) :-
849		findall((VarName,Candidates), idl_candidate_constants(VarName, Candidates), CandidateTuples).
850
851		set_bindings([], _).
852		set_bindings([binding(VarName,Val,_)|T], SmtBindings) :-
853		member(bind(VarName,Val), SmtBindings),
854		set_bindings(T, SmtBindings).
855
856		%% exclude_idl_solution(+IdlBindings, +SmtBindings, +StateTypedIds, +WfStoreSmt).
857		exclude_idl_solution(IdlBindings, SmtBindings, StateTypedIds, WfStoreSmt) :-
858		initial_solution,
859		exclude_solution(IdlBindings, StateTypedIds, Exclusion),
860		b_test_boolean_expression(Exclusion, SmtBindings, [], WfStoreSmt).
861		exclude_idl_solution(_, _, _, _) :-
862		\+ initial_solution.
863
864		%% exclude_solution(+Bindings, +StateTypedIds, -Exclusion).
865		exclude_solution([], _, b(truth,pred,[])).
866		exclude_solution([Binding|T], StateTypedIds, Exclusion) :-
867		get_equality_from_binding(Binding, StateTypedIds, EQ),
868		exclude_solution(T, EQ, StateTypedIds, Exclusion).
869
870		exclude_solution([], Acc, _, Acc).
871		exclude_solution([Binding|T], Acc, StateTypedIds, Exclusion) :-
872		get_equality_from_binding(Binding, StateTypedIds, EQ),
873		safe_create_texpr(negation(EQ), pred, [], Neg),
874		safe_create_texpr(disjunct(Neg,Acc), pred, [], NAcc),
875		exclude_solution(T, NAcc, StateTypedIds, Exclusion).
876
877		%% get_equality_from_binding(+Binding, +TypedIds, -EQ).
878		get_equality_from_binding(Binding, TypedIds, EQ) :-
879		( Binding = bind(VarName,Val)
880		; Binding = binding(VarName,Val,_)
881		),
882		( member(b(identifier(VarName),TType,_), TypedIds)
883		-> Type = TType
884		; infer_value_type(Val, Type)
885		),
886		( contains_any(Type)
887		-> add_error_and_fail(get_equality_from_binding, 'Cannot infer type of identifier to setup state for ', VarName)
888		; EQ = b(equal(b(identifier(VarName),Type,[]),b(value(Val),Type,[])),pred,[])
889		).
890
891		%% setup_theory_wf_store(+SmtVars, -SmtBindings, -WFStoreSMT).
892		setup_theory_wf_store(SmtVars, SmtBindings, WFStoreSMT) :-
893		set_up_typed_localstate(SmtVars, _, SmtTypedVals, [], SmtBindings, positive),
894		init_wait_flags(WFStoreSMT, [wf_smt_cdcl]),
895		b_tighter_enumerate_all_values(SmtTypedVals, WFStoreSMT),!.
896
897		log_solution :-
898		\+ initial_solution,
899		!,
900		asserta(initial_solution).
901		log_solution.
902
903		ground_state_binding(Binding) :-
904		Binding = bind(_,_),
905		ground(Binding).
906
907		get_typed_ids_in_scope_of_pred(Pred, TypedIds) :-
908		find_typed_identifier_uses(Pred, PTypedIds),
909		add_typed_ids_in_scope(PTypedIds, TypedIds).
910
911		add_typed_ids_in_scope(PTypedIds, TypedIds) :-
912		b_get_machine_variables(MachineVars),
913		b_get_machine_constants(MachineConstants),
914		append([PTypedIds,MachineVars,MachineConstants], TypedIds).
915
916		get_equalities_from_bindings([], _, b(truth,pred,[])).
917		get_equalities_from_bindings([bind(Id,Val)|T], TypedIds, EqConj) :-
918		get_equality_from_binding(bind(Id,Val), TypedIds, Eq),
919		get_equalities_from_bindings(T, TypedIds, Eq, EqConj).
920
921		get_equalities_from_bindings([], _, EqConj, EqConj).
922		get_equalities_from_bindings([bind(Id,Val)|T], TypedIds, EqAcc, EqConj) :-
923		get_equality_from_binding(bind(Id,Val), TypedIds, Eq),
924		safe_create_texpr(conjunct(Eq,EqAcc), pred, [], Conj),
925		get_equalities_from_bindings(T, TypedIds, Conj, EqConj).
926
927		% only for computing the amount of sat variables of benchmarks
928		get_amount_of_sat_variables(Pred, AmountOfSatVars) :-
929		simplify_negation(Pred, SPred),
930		reset_optimizer_state,
931		assert_ground_id_values(0, SPred),
932		replace_ids_with_ground_values(SPred, 0, [], AstCardOpt),
933		precompute_values(AstCardOpt, [instantiate_quantifier_limit(0)], AstPrecomputed),
934		(clean_up_pred(AstPrecomputed, _, CleanPred) -> true
935		; add_internal_error('Clean up failed ', cdclt), CleanPred=AstPrecomputed),
936		( CleanPred = b(truth,pred,_)
937		-> AmountOfSatVars = 1
938		; CleanPred = b(falsity,pred,_)
939		-> AmountOfSatVars = 1
940		; preprocess_predicate(false, false, CleanPred, LiftedPred, _, _),
941		predicate_to_sat(normal, LiftedPred, _, _, _, SatVars1)
942		),
943		length(SatVars1, AmountOfSatVars).
944
945		/* currently not used:
946		unfold_let(Pred, Unfolded) :-
947		unfold_let([], Pred, Unfolded).
948
949		unfold_let(IdTuples, b(identifier(Name),_,_), Replacement) :-
950		member((b(identifier(Name),_,_),Ast), IdTuples),
951		!,
952		Replacement = Ast.
953		unfold_let(IdTuples, b(Node,_,_), Replacement) :-
954		( Node = let_predicate(Ids,Asts,Body)
955		; Node = let_expression(Ids,Asts,Body)
956		),
957		!,
958		maplist(unfold_let(IdTuples), Asts, NAsts),
959		zip_acc(Ids, NAsts, IdTuples, NewIdTuples), % TO DO: ideally remove IdTuples which are clashing with Ids
960		unfold_let(NewIdTuples, Body, Replacement).
961		unfold_let(IdTuples, b(Node,Type,Info), Replacement) :-
962		syntaxtransformation(Node,Subs,Names,NSubs,NewNode),!,
963		Replacement = b(NewNode,Type,Info),
964		exclude(hidden_by_local_var(Names),IdTuples,NIdTuples),
965		l_unfold_let(Subs,NIdTuples,NSubs).
966		unfold_let(I, Ast, _) :- add_internal_error('Not a typed expression:', unfold_let(I,Ast,_)),fail.
967
968		hidden_by_local_var(Names,(TID,_)) :- def_get_texpr_id(TID,ID), member(ID,Names).
969
970		l_unfold_let([],_,[]).
971		l_unfold_let([H|T],IdTuples,[NH|NT]) :-
972		unfold_let(H,IdTuples,NH),
973		l_unfold_let(T,IdTuples,NT).
974
975		zip_acc([], [], Acc, Acc).
976		zip_acc([A|T1], [B|T2], Acc, Zipped) :-
977		zip_acc(T1, T2, [(A,B)|Acc], Zipped). % TO DO: should we just store ID and not typed ID in A?
978
979		*/
980
981		%% For debugging: transform bool formula back to SMT
982		/*bool_formula_to_smt(b(truth,pred,I), b(truth,pred,I)).
983		bool_formula_to_smt(b(falsity,pred,I), b(falsity,pred,I)).
984		bool_formula_to_smt(b(equal(Id,Bool),pred,_), Smt) :-
985		Id = b(identifier(_),boolean,IdInfo),
986		member(smt_formula(TSmt), IdInfo),
987		!,
988		( Bool = b(boolean_true,boolean,_)
989		-> Smt = TSmt
990		; Smt = b(negation(TSmt),pred,[])
991		).
992		bool_formula_to_smt(b(equal(Id,Bool),pred,I), Out) :- % bool ids from Tseitin optimization
993		!,
994		Out = b(equal(Id,Bool),pred,I).
995		bool_formula_to_smt(b(conjunct(A,B),pred,I), Out) :-
996		!,
997		bool_formula_to_smt(A, SmtA),
998		bool_formula_to_smt(B, SmtB),
999		Out = b(conjunct(SmtA,SmtB),pred,I).
1000		bool_formula_to_smt(b(disjunct(A,B),pred,I), Out) :-
1001		!,
1002		bool_formula_to_smt(A, SmtA),
1003		bool_formula_to_smt(B, SmtB),
1004		Out = b(disjunct(SmtA,SmtB),pred,I).*/
1005		%%