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