1		% (c) 2015-2019 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_add_predicate/5,
7		smt_solve_predicate_in_state/5,
8		init/0]).
9
10		:- use_module(probsrc(module_information),[module_info/2]).
11		:- module_info(group,smt_solvers).
12		:- module_info(description,'This module provides an interface to SMT-solvers like CVC4 or Z3.').
13
14		:- use_module(library(lists), [maplist/2,maplist/3,maplist/4,
15		append/2,exclude/3,
16		nth0/3,some/2]).
17		:- use_module(library(sets), [list_to_set/2]).
18
19		:- use_module(probsrc(bsyntaxtree), [map_over_typed_bexpr/3,
20		find_typed_identifier_uses/2,
21		find_typed_identifier_uses/3,
22		get_texpr_type/2,
23		get_texpr_info/2,
24		get_texpr_expr/2,
25		get_texpr_id/2,
26		conjunction_to_list/2,
27		conjunct_predicates/2,
28		disjunction_to_list/2,
29		syntaxtraversion/6]).
30		:- use_module(probsrc(error_manager), [add_error_fail/3]).
31		:- use_module(probsrc(translate), [translate_bexpression/2]).
32		:- use_module(probsrc(preferences), [get_preference/2]).
33		:- use_module(probsrc(b_global_sets), [b_global_deferred_set/1,
34		unfixed_deferred_set/1,
35		b_get_global_enumerated_sets/1,
36		is_b_global_constant/3,
37		b_global_set_cardinality/2]).
38		:- use_module(probsrc(custom_explicit_sets), [expand_custom_set_to_list_now/2]).
39		:- use_module(probsrc(eventhandling),[register_event_listener/3]).
40		:- use_module(probsrc(external_functions), [is_external_function_name/1]).
41		:- use_module(probsrc(debug), [debug_format/3]).
42
43		:- use_module(model_translation, [translate_smt_model_to_b_values/4]).
44		:- use_module(ast_cleanup_for_smt, [clean_up/2]).
45		:- use_module(prob_state_predicates, [create_state_pred/4]).
46		:- use_module(solver_dispatcher).
47		:- use_module(smt_common_predicates).
48
49		init :-
50		preferences:get_preference(smt_supported_interpreter,true), !,
51		register_event_listener(start_solving,retractall(backjumping_symbols(_)),'clean smt backjumping information'),
52		register_event_listener(start_solving,init_interface(z3),'Init Z3 Interface for a new solving'),
53		register_event_listener(end_solving,reset_interface(z3),'Reset Z3 Interface after solving').
54		init.
55
56		:- block smt_add_predicate(-,?,?,?,?).
57		smt_add_predicate(_EnumWf,Pred,ProBLocalState,ProBState,Symbol) :-
58		backjump_on_symbol(Symbol),
59		smt_add_predicate_to_solver(z3,Pred,ProBLocalState,ProBState,Symbol).
60
61		smt_add_predicate_to_solver(Solver,Pred,ProBLocalState,ProBState,Symbol) :-
62		init_interface(Solver),
63		smt_solver_interface_call(Solver,push_frame),
64		clean_up(Pred,CPred),
65		find_typed_identifier_uses(CPred,[],Identifiers),
66		(contains_introduced_identifiers(Identifiers,CPred)
67		-> debug_format(9,'z3: skip: ~w~n because there were introduced identifiers', [Symbol])
68		; create_state_pred(Identifiers,ProBLocalState,ProBState,StatePred),
69		conjunction_to_list(StatePred,StatePredConjuncts),
70		exclude(contains_unsupported_type_or_expression(Solver),StatePredConjuncts,FilteredStatePredConjuncts),
71		conjunct_predicates(FilteredStatePredConjuncts,FilteredStatePred),
72		conjunct_predicates([FilteredStatePred,CPred],FullPred),
73		setup_sets(Solver,GlobalIdentifiers),
74		create_smt_state(Solver,Identifiers,IdentifierState,_),
75		append(IdentifierState,GlobalIdentifiers,GlobalState),
76		mk_expr_skip(Solver,FullPred,[],GlobalState,Expr),
77		translate_bexpression(FullPred,PPExpr),
78		debug_format(9,'z3: add expr: ~w using symbol: ~w~n', [PPExpr,Symbol]),
79		!, smt_add_predicate_aux(Solver,Expr,Symbol)).
80		smt_add_predicate_to_solver(Solver,_,_,_,_) :- % in case the predicate contains unsupported types, etc.
81		smt_solver_interface_call(Solver,pop_frame).
82
83		contains_introduced_identifiers(FreeIDs,TExpr) :-
84		syntaxtraversion(TExpr,_,Type,Infos,Subs,_),
85		(member(introduced_by(_),Infos) % identifier that has been introduced
86		-> % check if it is not bound by some quantifiers
87		get_texpr_id(TExpr,Identifier),
88		member(b(identifier(Identifier),Type,_),FreeIDs)
89		; some(contains_introduced_identifiers(FreeIDs),Subs)).
90
91		smt_add_predicate_aux(Solver,Expr,Symbol) :-
92		get_preference(time_out,TO),
93		QuickTO is TO // 100,
94		% smt solver is called multiple times anyway
95		% and keeps its state inbetween
96		% thus we can use only a fraction of the time_out
97		% after e.g. 100 predicates, the whole timeout will be spent.
98		smt_solver_interface_call(Solver,add_interpreter_constraint(Expr,Symbol,QuickTO,SMTResult)),
99		(SMTResult = unsat(Core) -> % inconsistency detected
100		debug_format(9,'z3: false with core: ~w~n',[Core]),
101		store_core_for_backjumping(Core),
102		fail ;
103		otherwise -> true).
104		smt_add_predicate_aux(Solver,_,_) :-
105		% remove frame upon backtracking
106		smt_solver_interface_call(Solver,pop_frame), fail.
107
108		:- dynamic backjumping_symbols/1.
109		store_core_for_backjumping(Core) :-
110		retractall(backjumping_symbols(_)),
111		cleanup_core_for_backjumping(Core,CleanCore),
112		assert(backjumping_symbols(CleanCore)).
113		cleanup_core_for_backjumping([],[]).
114		cleanup_core_for_backjumping([E|Es],[CE|CEs]) :-
115		tools:split_atom(E,['|'],[CE]),
116		cleanup_core_for_backjumping(Es,CEs).
117
118		backjump_on_symbol(Symbol) :-
119		backjumping_symbols(Symbols),
120		member(Symbol,Symbols),
121		debug_format(9,'smt check for backjump:~ncurrent symbol: ~w~nbackjumping symbols: ~w~n',[Symbol,Symbols]),
122		!, debug_format(9,'backjumping!',[]), fail.
123		backjump_on_symbol(_) :-
124		retractall(backjumping_symbols(_)).
125
126
127		:- use_module(probsrc(specfile),[state_corresponds_to_set_up_constants/2]).
128		:- use_module(probsrc(state_space),[visited_expression/2]).
129		:- use_module(probsrc(error_manager),[add_internal_error/2]).
130		% solve in a state stored in the state space
131		smt_solve_predicate_in_state(StateID,Solver,Pred,SolutionState,Result) :-
132		visited_expression(StateID,StateExpr),
133		state_corresponds_to_set_up_constants(StateExpr,FullStore),
134		!,
135		append(FullStore,SolutionState,SMTState),
136		smt_solve_predicate(Solver,Pred,SMTState,Result).
137		smt_solve_predicate_in_state(StateID,Solver,Pred,SolutionState,Result) :-
138		(StateID=root -> true
139		; add_internal_error('Illegal state:',smt_solve_predicate_in_state(StateID,Solver,Pred,SolutionState,Result))),
140		smt_solve_predicate(Solver,Pred,SolutionState,Result).
141
142		smt_solve_predicate(Solver,Pred,State,Result) :-
143		get_texpr_type(Pred,pred),
144		clean_up(Pred,CPred), !,
145		catch(smt_solve_predicate_aux(Solver,CPred,State,Result),
146		SolverException, % exception most likely happened in the setup phase; in check_sat the exceptions are caught
147		treat_exception(Solver,SolverException,Result)).
148
149		% not a predicate or cleanup failed
150		smt_solve_predicate(_,_,_,error).
151
152		% remove bindings from environment which are not relevant
153		% (otherwise we get errors like z3exception in get_string: invalid usage)
154		remove_useless_bindings(X,_,Res) :- var(X),!,Res=X.
155		remove_useless_bindings([],_,[]).
156		remove_useless_bindings([bind(Var,Val)|T],Ids,Res) :-
157		(get_texpr_id(TVar,Var),member(TVar,Ids) -> Res = [bind(Var,Val)|RT] ; Res=RT),
158		remove_useless_bindings(T,Ids,RT).
159
160		smt_solve_predicate_aux(Solver,Pred,_,Result) :-
161		contains_unsupported_type_or_expression(Solver,Pred,Un), !,
162		Result = no_solution_found(unsupported_type_or_expression(Un)).
163		smt_solve_predicate_aux(Solver,Pred,ProBState,Result) :-
164		reset_interface(Solver) ->
165		find_typed_identifier_uses(Pred,Identifiers),
166		remove_useless_bindings(ProBState,Identifiers,ProBState2),
167		create_state_pred(Identifiers,[],ProBState2,StatePred),
168		conjunction_to_list(StatePred,StatePredConjuncts),
169		exclude(contains_unsupported_type_or_expression(Solver),StatePredConjuncts,FilteredStatePredConjuncts),
170		conjunct_predicates(FilteredStatePredConjuncts,FilteredStatePred),
171		conjunct_predicates([FilteredStatePred,Pred],FullPred),
172
173		setup_sets(Solver,GlobalIdentifiers),
174		create_smt_state(Solver,Identifiers,IdentifierState,_),
175		append(IdentifierState,GlobalIdentifiers,GlobalState),
176
177		% trace,
178		mk_expr(FullPred,Solver,[],GlobalState,PExpr),
179
180		translate_bexpression(FullPred,PPPred),
181		debug_format(9,'Sending to ~w:~w~n',[Solver,PPPred]),
182		flush_output,
183		(debug:debug_mode(off) -> true ; pretty_print_smt(Solver,PExpr)),
184		!, % all preparations done, cut before calling solver
185		% to avoid backtracking into setup and finding solutions twice
186		catch(check_sat(Solver,PExpr,ProBState2,GlobalState,Identifiers,Result),
187		model_translation_failed, Result = no_solution_found(model_translation_failed))
188		; Result = no_solution_found(solver_not_available).
189		smt_solve_predicate_aux(_,_Pred,_,no_solution_found(translation_or_setup_failed)).
190
191		mk_expr_skip(Solver,Pred,[],GlobalState,Expr) :-
192		clean_up(Pred,CPred), !,
193		conjunction_to_list(CPred,List),
194		exclude(contains_unsupported_type_or_expression(Solver),List,NList),
195		conjunct_predicates(NList,NewCPred),
196		mk_expr(NewCPred,Solver,[],GlobalState,Expr).
197		mk_expr_skip(_,Pred,_,_,_) :- !,
198		add_error_fail(smt_solvers_interface,'mk_expr_skip failed',Pred).
199
200		check_sat(Solver,Expr,ProBState,State,Identifiers,Result) :-
201		catch(check_sat_aux(Solver,Expr,ProBState,State,Identifiers,Result),
202		SolverException,
203		treat_exception(Solver,SolverException,Result)).
204		treat_exception(Solver,Exc,Result) :- known_solver_exception(Exc,Reason),!,
205		reset_interface(Solver),Result = no_solution_found(Reason).
206		treat_exception(Solver,Exc,_) :- format('Unknown exception in solver ~w: ~w~n',[Solver,Exc]),
207		throw(Exc).
208		known_solver_exception(z3_exception(Reason),Reason).
209		known_solver_exception(logic_exception(Reason),Reason).
210
211		check_sat_aux(Solver,Expr,ProBState,State,Identifiers,Result) :-
212		get_preference(time_out,TO),
213		smt_solver_interface_call(Solver,query(Expr,TO,SMTResult)),
214		get_model_or_return_result(SMTResult,Solver,Expr,ProBState,State,Identifiers,Result).
215
216		get_model_or_return_result(unsat,_,_,_,_,_,contradiction_found).
217		get_model_or_return_result(unknown,_,_,_,_,_,no_solution_found(solver_answered_unknown)).
218		get_model_or_return_result(time_out,_,_,_,_,_,time_out).
219		get_model_or_return_result(sat,Solver,_,ProBState,State,Identifiers,solution(Bindings)) :-
220		exclude(is_smt_temp_var,Identifiers,FilteredIDs),
221		(translate_smt_model_to_b_values(Solver,State,FilteredIDs,Bindings)
222		-> (maplist(bind_in_prob_state(Bindings),ProBState) -> true
223		; throw(model_solution_extraction_failed)
224		)
225		; throw(model_translation_failed)).
226		get_model_or_return_result(sat,Solver,Expr,ProBState,State,Identifiers,Result) :-
227		next_result(Solver,Expr,ProBState,State,Identifiers,Result).
228
229		bind_in_prob_state(Bindings,bind(Id,Val)) :-
230		member(binding(Id,Z3Val,_),Bindings), %format('~w: ~w = ~w~n',[Id,Z3Val,Val]),nl,
231		% Z3 may return solution in list form, ProB had it in AVL form: hence use equal_object
232		kernel_objects:equal_object(Z3Val,Val).
233
234		% no global identifiers -> no other solution
235		next_result(_,_,_,_,[],Result) :- !,
236		Result = contradiction_found.
237		next_result(Solver,Expr,ProBState,State,Identifiers,Result) :-
238		findall(Id,member(id(_,Id),State),ExprIds),
239		smt_solver_interface_call(Solver,conjoin_negated_state(ExprIds,Expr,NewExpr)),
240		check_sat(Solver,NewExpr,ProBState,State,Identifiers,Result).
241
242		unary_operator(negation).
243		unary_operator(unary_minus).
244		binary_operator(equivalence).
245		binary_operator(implication).
246		binary_operator(less).
247		binary_operator(less_equal).
248		binary_operator(greater).
249		binary_operator(greater_equal).
250		binary_operator(add).
251		binary_operator(modulo).
252		binary_operator(minus).
253		binary_operator(multiplication).
254		binary_operator(div).
255		binary_operator(power_of).
256		binary_operator(member).
257		binary_operator(subset).
258		binary_operator(union).
259		binary_operator(intersection).
260		binary_operator(set_subtraction).
261
262		mk_expr_maplist(Solver,LS,GS,Op,Expr) :-
263		mk_expr(Op,Solver,LS,GS,Expr).
264
265		mk_expr(b(Op,Type,_Infos),Solver,LS,GS,Expr) :-
266		mk_expr_aux(Op,Type,Solver,LS,GS,Expr).
267
268		% unary operators
269		mk_expr_aux(Op,_,Solver,LS,GS,Expr) :-
270		Op =.. [Functor,A],
271		unary_operator(Functor), !,
272		mk_expr(A,Solver,LS,GS,AE),
273		smt_solver_interface_call(Solver,mk_op_arglist(Functor,[AE],Expr)).
274		% binary operators
275		mk_expr_aux(Op,_,Solver,LS,GS,Expr) :-
276		Op =.. [Functor,A,B],
277		binary_operator(Functor), !,
278		mk_expr(A,Solver,LS,GS,AE), mk_expr(B,Solver,LS,GS,BE),
279		smt_solver_interface_call(Solver,mk_op(Functor,AE,BE,Expr)).
280		% conjunct and disjunct are deconstructed to lists
281		mk_expr_aux(conjunct(A,B),pred,Solver,LS,GS,Expr) :- !,
282		conjunction_to_list(b(conjunct(A,B),pred,[]),List),
283		maplist(mk_expr_maplist(Solver,LS,GS),List,ExprList),
284		% truth/0 are removed from the conjunction during list / from list
285		% the list might be empty now!
286		(ExprList = [] -> smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr)) ;
287		ExprList = [X] -> Expr = X ;
288		otherwise -> smt_solver_interface_call(Solver,mk_op_arglist(conjunct,ExprList,Expr))).
289		mk_expr_aux(disjunct(A,B),pred,Solver,LS,GS,Expr) :- !,
290		disjunction_to_list(b(disjunct(A,B),pred,[]),List),
291		maplist(mk_expr_maplist(Solver,LS,GS),List,ExprList),
292		smt_solver_interface_call(Solver,mk_op_arglist(disjunct,ExprList,Expr)).
293		% special case for if then else
294		mk_expr_aux(if_then_else(Pred,A,B),_,Solver,LS,GS,Expr) :- !,
295		maplist(mk_expr_maplist(Solver,LS,GS),[Pred,A,B],ArgList),
296		smt_solver_interface_call(Solver,mk_op_arglist(if_then_else,ArgList,Expr)).
297		% special case for partition
298		mk_expr_aux(partition(S,Sets),pred,Solver,LS,GS,Expr) :- !,
299		% definition: sets are disjoint and S is the union
300		maplist(mk_expr_maplist(Solver,LS,GS),Sets,SetExprs),
301		pairwise_union(SetExprs,Solver,UnionOfSets),
302		mk_expr(S,Solver,LS,GS,SExpr),
303		smt_solver_interface_call(Solver,mk_op(equal,SExpr,UnionOfSets,EqualToUnion)), % S = Union(Sets)
304		% enforce sets pairwise disjoint (= intersection is empty)
305		get_texpr_type(S,Type),
306		smt_solver_interface_call(Solver,mk_empty_set(Type,EmptySet)),
307		pairwise_disjoint(SetExprs,Solver,EmptySet,PWConstraint),
308		smt_solver_interface_call(Solver,mk_op_arglist(conjunct,[EqualToUnion,PWConstraint],Expr)).
309		% quantifiers
310		mk_expr_aux(forall(IDs,b(truth,pred,_),B),pred,Solver,LS,GS,Expr) :- !,
311		create_bounded_smt_state(Solver,IDs,State,SMTExprs),
312		append(State,LS,NLS),
313		mk_expr(B,Solver,NLS,GS,BE),
314		smt_solver_interface_call(Solver,mk_quantifier(forall,SMTExprs,BE,Expr)).
315		mk_expr_aux(forall(IDs,A,B),pred,Solver,LS,GS,Expr) :- !,
316		create_bounded_smt_state(Solver,IDs,State,SMTExprs),
317		append(State,LS,NLS),
318		mk_expr(A,Solver,NLS,GS,AE), mk_expr(B,Solver,NLS,GS,BE),
319		smt_solver_interface_call(Solver,mk_op(implication,AE,BE,InnerExpr)),
320		smt_solver_interface_call(Solver,mk_quantifier(forall,SMTExprs,InnerExpr,Expr)).
321		mk_expr_aux(exists(IDs,B),pred,Solver,LS,GS,Expr) :- !,
322		create_bounded_smt_state(Solver,IDs,State,SMTExprs),
323		append(State,LS,NLS),
324		mk_expr(B,Solver,NLS,GS,InnerExpr),
325		smt_solver_interface_call(Solver,mk_quantifier(exists,SMTExprs,InnerExpr,Expr)).
326		% equality is a special case as it needs to distinguish
327		% booleans and other types
328		mk_expr_aux(equal(A,B),pred,Solver,LS,GS,Expr) :- !,
329		mk_expr(A,Solver,LS,GS,AE), mk_expr(B,Solver,LS,GS,BE),
330		get_texpr_type(A,Type),
331		(Type = boolean -> smt_solver_interface_call(Solver,mk_op(equivalence,AE,BE,Expr)) ;
332		otherwise -> smt_solver_interface_call(Solver,mk_op(equal,AE,BE,Expr))).
333		% records
334		mk_expr_aux(rec(ListOfFields),Type,Solver,LS,GS,Expr) :- !,
335		findall(FieldExpr, member(field(_,FieldExpr),ListOfFields), FieldExprs),
336		maplist(mk_expr_maplist(Solver,LS,GS),FieldExprs,SMTFieldExprs),
337		smt_solver_interface_call(Solver,mk_record_const(Type,SMTFieldExprs,Expr)).
338		mk_expr_aux(record_field(Record,FieldName),Type,Solver,LS,GS,Expr) :- !,
339		get_texpr_type(Record,record(RFields)),
340		nth0(FieldNr,RFields,field(FieldName,Type)),
341		% debug_format(9,'Field: ~w Type: ~w~n-> FieldNr: ~w~n',[FieldName,RFields,FieldNr]),
342		mk_expr(Record,Solver,LS,GS,SMTRecordExpr),
343		smt_solver_interface_call(Solver,mk_record_field(SMTRecordExpr,FieldNr,FieldName,Expr)).
344		% couple construction
345		mk_expr_aux(couple(A,B),Type,Solver,LS,GS,Expr) :- !,
346		mk_expr(A,Solver,LS,GS,AE), mk_expr(B,Solver,LS,GS,BE),
347		smt_solver_interface_call(Solver,mk_couple(Type,AE,BE,Expr)).
348		% constants and identifiers
349		mk_expr_aux(identifier(Id),_,_Solver,LS,GS,Expr) :- !,
350		lookup(Id,LS,GS,Expr).
351		mk_expr_aux(integer(Int),integer,Solver,_LS,_GS,Expr) :- !,
352		smt_solver_interface_call(Solver,mk_int_const(Int,Expr)).
353		mk_expr_aux(min_int,integer,Solver,_LS,_GS,Expr) :- !,
354		get_preference(minint,MinInt),
355		smt_solver_interface_call(Solver,mk_int_const(MinInt,Expr)).
356		mk_expr_aux(max_int,integer,Solver,_LS,_GS,Expr) :- !,
357		get_preference(maxint,MaxInt),
358		smt_solver_interface_call(Solver,mk_int_const(MaxInt,Expr)).
359		mk_expr_aux(boolean_true,boolean,Solver,_LS,_GS,Expr) :- !,
360		smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr)).
361		mk_expr_aux(boolean_false,boolean,Solver,_LS,_GS,Expr) :- !,
362		smt_solver_interface_call(Solver,mk_bool_const(boolean_false,Expr)).
363		mk_expr_aux(string(S),string,Solver,_LS,_GS,Expr) :- !,
364		smt_solver_interface_call(Solver,mk_string_const(S,Expr)).
365		mk_expr_aux(truth,pred,Solver,_LS,_GS,Expr) :- !,
366		smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr)).
367		mk_expr_aux(falsity,pred,Solver,_LS,_GS,Expr) :- !,
368		smt_solver_interface_call(Solver,mk_bool_const(boolean_false,Expr)).
369		mk_expr_aux(bool_set,set(boolean),Solver,_LS,_GS,Expr) :- !,
370		smt_solver_interface_call(Solver,mk_bool_const(boolean_true,True)),
371		smt_solver_interface_call(Solver,mk_bool_const(boolean_false,False)),
372		smt_solver_interface_call(Solver,mk_set([True,False],Expr)).
373		mk_expr_aux(set_extension(List),set(T),Solver,LS,GS,Expr) :- !,
374		maplist(mk_expr_maplist(Solver,LS,GS),List,SubExprs),
375		(SubExprs = [] -> smt_solver_interface_call(Solver,mk_empty_set(set(T),Expr)) ;
376		otherwise -> smt_solver_interface_call(Solver,mk_set(SubExprs,Expr))).
377		mk_expr_aux(empty_set,Type,Solver,_LS,_GS,Expr) :- !,
378		smt_solver_interface_call(Solver,mk_empty_set(Type,Expr)).
379		% given values
380		mk_expr_aux(value(V),Type,Solver,LS,GS,Expr) :- !,
381		mk_value(Type,V,Solver,LS,GS,Expr).
382		% ast nodes that can be ignored
383		mk_expr_aux(convert_bool(P),boolean,Solver,LS,GS,Expr) :- !,
384		mk_expr(P,Solver,LS,GS,Expr).
385		% lets
386		mk_expr_aux(let_expression(ListOfIDs,ListOfDefinitions,LetExpression),_Type,Solver,LS,GS,Expr) :-
387		create_let_state(ListOfIDs,ListOfDefinitions,Solver,LS,GS,NewLS),
388		mk_expr(LetExpression,Solver,NewLS,GS,Expr).
389		mk_expr_aux(let_predicate(ListOfIDs,ListOfDefinitions,LetExpression),pred,Solver,LS,GS,Expr) :-
390		create_let_state(ListOfIDs,ListOfDefinitions,Solver,LS,GS,NewLS),
391		mk_expr(LetExpression,Solver,NewLS,GS,Expr).
392		% error case
393		mk_expr_aux(Expr,_,_,_,_,_) :- !,
394		add_error_fail(smt_solvers_interface,'mk_expr failed',Expr).
395
396		create_let_state([],[],_,S,_,S).
397		create_let_state([ID|IDs],[Def|Defs],Solver,StateSoFar,GS,State) :-
398		get_texpr_id(ID,UnwrappedId),
399		mk_expr(Def,Solver,StateSoFar,GS,Expr),
400		create_let_state(IDs,Defs,Solver,[id(UnwrappedId,Expr)|StateSoFar],GS,State).
401
402		mk_value_maplist(Type,Solver,LS,GS,Val,Expr) :-
403		mk_value(Type,Val,Solver,LS,GS,Expr).
404		mk_value(integer,int(Int),Solver,_LS,_GS,Expr) :-
405		smt_solver_interface_call(Solver,mk_int_const(Int,Expr)).
406		mk_value(boolean,pred_false,Solver,_LS,_GS,Expr) :-
407		smt_solver_interface_call(Solver,mk_bool_const(boolean_false,Expr)).
408		mk_value(boolean,pred_true,Solver,_LS,_GS,Expr) :-
409		smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr)).
410		% only supported thanks to z3 full sets
411		mk_value(set(integer),global_set('INTEGER'),z3,_LS,_GS,Expr) :-
412		smt_solver_interface_call(z3,mk_full_set(set(integer),Expr)).
413		mk_value(set(global(X)),global_set(X),_Solver,LS,GS,Expr) :-
414		lookup(X,LS,GS,Expr).
415		mk_value(set(X),avl_set(Val),Solver,LS,GS,Expr) :-
416		expand_custom_set_to_list_now(avl_set(Val),Values),
417		mk_value(set(X),Values,Solver,LS,GS,Expr).
418		mk_value(set(X),List,Solver,LS,GS,Expr) :-
419		maplist(mk_value_maplist(X,Solver,LS,GS),List,SubExprs),
420		(SubExprs = [] -> smt_solver_interface_call(Solver,mk_empty_set(set(X),Expr)) ;
421		otherwise -> smt_solver_interface_call(Solver,mk_set(SubExprs,Expr))).
422		mk_value(couple(AT,BT),(A,B),Solver,LS,GS,Expr) :-
423		mk_value(AT,A,Solver,LS,GS,AE),
424		mk_value(BT,B,Solver,LS,GS,BE),
425		smt_solver_interface_call(Solver,mk_couple(couple(AT,BT),AE,BE,Expr)).
426		mk_value(global(Name),fd(Num,Name),_Solver,LS,GS,Expr) :-
427		is_b_global_constant(Name,Num,Constant),
428		lookup(Constant,LS,GS,Expr).
429		% error case
430		mk_value(Type,Value,_,_,_,_) :- !,
431		add_error_fail(smt_solvers_interface,'mk_value failed',[Type,Value]).
432
433		pairwise_union([S],_Solver,S) :- !.
434		pairwise_union([S|Sets],Solver,Expr) :-
435		pairwise_union(Sets,Solver,SS),
436		smt_solver_interface_call(Solver,mk_op(union,S,SS,Expr)).
437
438		pairwise_disjoint([H,T],Solver,EmptySet,Constraint) :- !,
439		pairwise_disjoint_mk_expr(Solver,H,T,EmptySet,Constraint).
440		pairwise_disjoint([H|T],Solver,EmptySet,Constraint) :-
441		pairwise_disjoint(H,T,Solver,EmptySet,SubConstraints),
442		pairwise_disjoint(T,Solver,EmptySet,SubConstraint),
443		smt_solver_interface_call(Solver,mk_op_arglist(conjunct,[SubConstraint|SubConstraints],Constraint)).
444
445		pairwise_disjoint(E,[Last],Solver,EmptySet,[C]) :- !,
446		pairwise_disjoint_mk_expr(Solver,E,Last,EmptySet,C).
447		pairwise_disjoint(E,[H|T],Solver,EmptySet,[C|Cs]) :-
448		pairwise_disjoint_mk_expr(Solver,E,H,EmptySet,C),
449		pairwise_disjoint(E,T,Solver,EmptySet,Cs).
450
451		pairwise_disjoint_mk_expr(Solver,A,B,EmptySet,PWConstraint) :-
452		smt_solver_interface_call(Solver,mk_op(intersection,A,B,Inter)),
453		smt_solver_interface_call(Solver,mk_op(equal,Inter,EmptySet,PWConstraint)).
454
455		mk_sort(Solver,Set) :-
456		smt_solver_interface_call(Solver,mk_sort(Set)).
457
458		setup_sets(Solver,GlobalIdentifiers) :-
459		% deferred sets -> only create a sort
460		findall(X,b_global_deferred_set(X),DeferredSets),
461		maplist(mk_sort(Solver),DeferredSets),
462		mk_deferred_set_identifiers(Solver,DeferredSets,DefSetIdentifiers),
463		% enumerated sets -> create a sort
464		% & set up distinct identifiers
465		b_get_global_enumerated_sets(EnumeratedSets),
466		% can not use setof / bagof for some reason
467		list_to_set(EnumeratedSets,EnumeratedSetsNoDuplicates),
468		maplist(setup_enumerated_set(Solver),EnumeratedSetsNoDuplicates,IdentifierLists),
469		append([DefSetIdentifiers|IdentifierLists],GlobalIdentifiers).
470
471		% currently only functional for z3
472		mk_deferred_set_identifiers(cvc4,_,[]).
473		mk_deferred_set_identifiers(z3,DeferredSets,DefSetIdentifiers) :-
474		maplist(mk_deferred_set_identifiers2,DeferredSets,DefSetIdentifiers).
475		mk_deferred_set_identifiers2(SetName,id(SetName,SetExpression)) :-
476		smt_solver_interface_call(z3,mk_full_set(set(global(SetName)),SetExpression)).
477		setup_enumerated_set(Solver,SetName,[SetIdentifier|Identifiers]) :-
478		% find all global constants belonging to the given set
479		findall(b(identifier(Cst),global(SetName),[]),
480		is_b_global_constant(SetName,_,Cst),
481		SetElements),
482		b_global_set_cardinality(SetName,Cardinality),
483		% make a new sort and create identifiers
484		smt_solver_interface_call(Solver,mk_sort_with_cardinality(SetName,Cardinality)),
485		create_smt_state(Solver,SetElements,Identifiers,Exprs),
486		smt_solver_interface_call(Solver,setup_enumerated_set(Exprs)),
487		SetIdentifier = id(SetName,SetExpression),
488		smt_solver_interface_call(Solver,mk_set(Exprs,SetExpression)).
489
490		create_smt_state(Solver,Identifiers,State,Exprs) :-
491		exclude(is_external_function_identifier,Identifiers,LessIdentifiers),
492		maplist(create_smt_identifier(Solver),LessIdentifiers,State,Exprs).
493		create_bounded_smt_state(Solver,Identifiers,State,Exprs) :-
494		maplist(create_bounded_smt_identifier(Solver),Identifiers,State,Exprs).
495		create_smt_identifier(Solver,b(identifier(Id),Type,_Infos),id(Id,Expr),Expr) :-
496		smt_solver_interface_call(Solver,mk_var(Type,Id,Expr)).
497		create_bounded_smt_identifier(Solver,b(identifier(Id),Type,_Infos),id(Id,Expr),Expr) :-
498		smt_solver_interface_call(Solver,mk_bounded_var(Type,Id,Expr)).
499
500		is_external_function_identifier(Id) :-
501		get_texpr_id(Id,Name),
502		is_external_function_name(Name).
503
504		lookup(Id,[],[id(Id,Expr)|_],Expr) :- !.
505		lookup(Id,[],[_|T],Expr) :- lookup(Id,[],T,Expr).
506		lookup(Id,[id(Id,Expr)|_],_,Expr) :- !.
507		lookup(Id,[_|T],GS,Expr) :- lookup(Id,T,GS,Expr).
508
509		contains_unsupported_type_or_expression(Solver,TExpr) :-
510		contains_unsupported_type_or_expression(Solver,TExpr,_).
511		contains_unsupported_type_or_expression(Solver,TExpr,Unsupported) :-
512		% TODO: shouldnt this expansion by done automatically,
513		% because map_over_typed_bexpr is a meta-predicate?
514		map_over_typed_bexpr(smt_solvers_interface:contains_unsupported_aux(Solver),TExpr,Unsupported).
515		:- public contains_unsupported_aux/3.
516		contains_unsupported_aux(Solver,TExpr,Expr) :-
517		get_texpr_expr(TExpr,Expr),
518		get_texpr_type(TExpr,Type),
519		unsupported_expr_or_type(Expr,Type,Solver).
520
521		% these expressions are not supported at all
522		unsupported_expr_or_type(general_union(_),_,_).
523		unsupported_expr_or_type(general_intersection(_),_,_).
524		unsupported_expr_or_type(general_product(_,_,_),_,_).
525		unsupported_expr_or_type(general_sum(_,_,_),_,_).
526		unsupported_expr_or_type(composition(_,_),_,_).
527		unsupported_expr_or_type(first_of_pair(_),_,_).
528		unsupported_expr_or_type(second_of_pair(_),_,_).
529		unsupported_expr_or_type(iteration(_,_),_,_).
530		unsupported_expr_or_type(closure(_),_,_).
531		unsupported_expr_or_type(pow_subset(_),_,_).
532		unsupported_expr_or_type(pow1_subset(_),_,_).
533		unsupported_expr_or_type(fin_subset(_),_,_).
534		unsupported_expr_or_type(fin1_subset(_),_,_).
535		unsupported_expr_or_type(external_pred_call(_,_),_,_).
536		unsupported_expr_or_type(external_function_call(_,_),_,_).
537		unsupported_expr_or_type(function(Name,_),_,_) :-
538		is_external_function_name(Name).
539		% the following exprs should have been removed by a rewrite rule
540		unsupported_expr_or_type(min(_),_,_).
541		unsupported_expr_or_type(max(_),_,_).
542		unsupported_expr_or_type(card(_),_,_).
543		unsupported_expr_or_type(finite(_),_,_).
544		unsupported_expr_or_type(comprehension_set(_,_),_,_).
545		unsupported_expr_or_type(interval(_,_),_,_).
546		unsupported_expr_or_type(integer_set(_),_,_).
547		unsupported_expr_or_type(parallel_product(_,_),_,_).
548		unsupported_expr_or_type(direct_product(_,_),_,_).
549		unsupported_expr_or_type(domain_restriction(_,_),_,_).
550		unsupported_expr_or_type(range_restriction(_,_),_,_).
551		unsupported_expr_or_type(domain_subtraction(_,_),_,_).
552		unsupported_expr_or_type(range_subtraction(_,_),_,_).
553		unsupported_expr_or_type(overwrite(_,_),_,_).
554		unsupported_expr_or_type(cartesian_product(_,_),_,_).
555		unsupported_expr_or_type(image(_,_),_,_).
556		unsupported_expr_or_type(range(_),_,_).
557		unsupported_expr_or_type(domain(_),_,_).
558		unsupported_expr_or_type(function(_,_),_,_).
559		unsupported_expr_or_type(not_equal(_,_),_,_).
560		unsupported_expr_or_type(not_member(_,_),_,_).
561		unsupported_expr_or_type(relations(_,_),_,_).
562		unsupported_expr_or_type(partial_function(_,_),_,_).
563		unsupported_expr_or_type(total_function(_,_),_,_).
564		unsupported_expr_or_type(partial_injection(_,_),_,_).
565		unsupported_expr_or_type(total_injection(_,_),_,_).
566		unsupported_expr_or_type(partial_surjection(_,_),_,_).
567		unsupported_expr_or_type(total_surjection(_,_),_,_).
568		unsupported_expr_or_type(total_relation(_,_),_,_).
569		unsupported_expr_or_type(surjection_relation(_,_),_,_).
570		unsupported_expr_or_type(total_surjection_relation(_,_),_,_).
571		% certain values are not supported yet
572		unsupported_expr_or_type(value(X),_,_) :- \+ ground(X). % can not translate unknown values
573		unsupported_expr_or_type(value(couple(A,B)),couple(AT,BT),Solver) :-
574		unsupported_expr_or_type(value(A),AT,Solver) ;
575		unsupported_expr_or_type(value(B),BT,Solver).
576		unsupported_expr_or_type(value(closure(_,_,_)),_,_).
577		unsupported_expr_or_type(value(global_set('INTEGER')),_,cvc4).
578		unsupported_expr_or_type(value(_),Type,_) :-
579		unsupported_value_type(Type).
580		unsupported_expr_or_type(value(fd(Num,SetName)),global(SetName),_) :-
581		\+ is_b_global_constant(SetName,Num,_). % has been invented by prob but is unnamed
582		% cvc4 does not support generating a full set of a sort, thus there
583		% is currently no way of expressing a complete deferred set
584		unsupported_expr_or_type(identifier(SetName),set(global(SetName)),cvc4).
585		% some types are not supported / can not be translated at the moment
586		unsupported_expr_or_type(_,Type,Solver) :- unsupported_type(Type,Solver).
587		unsupported_type(string,z3).
588		unsupported_type(any,_).
589		unsupported_type(seq(_),_).
590		unsupported_type(set(X),S) :-
591		unsupported_type(X,S).
592		unsupported_type(couple(A,B),S) :-
593		unsupported_type(A,S) ; unsupported_type(B,S).
594		% currently unsupported values
595		unsupported_value_type(set(T)) :-
596		unsupported_value_type(T).
597		unsupported_value_type(couple(A,B)) :-
598		unsupported_value_type(A) ; unsupported_value_type(B).
599		unsupported_value_type(global(S)) :-
600		unfixed_deferred_set(S).