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