1		% (c) 2015-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(smt_solvers_interface, [smt_solve_predicate/4,
6		smt_solve_predicate/5,
7		smt_solve_predicate_free/3,
8		smt_add_predicate/5,
9		smt_solve_predicate_in_state/5,
10		reset_smt_supported_interpreter/0,
11		smt_add_cnf/3, smt_add_extra_clause_cnf/2, smt_solve_cnf/2, smt_reset_cnf/1]).
12
13		:- use_module(library(terms), [term_size/2]).
14		:- use_module(library(sets), [list_to_set/2]).
15		:- use_module(library(lists), [same_length/2,maplist/2, maplist/3, maplist/4,
16		append/2, exclude/3, include/3, select/3,
17		nth0/3, some/2, is_list/1]).
18		:- use_module(probsrc(tools_timeout),[get_time_out_with_factor/2]).
19		:- use_module(probsrc(specfile),[get_state_for_b_formula/3]).
20		:- use_module(probsrc(debug), [debug_mode/1, debug_level_active_for/1,debug_format/3]).
21		:- use_module(probsrc(bmachine), [b_get_machine_set/1]).
22		:- use_module(probsrc(kernel_objects), [infer_value_type/2,
23		equal_object/2]).
24		:- use_module(probsrc(bsyntaxtree), [map_over_typed_bexpr/3,
25		safe_create_texpr/4,
26		find_typed_identifier_uses/2,
27		find_typed_identifier_uses/3,
28		get_texpr_type/2,
29		get_texpr_expr/2,
30		get_texpr_id/2,
31		predicate_components_in_scope/3,
32		conjunction_to_list/2,
33		conjunct_predicates/2,
34		disjunction_to_list/2,
35		syntaxtraversion/6]).
36		:- use_module(probsrc(error_manager), [add_error_fail/3, add_message/2, add_message/3, add_message/4,
37		add_error/3, add_internal_error/2, add_warning/3]).
38		:- use_module(probsrc(tools), [start_ms_timer/1,stop_ms_timer_with_debug_msg/2,split_atom/3]).
39		:- use_module(probsrc(tools_strings), [atom_prefix/2]).
40		:- use_module(probsrc(translate), [translate_bexpression/2]).
41		:- use_module(probsrc(preferences), [get_preference/2]).
42		:- use_module(probsrc(b_interpreter), [b_test_boolean_expression_cs/5]).
43		:- use_module(probsrc(tools_meta),[safe_time_out/3]).
44		:- use_module(probsrc(b_global_sets), [b_global_deferred_set/1,
45		unfixed_deferred_set/1,
46		b_get_global_enumerated_sets/1,
47		is_b_global_constant/3,
48		get_user_defined_scope/4,
49		list_contains_unfixed_deferred_set_id/1]).
50		:- use_module(probsrc(custom_explicit_sets), [expand_custom_set_to_list_now/2]).
51		:- use_module(probsrc(eventhandling),[register_event_listener/3]).
52		:- use_module(probsrc(external_functions), [is_external_function_name/1]).
53		:- use_module(cdclt_solver('cdclt_preprocessing'), [preprocess_predicate/6]).
54		:- use_module(cdclt_solver('cdclt_pred_to_sat'), [predicate_to_sat/6]).
55		:- use_module(smt_solvers_interface(model_translation), [translate_smt_model_to_b_values/4,
56		consistent_deferred_set_sizes/0,
57		store_explicit_set_unique_id/2,
58		assert_virtual_deferred_set_id/2]).
59		:- use_module(smt_solvers_interface(ast_cleanup_for_smt)).
60		:- use_module(smt_solvers_interface(prob_state_predicates), [create_state_pred/4, create_state_pred/5]).
61		:- use_module(smt_solvers_interface(solver_dispatcher)).
62		:- use_module(smt_solvers_interface(smt_common_predicates)).
63
64		:- use_module(probsrc(module_information),[module_info/2]).
65		:- module_info(group,smt_solvers).
66		:- module_info(description,'This module provides an interface to SMT-solvers like CVC4 or Z3.').
67
68		:- dynamic backjumping_symbols/1, solve_in_state/0.
69
70		clear_state :-
71		reset_interface(z3),
72		garbage_collect,
73		trimcore,
74		retractall(solve_in_state),
75		model_translation:clear_translation_state.
76
77		init_smt_supported_interpreter :-
78		retractall(backjumping_symbols(_)), %clean smt backjumping information
79		(get_preference(smt_supported_interpreter,true) -> init_interface(z3) ; true).
80		reset_smt_supported_interpreter :-
81		(get_preference(smt_supported_interpreter,true) -> clear_state
82		; true).
83
84		:- register_event_listener(start_solving,init_smt_supported_interpreter,'Init Z3 for new solving, clean backjumping'),
85		register_event_listener(end_solving,reset_smt_supported_interpreter,'Reset Z3 after solving').
86
87
88		:- block smt_add_predicate(-,?,?,?,?).
89		smt_add_predicate(_EnumWf, Pred, ProBLocalState, ProBState, Symbol) :-
90		backjump_on_symbol(Symbol),
91		smt_add_predicate_to_solver(z3, Pred, ProBLocalState, ProBState, Symbol).
92
93		smt_add_predicate_to_solver(Solver, Pred, ProBLocalState, ProBState, Symbol) :-
94		init_interface(Solver),
95		smt_clean_up_opts(axiomatic, Pred, [instantiate_quantifier_limit(20)], AxmCPred), % constructive translation isn't fully supported by the incremental solver
96		find_typed_identifier_uses(AxmCPred, [], Identifiers),
97		( contains_introduced_identifiers(Identifiers, AxmCPred)
98		-> debug_format(9, 'z3: skip: ~w~n because there were introduced identifiers', [Symbol])
99		; smt_solver_interface_call(Solver, push_frame),
100		create_state_pred(Identifiers, ProBLocalState, ProBState, StatePred),
101		conjunction_to_list(StatePred, StatePredConjuncts),
102		exclude(contains_unsupported_type_or_expression(axiomatic, Solver), StatePredConjuncts, FilteredStatePredConjuncts),
103		conjunct_predicates(FilteredStatePredConjuncts, FilteredStatePred),
104		conjunct_predicates([FilteredStatePred, AxmCPred], FullPred),
105		setup_sets(axiomatic, Solver, GlobalIdentifiers),
106		create_smt_state(axiomatic, Solver, Identifiers, IdentifierState, _),
107		append(IdentifierState, GlobalIdentifiers, GlobalState),
108		mk_expr_skip(axiomatic, Solver, FullPred, [], GlobalState, Expr),
109		translate_bexpression(FullPred, PPExpr),
110		debug_format(9, 'z3: add expr: ~w using symbol: ~w~n', [PPExpr, Symbol]),
111		!,
112		smt_add_predicate_aux(Solver, Expr, Symbol)
113		).
114		smt_add_predicate_to_solver(Solver, _, _, _, _) :- % in case the predicate contains unsupported types, etc.
115		smt_solver_interface_call(Solver, pop_frame).
116
117		contains_introduced_identifiers(FreeIDs,TExpr) :-
118		syntaxtraversion(TExpr,_,Type,Infos,Subs,_),
119		(member(introduced_by(_),Infos) % identifier that has been introduced
120		-> % check if it is not bound by some quantifiers
121		get_texpr_id(TExpr,Identifier),
122		member(b(identifier(Identifier),Type,_),FreeIDs)
123		; some(contains_introduced_identifiers(FreeIDs),Subs)).
124
125		smt_add_predicate_aux(Solver,Expr,Symbol) :-
126		get_preference(time_out,TO),
127		QuickTO is TO // 100,
128		% smt solver is called multiple times anyway
129		% and keeps its state inbetween
130		% thus we can use only a fraction of the time_out
131		% after e.g. 100 predicates, the whole timeout will be spent.
132		smt_solver_interface_call(Solver,add_interpreter_constraint(Expr,Symbol,QuickTO,SMTResult)),
133		( SMTResult = unsat(Core)
134		-> % inconsistency detected
135		debug_format(9,'z3: false with core: ~w~n',[Core]),
136		store_core_for_backjumping(Core),
137		fail
138		; true
139		).
140		smt_add_predicate_aux(Solver,_,_) :-
141		% remove frame upon backtracking
142		smt_solver_interface_call(Solver,pop_frame), fail.
143
144		store_core_for_backjumping(Core) :-
145		retractall(backjumping_symbols(_)),
146		cleanup_core_for_backjumping(Core,CleanCore),
147		assertz(backjumping_symbols(CleanCore)).
148		cleanup_core_for_backjumping([],[]).
149		cleanup_core_for_backjumping([E|Es],[CE|CEs]) :-
150		split_atom(E,['|'],[CE]),
151		cleanup_core_for_backjumping(Es,CEs).
152
153		backjump_on_symbol(Symbol) :-
154		backjumping_symbols(Symbols),
155		member(Symbol,Symbols),
156		debug_format(9,'smt check for backjump:~ncurrent symbol: ~w~nbackjumping symbols: ~w~n',[Symbol,Symbols]),
157		!, debug_format(9,'backjumping!',[]), fail.
158		backjump_on_symbol(_) :-
159		retractall(backjumping_symbols(_)).
160
161		% solve a predicate freely (without any given state or values)
162		smt_solve_predicate_free(SolverName,Pred,Store) :-
163		write(solving_with(SolverName)),nl,
164		smt_solve_predicate(SolverName, Pred, _, Result),
165		write(result(Result)),nl,
166		% TODO: provide enumeration warnings / timeouts in other cases
167		Result = solution(Bindings),
168		maplist(translate_binding,Bindings,Store).
169
170		% translate solver binding to ProB interpreter store
171		translate_binding(binding(ID,Val,_),bind(ID,Val)).
172
173		% solve in a state stored in the state space
174		smt_solve_predicate_in_state(StateID, Solver, Pred, SolutionState, Result) :-
175		get_state_for_b_formula(StateID, Pred, FullStore),
176		!,
177		asserta(solve_in_state),
178		debug_format(19, 'Solving predicate with ~w in state ~w~n', [Solver,StateID]),
179		append(FullStore, SolutionState, SMTState),
180		smt_solve_predicate(Solver, Pred, SMTState, Result).
181		smt_solve_predicate_in_state(StateID, Solver, _, _, _) :-
182		debug_format(19, 'Cannot solve predicate with ~w in state ~w~n', [Solver,StateID]),
183		fail.
184
185		%% smt_solve_predicate(+SolverName, +Pred, +State, -Result).
186		smt_solve_predicate(SolverName, Pred, State, Result) :-
187		smt_solve_predicate(SolverName, [check_sat_skeleton(250),instantiate_quantifier_limit(50)], Pred, State, Result).
188
189		%% smt_solve_predicate(+Solver, +OptionList, +Pred, +State, -Result).
190		% valid options: decompose_into_components, check_sat_skeleton(+TimeOut)
191		smt_solve_predicate(SolverName, Options, Pred, State, Result) :-
192		translate_solver_name(SolverName,Solver,SelectedTranslations),!,
193		get_preference(time_out, TO),
194		safe_time_out(smt_solve_predicate6(SelectedTranslations, Solver, Options, Pred, State, TResult), TO, TORes),
195		( TORes == time_out
196		-> Result = time_out,
197		clear_state
198		; Result = TResult
199		).
200
201		translate_solver_name(z3sat,z3,[sat,sat_cdcl]). % specialized SAT solver for QF_FD; runs two SAT solvers in parallel using local search and CDCL
202		translate_solver_name(z3axm,z3,[axm_ninc]). % axiomatic translation
203		translate_solver_name(z3cns,z3,[cns_ninc]). % constructive translation
204		translate_solver_name(z3,z3,T) :- T=[axm_ninc,cns_ninc]. % multithreading of the above
205		translate_solver_name(cvc4,cvc4,[axm_inc]).
206		translate_solver_name(S,_,_) :- add_internal_error('Unknown solver name: ', S), fail.
207
208		%% smt_solve_predicate6(+SelectedSolvers, +Solver, +Options, +Pred, +State, -Result).
209		% +Solver is either cvc4 or z3.
210		% We provide different translations and solver configurations for Z3, e.g., (non-)incremental.
211		% For z3, SelectedSolvers is a list of atoms representing the names of specific solvers
212		% defined in the Z3 C++ interface.
213		smt_solve_predicate6(SelectedSolvers, Solver, Options, Pred, State, Result) :-
214		model_translation:clear_translation_state,
215		is_list(SelectedSolvers),
216		get_texpr_type(Pred, pred),
217		!,
218		start_ms_timer(T0),
219		smt_clean_up_pre(Pred, State, Options, CPred),
220		stop_ms_timer_with_debug_msg(T0,smt_clean_up_pre(Solver,Options)),
221		( CPred = b(truth,pred,_)
222		-> Result = solution([])
223		; CPred = b(falsity,pred,_)
224		-> Result = contradiction_found
225		; catch(smt_solve_predicate_aux(SelectedSolvers, Solver, Options, CPred, State, Result),
226		SolverException, % exception most likely happened in the setup phase; in check_sat the exceptions are caught
227		treat_exception(Solver, SolverException, Result))
228		).
229		% not a predicate or cleanup failed
230		smt_solve_predicate6(SelectedSolvers, _, _, _, _, error) :-
231		add_internal_error('Unknown solver config: ', SelectedSolvers).
232
233		% remove bindings from environment which are not relevant
234		% (otherwise we get errors like z3exception in get_model_string: invalid usage)
235		remove_useless_bindings(X,_,Res) :- var(X),!,Res=X.
236		remove_useless_bindings([],_,[]).
237		remove_useless_bindings([bind(Var,Val)|T],Ids,Res) :-
238		( (get_texpr_id(TVar,Var), member(TVar,Ids))
239		-> Res = [bind(Var,Val)|RT]
240		; Res=RT
241		),
242		remove_useless_bindings(T,Ids,RT).
243
244		filter_unsupported_types_or_expressions(_, _, [], [], []).
245		filter_unsupported_types_or_expressions(TranslationType, Solver, [LP|T], FilteredLPs, UnsupportedLPs) :-
246		contains_unsupported_type_or_expression(TranslationType, Solver, LP),
247		!,
248		UnsupportedLPs = [LP|TUnsupportedLPs],
249		filter_unsupported_types_or_expressions(TranslationType, Solver, T, FilteredLPs, TUnsupportedLPs).
250		filter_unsupported_types_or_expressions(TranslationType, Solver, [LP|T], [LP|TFilteredLPs], UnsupportedLPs) :-
251		filter_unsupported_types_or_expressions(TranslationType, Solver, T, TFilteredLPs, UnsupportedLPs).
252
253		%% get_full_pred(+TranslationType, +Solver, +Pred, +ProBState, -FullPred, -FullProBState, -Filtered, -SkippedVars, -UnsupportedLPs).
254		get_full_pred(TranslationType, Solver, Pred, ProBState, FullPred, FullProBState, Filtered, SkippedVars, UnsupportedLPs) :-
255		find_typed_identifier_uses(Pred, Identifiers),
256		remove_useless_bindings(ProBState, Identifiers, FullProBState),
257		create_state_pred(Identifiers, [], FullProBState, StatePred, [skipped_variables(SkippedVars)]),
258		% print(state),nl,translate:nested_print_bexpr(StatePred),nl,
259		safe_create_texpr(conjunct(StatePred,Pred), pred, [], FullConj),
260		conjunction_to_list(FullConj, LPs),
261		filter_unsupported_types_or_expressions(TranslationType, Solver, LPs, FilteredLPs, UnsupportedLPs),
262		( same_length(LPs, FilteredLPs)
263		-> Filtered = false
264		; Filtered = true,
265		( debug_mode(off)
266		-> true
267		; include(contains_unsupported_type_or_expression(TranslationType, Solver), LPs, Unsupported),
268		conjunct_predicates(Unsupported,US),
269		add_message(Solver, 'Unsupported constraints were discarded for SMT solver: ', US, US)
270		)
271		),
272		conjunct_predicates(FilteredLPs, FullPred).
273
274		validate_selected_solvers(cvc4, SelectedSolvers) :-
275		SelectedSolvers == [axm_inc],
276		!.
277		validate_selected_solvers(cvc4, _) :-
278		add_error_fail(validate_selected_solvers, 'Only axiomatic translation with incremental solver (axm_inc) available for cvc4.', []).
279		validate_selected_solvers(z3, SelectedSolvers) :-
280		validate_selected_z3_solvers(SelectedSolvers).
281
282		validate_selected_z3_solvers(SelectedSolvers) :-
283		AvailableSolvers = [axm_inc,axm_ninc,sat,sat_cdcl,cns_ninc], % see z3interface/main.cpp:available_solvers
284		findall(Solver, (member(Solver, SelectedSolvers), \+ member(Solver, AvailableSolvers)), UnavailableSolvers),
285		UnavailableSolvers == [],
286		!.
287		validate_selected_z3_solvers(_) :-
288		add_error_fail(validate_selected_z3_solvers, 'At least one selected Z3 solver is not available.', []).
289
290		add_translation_for_solver(TranslationType, Solver, ProBState, Pred, Options, TranslationsAcc, NewAcc, IsUnfilteredTruth, Result) :-
291		start_ms_timer(T0),
292		smt_clean_up_post(TranslationType, Pred, Options, CPred),
293		( CPred = b(truth,pred,_)
294		-> Result = solution([])
295		; CPred = b(falsity,pred,_)
296		-> Result = contradiction_found
297		; get_full_pred(TranslationType, Solver, CPred, ProBState, FullPred, FullProBState, Filtered, SkippedVars, UnsupportedLPs),
298		stop_ms_timer_with_debug_msg(T0,add_translation_for_solver_preprocessing(TranslationType,Solver)),
299		start_ms_timer(T1),
300		( nonvar(FullPred), FullPred = b(truth,pred,_)
301		-> % fail if all operators are unsupported
302		( Filtered == false
303		-> IsUnfilteredTruth = true,
304		NewAcc = TranslationsAcc
305		; add_message(smt_solvers_interface, 'Could not translate predicate for solver: ', Solver:TranslationType),
306		add_message(smt_solvers_interface, 'Unsupported predicates: ', UnsupportedLPs),
307		fail
308		)
309		; IsUnfilteredTruth = false,
310		setup_sets(TranslationType, Solver, GlobalIdentifiers),
311		find_typed_identifier_uses(FullPred, Ids),
312		create_smt_state(TranslationType, Solver, Ids, IdState, _),
313		append(IdState, GlobalIdentifiers, GlobalState),
314		mk_expr(FullPred, TranslationType, Solver, [], GlobalState, PExpr),
315		%format("~w:~n", [TranslationType]), translate:nested_print_bexpr_as_classicalb(FullAxmPred),nl,
316		( debug:debug_mode(on)
317		-> translate_bexpression(FullPred, PPPred),
318		format('Sending to ~w translation to ~w: ~w~n', [TranslationType,Solver,PPPred])
319		; true
320		),
321		flush_output,
322		% comment next line in if you want to directly test ProB on the translated constraint:
323		%write(solving_with_prob(TranslationType)),nl,(solver_interface:solve_predicate(FullPred,_,3,[],CBCResult) -> write(CBCResult) ; write(fail)),nl,
324		Translation = (TranslationType,PExpr,ProBState,FullProBState,Ids,GlobalState,Filtered,SkippedVars,UnsupportedLPs),
325		NewAcc = [Translation|TranslationsAcc]
326		),
327		stop_ms_timer_with_debug_msg(T1,add_translation_for_solver_core(TranslationType,Solver))
328		).
329
330		contains_solver_name_with_prefix(Prefix, SelectedSolvers) :-
331		member(Name, SelectedSolvers),
332		atom_prefix(Prefix, Name),
333		!.
334
335		%% remove_solvers_with_prefix(+Prefix, +SelectedSolvers, -NewSelectedSolvers).
336		% Remove solvers for specific translation, e.g., if all operators are unsupported.
337		remove_solvers_with_prefix(_, [], []).
338		remove_solvers_with_prefix(Prefix, [SelectedSolver|T], NT) :-
339		atom_prefix(Prefix, SelectedSolver),
340		!,
341		remove_solvers_with_prefix(Prefix, T, NT).
342		remove_solvers_with_prefix(Prefix, [SelectedSolver|T], [SelectedSolver|NT]) :-
343		remove_solvers_with_prefix(Prefix, T, NT).
344
345		combine_satisfiable_component_results([], SatComponentResult, NResultAcc) :-
346		!,
347		NResultAcc = SatComponentResult.
348		combine_satisfiable_component_results(solution(AccBindings), solution(ComponentBindings), NResultAcc) :-
349		append(AccBindings, ComponentBindings, NAccBindings),
350		NResultAcc = solution(NAccBindings).
351
352		create_term_size_pairs([], []).
353		create_term_size_pairs([component(C,_)|T], [NTS-C|NT]) :-
354		term_size(C, TS),
355		NTS is TS * -1, % so that we can use keysort which sorts in ascending order
356		create_term_size_pairs(T, NT).
357
358		sort_components_descending_term_size(Components, SortedComponents) :-
359		% term sizes are negative so that we can use keysort to derive a descending order
360		% but we don't need the actual term sizes anyway
361		create_term_size_pairs(Components, TermSizePairs),
362		keysort(TermSizePairs, SortedComponents).
363
364		%% solve_components_with_z3(+Components, +AvailableSolvers, +Options, +State, +ResultAcc, +UnknownOccurred, -Result).
365		% Log unknown in +UnknownOccurred so that a contradiction can possibly be found in a specific component
366		% although a prior component's satisfiability couldn't be decided.
367		solve_components_with_z3([], _, _, _, _, true, no_solution_found(solver_answered_unknown)).
368		solve_components_with_z3([], _, _, _, ResultAcc, false, ResultAcc).
369		solve_components_with_z3([ComponentTerm|T], AvailableSolvers, Options, State, ResultAcc, UnknownOccurred, Result) :-
370		( ComponentTerm = component(Component,_)
371		; ComponentTerm = _TermSize-Component
372		), !,
373		smt_solve_pre_cleaned_predicate(AvailableSolvers, z3, Options, Component, State, ComponentResult),
374		constraint_uses_unfixed_deferred_set(Component, UsesDefSet),
375		( ( ComponentResult == contradiction_found,
376		( UsesDefSet == false
377		; get_preference(z3_solve_for_animation, false) % this is a genuine contradiction without considering DEFAULT_SETSIZE
378		)
379		)
380		-> Result = contradiction_found
381		; ( ComponentResult = solution(_)
382		-> combine_satisfiable_component_results(ResultAcc, ComponentResult, NResultAcc),
383		solve_components_with_z3(T, AvailableSolvers, Options, State, NResultAcc, UnknownOccurred, Result)
384		; % unknown, unfixed deferred sets or translation failed
385		solve_components_with_z3(T, AvailableSolvers, Options, State, ResultAcc, true, Result)
386		)
387		).
388
389		%% sat_skeleton_is_contradictory(+Pred, +Solver).
390		% Is true if a contradiction has been found for the predicate's SAT skeleton. Otherwise, the call fails.
391		sat_skeleton_is_contradictory(Pred, Solver) :-
392		start_ms_timer(T0),
393		preprocess_predicate(false, false, Pred, LiftedPred, _, _),
394		% abstract formula to SAT as is done by lazy SMT solvers
395		predicate_to_sat(normal, LiftedPred, _, _TopLevelWDPOs, SmtBoolFormula, SatVars),
396		findall(bind(IdName,_), member(b(identifier(IdName),_,_), SatVars), Bindings),
397		stop_ms_timer_with_debug_msg(T0, preprocess_predicate_to_sat_predicate_to_find_contradiction(Solver)),
398		start_ms_timer(T1),
399		( b_test_boolean_expression_cs(SmtBoolFormula, [], Bindings, 'SMT Boolean abstraction', Solver)
400		-> stop_ms_timer_with_debug_msg(T1, no_contradiction_found),
401		fail
402		; stop_ms_timer_with_debug_msg(T1, contradiction_found)
403		).
404
405		%% smt_solve_predicate_aux(+SelectedSolvers, +Solver, +OptionsList, +CPred, +ProBState, -Result).
406		% smt_clean_up_pre/4 has been called on +CPred.
407		smt_solve_predicate_aux(_, Solver, Options, CPred, _, Result) :-
408		member(check_sat_skeleton(TimeOut), Options),
409		TimeOut > 0,
410		% don't translate to SMT-LIB if formula has static contradiction, e.g., a:INT & a/:INT
411		safe_time_out(sat_skeleton_is_contradictory(CPred, Solver), TimeOut, TimeOutRes),
412		TimeOutRes \== time_out,
413		!,
414		Result = contradiction_found,
415		clear_state.
416		smt_solve_predicate_aux(SelectedSolvers, Solver, Options, CPred, ProBState, Result) :-
417		member(decompose_into_components, Options),!,
418		% decompose predicate into components to be solved independently
419		% important to not split among deferred sets since we need to know the cardinality if is set
420		start_ms_timer(T0),
421		findall(DeferredSetId, b_get_machine_set(DeferredSetId), DeferredSetIds),
422		predicate_components_in_scope(CPred, DeferredSetIds, Components),
423		stop_ms_timer_with_debug_msg(T0,predicate_components_in_scope(SelectedSolvers)),
424		( Components = [component(SingleComponent,_)]
425		-> smt_solve_pre_cleaned_predicate(SelectedSolvers, Solver, Options, SingleComponent, ProBState, FreshResult)
426		; ( member(sort_components,Options)
427		-> sort_components_descending_term_size(Components, SortedComponents)
428		; SortedComponents = Components
429		),
430		solve_components_with_z3(SortedComponents, SelectedSolvers, Options, ProBState, solution([]), false, FreshResult)
431		),
432		Result = FreshResult,
433		clear_state.
434		smt_solve_predicate_aux(SelectedSolvers, Solver, Options, CPred, ProBState, Result) :-
435		smt_solve_pre_cleaned_predicate(SelectedSolvers, Solver, Options, CPred, ProBState, Result).
436
437		%% smt_solve_pre_cleaned_predicate(+SelectedSolvers, +Solver, +CPred, +ProBState, -Result).
438		% smt_clean_up_pre/4 has been called on +CPred.
439		smt_solve_pre_cleaned_predicate(SelectedSolvers, Solver, Options, CPred, ProBState, Result) :-
440		validate_selected_solvers(Solver, SelectedSolvers),
441		( init_interface(Solver)
442		-> % one translation for each type, contexts are copied in the C++ interface
443		% if more than one solver uses a specific translation
444		( (contains_solver_name_with_prefix(axm, SelectedSolvers),
445		add_translation_for_solver(axiomatic, Solver, ProBState, CPred, Options, [], TranslationsAcc1, AxmIsUnfilteredTruth, AxmResult))
446		-> SelectedSolvers2 = SelectedSolvers
447		; TranslationsAcc1 = [],
448		AxmIsUnfilteredTruth = false,
449		remove_solvers_with_prefix(axm, SelectedSolvers, SelectedSolvers2)
450		),
451		( ground(AxmResult)
452		-> Result = AxmResult
453		; ( (contains_solver_name_with_prefix(cns, SelectedSolvers),
454		add_translation_for_solver(constructive, Solver, ProBState, CPred, Options, TranslationsAcc1, TranslationsAcc2, CnsIsUnfilteredTruth, CnsResult))
455		-> RestSelectedSolvers = SelectedSolvers2
456		; TranslationsAcc2 = TranslationsAcc1,
457		CnsIsUnfilteredTruth = false,
458		remove_solvers_with_prefix(cns, SelectedSolvers2, RestSelectedSolvers)
459		),
460		( ground(CnsResult)
461		-> Result = CnsResult
462		; ( (contains_solver_name_with_prefix(sat, SelectedSolvers),
463		add_translation_for_solver(sat, Solver, ProBState, CPred, Options, TranslationsAcc2, Translations, SatIsUnfilteredTruth, SatResult))
464		-> RestSelectedSolvers2 = RestSelectedSolvers
465		; Translations = TranslationsAcc2,
466		SatIsUnfilteredTruth = false,
467		remove_solvers_with_prefix(sat, RestSelectedSolvers, RestSelectedSolvers2)
468		),
469		( ground(SatResult)
470		-> Result = SatResult
471		; Translations \== [],
472		RestSelectedSolvers2 \== [],
473		constraint_uses_unfixed_deferred_set(CPred, UsesDefSet),
474		!,
475		( (AxmIsUnfilteredTruth; CnsIsUnfilteredTruth; SatIsUnfilteredTruth)
476		-> Result = solution([])
477		; catch(check_sat(RestSelectedSolvers2, Solver, UsesDefSet, Translations, Options, SolverResult, SolvedTranslation),
478		model_translation_failed, Result = no_solution_found(model_translation_failed)),
479		member((SolvedTranslation,_,_,_,_,_,Filtered,SkippedVars), Translations),
480		( (SolverResult=solution(_), nonvar(SkippedVars), is_list(SkippedVars)) % is_list grounds list
481		-> Result = no_solution_found(complex_state_values(SkippedVars)),
482		add_message(smt_solve_predicate,'Some variable values were discarded as they are not supported: ',SkippedVars)
483		; SolverResult = solution(_), Filtered == true
484		-> Result = no_solution_found(unsupported_predicates)
485		; Result = SolverResult
486		)
487		)
488		)
489		),
490		!, % not backtrackable
491		clear_state
492		)
493		; Result = no_solution_found(solver_not_available)
494		).
495		smt_solve_pre_cleaned_predicate(_,_,_,_Pred,_,no_solution_found(translation_or_setup_failed)) :-
496		clear_state.
497
498		mk_expr_skip(TranslationType, Solver, Pred, [], GlobalState, Expr) :-
499		smt_clean_up(TranslationType, Pred, AxmCPred),
500		!,
501		conjunction_to_list(AxmCPred, List),
502		exclude(contains_unsupported_type_or_expression(TranslationType, Solver), List, NList),
503		conjunct_predicates(NList, NewCPred),
504		mk_expr(NewCPred, TranslationType, Solver, [], GlobalState, Expr).
505		mk_expr_skip(_, _, Pred, _, _, _) :- !,
506		add_error_fail(smt_solvers_interface, 'mk_expr_skip failed', Pred).
507
508		%% check_sat(+SelectedSolvers, +Solver, +UsesDefSet, +Translations, -Result, -SolvedTranslation).
509		% SolvedTranslation is either axiomatic or constructive.
510		check_sat(SelectedSolvers, Solver, UsesDefSet, Translations, Options, Result, SolvedTranslation) :-
511		start_ms_timer(T1),
512		catch(check_sat_aux(SelectedSolvers, Solver, UsesDefSet, Translations, Options, Result, SolvedTranslation),
513		SolverException,
514		treat_exception(Solver, SolverException, Result)),
515		stop_ms_timer_with_debug_msg(T1,check_sat(SelectedSolvers,Solver, Options)).
516
517		treat_exception(Solver, Exc, Result) :-
518		known_solver_exception(Exc, Reason),
519		add_internal_error('Exception occurred during SMT solving: ', Reason),
520		!,
521		reset_interface(Solver),
522		Result = no_solution_found(solver_answered_unknown).
523		treat_exception(Solver, Exc, _) :-
524		format('Unknown exception in solver ~w: ~w~n', [Solver, Exc]),
525		throw(Exc).
526
527		known_solver_exception(model_translation_failed, model_translation_failed).
528		known_solver_exception(z3_exception(Reason), Reason).
529		known_solver_exception(logic_exception(Reason), Reason).
530		known_solver_exception(error(representation_error(nofit(integer)),representation_error(_,_,nofit(integer))), integer_overflow).
531
532		constraint_uses_unfixed_deferred_set(Constraint, UsesDefSet) :-
533		find_typed_identifier_uses(Constraint, [], UsedIds),
534		( list_contains_unfixed_deferred_set_id(UsedIds)
535		-> UsesDefSet = true
536		; UsesDefSet = false
537		).
538
539		check_sat_aux(_, cvc4, UsesDefSet, Translations, Options, Result, SolvedTranslation) :-
540		memberchk((axiomatic,AxmPExpr,_,_,_,_,_,_,_), Translations),
541		get_smt_time_out(Options,TO),
542		smt_solver_interface_call(cvc4, cvc4interface:smt_solve_query(AxmPExpr, TO, SMTResult)),
543		get_model_or_return_result(SMTResult, UsesDefSet, TO, axiomatic, Translations, cvc4, Result, SolvedTranslation),
544		SolvedTranslation == axiomatic.
545		check_sat_aux(SelectedSolvers, z3, UsesDefSet, Translations, Options, Result, SolvedTranslation) :-
546		( memberchk((axiomatic,AxmPExpr,_,_,_,_,_,_,_), Translations),
547		!
548		; AxmPExpr = -1 % do not solve any Z3 formula with axiomatic solver
549		),
550		( memberchk((constructive,CnsPExpr,_,_,_,_,_,_,_), Translations),
551		!
552		; CnsPExpr = -1 % do not solve any Z3 formula with constructive solver
553		),
554		( memberchk((sat,SatPExpr,_,_,_,_,_,_,_), Translations),
555		!
556		; SatPExpr = -1
557		),
558		get_smt_time_out(Options,TO),
559		% format('Calling Z3 with time-out ~w, solvers:~w (~w:~w)~n',[TO,SelectedSolvers,AxmPExpr,CnsPExpr]),
560		% Selected Solvers can be axm_inc, axm_ninc, sat or cns_ninc
561		smt_solver_interface_call(z3, z3interface:smt_solve_query(SelectedSolvers, AxmPExpr, CnsPExpr, SatPExpr, TO, SMTResultData)),
562		( debug_level_active_for(9)
563		-> write('; SMT TRANSLATION: '), nl, pretty_print_smt(z3), nl
564		; true
565		),
566		SMTResultData = result_tuple(TempSolvedTranslation,SMTResult),
567		%format('Calling get_model_or_return_result ~w~n',[SMTResult]),
568		get_model_or_return_result(SMTResult, UsesDefSet, TO, TempSolvedTranslation, Translations, z3, Result, SolvedTranslation).
569
570		get_smt_time_out(Options,TO) :-
571		member(smt_time_out_factor(TOFactor),Options),!,
572		get_time_out_with_factor(TOFactor,TO).
573		get_smt_time_out(_,TO) :- get_preference(time_out, TO).
574
575		add_state_to_bindings([], FullBindings, FullBindings).
576		add_state_to_bindings([bind(IdName,Value)|T], Bindings, FullBindings) :-
577		( member(binding(IdName,ModelValue,_), Bindings)
578		-> equal_object(Value, ModelValue),
579		NewAcc = Bindings
580		; infer_value_type(Value, Type),
581		translate_bexpression(b(value(Value),Type,[]), PrettyValue),
582		NewAcc = [binding(IdName,Value,PrettyValue)|Bindings]
583		),
584		!,
585		add_state_to_bindings(T, NewAcc, FullBindings).
586		add_state_to_bindings([bind(IdName,_)|_], _, _) :-
587		add_error_fail(add_state_to_bindings, 'The synchronisation of the model found by Z3 with the global state bindings failed.', [IdName]).
588
589		get_model_or_return_result(unsat, UsesDefSet, _, SolvedTranslation, _, _, Solution, SolvedTranslationOut) :-
590		get_preference(z3_solve_for_animation, true), % behave such as ProB by considering DEFAULT_SETSIZE
591		!,
592		SolvedTranslation = SolvedTranslationOut,
593		( (UsesDefSet == true, \+ solve_in_state)
594		-> Solution = no_solution_found(unfixed_deferred_sets)
595		; Solution = contradiction_found
596		).
597		get_model_or_return_result(unsat, _, _, SolvedTranslation, _, _, contradiction_found, SolvedTranslation).
598		get_model_or_return_result(unknown, _, _, SolvedTranslation, _, _, no_solution_found(solver_answered_unknown), SolvedTranslation).
599		get_model_or_return_result(time_out, _, _, SolvedTranslation, _, _, time_out, SolvedTranslation).
600		get_model_or_return_result(sat, _, TO, SolvedTranslation, Translations, Solver, Solution, SolvedTranslation) :-
601		memberchk((SolvedTranslation,_,ProBState,_,Ids,GlobalState,_,_,UnsupportedLPs), Translations),
602		( UnsupportedLPs \== []
603		-> add_message(get_model_or_return_result, 'A solution has been found but some predicates are not supported and were not considered: ', UnsupportedLPs),
604		Solution = no_solution_found(solver_answered_unknown)
605		; exclude(is_smt_temp_var, Ids, FilteredIDs),
606		% we replaced ProBState ids with values in ast_cleanup_for_smt so we add them to the solution here
607		( catch(
608		translate_smt_model_to_b_values_with_timeout(TO,Solver, GlobalState, FilteredIDs, Bindings),
609		E,
610		(add_error(smt_solvers_interface,'Exception in model translation: ',E),
611		throw(model_translation_failed)))
612		-> ( (
613		get_preference(z3_solve_for_animation, true),
614		% Z3 behaves as ProB by considering its deferred set size preference
615		\+ consistent_deferred_set_sizes
616		)
617		-> Solution = no_solution_found(unfixed_deferred_sets)
618		; add_state_to_bindings(ProBState, Bindings, FullBindings),
619		maplist(bind_in_prob_state(FullBindings), ProBState)
620		-> % for this solution, Z3 possibly considered a smaller deferred set size than ProB
621		% if Z3 considered a larger deferred set size, an error would have been thrown by model_translation:handle_globalsets_fdrange_contradiction/2
622		( \+ consistent_deferred_set_sizes
623		-> add_message(get_model_or_return_result, 'Deferred set size considered by Z3 is smaller than the one of ProB (DEFAULT_SETSIZE)')
624		; true
625		),
626		Solution = solution(FullBindings)
627		; throw(model_solution_extraction_failed)
628		)
629		; add_warning(smt_solvers_interface,'Failure in model translation: ',Solver),
630		throw(model_translation_failed)
631		)
632		).
633		%get_model_or_return_result(sat, _, TO, PreSolvedTranslation, Translations, Solver, Result, SolvedTranslation) :-
634		% memberchk((PreSolvedTranslation,_,_,Ids,_,_,_), Translations),
635		% next_result(Solver, PreSolvedTranslation, Translations, Ids, Result, SolvedTranslation).
636
637		translate_smt_model_to_b_values_with_timeout(TO,Solver, GlobalState, FilteredIDs, Bindings) :-
638		safe_time_out(translate_smt_model_to_b_values(Solver, GlobalState, FilteredIDs, Bindings),TO,TORes),
639		( TORes = time_out
640		-> add_warning(smt_solvers_interface,'Time-out in model translation: ',Solver),
641		throw(model_translation_failed)
642		; true
643		).
644
645		bind_in_prob_state(Bindings,bind(Id,Val)) :-
646		member(binding(Id,Z3Val,_),Bindings), %format('~w: ~w = ~w~n',[Id,Z3Val,Val]),nl,
647		% Z3 may return solution in list form, ProB had it in AVL form: hence use equal_object
648		equal_object(Z3Val,Val).
649
650		/*next_result(_,PreSolvedTranslation,_,[],Result,SolvedTranslation) :- !,
651		% no global identifiers -> no other solution
652		Result = contradiction_found,
653		SolvedTranslation = PreSolvedTranslation.
654		next_result(Solver,_,Translations,_,Result,SolvedTranslation) :-
655		memberchk((axiomatic,AxmPExpr,AxmProBState,AxmIds,AxmGlobalState,AxmFiltered,AxmSkippedVars), Translations),
656		memberchk((constructive,CnsPExpr,CnsProBState,CnsIds,CnsGlobalState,CnsFiltered,CnsSkippedVars), Translations),
657		findall(Id,member(id(_,Id),AxmGlobalState),AxmExprIds),
658		findall(Id,member(id(_,Id),CnsGlobalState),CnsExprIds),
659		smt_solver_interface_call(Solver,conjoin_negated_state(axiomatic,AxmExprIds,AxmPExpr,NewAxmPExpr)),
660		smt_solver_interface_call(Solver,conjoin_negated_state(constructive,CnsExprIds,CnsPExpr,NewCnsPExpr)),
661		NewTranslations = [
662		(axiomatic,NewAxmPExpr,AxmProBState,AxmIds,AxmGlobalState,AxmFiltered,AxmSkippedVars),
663		(constructive,NewCnsPExpr,CnsProBState,CnsIds,CnsGlobalState,CnsFiltered,CnsSkippedVars)],
664		check_sat(Solver,NewTranslations,Result,SolvedTranslation).
665		*/
666
667		% Unary and binary operators that have a direct counterpart in SMT-LIB.
668		unary_operator(negation).
669		unary_operator(unary_minus).
670		unary_operator(unary_minus_real).
671		unary_operator(convert_real).
672		binary_operator(floored_div).
673		binary_operator(equivalence).
674		binary_operator(implication).
675		binary_operator(less).
676		binary_operator(less_equal).
677		binary_operator(less_real).
678		binary_operator(less_equal_real).
679		binary_operator(greater).
680		binary_operator(greater_equal).
681		binary_operator(add).
682		binary_operator(modulo).
683		binary_operator(minus).
684		binary_operator(multiplication).
685		binary_operator(div).
686		binary_operator(power_of).
687		binary_operator(member).
688		binary_operator(subset).
689		binary_operator(union).
690		binary_operator(intersection).
691		binary_operator(set_subtraction).
692		binary_operator(add_real).
693		binary_operator(minus_real).
694		binary_operator(multiplication_real).
695		binary_operator(div_real).
696
697		% Collect couple types from a list of identifiers to reduce the list to a single couple afterwards (left-associative).
698		% We need the couple types for the constructors in SMT-Lib.
699		get_couple_types_comp_args([Arg1,Arg2|T], CoupleTypes) :-
700		Arg1 = b(identifier(_),Type1,_),
701		Arg2 = b(identifier(_),Type2,_),
702		get_couple_types_comp_args(T, couple(Type1,Type2), [couple(Type1,Type2)|D]-D, CoupleTypes).
703
704		get_couple_types_comp_args([], _, CoupleTypes-D, CoupleTypes) :-
705		D = [].
706		get_couple_types_comp_args([Arg|T], LastCoupleType, Acc-D, CoupleTypes) :-
707		Arg = b(identifier(_),Type,_),
708		D = [couple(LastCoupleType,Type)|ND],
709		get_couple_types_comp_args(T, couple(LastCoupleType,Type), Acc-ND, CoupleTypes).
710
711		mk_expr_maplist(TranslationType,Solver,LS,GS,Op,Expr) :-
712		mk_expr(Op,TranslationType,Solver,LS,GS,Expr).
713
714		mk_expr(b(Op,Type,_Infos),TranslationType,Solver,LS,GS,Expr) :-
715		mk_expr_aux(Op,Type,TranslationType,Solver,LS,GS,Expr).
716
717		% unary operators
718		mk_expr_aux(first_of_pair(Couple), _, TranslationType, Solver, LS, GS, Expr) :-
719		get_texpr_type(Couple, CoupleType),
720		mk_expr(Couple, TranslationType, Solver, LS, GS, AE),
721		smt_solver_interface_call(Solver, mk_op_couple_prj(TranslationType, first, AE, CoupleType, Expr)).
722		mk_expr_aux(second_of_pair(Couple), _, TranslationType, Solver, LS, GS, Expr) :-
723		get_texpr_type(Couple, CoupleType),
724		mk_expr(Couple, TranslationType, Solver, LS, GS, AE),
725		smt_solver_interface_call(Solver, mk_op_couple_prj(TranslationType, second, AE, CoupleType, Expr)).
726		/*
727		% change in Z3: lambda inside recursive functions was declared unsupported until proper support is provided (see https://github.com/Z3Prover/z3/issues/5813)
728		% see mk_op_iteration_func_decl in /extensions/z3interface/src/cpp/main.cpp
729		mk_expr_aux(Op, Type, TranslationType, Solver, LS, GS, Expr) :-
730		functor(Op, Functor, 1),
731		( (Functor == closure, IsReflexive = 0)
732		; (Functor == reflexive_closure, IsReflexive = 1)
733		),
734		!,
735		arg(1, Op, A),
736		Type = set(CoupleType),
737		CoupleType = couple(_,ExistsVarType),
738		mk_expr(A, TranslationType, Solver, LS, GS, AE),
739		smt_solver_interface_call(Solver, mk_op_closure(TranslationType, IsReflexive, AE, Type, CoupleType, ExistsVarType, Expr)).
740		mk_expr_aux(iteration(A1,A2), Type, TranslationType, Solver, LS, GS, Expr) :-
741		!,
742		Type = set(CoupleType),
743		CoupleType = couple(_,ExistsVarType),
744		mk_expr(A1, TranslationType, Solver, LS, GS, AE1),
745		mk_expr(A2, TranslationType, Solver, LS, GS, AE2),
746		smt_solver_interface_call(Solver, mk_op_iteration(TranslationType, AE1, AE2, Type, CoupleType, ExistsVarType, Expr)).*/
747		mk_expr_aux(interval(A1,A2), _, TranslationType, Solver, LS, GS, Expr) :-
748		!,
749		mk_expr(A1, TranslationType, Solver, LS, GS, AE1),
750		mk_expr(A2, TranslationType, Solver, LS, GS, AE2),
751		smt_solver_interface_call(Solver, mk_op_interval(TranslationType, AE1, AE2, Expr)).
752		mk_expr_aux(direct_product(Arg1,Arg2), Type, TranslationType, Solver, LS, GS, Expr) :-
753		!,
754		Type = set(CoupleOutType),
755		CoupleOutType = couple(_,Couple2Type),
756		mk_expr(Arg1, TranslationType, Solver, LS, GS, Arg1E),
757		mk_expr(Arg2, TranslationType, Solver, LS, GS, Arg2E),
758		Arg1 = b(_,set(CoupleType1),_),
759		Arg2 = b(_,set(CoupleType2),_),
760		smt_solver_interface_call(Solver, mk_op_direct_product(TranslationType, Arg1E, Arg2E, Couple2Type, CoupleType1, CoupleType2, CoupleOutType, Expr)).
761		mk_expr_aux(parallel_product(Arg1,Arg2), Type, TranslationType, Solver, LS, GS, Expr) :-
762		!,
763		Type = set(CoupleOutType),
764		mk_expr(Arg1, TranslationType, Solver, LS, GS, Arg1E),
765		mk_expr(Arg2, TranslationType, Solver, LS, GS, Arg2E),
766		Arg1 = b(_,set(CoupleType1),_),
767		Arg2 = b(_,set(CoupleType2),_),
768		CoupleOutType = couple(ExistsCoupleType1,ExistsCoupleType2),
769		smt_solver_interface_call(Solver, mk_op_parallel_product(TranslationType, Arg1E, Arg2E, CoupleType1, CoupleType2, ExistsCoupleType1, ExistsCoupleType2, CoupleOutType, Expr)).
770		mk_expr_aux(composition(Arg1,Arg2), Type, TranslationType, Solver, LS, GS, Expr) :-
771		!,
772		Type = set(CoupleOutType),
773		Arg1 = b(_,set(CoupleType1),_),
774		CoupleType1 = couple(A,B),
775		Arg2 = b(_,set(CoupleType2),_),
776		CoupleType2 = couple(B,C),
777		CoupleOutType = couple(A,C),
778		mk_expr(Arg1, TranslationType, Solver, LS, GS, Arg1E),
779		mk_expr(Arg2, TranslationType, Solver, LS, GS, Arg2E),
780		smt_solver_interface_call(Solver, mk_op_composition(TranslationType, Arg1E, Arg2E, B, CoupleType1, CoupleType2, CoupleOutType, Expr)).
781		mk_expr_aux(cartesian_product(A1,A2), Type, TranslationType, Solver, LS, GS, Expr) :-
782		!,
783		Type = set(CoupleType),
784		mk_expr(A1, TranslationType, Solver, LS, GS, AE1),
785		mk_expr(A2, TranslationType, Solver, LS, GS, AE2),
786		smt_solver_interface_call(Solver, mk_op_cartesian(TranslationType, AE1, AE2, CoupleType, Expr)).
787		mk_expr_aux(identity(A), Type, TranslationType, Solver, LS, GS, Expr) :-
788		!,
789		Type = set(CoupleType),
790		CoupleType = couple(InnerSetType,_),
791		mk_expr(A, TranslationType, Solver, LS, GS, AE),
792		smt_solver_interface_call(Solver, mk_op_identity(TranslationType, AE, InnerSetType, CoupleType, Expr)).
793		mk_expr_aux(reverse(A), Type, TranslationType, Solver, LS, GS, Expr) :-
794		!,
795		Type = set(CoupleType),
796		mk_expr(A, TranslationType, Solver, LS, GS, AE),
797		smt_solver_interface_call(Solver, mk_op_reverse(TranslationType, AE, CoupleType, Expr)).
798		% binary operators
799		mk_expr_aux(comprehension_set(Args,Body), Type, TranslationType, Solver, LS, GS, Expr) :-
800		LambdaId = b(identifier('_lambda_result_'),_,_),
801		select(LambdaId, Args, LambdaArgs),
802		create_bounded_smt_state(TranslationType, Solver, LambdaArgs, State, ArgsE),
803		ArgsE = [Arg],
804		append(State, LS, NLS),
805		conjunction_to_list(Body, ConjList),
806		select(b(equal(LambdaId,BodyExpr),pred,Info), ConjList, RestConjList),
807		member(prob_annotation('LAMBDA-EQUALITY'), Info),
808		conjunct_predicates(RestConjList, BodyPred),
809		Type = set(CoupleType),
810		!,
811		mk_expr(BodyExpr, TranslationType, Solver, NLS, GS, BodyE),
812		mk_expr(BodyPred, TranslationType, Solver, NLS, GS, BodyP),
813		smt_solver_interface_call(Solver, mk_op_lambda(TranslationType, Arg, BodyP, BodyE, CoupleType, Expr)).
814		mk_expr_aux(comprehension_set(Args,Body), _, TranslationType, Solver, LS, GS, Expr) :-
815		!,
816		create_bounded_smt_state(TranslationType, Solver, Args, State, ArgsE),
817		append(State, LS, NLS),
818		mk_expr(Body, TranslationType, Solver, NLS, GS, BodyE),
819		length(ArgsE, ArgAmount),
820		( ArgAmount == 1
821		-> ArgsE = [Arg],
822		smt_solver_interface_call(Solver, mk_op_comprehension_set_singleton(TranslationType, Arg, BodyE, Expr))
823		; get_couple_types_comp_args(Args, CoupleTypes),
824		smt_solver_interface_call(Solver, mk_op_comprehension_set_multi(TranslationType, ArgsE, CoupleTypes, BodyE, Expr))
825		).
826		mk_expr_aux(image(A,B), _, TranslationType, Solver, LS, GS, Expr) :-
827		!,
828		A = b(_,set(couple(Prj1Type,Prj2Type)),_),
829		mk_expr(A, TranslationType, Solver, LS, GS, AE),
830		mk_expr(B, TranslationType, Solver, LS, GS, BE),
831		smt_solver_interface_call(Solver, mk_op_image(TranslationType, AE,BE,couple(Prj1Type,Prj2Type),Prj1Type,Prj2Type,Expr)).
832		% conjunct and disjunct are deconstructed to lists
833		mk_expr_aux(conjunct(A,B),pred,TranslationType, Solver,LS,GS,Expr) :-
834		!,
835		conjunction_to_list(b(conjunct(A,B),pred,[]),List),
836		maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),List,ExprList), % apply mk_expr on List
837		% truth/0 are removed from the conjunction during list / from list
838		% the list might be empty now!
839		( ExprList = []
840		-> smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr))
841		; ( ExprList = [X]
842		-> Expr = X
843		; smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, conjunct,ExprList,Expr))
844		)
845		).
846		mk_expr_aux(disjunct(A,B),pred,TranslationType, Solver,LS,GS,Expr) :-
847		!,
848		disjunction_to_list(b(disjunct(A,B),pred,[]),List),
849		maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),List,ExprList),
850		smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, disjunct,ExprList,Expr)).
851		% special case for if then else
852		mk_expr_aux(if_then_else(Pred,A,B),_,TranslationType, Solver,LS,GS,Expr) :-
853		!,
854		maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),[Pred,A,B],ArgList),
855		smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, if_then_else,ArgList,Expr)).
856		% special case for partition
857		mk_expr_aux(partition(S,Sets),pred,TranslationType, Solver,LS,GS,Expr) :-
858		!,
859		% definition: sets are disjoint and S is the union
860		maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),Sets,SetExprs),
861		pairwise_union(TranslationType,SetExprs,Solver,UnionOfSets),
862		mk_expr(S,TranslationType, Solver,LS,GS,SExpr),
863		smt_solver_interface_call(Solver,mk_op(TranslationType, equal,SExpr,UnionOfSets,EqualToUnion)), % S = Union(Sets)
864		% enforce sets pairwise disjoint (= intersection is empty)
865		get_texpr_type(S,Type),
866		smt_solver_interface_call(Solver,mk_empty_set(TranslationType, Type,EmptySet)),
867		pairwise_disjoint(TranslationType,SetExprs,Solver,EmptySet,PWConstraint),
868		smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, conjunct,[EqualToUnion,PWConstraint],Expr)).
869		% quantifiers
870		mk_expr_aux(forall(IDs,b(truth,pred,_),B),pred,TranslationType, Solver,LS,GS,Expr) :-
871		!,
872		create_bounded_smt_state(TranslationType, Solver,IDs,State,SMTExprs),
873		append(State,LS,NLS),
874		mk_expr(B,TranslationType, Solver,NLS,GS,BE),
875		smt_solver_interface_call(Solver,mk_quantifier(TranslationType, forall,SMTExprs,BE,Expr)).
876		mk_expr_aux(forall(IDs,A,B),pred,TranslationType, Solver,LS,GS,Expr) :-
877		!,
878		create_bounded_smt_state(TranslationType, Solver,IDs,State,SMTExprs),
879		append(State,LS,NLS),
880		mk_expr(A,TranslationType, Solver,NLS,GS,AE), mk_expr(B,TranslationType, Solver,NLS,GS,BE),
881		smt_solver_interface_call(Solver,mk_op(TranslationType, implication,AE,BE,InnerExpr)),
882		smt_solver_interface_call(Solver,mk_quantifier(TranslationType, forall,SMTExprs,InnerExpr,Expr)).
883		mk_expr_aux(exists(IDs,B),pred,TranslationType, Solver,LS,GS,Expr) :-
884		!,
885		create_bounded_smt_state(TranslationType, Solver,IDs,State,SMTExprs),
886		append(State,LS,NLS),
887		mk_expr(B,TranslationType, Solver,NLS,GS,InnerExpr),
888		smt_solver_interface_call(Solver,mk_quantifier(TranslationType, exists,SMTExprs,InnerExpr,Expr)).
889		% equality is a special case as it needs to distinguish between booleans and other types
890		mk_expr_aux(equal(A,B),pred,TranslationType, Solver,LS,GS,Expr) :-
891		!,
892		mk_expr(A,TranslationType, Solver,LS,GS,AE),
893		mk_expr(B,TranslationType, Solver,LS,GS,BE),
894		get_texpr_type(A,Type),
895		( Type = boolean
896		-> smt_solver_interface_call(Solver, mk_op(TranslationType, equivalence, AE, BE, Expr))
897		; smt_solver_interface_call(Solver, mk_op(TranslationType, equal, AE, BE, Expr))
898		).
899		mk_expr_aux(convert_int_floor(Real),integer,TranslationType, Solver,LS,GS,Expr) :-
900		mk_expr(Real, TranslationType, Solver, LS, GS, RealExpr),
901		!,
902		number_codes(RealExpr, ECodes),
903		append([102,108,111,111,114], ECodes, EECodes),
904		atom_codes(EAtom, EECodes),
905		( is_ground_real(Real)
906		-> IsGroundArg = 1
907		; IsGroundArg = 0
908		),
909		smt_solver_interface_call(Solver,mk_op_floor(TranslationType,IsGroundArg,EAtom,RealExpr,Expr)).
910		mk_expr_aux(convert_int_ceiling(Real),integer,TranslationType, Solver,LS,GS,Expr) :-
911		mk_expr(Real, TranslationType, Solver, LS, GS, RealExpr),
912		!,
913		number_codes(RealExpr, ECodes),
914		append([99,101,105,108,105,110,103], ECodes, EECodes),
915		atom_codes(EAtom, EECodes),
916		( is_ground_real(Real)
917		-> IsGroundArg = 1
918		; IsGroundArg = 0
919		),
920		smt_solver_interface_call(Solver,mk_op_ceiling(TranslationType,IsGroundArg,EAtom,RealExpr,Expr)).
921		% records
922		mk_expr_aux(rec(ListOfFields),Type,TranslationType, Solver,LS,GS,Expr) :-
923		!,
924		findall(FieldExpr, member(field(_,FieldExpr),ListOfFields), FieldExprs),
925		maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),FieldExprs,SMTFieldExprs),
926		smt_solver_interface_call(Solver,mk_record_const(TranslationType, Type,SMTFieldExprs,Expr)).
927		mk_expr_aux(record_field(Record,FieldName),Type,TranslationType, Solver,LS,GS,Expr) :-
928		!,
929		get_texpr_type(Record,record(RFields)),
930		nth0(FieldNr,RFields,field(FieldName,Type)),
931		% debug_format(9,'Field: ~w Type: ~w~n-> FieldNr: ~w~n',[FieldName,RFields,FieldNr]),
932		mk_expr(Record,TranslationType, Solver,LS,GS,SMTRecordExpr),
933		smt_solver_interface_call(Solver,mk_record_field(TranslationType, SMTRecordExpr,FieldNr,Expr)).
934		% couple construction
935		mk_expr_aux(couple(A,B),Type,TranslationType, Solver,LS,GS,Expr) :-
936		!,
937		mk_expr(A,TranslationType, Solver,LS,GS,AE),
938		mk_expr(B,TranslationType, Solver,LS,GS,BE),
939		smt_solver_interface_call(Solver,mk_couple(TranslationType, Type,AE,BE,Expr)).
940		% constants and identifiers
941		mk_expr_aux(identifier(Id),_,_,_Solver,LS,GS,Expr) :-
942		!,
943		lookup(Id,LS,GS,Expr).
944		mk_expr_aux(real(RealAtom),real,TranslationType, Solver,_LS,_GS,Expr) :-
945		!,
946		smt_solver_interface_call(Solver,mk_real_const(TranslationType, RealAtom,Expr)).
947		mk_expr_aux(integer(Int),integer,TranslationType, Solver,_LS,_GS,Expr) :-
948		!,
949		smt_solver_interface_call(Solver,mk_int_const(TranslationType, Int,Expr)).
950		mk_expr_aux(min_int,integer,TranslationType, Solver,_LS,_GS,Expr) :-
951		!,
952		get_preference(minint,MinInt),
953		smt_solver_interface_call(Solver,mk_int_const(TranslationType, MinInt,Expr)).
954		mk_expr_aux(max_int,integer,TranslationType, Solver,_LS,_GS,Expr) :-
955		!,
956		get_preference(maxint,MaxInt),
957		smt_solver_interface_call(Solver,mk_int_const(TranslationType, MaxInt,Expr)).
958		mk_expr_aux(boolean_true,boolean,_,Solver,_LS,_GS,Expr) :-
959		!,
960		smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr)).
961		mk_expr_aux(boolean_false,boolean,_,Solver,_LS,_GS,Expr) :-
962		!,
963		smt_solver_interface_call(Solver,mk_bool_const(boolean_false,Expr)).
964		mk_expr_aux(string(S),string,TranslationType,Solver,_LS,_GS,Expr) :-
965		!,
966		smt_solver_interface_call(Solver,mk_string_const(TranslationType, S,Expr)).
967		mk_expr_aux(truth,pred,_,Solver,_LS,_GS,Expr) :-
968		!,
969		smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr)).
970		mk_expr_aux(falsity,pred,_,Solver,_LS,_GS,Expr) :-
971		!,
972		smt_solver_interface_call(Solver,mk_bool_const(boolean_false,Expr)).
973		mk_expr_aux(bool_set,set(boolean),TranslationType, Solver,_LS,_GS,Expr) :-
974		!,
975		smt_solver_interface_call(Solver,mk_bool_const(boolean_true,True)),
976		smt_solver_interface_call(Solver,mk_bool_const(boolean_false,False)),
977		smt_solver_interface_call(Solver,mk_set(TranslationType, [True,False],Expr)).
978		mk_expr_aux(set_extension(List),set(T),TranslationType, Solver,LS,GS,Expr) :-
979		!,
980		maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),List,SubExprs),
981		( SubExprs = []
982		-> smt_solver_interface_call(Solver,mk_empty_set(TranslationType, set(T),Expr))
983		; smt_solver_interface_call(Solver,mk_set(TranslationType, SubExprs,Expr))
984		).
985		mk_expr_aux(empty_set,Type,TranslationType, Solver,_LS,_GS,Expr) :-
986		!,
987		smt_solver_interface_call(Solver,mk_empty_set(TranslationType, Type,Expr)).
988		% given values
989		mk_expr_aux(value(V),Type,TranslationType, Solver,LS,GS,Expr) :-
990		!,
991		mk_value(Type,V,TranslationType, Solver,LS,GS,Expr).
992		% ast nodes that can be ignored
993		mk_expr_aux(convert_bool(P),boolean,TranslationType, Solver,LS,GS,Expr) :-
994		!,
995		mk_expr(P,TranslationType, Solver,LS,GS,Expr).
996		% lets
997		mk_expr_aux(let_expression(ListOfIDs,ListOfDefinitions,LetExpression),_Type,TranslationType, Solver,LS,GS,Expr) :-
998		create_let_state(ListOfIDs,ListOfDefinitions,TranslationType, Solver,LS,GS,NewLS),
999		!,
1000		mk_expr(LetExpression,TranslationType, Solver,NewLS,GS,Expr).
1001		mk_expr_aux(let_predicate(ListOfIDs,ListOfDefinitions,LetExpression),pred,TranslationType, Solver,LS,GS,Expr) :-
1002		create_let_state(ListOfIDs,ListOfDefinitions,TranslationType, Solver,LS,GS,NewLS),
1003		!,
1004		mk_expr(LetExpression,TranslationType, Solver,NewLS,GS,Expr).
1005		% -- cases with functor:
1006		mk_expr_aux(Op, Type, TranslationType, Solver, LS, GS, Expr) :-
1007		functor(Op, Functor, 1),
1008		(Functor == pow_subset; Functor == pow1_subset; Functor == fin_subset; Functor == fin1_subset),
1009		!,
1010		arg(1, Op, A),
1011		Type = set(set(InnerSetType)),
1012		mk_expr(A, TranslationType, Solver, LS, GS, AE),
1013		( Functor == pow_subset
1014		-> smt_solver_interface_call(Solver, mk_op_pow_subset(TranslationType, AE, set(InnerSetType), Expr))
1015		; Functor == pow1_subset
1016		-> smt_solver_interface_call(Solver, mk_op_pow1_subset(TranslationType, AE, set(InnerSetType), InnerSetType, Expr))
1017		; Functor == fin_subset
1018		-> smt_solver_interface_call(Solver, mk_op_fin_subset(TranslationType, AE, set(InnerSetType), Expr))
1019		; smt_solver_interface_call(Solver, mk_op_fin1_subset(TranslationType, AE, set(InnerSetType), InnerSetType, Expr))
1020		).
1021		mk_expr_aux(Op, _, TranslationType, Solver, LS, GS, Expr) :-
1022		functor(Op, Functor, 1),
1023		(Functor == domain; Functor == range),
1024		!,
1025		arg(1, Op, A),
1026		mk_expr(A, TranslationType, Solver, LS, GS, AE),
1027		A = b(_,set(CoupleType),_),
1028		CoupleType = couple(Prj1Type,Prj2Type),
1029		( Functor == domain
1030		-> smt_solver_interface_call(Solver, mk_op_domain(TranslationType, AE, CoupleType, Prj1Type, Prj2Type, Expr))
1031		; smt_solver_interface_call(Solver, mk_op_range(TranslationType, AE, CoupleType, Prj1Type, Prj2Type, Expr))
1032		).
1033		mk_expr_aux(Op, Type, TranslationType, Solver, LS, GS, Expr) :-
1034		functor(Op, Functor, 2),
1035		(Functor == domain_restriction; Functor == domain_subtraction; Functor == range_restriction; Functor == range_subtraction),
1036		!,
1037		Type = set(CoupleType),
1038		arg(1, Op, A1),
1039		arg(2, Op, A2),
1040		mk_expr(A1, TranslationType, Solver, LS, GS, AE1),
1041		mk_expr(A2, TranslationType, Solver, LS, GS, AE2),
1042		( Functor == domain_restriction
1043		-> smt_solver_interface_call(Solver, mk_op_dom_res(TranslationType, AE1, AE2, CoupleType, Expr))
1044		; Functor == domain_subtraction
1045		-> smt_solver_interface_call(Solver, mk_op_dom_sub(TranslationType, AE1, AE2, CoupleType, Expr))
1046		; Functor == range_restriction
1047		-> smt_solver_interface_call(Solver, mk_op_ran_res(TranslationType, AE1, AE2, CoupleType, Expr))
1048		; smt_solver_interface_call(Solver, mk_op_ran_sub(TranslationType, AE1, AE2, CoupleType, Expr))
1049		).
1050		mk_expr_aux(Op,_,TranslationType, Solver,LS,GS,Expr) :-
1051		functor(Op,Functor,1),
1052		unary_operator(Functor),
1053		!,
1054		arg(1,Op,A),
1055		mk_expr(A,TranslationType, Solver,LS,GS,AE),
1056		smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, Functor, [AE], Expr)).
1057		mk_expr_aux(Op, _, TranslationType, Solver, LS, GS, Expr) :-
1058		functor(Op, Functor, 1),
1059		( Functor == general_union; Functor == general_intersection),
1060		!,
1061		arg(1, Op, A),
1062		A = b(_,set(set(InnerType)),_),
1063		mk_expr(A, TranslationType, Solver, LS, GS, AE),
1064		( Functor == general_union
1065		-> smt_solver_interface_call(Solver, mk_op_general_union(TranslationType, AE, set(InnerType), InnerType, Expr))
1066		; store_explicit_set_unique_id(A, UniqueIdName),
1067		smt_solver_interface_call(Solver, mk_op_general_intersection(TranslationType, UniqueIdName, AE, set(InnerType), InnerType, Expr))
1068		).
1069		mk_expr_aux(Op,_,TranslationType, Solver,LS,GS,Expr) :-
1070		functor(Op,Functor,2),
1071		binary_operator(Functor),
1072		!,
1073		arg(1,Op,A),
1074		mk_expr(A,TranslationType, Solver,LS,GS,AE),
1075		arg(2,Op,B),
1076		mk_expr(B,TranslationType, Solver,LS,GS,BE),
1077		smt_solver_interface_call(Solver,mk_op(TranslationType, Functor,AE,BE,Expr)).
1078		% error case
1079		mk_expr_aux(Expr,_,_,_,_,_,_) :- !,
1080		add_error_fail(smt_solvers_interface,'mk_expr failed',Expr).
1081
1082		create_let_state([],[],_,_,S,_,S).
1083		create_let_state([ID|IDs],[Def|Defs],TranslationType, Solver,StateSoFar,GS,State) :-
1084		get_texpr_id(ID,UnwrappedId),
1085		mk_expr(Def,TranslationType, Solver,StateSoFar,GS,Expr),
1086		create_let_state(IDs,Defs,TranslationType, Solver,[id(UnwrappedId,Expr)|StateSoFar],GS,State).
1087
1088		mk_value_maplist(Type,TranslationType, Solver,LS,GS,Val,Expr) :-
1089		mk_value(Type,Val,TranslationType, Solver,LS,GS,Expr).
1090
1091		mk_value(Type,Val,TranslationType, Solver,LS,GS,Expr) :-
1092		(mk_value_aux(Type,Val,TranslationType, Solver,LS,GS,Expr) -> true). % avoid spurious error messages upon backtrack
1093
1094		mk_value_aux(real,RealTerm,TranslationType, Solver,_LS,_GS,Expr) :-
1095		( RealTerm = term(floating(Real))
1096		; RealTerm = real(Real)
1097		),
1098		float(Real),
1099		!,
1100		number_codes(Real, RealCodes),
1101		atom_codes(RealAtom, RealCodes),
1102		smt_solver_interface_call(Solver,mk_real_const(TranslationType,RealAtom,Expr)).
1103		mk_value_aux(real,real(RealAtom),TranslationType, Solver,_LS,_GS,Expr) :-
1104		!,
1105		smt_solver_interface_call(Solver,mk_real_const(TranslationType,RealAtom,Expr)).
1106		mk_value_aux(string,string(Atom),TranslationType, Solver,_LS,_GS,Expr) :-
1107		!,
1108		smt_solver_interface_call(Solver,mk_string_const(TranslationType,Atom,Expr)).
1109		mk_value_aux(integer,int(Int),TranslationType, Solver,_LS,_GS,Expr) :-
1110		!,
1111		smt_solver_interface_call(Solver,mk_int_const(TranslationType,Int,Expr)).
1112		mk_value_aux(boolean,pred_false,_,Solver,_LS,_GS,Expr) :-
1113		!,
1114		smt_solver_interface_call(Solver,mk_bool_const(boolean_false,Expr)).
1115		mk_value_aux(boolean,pred_true,_,Solver,_LS,_GS,Expr) :-
1116		!,
1117		smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr)).
1118		% only supported thanks to z3 full sets
1119		mk_value_aux(set(integer),global_set('INTEGER'),TranslationType, z3,_LS,_GS,Expr) :-
1120		!,
1121		smt_solver_interface_call(z3,mk_full_set(TranslationType,set(integer),Expr)).
1122		mk_value_aux(set(string),global_set('STRING'),TranslationType, z3,_LS,_GS,Expr) :-
1123		!,
1124		smt_solver_interface_call(z3,mk_full_set(TranslationType,set(string),Expr)).
1125		mk_value_aux(set(global(X)),global_set(X),_,_Solver,LS,GS,Expr) :-
1126		lookup(X,LS,GS,Expr).
1127		mk_value_aux(set(X),avl_set(Val),TranslationType, Solver,LS,GS,Expr) :-
1128		expand_custom_set_to_list_now(avl_set(Val),Values),
1129		!,
1130		mk_value(set(X),Values,TranslationType, Solver,LS,GS,Expr).
1131		mk_value_aux(set(X),List,TranslationType, Solver,LS,GS,Expr) :-
1132		maplist(mk_value_maplist(X,TranslationType, Solver,LS,GS),List,SubExprs),
1133		!,
1134		( SubExprs = []
1135		-> smt_solver_interface_call(Solver,mk_empty_set(TranslationType,set(X),Expr))
1136		; smt_solver_interface_call(Solver,mk_set(TranslationType,SubExprs,Expr))
1137		).
1138		mk_value_aux(couple(AT,BT),(A,B), TranslationType, Solver,LS,GS,Expr) :-
1139		mk_value(AT,A,TranslationType, Solver,LS,GS,AE),!,
1140		mk_value(BT,B,TranslationType, Solver,LS,GS,BE),
1141		!,
1142		smt_solver_interface_call(Solver,mk_couple(TranslationType, couple(AT,BT),AE,BE,Expr)).
1143		mk_value_aux(record(FieldTypes), rec(Fields), TranslationType, Solver, LS, GS, Expr) :-
1144		create_exprs_for_rec_value_fields(FieldTypes, Fields, TranslationType, Solver, LS, GS, SMTFieldExprs),
1145		!,
1146		smt_solver_interface_call(Solver, mk_record_const(TranslationType,record(FieldTypes),SMTFieldExprs,Expr)).
1147		mk_value_aux(global(Name),fd(Num,Name),_,_Solver,LS,GS,Expr) :-
1148		is_b_global_constant(Name,Num,Constant),
1149		!,
1150		lookup(Constant,LS,GS,Expr).
1151		% error case
1152		mk_value_aux(Type,Value,_,_,_,_,_) :- !,
1153		add_error_fail(smt_solvers_interface,'mk_value failed',[Type,Value]).
1154
1155		is_ground_real(b(unary_minus_real(Real),real,_)) :-
1156		is_ground_real(Real).
1157		is_ground_real(b(real(_),real,_)).
1158		is_ground_real(b(value(_),real,_)).
1159
1160		%% create_exprs_for_rec_value_fields(+FieldTypes, +Fields, +TranslationType, +Solver, +LS, +GS, -FieldExprs).
1161		create_exprs_for_rec_value_fields([], [], _, _, _, _, []).
1162		create_exprs_for_rec_value_fields([field(Name,Type)|TT], [field(Name,Value)|FT], TranslationType, Solver, LS, GS, [Expr|NT]) :-
1163		mk_value(Type, Value, TranslationType, Solver, LS, GS, Expr),
1164		create_exprs_for_rec_value_fields(TT, FT, TranslationType, Solver, LS, GS, NT).
1165
1166		pairwise_union(_, [S],_Solver,Out) :-
1167		!,
1168		Out = S.
1169		pairwise_union(TranslationType, [S|Sets],Solver,Expr) :-
1170		pairwise_union(TranslationType, Sets,Solver,SS),
1171		smt_solver_interface_call(Solver,mk_op(TranslationType,union,S,SS,Expr)).
1172
1173		pairwise_disjoint(TranslationType, [H,T],Solver,EmptySet,Constraint) :- !,
1174		pairwise_disjoint_mk_expr(TranslationType, Solver,H,T,EmptySet,Constraint).
1175		pairwise_disjoint(TranslationType, [H|T],Solver,EmptySet,Constraint) :-
1176		pairwise_disjoint(TranslationType, H,T,Solver,EmptySet,SubConstraints),
1177		pairwise_disjoint(TranslationType, T,Solver,EmptySet,SubConstraint),
1178		smt_solver_interface_call(Solver,mk_op_arglist(TranslationType,conjunct,[SubConstraint|SubConstraints],Constraint)).
1179
1180		pairwise_disjoint(TranslationType, E,[Last],Solver,EmptySet,[C]) :- !,
1181		pairwise_disjoint_mk_expr(TranslationType, Solver,E,Last,EmptySet,C).
1182		pairwise_disjoint(TranslationType, E,[H|T],Solver,EmptySet,[C|Cs]) :-
1183		pairwise_disjoint_mk_expr(TranslationType, Solver,E,H,EmptySet,C),
1184		pairwise_disjoint(TranslationType, E,T,Solver,EmptySet,Cs).
1185
1186		pairwise_disjoint_mk_expr(TranslationType, Solver,A,B,EmptySet,PWConstraint) :-
1187		smt_solver_interface_call(Solver,mk_op(TranslationType,intersection,A,B,Inter)),
1188		smt_solver_interface_call(Solver,mk_op(TranslationType,equal,Inter,EmptySet,PWConstraint)).
1189
1190		mk_sort(TranslationType,Solver,Set) :-
1191		smt_solver_interface_call(Solver,mk_sort(TranslationType,Set)).
1192
1193		setup_deferred_sets(_, _, [], DefSetIdentifiers) :-
1194		!,
1195		DefSetIdentifiers = [].
1196		setup_deferred_sets(TranslationType, Solver, DeferredSets, DefSetIdentifiers) :-
1197		% deferred sets and which are either not unfixed or ProB's default set size preference is not considered -> only create a sort
1198		maplist(mk_sort(TranslationType, Solver), DeferredSets),
1199		mk_deferred_set_identifiers(TranslationType, Solver, DeferredSets, DefSetIdentifiers).
1200
1201		%% create_virtual_enum_elms(+DefaultSetSize, +DefSet, -DefElms).
1202		% For a deferred set D and preference DEFAULT_SETSIZE of 3 we create 'D1', 'D2', and 'D3'.
1203		create_virtual_enum_elms(DefaultSetSize, DefSet, DefElms) :-
1204		create_virtual_enum_elms(1, DefaultSetSize, DefSet, DefElms).
1205
1206		create_virtual_enum_elms(Counter, DefaultSetSize, _, Out) :-
1207		Counter > DefaultSetSize,
1208		!,
1209		Out = [].
1210		create_virtual_enum_elms(Counter, DefaultSetSize, DefSet, [EnumElm|NT]) :-
1211		number_codes(Counter, NC),
1212		atom_codes(AC, NC),
1213		atom_concat(DefSet, AC, EnumElm),
1214		Counter1 is Counter + 1,
1215		assert_virtual_deferred_set_id(EnumElm, fd(Counter,DefSet)),
1216		create_virtual_enum_elms(Counter1, DefaultSetSize, DefSet, NT).
1217
1218		prepare_unfixed_deferred_sets_with_virtual_elms(_, [], []).
1219		prepare_unfixed_deferred_sets_with_virtual_elms(DefaultSetSize, [DefSet|T], [(DefSet,DefElms)|NT]) :-
1220		( get_user_defined_scope(DefSet,Low,Up,_Span)
1221		-> % a specific deferred set's size might be user defined in the definitions
1222		DeferredSetSize is 1+Up-Low
1223		; DeferredSetSize = DefaultSetSize
1224		),
1225		create_virtual_enum_elms(DeferredSetSize, DefSet, DefElms),
1226		prepare_unfixed_deferred_sets_with_virtual_elms(DefaultSetSize, T, NT).
1227
1228		prepare_enumerated_sets_with_elms([], []).
1229		prepare_enumerated_sets_with_elms([EnumSet|T], [(EnumSet,EnumElms)|NT]) :-
1230		% find all global constants belonging to the given set
1231		findall(Cst, is_b_global_constant(EnumSet, _, Cst), EnumElms),
1232		prepare_enumerated_sets_with_elms(T, NT).
1233
1234		setup_sets(TranslationType, Solver, GlobalIdentifiers) :-
1235		( get_preference(z3_solve_for_animation, true)
1236		-> % Z3 behaves as ProB by considering DEFAULT_SETSIZE preference
1237		findall(DS, (b_global_deferred_set(DS), unfixed_deferred_set(DS)), UnfixedDefSets),
1238		get_preference(globalsets_fdrange, DefaultSetSize),
1239		prepare_unfixed_deferred_sets_with_virtual_elms(DefaultSetSize, UnfixedDefSets, EnumDefSetPairs),
1240		findall(DS, (b_global_deferred_set(DS), \+ unfixed_deferred_set(DS)), DeferredSets),
1241		setup_deferred_sets(TranslationType, Solver, DeferredSets, DefSetIdentifiers)
1242		; % Z3 behaves differently compared to ProB if deferred sets are used
1243		findall(X, b_global_deferred_set(X), DeferredSets),
1244		setup_deferred_sets(TranslationType, Solver, DeferredSets, DefSetIdentifiers),
1245		EnumDefSetPairs = []
1246		),
1247		% enumerated sets -> create a dedicated datatype in SMT-LIB
1248		b_get_global_enumerated_sets(EnumeratedSets),
1249		% can not use setof / bagof for some reason
1250		list_to_set(EnumeratedSets, EnumeratedSetsNoDuplicates),
1251		prepare_enumerated_sets_with_elms(EnumeratedSetsNoDuplicates, EnumSetPairs),
1252		append(EnumSetPairs, EnumDefSetPairs, GlobalSetPairs),
1253		maplist(setup_enumerated_set(TranslationType, Solver), GlobalSetPairs, IdentifierLists),
1254		append([DefSetIdentifiers|IdentifierLists], GlobalIdentifiers).
1255
1256		% currently only functional for z3
1257		mk_deferred_set_identifiers(_, cvc4, _, []).
1258		mk_deferred_set_identifiers(TranslationType, z3, DeferredSets, DefSetIdentifiers) :-
1259		maplist(mk_deferred_set_identifiers2(TranslationType), DeferredSets, DefSetIdentifiers).
1260
1261		mk_deferred_set_identifiers2(TranslationType, SetName, id(SetName, SetExpression)) :-
1262		smt_solver_interface_call(z3, mk_full_set(TranslationType, set(global(SetName)), SetExpression)).
1263
1264		setup_enumerated_set(TranslationType, Solver, (SetName,SetElements), [SetIdentifier|Identifiers]) :-
1265		%b_global_set_cardinality(SetName, Cardinality), % don't use b_global_set_cardinality/2 here since it can be different than the actual cardinality due to the preference globalsets_fdrange
1266		length(SetElements, Cardinality),
1267		% make a new sort and create identifiers
1268		smt_solver_interface_call(Solver, mk_sort_with_cardinality(TranslationType, SetName, Cardinality, SetElements, EnumExprs)),
1269		SetIdentifier = id(SetName, SetExpression),
1270		create_enum_element_smt_state(SetElements, EnumExprs, Identifiers),
1271		smt_solver_interface_call(Solver, mk_set(TranslationType, EnumExprs, SetExpression)).
1272
1273		create_enum_element_smt_state([], [], []).
1274		create_enum_element_smt_state([IdName|TIds], [EnumExpr|TExprs], [id(IdName,EnumExpr)|T]) :-
1275		create_enum_element_smt_state(TIds, TExprs, T).
1276
1277		create_smt_state(TranslationType, Solver,Identifiers,State,Exprs) :-
1278		exclude(is_external_function_identifier,Identifiers,LessIdentifiers),
1279		maplist(create_smt_identifier(TranslationType, Solver),LessIdentifiers,State,Exprs).
1280
1281		create_bounded_smt_state(TranslationType, Solver,Identifiers,State,Exprs) :-
1282		maplist(create_bounded_smt_identifier(TranslationType, Solver),Identifiers,State,Exprs).
1283
1284		create_smt_identifier(TranslationType, Solver,b(identifier(Id),Type,_Infos),id(Id,Expr),Expr) :-
1285		ground(Id),
1286		!,
1287		smt_solver_interface_call(Solver,mk_var(TranslationType, Type,Id,Expr)).
1288		create_smt_identifier(_, _, b(identifier(_),Type,_Infos), _, _) :-
1289		add_error_fail(create_smt_identifier, 'Identifier name is not ground for type ~w~n', [Type]).
1290
1291		create_bounded_smt_identifier(TranslationType, Solver, b(identifier(Id),Type,_Infos), id(Id,Expr), Expr) :-
1292		ground(Id),
1293		!,
1294		smt_solver_interface_call(Solver,mk_bounded_var(TranslationType, Type,Id,Expr)).
1295		create_bounded_smt_identifier(_, _, b(identifier(_),Type,_Infos), _, _) :-
1296		add_error_fail(create_bounded_smt_identifier, 'Identifier name is not ground for type ~w~n', [Type]).
1297
1298		is_external_function_identifier(Id) :-
1299		get_texpr_id(Id,Name),
1300		is_external_function_name(Name).
1301
1302		lookup(Id,LS,GS,Expr) :-
1303		( member(id(Id,Expr),LS) % id defined in local store
1304		; member(id(Id,Expr),GS) % id defined in global store
1305		).
1306
1307		contains_unsupported_type_or_expression(TranslationType, Solver, TExpr) :-
1308		contains_unsupported_type_or_expression(TranslationType, Solver, TExpr, _).
1309		contains_unsupported_type_or_expression(TranslationType, Solver, TExpr, Unsupported) :-
1310		map_over_typed_bexpr(smt_solvers_interface:contains_unsupported_aux(TranslationType, Solver), TExpr, Unsupported).
1311
1312		:- public contains_unsupported_aux/4.
1313		contains_unsupported_aux(TranslationType, Solver, TExpr, Expr) :-
1314		get_texpr_expr(TExpr, Expr),
1315		get_texpr_type(TExpr, Type),
1316		( unsupported_type(TranslationType, Type, Solver)
1317		-> debug:debug_println(9,unsupported_type(TranslationType,Type,Solver))
1318		; ( unsupported_expr(TranslationType, Expr, Type, Solver)
1319		-> functor(Expr,F,A),
1320		debug:debug_println(9,unsupported_expr(TranslationType,F/A))
1321		)
1322		).
1323
1324		% these expressions are not supported by one or more translation types
1325		%% change in Z3: lambda inside recursive functions was declared unsupported until proper support is provided (see https://github.com/Z3Prover/z3/issues/5813)
1326		%% see mk_op_iteration_func_decl in /extensions/z3interface/src/cpp/main.cpp
1327		unsupported_expr(sat, Expr, _, _) :-
1328		!,
1329		\+ (Expr = conjunct(_,_); Expr = disjunct(_,_); Expr = identifier(_); Expr = equal(_,_); Expr = implication(_,_); Expr = equivalence(_,_);
1330		Expr = negation(_); Expr = boolean_true; Expr = boolean_false; Expr = value(pred_true); Expr = value(pred_false)).
1331		unsupported_expr(_, power_of_real(_,_),_,_).
1332		unsupported_expr(_, struct(_),_,_).
1333		unsupported_expr(constructive, closure(_),_,_).
1334		unsupported_expr(constructive, iteration(_,_),_,_).
1335		%%
1336		unsupported_expr(axiomatic, general_union(_),_,_).
1337		unsupported_expr(axiomatic, general_intersection(_),_,_).
1338		unsupported_expr(_,general_product(_,_,_),_,_).
1339		unsupported_expr(_,general_sum(_,_,_),_,_).
1340		unsupported_expr(axiomatic, iteration(_,_),_,_).
1341		unsupported_expr(axiomatic, closure(_),_,_).
1342		unsupported_expr(_,external_pred_call(Pred,_),_,_) :-
1343		Pred \= 'LEQ_SYM'. % introduced by symmetry breaking; we could also try and turn this off in ast_cleanup
1344		unsupported_expr(_,external_function_call(_,_),_,_).
1345		unsupported_expr(_,function(Name,_),_,_) :-
1346		is_external_function_name(Name).
1347		unsupported_expr(_, general_concat(_),_,_).
1348		% the following exprs should have been removed by a rewrite rule
1349		unsupported_expr(axiomatic, pow_subset(_),_,_).
1350		unsupported_expr(axiomatic, pow1_subset(_),_,_).
1351		unsupported_expr(axiomatic, fin_subset(_),_,_).
1352		unsupported_expr(axiomatic, fin1_subset(_),_,_).
1353		unsupported_expr(axiomatic, composition(_,_),_,_).
1354		unsupported_expr(axiomatic, comprehension_set(_,_),_,_).
1355		unsupported_expr(axiomatic, image(_,_),_,_).
1356		unsupported_expr(axiomatic, reverse(_),_,_).
1357		unsupported_expr(axiomatic, range(_),_,_).
1358		unsupported_expr(axiomatic, domain(_),_,_).
1359		unsupported_expr(_,min(_),_,_).
1360		unsupported_expr(_,max(_),_,_).
1361		unsupported_expr(_,card(_),_,_).
1362		unsupported_expr(_,finite(_),_,_).
1363		unsupported_expr(axiomatic, interval(_,_),_,_).
1364		unsupported_expr(_,integer_set(_),_,_).
1365		unsupported_expr(_,real_set(_),_,_).
1366		unsupported_expr(_,float_set(_),_,_).
1367		unsupported_expr(axiomatic,parallel_product(_,_),_,_).
1368		unsupported_expr(axiomatic,direct_product(_,_),_,_).
1369		unsupported_expr(axiomatic, domain_restriction(_,_),_,_).
1370		unsupported_expr(axiomatic, range_restriction(_,_),_,_).
1371		unsupported_expr(axiomatic, domain_subtraction(_,_),_,_).
1372		unsupported_expr(axiomatic, range_subtraction(_,_),_,_).
1373		unsupported_expr(_,overwrite(_,_),_,_).
1374		unsupported_expr(axiomatic, cartesian_product(_,_),_,_).
1375		unsupported_expr(_,function(_,_),_,_).
1376		unsupported_expr(_,not_equal(_,_),_,_).
1377		unsupported_expr(_,not_member(_,_),_,_).
1378		unsupported_expr(_,relations(_,_),_,_).
1379		unsupported_expr(_,partial_function(_,_),_,_).
1380		unsupported_expr(_,total_function(_,_),_,_).
1381		unsupported_expr(_,partial_injection(_,_),_,_).
1382		unsupported_expr(_,total_injection(_,_),_,_).
1383		unsupported_expr(_,partial_surjection(_,_),_,_).
1384		unsupported_expr(_,total_surjection(_,_),_,_).
1385		unsupported_expr(_,total_relation(_,_),_,_).
1386		unsupported_expr(_,surjection_relation(_,_),_,_).
1387		unsupported_expr(_,total_surjection_relation(_,_),_,_).
1388		% certain values are not supported yet
1389		unsupported_expr(_,value(X),_,_) :- \+ ground(X). % can not translate unknown values
1390		unsupported_expr(TranslationType,value(couple(A,B)),couple(AT,BT),Solver) :-
1391		unsupported_expr(TranslationType,value(A),AT,Solver) ;
1392		unsupported_expr(TranslationType,value(B),BT,Solver).
1393		unsupported_expr(_,value(global_set('INTEGER')),_,cvc4).
1394		unsupported_expr(_,value(V),Type,_) :-
1395		V \= [], % empty set can be translated
1396		unsupported_value_type(Type).
1397		unsupported_expr(_,value(fd(Num,SetName)),global(SetName),_) :-
1398		\+ is_b_global_constant(SetName,Num,_). % has been invented by prob but is unnamed
1399		% cvc4 does not support generating a full set of a sort, thus there
1400		% is currently no way of expressing a complete deferred set
1401		unsupported_expr(_,identifier(SetName),set(global(SetName)),cvc4).
1402
1403		% some types are not supported / can not be translated at the moment
1404		unsupported_type(sat,Type,_) :-
1405		!,
1406		\+ (Type == pred; Type == boolean).
1407		unsupported_type(_,freetype,_).
1408		unsupported_type(_,any,_).
1409		unsupported_type(_,seq(_),_). % seq(S) is set(couple(integer,S)) and has been rewritten by seq_rewriter.pl
1410		unsupported_type(TranslationType,set(X),S) :-
1411		unsupported_type(TranslationType,X,S).
1412		unsupported_type(TranslationType,couple(A,B),S) :-
1413		unsupported_type(TranslationType,A,S) ; unsupported_type(TranslationType,B,S).
1414
1415		% currently unsupported values
1416		unsupported_value_type(set(T)) :-
1417		unsupported_value_type(T).
1418		unsupported_value_type(couple(A,B)) :-
1419		unsupported_value_type(A) ; unsupported_value_type(B).
1420		unsupported_value_type(global(S)) :-
1421		unfixed_deferred_set(S).
1422
1423
1424		% --------------------------------
1425
1426		% use_module(smt_solvers_interface(smt_solvers_interface)),smt_solvers_interface:smt_add_cnf([1,2,3],[[1],[2,3]]).
1427
1428		smt_add_cnf(Literals,Clauses) :-
1429		smt_add_cnf(z3sat,Literals,Clauses).
1430
1431		:- dynamic stored_solver_cnf_reference/1, stored_literal_avl_map/1.
1432
1433		:- use_module(library(avl),[list_to_avl/2, avl_fetch/3]).
1434		smt_add_cnf(Solver,Literals,Clauses) :-
1435		retractall(stored_solver_cnf_reference(_)),
1436		retractall(stored_literal_avl_map(_)),
1437		init_interface(Solver),
1438		smt_reset_cnf(Solver),
1439		format('Sending CNF to solver ~w~n',[Solver]),
1440		start_ms_timer(T0),
1441		maplist(add_literal(Solver),Literals,LitMap),
1442		list_to_avl([pred_true-1,pred_false-2|LitMap],LitAvl), % not sure we need pred_true-1 and pred_false-2 map
1443		assert(stored_literal_avl_map(LitAvl)),nl,
1444		debug_format(9,'Registered literals: ~w~n',[LitMap]),
1445		maplist(add_clause(Solver,LitAvl),Clauses,ClauseRefs),
1446		smt_solver_interface_call(Solver,mk_op_arglist(sat,conjunct,ClauseRefs,CNFRef)),
1447		tools:stop_ms_timer_with_msg(T0,sending_cnf_to_smt_solver(Solver)),
1448		assert(stored_solver_cnf_reference(CNFRef)).
1449
1450		add_clause(Solver,LitAvl,Clause,ClauseRef) :-
1451		maplist(translate_literal(Solver,LitAvl),Clause,ExprList),
1452		debug_format(9,'Sending clause to solver ~w~n',[ExprList]),
1453		smt_solver_interface_call(Solver,mk_op_arglist(sat,disjunct,ExprList,ClauseRef)).
1454
1455		smt_add_extra_clause_cnf(Solver,Clause) :-
1456		retract(stored_solver_cnf_reference(CNFRef)),
1457		stored_literal_avl_map(LitAvl),!,
1458		add_clause(Solver,LitAvl,Clause,NewClauseRef),
1459		smt_solver_interface_call(Solver,mk_op_arglist(sat,conjunct,[CNFRef,NewClauseRef],NewCNFRef)),
1460		debug:debug_println(19,stored_new_clause(Clause)),
1461		assert(stored_solver_cnf_reference(NewCNFRef)).
1462		smt_add_extra_clause_cnf(Solver,Clause) :-
1463		add_internal_error('No CNF stored for adding clause:',smt_add_extra_clause_cnf(Solver,Clause)),fail.
1464
1465
1466		smt_solve_cnf(Solver,Model) :-
1467		\+ stored_solver_cnf_reference(_),!,
1468		add_internal_error('No CNF stored for solving:',smt_solve_cnf(Solver,Model)),fail.
1469		smt_solve_cnf(Solver,Model) :-
1470		stored_solver_cnf_reference(CNFRef),
1471		start_ms_timer(T1),
1472		get_preference(time_out, TO),
1473		SelectedSolvers = [sat,sat_cdcl],
1474		AxmRef = -1, % do not solve anything with axiomatic and constructive z3 solver
1475		CnsRef = -1,
1476		smt_solver_interface_call(z3, z3interface:smt_solve_query(SelectedSolvers,AxmRef,CnsRef,CNFRef,TO,SMTResultData)),
1477		tools:stop_ms_timer_with_msg(T1,solving_cnf_with_smt_solver(Solver)),
1478		(debug_mode(off) -> true
1479		; write('; SMT TRANSLATION: '), nl, pretty_print_smt(z3), nl
1480		),
1481		write(result_data(SMTResultData)),nl,
1482		SMTResultData = result_tuple(_,SMTResult),
1483		( SMTResult=sat
1484		-> %smt_solver_interface_call(z3,get_full_model_string(FullModel)),
1485		model_translation:get_full_model_as_avl(Solver,AVL),
1486		%avl:portray_avl(AVL),nl,
1487		avl:avl_to_list(AVL,List),
1488		convert_to_cnf_model(List,1,Model)
1489		; write('UNSAT'),nl,flush_output,
1490		fail
1491		).
1492
1493
1494		smt_reset_cnf(_Solver) :- clear_state.
1495
1496		convert_to_cnf_model([],_,R) :- !, R=[].
1497		convert_to_cnf_model([_-X|T],Nr,[Lit|TM]) :-
1498		is_bool(X,Val),!,
1499		(Val=true -> Lit=Nr ; Lit is -Nr),
1500		N1 is Nr+1,
1501		convert_to_cnf_model(T,N1,TM).
1502		convert_to_cnf_model(L,_,R) :- add_error(smt_solvers_interface,'Invalid model value:',L),R=[].
1503
1504		is_bool('z3-define-fun'([],'Bool',Val),Val).
1505
1506
1507		%:- use_module(probsrc(tools_meta), [translate_term_into_atom/2]).
1508		add_literal(Solver,Number,Number-Z3Ref) :-
1509		number_to_atom(Number,Atom),
1510		smt_solver_interface_call(Solver,mk_bounded_var(sat,boolean,Atom,Z3Ref)).
1511
1512		lookup_literal(Literal,LitAvl,Z3Expr) :-
1513		avl_fetch(Literal,LitAvl,Z3Expr).
1514
1515		% we need to ensure that atoms have same order as numbers; otherwise we need to sort model
1516		number_to_atom(Nr,Atom) :- number_codes(Nr,C),
1517		gen_leading_zeros(Nr,9999999,C0s,C),
1518		(10*Nr>=9999999 -> add_warning(smt_solvers_interface,'Too many SAT variables:',Nr) ; true),
1519		atom_codes(Atom,[0'x|C0s]).
1520
1521		gen_leading_zeros(Nr,Lim) --> {Nr>Lim},!.
1522		gen_leading_zeros(Nr,Lim) --> [0'0], {N1 is Nr*10}, gen_leading_zeros(N1,Lim).
1523
1524
1525		translate_literal(Solver,LitAvl,neg(PLiteral),LitRef) :- !,
1526		lookup_literal(PLiteral,LitAvl,Z3Expr) ,
1527		smt_solver_interface_call(Solver,mk_op_arglist(sat,negation,[Z3Expr],LitRef)).
1528		translate_literal(_Solver,LitAvl,Literal,Z3Expr) :-
1529		(prob_pred_literal(Literal) ; Literal > 0),
1530		!,
1531		lookup_literal(Literal,LitAvl,Z3Expr).
1532		translate_literal(Solver,LitAvl,Literal,LitRef) :-
1533		Literal < 0,
1534		PLiteral is Literal * -1,
1535		translate_literal(Solver,LitAvl,neg(PLiteral),LitRef).
1536
1537		prob_pred_literal(pred_true).
1538		prob_pred_literal(pred_false).
1539
1540