1 | % (c) 2009-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(solver_interface, [solve_predicate/3, solve_predicate/4, solve_predicate/5, | |
6 | set_up_typed_localstate_for_pred/4, | |
7 | type_check_in_machine_context/2, | |
8 | predicate_uses_unfixed_deferred_set/1, predicate_uses_unfixed_deferred_set/2, | |
9 | unfixed_typed_id_in_list/3, | |
10 | call_with_smt_mode_enabled/1]). | |
11 | ||
12 | :- use_module(module_information,[module_info/2]). | |
13 | :- module_info(group,cbc). | |
14 | :- module_info(description,'This module provides an interface to ProB\'s constraint solving kernel.'). | |
15 | ||
16 | :- use_module(library(lists), [include/3,keys_and_values/3]). | |
17 | ||
18 | :- use_module(bmachine, [b_get_machine_variables/1, b_get_machine_constants/1, full_b_machine/1]). | |
19 | :- use_module(btypechecker,[env_empty/1,opentype/5, add_identifiers_to_environment/3, env_store_operator/4, env_store_definition/3]). | |
20 | :- use_module(b_global_sets, [is_b_global_constant/3, | |
21 | b_global_set/1, unfixed_deferred_set/1, | |
22 | contains_unfixed_deferred_set/1]). | |
23 | :- use_module(b_interpreter, [set_up_typed_localstate/6]). | |
24 | :- use_module(tools_timeout, [time_out_with_factor_call/4]). | |
25 | :- use_module(bsyntaxtree, [find_typed_identifier_uses/3, find_typed_identifier_uses/2, | |
26 | map_over_typed_bexpr/3, get_texpr_id/2, get_texpr_type/2, get_texpr_types/2]). | |
27 | :- use_module(error_manager). | |
28 | :- use_module(tools,[assert_once/1,foldl/5,foldl/4]). | |
29 | :- use_module(translate, [translate_bvalue/2, translate_bvalue_with_limit/3]). | |
30 | :- use_module(bmachine_structure,[get_section/3]). | |
31 | :- use_module(debug,[debug_println/2]). | |
32 | :- use_module(preferences). | |
33 | :- use_module(eventhandling,[announce_event/1]). | |
34 | :- use_module(smt_solvers_interface(smt_solvers_interface)). | |
35 | :- use_module(store, [normalise_value_for_var/4]). | |
36 | ||
37 | :- meta_predicate call_with_smt_mode_enabled(0). | |
38 | %:- meta_predicate call_with_chr(0). | |
39 | %call_with_chr(Call) :- call_with_preference(Call,use_chr_solver,true). | |
40 | ||
41 | ||
42 | % :- meta_predicate call_with_smt_mode_enabled(0). % directive above for Spider | |
43 | call_with_smt_mode_enabled(Call) :- | |
44 | temporary_set_preference(use_smt_mode,true,SMT), | |
45 | temporary_set_preference(use_clpfd_solver,true,CLPFD), % we also enable CLPFD | |
46 | % TO DO: also enable CHR | |
47 | call_cleanup( (Call,!), | |
48 | (reset_temporary_preference(use_smt_mode,SMT), | |
49 | reset_temporary_preference(use_clpfd_solver,CLPFD) | |
50 | )). | |
51 | ||
52 | % solve predicate finds *one* solution for predicate in State | |
53 | solve_predicate(Pred,State,Res) :- solve_predicate(Pred,State,1,Res). | |
54 | solve_predicate(Pred,State,TimeoutFactor,Res) :- | |
55 | solve_predicate(Pred,State,TimeoutFactor,[use_smt_mode/true,use_clpfd_solver/true],Res). | |
56 | ||
57 | % one could add a preference to try Z3 instead/or first: | |
58 | %solve_predicate(Pred,State,TimeoutFactor,Options,RealRes) :- | |
59 | % % preference(solve_predicates_with_z3,true), | |
60 | % !, print(solve_with_z3),nl, translate:print_bexpr(Pred),nl, | |
61 | % ((TimeoutFactor=1,Options=[]) -> true | |
62 | % ; format('TO DO; ignoring Timeout Factor ~w and Options ~w for Z3~n',[TimeoutFactor,Options])), | |
63 | % smt_solvers_interface:smt_solve_predicate(z3,Pred,State,RealRes), | |
64 | % print(z3_result(RealRes)),nl. | |
65 | solve_predicate(Pred,State,TimeoutFactor,Options,RealRes) :- | |
66 | solve_predicate_with_options(Options,[],Pred,State,TimeoutFactor,Res), !, | |
67 | if(solver_result(Res,Pred,State,Options,RealResBeforeFallback),true, | |
68 | (add_internal_error('Unknown solver_result: ',Res),RealResBeforeFallback=error)), | |
69 | fallback_to_smt_if_requested(RealResBeforeFallback,Pred,State,RealRes). | |
70 | ||
71 | % no fallback if solution / contradiction | |
72 | fallback_to_smt_if_requested(solution(S),_,_,Res) :- !, Res=solution(S). | |
73 | fallback_to_smt_if_requested(contradiction_found,_,_,Res) :- !,Res=contradiction_found. | |
74 | fallback_to_smt_if_requested(S,_,_,Res) :- | |
75 | \+ preferences:get_preference(smt_supported_interpreter,true), ! , Res = S. | |
76 | fallback_to_smt_if_requested(_,Pred,State,Res) :- | |
77 | smt_solve_predicate(z3,Pred,State,Res), !. | |
78 | ||
79 | solve_predicate_with_options([],RestOptions,Pred,State,TimeoutFactor,Res) :- | |
80 | solve_predicate_direct(Pred,State,TimeoutFactor,RestOptions,Res). | |
81 | solve_predicate_with_options([Option|T],RestOptions,Pred,State,TimeoutFactor,Res) :- | |
82 | solve_with_option(Option,T,RestOptions,Pred,State,TimeoutFactor,Res). | |
83 | ||
84 | solve_with_option('CHR',T,Rest,Pred,State,TimeoutFactor,Res) :- !, | |
85 | solve_with_option(use_chr_solver/true,T,Rest,Pred,State,TimeoutFactor,Res). | |
86 | solve_with_option('SMT',T,Rest,Pred,State,TimeoutFactor,Res) :- !, | |
87 | solve_with_option(use_smt_mode/true,T,Rest,Pred,State,TimeoutFactor,Res). | |
88 | solve_with_option('KODKOD',T,Rest,Pred,State,TimeoutFactor,Res) :- !, | |
89 | solve_with_option(try_kodkod_on_load/true,T,Rest,Pred,State,TimeoutFactor,Res). | |
90 | solve_with_option('SMT_SUPPORTED_INTERPRETER',T,Rest,Pred,State,TimeoutFactor,Res) :- !, | |
91 | solve_with_option(smt_supported_interpreter/true,T,Rest,Pred,State,TimeoutFactor,Res). | |
92 | solve_with_option('CLPFD',T,Rest,Pred,State,TimeoutFactor,Res) :- !, | |
93 | solve_with_option(use_clpfd_solver/true,T,Rest,Pred,State,TimeoutFactor,Res). | |
94 | solve_with_option(Pref/Val,T,Rest,Pred,State,TimeoutFactor,Res) :- !, | |
95 | call_with_preference(solve_predicate_with_options(T,Rest,Pred,State,TimeoutFactor,Res),Pref,Val). | |
96 | solve_with_option(Opt,T,Rest,Pred,State,TimeoutFactor,Res) :- | |
97 | valid_option(Opt),!, | |
98 | solve_predicate_with_options(T,[Opt|Rest],Pred,State,TimeoutFactor,Res). | |
99 | solve_with_option(Opt,T,Rest,Pred,State,TimeoutFactor,Res) :- | |
100 | add_warning(solve_with_option,'Unrecognised option: ',Opt), | |
101 | solve_predicate_with_options(T,Rest,Pred,State,TimeoutFactor,Res). | |
102 | ||
103 | valid_option(full_machine_state). | |
104 | valid_option(solve_in_visited_state(S)) :- atomic(S). | |
105 | valid_option(truncate(Limit)) :- number(Limit). % truncate pretty printing | |
106 | valid_option(truncate). % 10000 | |
107 | valid_option(force_evaluation). % force evaluation of symbolic results | |
108 | ||
109 | solve_predicate_direct(Pred,State,TimeoutFactor,Options,Res) :- | |
110 | %temporary_set_preference(randomise_enumeration_order,true), | |
111 | %temporary_set_preference(find_abort_values,true), % I am not sure we should do this; we want to find counter-examples quickly, we are less worried with finding WD-problems ?! | |
112 | ||
113 | %temporary_set_preference(minint,-2147483648), % disabled to pass tests 1004,1015,.. | |
114 | %temporary_set_preference(maxint,2147483647), | |
115 | (real_error_occurred -> reset_real_error_occurred, PrevErr=true ; PrevErr=false), | |
116 | ||
117 | smt_solvers_interface:init, | |
118 | announce_event(start_solving), | |
119 | solve_predicate_aux(Pred,State,TimeoutFactor,Options,InnerRes), | |
120 | announce_event(end_solving), | |
121 | ||
122 | (InnerRes = overflow -> Res = overflow ; real_error_occurred -> Res = error; Res = InnerRes), | |
123 | (PrevErr -> assert_real_error_occurred ; true). % re-establish real-error occured | |
124 | ||
125 | %:- use_module(clpfd_interface,[clpfd_overflow_error_message/0]). | |
126 | solve_predicate_aux(Pred,State,TimeoutFactor,Options,Res) :- | |
127 | enter_new_error_scope(ScopeID,solve_predicate), %print(enter_scope(ScopeID)),nl, | |
128 | call_cleanup(solve_predicate_aux1(Pred,State,TimeoutFactor,Options,Res), | |
129 | exit_error_scope(ScopeID,_,solve_predicate_aux)). | |
130 | ||
131 | solve_predicate_aux1(Pred,State,TimeoutFactor,Options,Res) :- | |
132 | solve_predicate_aux2(Pred,State,TimeoutFactor,Options,Res), | |
133 | !, % we only look for one solution | |
134 | clear_enumeration_warnings. % avoid propagating them higher up | |
135 | solve_predicate_aux1(_Pred,State,_TimeoutFactor,_Options,Res) :- | |
136 | critical_enumeration_warning_occured_in_error_scope(A,B,C,D), % we did not find a solution: check for enum warnings | |
137 | !, | |
138 | clear_enumeration_warnings, | |
139 | State = no_state, | |
140 | Res = virtual_time_out(enumeration_warning(A,B,C,D,critical)). | |
141 | solve_predicate_aux1(_Pred,State,_TimeoutFactor,_Options,Res) :- | |
142 | State = no_state, | |
143 | Res = no. | |
144 | ||
145 | ||
146 | :- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]). | |
147 | solve_predicate_aux2(Pred,State,TimeoutFactor,Options,Res) :- | |
148 | %predicate_level_optimizations(Pred,OptPred), % is now done in b_interpreter_components; to avoid that CSE disrupts partitioning | |
149 | catch_clpfd_overflow_call2( | |
150 | solve_predicate_aux3(Pred,State,TimeoutFactor,Options,Res), | |
151 | ( %print(overflow),nl,trace, | |
152 | %clpfd_interface:clpfd_overflow_warning_message, % message is already printed by catch_clpfd_overflow_call2 | |
153 | % we could try and solve without CLPFD ?!! | |
154 | Res=overflow,State=no_state)). | |
155 | ||
156 | /* | |
157 | filter_global_identifiers([],[]). | |
158 | filter_global_identifiers([Identifier|IDs],Out) :- | |
159 | filter_global_identifiers(IDs,TempOut), | |
160 | (is_global(Identifier) | |
161 | -> Out = TempOut | |
162 | ; Out = [Identifier|TempOut] | |
163 | ). | |
164 | ||
165 | is_global(Identifier) :- | |
166 | get_texpr_id(Identifier,Name), get_texpr_type(Identifier,Type), | |
167 | Type = global(Set), is_b_global_constant(Set,_Nr,Name). | |
168 | is_global(Identifier) :- | |
169 | get_texpr_id(Identifier,Name), get_texpr_type(Identifier,Type), | |
170 | Type = set(global(Name)), b_global_set(Name). | |
171 | */ | |
172 | ||
173 | :- use_module(b_interpreter_components). | |
174 | :- use_module('kodkod/kodkod',[apply_kodkod/3]). | |
175 | :- use_module(specfile,[state_corresponds_to_set_up_constants/2]). | |
176 | :- use_module(state_space,[visited_expression/2]). | |
177 | :- use_module(library(lists),[maplist/2]). | |
178 | solve_predicate_aux3(Pred,State,TimeoutFactor,Options,Res) :- | |
179 | % find all identifiers used in the predicate and create a state | |
180 | % was done by the caller, leading to code duplication | |
181 | (member(full_machine_state,Options) -> get_full_machine_state_typed_identifiers(FilteredIdentifiers) | |
182 | ; find_typed_identifier_uses(Pred,FilteredIdentifiers)), | |
183 | !, | |
184 | % global constants should not appear in the state | |
185 | % otherwise they treated are as variables by the solver | |
186 | % -> we now call find_typed_identifier_uses; we used to call filter_global_identifiers(Identifiers,FilteredIdentifiers), | |
187 | % state may be predefined / partially set up | |
188 | apply_kodkod(FilteredIdentifiers,Pred,Pred2), | |
189 | (member(solve_in_visited_state(StateID),Options) | |
190 | -> set_up_typed_localstate_for_pred(FilteredIdentifiers,Pred2,TypedVals,State), | |
191 | (visited_expression(StateID,StateExpr), | |
192 | state_corresponds_to_set_up_constants(StateExpr,FullStore) | |
193 | -> maplist(initialise_localstate(FullStore),State) | |
194 | ; StateID=root -> true | |
195 | ; add_internal_error('Illegal State:',use_visited_state(StateID)) | |
196 | ) | |
197 | ; var(State) | |
198 | -> set_up_typed_localstate_for_pred(FilteredIdentifiers,Pred2,TypedVals,State) | |
199 | % TypedVals contains typedval(Val,Type,Var,TriggersEnumWarning) | |
200 | % TO DO: add static_symmetry detection b_global_sets:static_symmetry_reduction_for_global_sets(State), | |
201 | ; add_warning(solve_predicate,'Non-variable state: ',State) | |
202 | % TypedVals is unbound, is this a problem !?? TO DO: investigate | |
203 | ), | |
204 | %tools_printing:print_term_summary(b_trace_test_components(Pred2,State,TypedVals)),nl, | |
205 | b_interpreter_components:reset_component_info(false), | |
206 | time_out_with_factor_call( | |
207 | b_interpreter_components:b_trace_test_components(Pred2,State,TypedVals), | |
208 | TimeoutFactor, [silent], | |
209 | TO='time_out'), | |
210 | (TO==time_out -> Res = TO ; Res = yes). | |
211 | ||
212 | % set up a complete typed solver state for machine with all constants and variables, even if typing invariants removed and no reference anymore to variable in Invariant | |
213 | % TypedVals need to be enumerated after calling solve_predicate, in case some variables are not constrained | |
214 | get_full_machine_state_typed_identifiers(TIds) :- | |
215 | b_get_machine_variables(Variables), | |
216 | b_get_machine_constants(Constants), append(Constants,Variables,TIds). | |
217 | ||
218 | :- use_module(static_ordering,[sort_ids_by_usage/4,reorder_state/3]). | |
219 | set_up_typed_localstate_for_pred(CV,Pred,TypedVals,State) :- | |
220 | (preferences:preference(use_static_ordering,true) | |
221 | -> static_ordering:sort_ids_by_usage(CV,Pred,SortedVarlist,no_warnings) , | |
222 | set_up_typed_localstate(SortedVarlist,_FreshVars,TypedVals,[],SortedState,positive), | |
223 | reorder_state(CV,SortedState,State) % SortedState can have issues with pack_state skeleton | |
224 | ; set_up_typed_localstate(CV,_FreshVars,TypedVals,[],State,positive)). | |
225 | ||
226 | % initialise local state with values found in bind list | |
227 | initialise_localstate(FullStore,bind(Var,Val)) :- | |
228 | (member(bind(Var,VarVal),FullStore) | |
229 | -> Val=VarVal ; true). | |
230 | ||
231 | % translate solver_result for use by Disprover/Prover or similar: | |
232 | solver_result(time_out,_P,_State,_,time_out). | |
233 | solver_result(error,_P,_State,_,error). | |
234 | solver_result(no,P,_State,_,Res) :- | |
235 | % there are two cases in which we might have a false negative: | |
236 | % we enumerated a critical variable | |
237 | %\+ event_occurred_in_error_scope(enumeration_warning(_,_,_,_,critical)), % we now check this in solve_predicate_aux1 | |
238 | % or there are unfixed / deferred global sets involved. | |
239 | (predicate_uses_unfixed_deferred_set(P,CType) | |
240 | % no unfixed global sets involved -> real contradiction found | |
241 | -> debug_println(10,solver_predicate_contains_unfixed_deferred_set(CType)), | |
242 | Res=no_solution_found(unfixed_deferred_sets) | |
243 | ; Res=contradiction_found | |
244 | ). | |
245 | solver_result(virtual_time_out(Reason),_P,_State,_,no_solution_found(Reason)) :- | |
246 | true. % this is now checked in solve_predicate_aux1: event_occurred_in_error_scope(enumeration_warning(A,B,C,D,critical)). | |
247 | solver_result(overflow,_P,_State,_,no_solution_found(clpfd_overflow)). | |
248 | solver_result(yes,_P,State,Options,solution(Solution)) :- | |
249 | findall(binding(Id,EValue,PPValue), | |
250 | (member(bind(Id,Value),State), | |
251 | (solver_pp_bvalue(Value,Options,EValue,PPValue) -> true ; PPValue='**pretty-print failed**')), | |
252 | Solution). | |
253 | ||
254 | % expand and pretty print solver result values: | |
255 | solver_pp_bvalue(Value,Options,EValue,PPValue) :- member(force_evaluation,Options),!, | |
256 | EXPAND=force, | |
257 | normalise_value_for_var(solver_result,EXPAND,Value,EValue), | |
258 | solver_pp_bvalue2(EValue,Options,PPValue). | |
259 | solver_pp_bvalue(Value,Options,Value,PPValue) :- solver_pp_bvalue2(Value,Options,PPValue). | |
260 | ||
261 | solver_pp_bvalue2(Value,Options,PPValue) :- member(truncate(Limit),Options),!, | |
262 | translate_bvalue_with_limit(Value,Limit,PPValue). % should we also control expand_avl_upto ?? | |
263 | solver_pp_bvalue2(Value,Options,PPValue) :- member(truncate,Options),!, | |
264 | translate_bvalue_with_limit(Value,10000,PPValue). | |
265 | solver_pp_bvalue2(Value,_,PPValue) :- translate_bvalue(Value,PPValue). | |
266 | ||
267 | % check if a typed expression references an unfixed deferred set in some inner node | |
268 | predicate_uses_unfixed_deferred_set(TExpr) :- predicate_uses_unfixed_deferred_set(TExpr,_). | |
269 | ||
270 | predicate_uses_unfixed_deferred_set(TExpr,CType) :- | |
271 | unfixed_deferred_set(_), % check first if some unfixed deferred set exists | |
272 | map_over_typed_bexpr(solver_interface:uses_unfixed_ds_aux,TExpr,CType). | |
273 | :- public uses_unfixed_ds_aux/2. | |
274 | uses_unfixed_ds_aux(TExpr,Type) :- get_texpr_type(TExpr,Type), | |
275 | contains_unfixed_deferred_set(Type). | |
276 | ||
277 | % find a typed id whose type references an unfixed deferred set | |
278 | unfixed_typed_id_in_list(TID,CType,Constants) :- | |
279 | unfixed_deferred_set(_), % check first if some unfixed deferred set exists | |
280 | member(TID,Constants), get_texpr_type(TID,CType), | |
281 | contains_unfixed_deferred_set(CType). | |
282 | ||
283 | :- use_module(library(lists),[maplist/3, include/3]). | |
284 | type_check_in_machine_context(Predicates, TPredicates) :- | |
285 | % create an empty type environment | |
286 | % and store the known types of variables / constants | |
287 | % otherwise, we might be unable to type variables from | |
288 | % machines somewhere in the refinement hierarchy | |
289 | % (their typing predicate might not be in the hypothesis) | |
290 | % Definitions are also added to the environment since the typechecker | |
291 | % inlines definitions. | |
292 | env_empty(E), | |
293 | b_get_machine_variables(V), b_get_machine_constants(C), | |
294 | % add theory operators | |
295 | full_b_machine(Machine), | |
296 | get_section(operators,Machine,Operators), | |
297 | keys_and_values(Operators,Ids,Ops), | |
298 | foldl(env_store_operator,Ids,Ops,E,EWithTheories), | |
299 | get_section(definitions, Machine, Definitions), | |
300 | foldl(env_store_definition, Definitions, EWithTheories, EWithDefinitions), | |
301 | % constants and variables | |
302 | findall(b(identifier(Name),global(GlobalSet),[enumerated_set_element]),is_b_global_constant(GlobalSet,_Nr,Name),GC), | |
303 | findall(b(identifier(Set),set(global(Set)),[given_set]),b_global_set(Set),GS), | |
304 | add_identifiers_to_environment(V,EWithDefinitions,EV), | |
305 | add_identifiers_to_environment(C,EV,EVC), | |
306 | add_identifiers_to_environment(GC,EVC,EVCGC), | |
307 | add_identifiers_to_environment(GS,EVCGC,EOut), | |
308 | opentype(Predicates, EOut, Identifiers, DeferredSets, TPredicates), | |
309 | % DeferredSets should be empty? I.e. should this be allowed to create new types? | |
310 | % currently this would not work as these types have not been added/registered in b_global_sets ! kernel_objects:basic_type would fail | |
311 | (DeferredSets = [] -> true | |
312 | ; include(problematic_id(DeferredSets),Identifiers,TErrIds), | |
313 | maplist(get_texpr_id,TErrIds,ErrIds), | |
314 | add_warning(solver_interface,'The types of some variables could not be determined: ',ErrIds), | |
315 | fail). | |
316 | % a possible refactoring for the above - however, it does not type with open identifiers | |
317 | % reverted it for now | |
318 | % bmachine:b_type_expressions(Predicates,[constants],_Types,TPredicates,Errors), | |
319 | % add_all_perrors(Errors,[],type_expression_error), | |
320 | % no_real_perror_occurred(Errors). | |
321 | ||
322 | problematic_id(DeferredSets,TID) :- get_texpr_type(TID,Type), | |
323 | uses_def_set(Type,DeferredSets). | |
324 | ||
325 | uses_def_set(global(T),DeferredSets) :- member(T,DeferredSets). | |
326 | uses_def_set(set(A),DeferredSets) :- uses_def_set(A,DeferredSets). | |
327 | uses_def_set(seq(A),DeferredSets) :- uses_def_set(A,DeferredSets). | |
328 | uses_def_set(couple(A,_),DeferredSets) :- uses_def_set(A,DeferredSets). | |
329 | uses_def_set(couple(_,A),DeferredSets) :- uses_def_set(A,DeferredSets). | |
330 | uses_def_set(record(F),DS) :- member(field(_,T),F), uses_def_set(T,DS). | |
331 | % TO DO: add freetypes |