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). |