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