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