1 | % (c) 2009-2024 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(b_interpreter_components,[ | |
6 | reset_component_info/1, | |
7 | b_trace_test_components/3, b_trace_test_components/4, | |
8 | b_trace_test_components_wf/4, | |
9 | unsat_component/2, unsat_component_enumeration_warning/1, | |
10 | unsat_or_unknown_component_exists/0, | |
11 | unsat_component_abort_error/1, | |
12 | unsat_conjunct_inside_component/4, | |
13 | det_solution_for_constant/2, | |
14 | det_solution_for_constant_was_stored/0, det_solution_for_constant_was_stored/1, | |
15 | b_tracetest_boolean_expression/5, | |
16 | observe_state/3, | |
17 | ||
18 | construct_optimized_exists/3, construct_optimized_exists/4, | |
19 | construct_optimized_exists/5, | |
20 | extract_equalities_in_quantifier/4 | |
21 | ]). | |
22 | ||
23 | :- use_module(b_interpreter,[b_test_boolean_expression/6]). | |
24 | :- use_module(preferences). | |
25 | :- use_module(kernel_waitflags). | |
26 | :- use_module(tools). | |
27 | :- use_module(translate). | |
28 | :- use_module(error_manager). | |
29 | :- use_module(library(lists)). | |
30 | :- use_module(b_enumerate, [b_tighter_enumerate_all_values/2, b_tighter_enumerate_values/3]). | |
31 | ||
32 | :- use_module(debug,[debug_println/2, debug_mode/1]). | |
33 | :- use_module(tools,[start_ms_timer/1, stop_ms_timer_with_msg/2, stop_ms_timer_with_debug_msg/2]). | |
34 | ||
35 | :- use_module(chrsrc(chr_integer_inequality),[attach_chr_integer_inequality_to_wf_store/1]). | |
36 | ||
37 | ||
38 | :- use_module(module_information,[module_info/2]). | |
39 | :- module_info(group,interpreter). | |
40 | :- module_info(description,'This module can be used to split a predicate into components and solving each component individually (with tracing feedback).'). | |
41 | ||
42 | /* -------------- */ | |
43 | /* dynamic bits */ | |
44 | /* -------------- */ | |
45 | ||
46 | :- dynamic skipped_unsat_conjunct/1, unsat_conjunct_inside_component/4. | |
47 | reset_unsat_conjunct_inside_component_info :- | |
48 | retractall(skipped_unsat_conjunct(_)), | |
49 | retractall(unsat_conjunct_inside_component(_,_,_,_)). | |
50 | reset_tracetest_for_component :- retractall(skipped_unsat_conjunct(_)). % to be called before trace checking a component | |
51 | ||
52 | % individual conjuncts which are directly unsatisfiable | |
53 | assert_skipped_failed_conjunct(ComponentNr,BE) :- assert_skipped_unsat_conjunct, | |
54 | assertz(unsat_conjunct_inside_component(ComponentNr,BE,false,'')), | |
55 | (preferences:get_preference(provide_trace_information,false) -> true | |
56 | ; add_message(b_interpreter_components,' *** INCONSISTENCY DETECTED, SKIPPING COMPONENT NR: ',ComponentNr, BE), | |
57 | (debug_mode(on) -> print_bexpr_with_limit(BE,500) ; print_bexpr_with_limit(BE,150)), nl | |
58 | ). | |
59 | assert_skipped_unknown_conjunct(ComponentNr,BE,Reason) :- assert_skipped_unknown_conjunct, | |
60 | assertz(unsat_conjunct_inside_component(ComponentNr,BE,unknown,Reason)), | |
61 | ((Reason=abort_error; Reason=well_definedness_error) | |
62 | -> assert_unsat_component_abort_error(ComponentNr) | |
63 | ; true), | |
64 | (preferences:get_preference(provide_trace_information,false) -> true | |
65 | ; get_reason_msg(Reason,MSG),format(' *** Skipping predicate due to ~w:',[MSG]), | |
66 | write(' '),print_bexpr_with_limit(BE,150),nl, | |
67 | format('~n *** Predicate is unknown~n *** COMPONENT NUMBER: ~w~n',[ComponentNr]) | |
68 | ). | |
69 | assert_skipped_unsat_conjunct :- | |
70 | (skipped_unsat_conjunct(false) -> true | |
71 | ; retractall(skipped_unsat_conjunct(_)), assertz(skipped_unsat_conjunct(false))). | |
72 | assert_skipped_unknown_conjunct :- | |
73 | (skipped_unsat_conjunct(_) -> true ; assertz(skipped_unsat_conjunct(unknown))). | |
74 | ||
75 | get_reason_msg(enumeration_warning,R) :- !, R='ENUMERATION WARNING'. | |
76 | get_reason_msg(M,M). | |
77 | ||
78 | ||
79 | :- dynamic unsat_component/2, unsat_component_enumeration_warning/1, unsat_component_abort_error/1. | |
80 | reset_unsat_component_info :- | |
81 | retractall(unsat_component(_,_)), | |
82 | retractall(unsat_component_enumeration_warning(_)), | |
83 | retractall(unsat_component_abort_error(_)). | |
84 | ||
85 | :- use_module(eventhandling,[register_event_listener/3]). | |
86 | :- register_event_listener(clear_specification,reset_unsat_component_info, | |
87 | 'Reset b_interpreter_components unsat component info.'). | |
88 | ||
89 | ||
90 | store_unsat_component_nr(X) :- % use if you do not know if it is unknown or unsat | |
91 | %error_manager:print_error_scopes, | |
92 | (critical_enumeration_warning_occured_in_error_scope | |
93 | -> Res = unknown | |
94 | % should we also detect abort_error_occured_in_error_scope ? | |
95 | ; Res=false), | |
96 | store_unsat_component_nr(X,Res). | |
97 | ||
98 | store_unsat_component_nr(X,FalseOrUnknown) :- | |
99 | debug_println(9,store_unsat_component_nr(X,FalseOrUnknown)), | |
100 | (unsat_component(X,false) -> true | |
101 | ; retractall(unsat_component(X,_)),assertz(unsat_component(X,FalseOrUnknown)) | |
102 | ), | |
103 | (critical_enumeration_warning_occured_in_error_scope, | |
104 | \+ unsat_component_enumeration_warning(X) | |
105 | -> assertz(unsat_component_enumeration_warning(X)), | |
106 | debug_println(19,enumeration_warning_in_component(X)) | |
107 | ; true), | |
108 | (abort_error_occured_in_error_scope | |
109 | -> assert_unsat_component_abort_error(X) | |
110 | ; true). | |
111 | %portray_unsat_components. | |
112 | unsat_component_exists :- unsat_component(_,false),!. | |
113 | unsat_or_unknown_component_exists :- unsat_component(_,_),!. | |
114 | ||
115 | % store the fact that an abort or wd error occurred for component | |
116 | assert_unsat_component_abort_error(X) :- \+ unsat_component_abort_error(X), | |
117 | assertz(unsat_component_abort_error(X)), | |
118 | debug_println(19,unsat_component_abort_error(X)). | |
119 | ||
120 | % small utility to display status of components | |
121 | :- public portray_unsat_components/0. | |
122 | portray_unsat_components :- format('Unsat components~n',[]), | |
123 | unsat_component(Comp,Status), | |
124 | (unsat_component_abort_error(Comp) -> Abort='abort/well_definedness error' ; Abort=''), | |
125 | (unsat_component_enumeration_warning(Comp) -> EW='enumeration_warning' ; EW=''), | |
126 | format('* component: ~w -> ~w ~w ~w~n',[Comp,Status,Abort,EW]), | |
127 | unsat_conjunct_inside_component(Comp,BE,S,Reason), | |
128 | format(' -> reason for ~w: ~w : ',[S,Reason]), translate:print_bexpr_with_limit(BE,100),nl, | |
129 | fail. | |
130 | portray_unsat_components. | |
131 | ||
132 | :- public nr_of_components/1. | |
133 | :- dynamic nr_of_components/1. | |
134 | :- dynamic allow_skipping_over_components/0. | |
135 | reset_component_info(AllowSkip) :- retractall(allow_skipping_over_components), | |
136 | (AllowSkip==true -> assertz(allow_skipping_over_components) ; true), | |
137 | reset_unsat_component_info, | |
138 | reset_unsat_conjunct_inside_component_info. | |
139 | ||
140 | % in Disprover mode we can stop straightaway; we are not interested in finding values for identifiers in other components; unless we have an enumeration warning !! | |
141 | % TO DO: keep track of enumeration warnings per component | |
142 | ||
143 | /* -------------- */ | |
144 | ||
145 | ||
146 | :- use_module(library(avl)). | |
147 | % You can use the term one as ComponentNr if you don't know the number or it is not relevant | |
148 | b_tracetest_boolean_expression(BE,LS,S,WF,ComponentNr) :- %print(catch(ComponentNr)),nl, | |
149 | empty_avl(Ai), | |
150 | catch_enumeration_warning_exceptions_and_wd_failures( | |
151 | b_tracetest_boolean_expression1(BE,LS,S,WF,ComponentNr,Ai,_Ao), | |
152 | % this should not backtrack (without WF0 set); otherwise we may get problems with error blocks nesting | |
153 | assert_skipped_unknown_conjunct(ComponentNr,BE,enumeration_warning), | |
154 | true, % true: add exceptions as event errors | |
155 | assert_skipped_unknown_conjunct(ComponentNr,BE,well_definedness_error), % for WD error | |
156 | component(ComponentNr)). % Source argument for debugging | |
157 | ||
158 | b_tracetest_boolean_expression1(b(Expr,_,Infos),LS,S,WF,ComponentNr,Ai,Ao) :- | |
159 | b_tracetest_boolean_expression2(Expr,Infos,LS,S,WF,ComponentNr,Ai,Ao). | |
160 | ||
161 | :- use_module(bsyntaxtree,[is_a_conjunct_or_neg_disj/3]). | |
162 | b_tracetest_boolean_expression2(Conjunct,Info,LocalState,State,WF,ComponentNr,Ai,Ao) :- | |
163 | is_a_conjunct_or_neg_disj(b(Conjunct,pred,Info),LHS,RHS), | |
164 | % also detects: not(A or B) <=> not(A) & not(B) and not(A=>B) <=> A & not(B) | |
165 | % \+(Info = [try_smt|_]), | |
166 | !, | |
167 | %% print('check lhs of conjunct: '), translate:print_bexpr(LHS),nl, | |
168 | b_tracetest_boolean_expression1(LHS,LocalState,State,WF,ComponentNr,Ai,Aii), | |
169 | %% print('check rhs of conjunct: '), translate:print_bexpr(RHS),nl, | |
170 | b_tracetest_boolean_expression1(RHS,LocalState,State,WF,ComponentNr,Aii,Ao). | |
171 | b_tracetest_boolean_expression2(BE,Infos,LS,S,WF,ComponentNr,Ai,Ao) :- | |
172 | (get_preference(provide_trace_information,true) | |
173 | -> format('~n ====> (~w) ',[ComponentNr]), | |
174 | print_bexpr_with_limit(b(BE,pred,Infos),250),nl | |
175 | ; true), | |
176 | if(safe_b_test_boolean_expression(ComponentNr,b(BE,pred,Infos),LS,S,WF,Ai,Ao), | |
177 | true, | |
178 | (assert_skipped_failed_conjunct(ComponentNr,b(BE,pred,Infos)), | |
179 | Ai=Ao)). | |
180 | ||
181 | ||
182 | safe_b_test_boolean_expression(ComponentNr,BE,LS,S,WF,Ai,Ao) :- %print(c(_ComponentNr,WF)),nl, translate:print_bexpr(BE),nl, | |
183 | preferences:get_preference(provide_trace_information,false), | |
184 | \+ abort_error_occured_in_error_scope, | |
185 | % avoid setting up new error scope for every conjunct with catch_enumeration_warning | |
186 | % BE is only displayed in TRACE_INFO mode anyway | |
187 | % can be a bottleneck, e.g., for :prob-file ../prob_examples/public_examples/Eval/Sudoku_SAT.eval | |
188 | !, | |
189 | if(b_test_boolean_expression(BE,LS,S,WF,Ai,Ao),true, | |
190 | (abort_error_occured_in_error_scope | |
191 | -> assert_unknown(ComponentNr,BE,abort_error,Ai,Ao) | |
192 | ; fail) | |
193 | ). | |
194 | safe_b_test_boolean_expression(ComponentNr,BE,LS,S,WF,Ai,Ao) :- | |
195 | catch_enumeration_warning_exceptions_and_wd_failures( | |
196 | b_test_boolean_expression(BE,LS,S,WF,Ai,Ao), % this should not backtrack (without WF0 set); | |
197 | % otherwise we may get problems with error blocks nesting | |
198 | assert_unknown(ComponentNr,BE,enumeration_warning,Ai,Ao), % call when exception caught | |
199 | true, % true: add exceptions as event errors | |
200 | assert_unknown(ComponentNr,BE,well_definedness_error,Ai,Ao), % call when wd_error caught | |
201 | component(ComponentNr)). % Source argument for debugging | |
202 | ||
203 | % Note: this will only detect enumeration warnings and WD errors in WF0 phase | |
204 | ||
205 | assert_unknown(ComponentNr,BE,Reason,Ai,Ao) :- % print(assert_unknown(ComponentNr,Reason)),nl, | |
206 | assert_skipped_unknown_conjunct(ComponentNr,BE,Reason),Ai=Ao. | |
207 | ||
208 | :- use_module(bsyntaxtree,[predicate_components_in_scope/3, | |
209 | predicate_identifiers_in_scope/3]). | |
210 | :- use_module(b_enumerate,[extract_do_not_enum_ids_from_predicate/2]). | |
211 | ||
212 | get_typedval_id(typedval(_Val,_Type,ID,_),ID). | |
213 | b_trace_test_components(Properties,ConstantsState,TypedVals) :- | |
214 | %format('b_trace_test_components(~w,~w,~w)',[Properties,ConstantsState,TypedVals]), | |
215 | ? | b_trace_test_components(Properties,ConstantsState,TypedVals,all). |
216 | b_trace_test_components_wf(Properties,ConstantsState,TypedVals,WF) :- | |
217 | b_trace_test_components_wf(Properties,ConstantsState,TypedVals,all,[],WF). | |
218 | b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables) :- | |
219 | ? | b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables,[]). |
220 | % in constract to /3 and /4 b_trace_test_components/5 does not fail if the predicate is unsatisfiable. | |
221 | % instead it returns the unsatisfiable component as the last argument | |
222 | % the other predicates still fail because they expect to find an empty list there | |
223 | b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables,UnsatConjuncts) :- | |
224 | ? | b_trace_test_components_wf(Properties,ConstantsState,TypedVals,RelevantVariables,UnsatConjuncts,no_wf_available). |
225 | b_trace_test_components_wf(Properties,ConstantsState,TypedVals,RelevantVariables,UnsatConjuncts,OuterWF) :- | |
226 | % we now treat all TypedVals as local variables: | |
227 | % ensure that we count them in predicate_components/predicate_identifiers | |
228 | % (in case they clash with global identifiers)! | |
229 | %start_ms_timer(T0), | |
230 | maplist(get_typedval_id,TypedVals,LocalVars), | |
231 | extract_do_not_enum_ids_from_predicate(Properties,DoNotEnumVars), | |
232 | (preferences:get_preference(partition_predicates,true) | |
233 | -> predicate_components_in_scope(Properties,LocalVars,Components), | |
234 | length(Components,Len), print_trace_message(nr_of_components(Len)) | |
235 | ; predicate_identifiers_in_scope(Properties,LocalVars,PropVars), | |
236 | Components = [component(Properties,PropVars)], Len=1 | |
237 | ), | |
238 | retractall(nr_of_components(_)),assertz(nr_of_components(Len)), | |
239 | reset_observe_state, | |
240 | %stop_ms_timer_with_debug_msg(T0,b_trace_test_components_preprocessing), | |
241 | b_trace_test_components2(Components,ConstantsState,TypedVals,RelevantVariables,DoNotEnumVars,1,WFList,OuterWF), | |
242 | ? | get_unsat_component(WFList,Components,UnsatConjuncts). |
243 | ||
244 | ||
245 | get_unsat_component(_,Components,UnsatConjuncts) :- | |
246 | unsat_component_exists, !, | |
247 | debug_println(9,unsatisfiable_predicate), | |
248 | unsat_component(UnsatComponentNr,false),!, | |
249 | nth1(UnsatComponentNr,Components,component(UnsatConjuncts,_)). | |
250 | get_unsat_component(WFList,Components,UnsatConjuncts) :- | |
251 | ? | get_unsat_component_aux(WFList,Components,UnsatConjuncts). |
252 | ||
253 | get_unsat_component_aux(WFList,Components,UnsatConjuncts) :- | |
254 | print_trace_message(grounding_wait_flags), % Note: for unknown components we continue grounding | |
255 | ? | l_ground_wait_flags(WFList), |
256 | (unsat_component(UnsatComponentNr,Status) | |
257 | -> debug_println(19,unsat_component(UnsatComponentNr,Status)), UnsatConjuncts \== [], | |
258 | nth1(UnsatComponentNr,Components,component(UnsatConjuncts,_)) | |
259 | ; UnsatConjuncts=[]). | |
260 | get_unsat_component_aux(_,Components,UnsatConjuncts) :- | |
261 | unsat_component(UnsatComponentNr,_),!, | |
262 | nth1(UnsatComponentNr,Components,component(UnsatConjuncts,_)). | |
263 | ||
264 | ||
265 | :- use_module(b_ast_cleanup,[predicate_level_optimizations/2]). | |
266 | :- use_module(debug,[printsilent_message/1]). | |
267 | print_trace_message(Msg) :- | |
268 | (preference(provide_trace_information,false) -> true | |
269 | ; printsilent_message(Msg)). | |
270 | print_trace_message_with_typed_vals(Msg,TypedVals) :- | |
271 | (preference(provide_trace_information,false) -> true | |
272 | ; printsilent_message(Msg), | |
273 | maplist(get_typedval_id,TypedVals,IDs), | |
274 | printsilent_message(IDs) | |
275 | ). | |
276 | ||
277 | b_trace_test_components2([],_ConstantsState,TypedVals,_,_,Nr,ResWF,OuterWF) :- | |
278 | (TypedVals=[] | |
279 | -> print_trace_message(finished_processing_component_predicates), | |
280 | ResWF=[] | |
281 | ; print_trace_message_with_typed_vals('Enumerating Identifiers without constraints: ',TypedVals), | |
282 | init_wait_flags(WF0,[b_tighter_enumerate_values]), | |
283 | copy_wait_flag_call_stack_info(OuterWF,WF0,WF), | |
284 | b_tighter_enumerate_all_values(TypedVals,WF), ResWF=[wf_comp(WF,Nr)]). | |
285 | b_trace_test_components2([component(Pred,ComponentVars)|T],ConstantsState,TypedVals,RelevantVariables,DoNotEnumVars, | |
286 | Nr,ResWF,OuterWF) :- | |
287 | N1 is Nr+1, | |
288 | ( RelevantVariables\=all, ComponentVars\= all, | |
289 | lists_are_disjoint(RelevantVariables,ComponentVars) | |
290 | -> print_trace_message(skipping_irrelevant_component(Nr,ComponentVars)), | |
291 | b_trace_test_components2(T,ConstantsState,TypedVals,RelevantVariables,DoNotEnumVars,N1,ResWF,OuterWF) | |
292 | ; %% print(checking_component_properties(Nr,ComponentVars)),nl, %% | |
293 | %% print(component(Nr)),nl, translate:nested_print_bexpr_as_classicalb(Pred),debug:nl_time, | |
294 | ResWF = [wf_comp(WF,Nr)|TWF], | |
295 | init_wait_flags(WF0,[wf_comp(Nr)]), | |
296 | copy_wait_flag_call_stack_info(OuterWF,WF0,WF), | |
297 | (preferences:preference(use_chr_solver,true) -> attach_chr_integer_inequality_to_wf_store(WF) ; true), | |
298 | (ComponentVars=all -> InTypedVals=TypedVals, OutTypedVals=[], ProjectedState=ConstantsState | |
299 | ; project_typed_vals(TypedVals,ComponentVars,InTypedVals,OutTypedVals), | |
300 | project_state(ConstantsState,ComponentVars,ProjectedState) % relevant, e.g., for exists which may wait on state becoming ground | |
301 | ), | |
302 | observe_state(InTypedVals,WF,Nr), %% | |
303 | reset_tracetest_for_component, | |
304 | predicate_level_optimizations(Pred,OPred), | |
305 | %%nl,nl,print(component(Nr,ComponentVars,ProjectedState)),nl,nl,translate:print_bexpr(Pred),nl,nl, | |
306 | %%start_ms_timer(T1), | |
307 | b_tracetest_boolean_expression(OPred,[],ProjectedState,WF,Nr), | |
308 | % Skipping can only occur in this call above, not in enumeration phase | |
309 | %% stop_ms_timer_with_debug_msg(T1,b_tracetest_boolean_expression(Nr)), | |
310 | %print(done_comp(Nr,WF,ComponentVars)),nl, | |
311 | (skipped_unsat_conjunct(FalseOrUnknown) | |
312 | -> store_unsat_component_nr(Nr,FalseOrUnknown), % can be unknown due to an enumeration warning, cf. test 1390 | |
313 | %print('UNSAT: '),translate:nested_print_bexpr(Pred),nl,nl, | |
314 | allow_skipping_over_components % check if we allow skipping over unsat components to | |
315 | % maybe find as many values for constants as possible (partial setup_constants),... | |
316 | % Note: in Disprover mode or solve_predicate (REPL) we can stop and fail straightaway | |
317 | ; %print_bt_message(setup_enumerating_constants(Nr)), %%(TypedVals)), %% | |
318 | b_tighter_enumerate_values(InTypedVals,DoNotEnumVars,WF), | |
319 | (preferences:get_preference(disprover_mode,false) -> true | |
320 | ; ground_wait_flag0(WF) % ensure that we give each component the chance to run WF0 inconsistency checks | |
321 | %, print(finished_wf0_grounding_in_disprover_mode(Nr)),nl | |
322 | ) | |
323 | ), | |
324 | % we could ground waitflag 1 (deterministic computations) ? | |
325 | b_trace_test_components2(T,ConstantsState,OutTypedVals,RelevantVariables,DoNotEnumVars,N1,TWF,OuterWF) | |
326 | ). | |
327 | ||
328 | ||
329 | l_ground_wait_flags(WF) :- | |
330 | ? | l_ground_wait_flags(WF,WFE,Result), |
331 | (Result=false | |
332 | -> (!,fail) % Cut: to prevent backtracking to find other solutions for earlier components ! | |
333 | % Assumption: each component is independent and finding other solution for earlier component would again lead to failure in last component checked by l_ground_wait_flags/2 | |
334 | ; grd_ef(WFE)). | |
335 | ||
336 | l_ground_wait_flags([],_,true). | |
337 | l_ground_wait_flags([wf_comp(_,ComponentNr)|TWF],WFE,SatResult) :- | |
338 | unsat_component(ComponentNr,_),!, % We now longer try and ground unknown components | |
339 | l_ground_wait_flags(TWF,WFE,SatResult). | |
340 | l_ground_wait_flags([wf_comp(WF,ComponentNr)|TWF],WFE,SatResult) :- | |
341 | (debug_mode(off) -> true ; print(grounding_component(ComponentNr)),nl, start_ms_timer(Timer)), | |
342 | % print_bt_message(grounding_component(ComponentNr)), portray_waitflags(WF),nl, %% | |
343 | % maybe we should set up new error scope ? <--- TO DO | |
344 | ? | if(ground_constraintprop_wait_flags(WF), |
345 | ((pending_abort_error(WF) -> assert_unsat_component_abort_error(ComponentNr) ; true), | |
346 | (debug_mode(on) -> (pending_abort_error(WF) -> Msg='PENDING WD/ABORT ERROR'; Msg='true'), | |
347 | stop_ms_timer_with_msg(Timer,component(ComponentNr,Msg)) | |
348 | ; true), | |
349 | get_enumeration_finished_wait_flag(WF,WFE), % bind enumeration finished to the global outer WFE flag | |
350 | l_ground_wait_flags(TWF,WFE,SatResult) % continue with other components | |
351 | ), | |
352 | ((debug_mode(on) -> print(unsatisfiable_component(ComponentNr)),nl, | |
353 | stop_ms_timer_with_msg(Timer,component(ComponentNr,'false')) ; true), | |
354 | store_unsat_component_nr(ComponentNr), | |
355 | SatResult=false)). | |
356 | ||
357 | project_typed_vals([],_,[],[]). | |
358 | project_typed_vals([typedval(Val,Type,VarID,EnumWarningInfos)|Rest],ComponentVars,In,Out) :- | |
359 | (member(VarID,ComponentVars) | |
360 | -> In = [typedval(Val,Type,VarID,EnumWarningInfos)|In2], Out2=Out | |
361 | ; Out = [typedval(Val,Type,VarID,EnumWarningInfos)|Out2], In2=In | |
362 | ), project_typed_vals(Rest,ComponentVars,In2,Out2). | |
363 | project_state([],_,[]). | |
364 | project_state([bind(VarID,Value)|Rest],ComponentVars,Out) :- | |
365 | (member(VarID,ComponentVars) | |
366 | -> Out=[bind(VarID,Value)|Out2] | |
367 | ; Out=Out2 | |
368 | ), project_state(Rest,ComponentVars,Out2). | |
369 | ||
370 | ||
371 | :- use_module(specfile,[get_specification_description/2]). | |
372 | :- use_module(state_packing,[pack_value/2,unpack_value/2]). | |
373 | :- volatile det_solution_for_constant_packed/2. | |
374 | :- dynamic det_solution_for_constant_packed/2. | |
375 | assert_det_solution_for_constant(Var,Val) :- | |
376 | (value_too_large(Val) -> PVal = '$TOO_LARGE' ,debug_println(4,not_storing(Var)) | |
377 | ; pack_value(Val,PVal) | |
378 | %,translate:translate_bvalue_with_limit(Val,200,VS),format(' STORING ---> ~w = ~w~n',[Var,VS]) | |
379 | ), | |
380 | assertz(det_solution_for_constant_packed(Var,PVal)). | |
381 | ||
382 | det_solution_for_constant(Var,Val) :- | |
383 | if(det_solution_for_constant_packed(Var,PVal), | |
384 | unpack_det_sol(Var,PVal,Val), | |
385 | (get_specification_description(properties,PROPS), | |
386 | ajoin([PROPS, ' are *not* true and no value was found (deterministically) for the following CONSTANT: '], Msg), | |
387 | add_message(det_value_not_found_for_constant,Msg,Var), | |
388 | fail) | |
389 | ). | |
390 | unpack_det_sol(Var,PVal,Val) :- | |
391 | (PVal = '$TOO_LARGE' | |
392 | -> get_specification_description(properties,PROPS), | |
393 | ajoin([PROPS, ' are *not* true and the following CONSTANT was not stored due to its size (set preference ALLOW_INCOMPLETE_SETUP_CONSTANTS to TRUE to store all constants found): '], Msg), | |
394 | add_message(det_value_not_stored_for_constant,Msg,Var), | |
395 | fail | |
396 | ; unpack_value(PVal,Val) | |
397 | ). | |
398 | ||
399 | det_solution_for_constant_was_stored :- (det_solution_for_constant_was_stored(_) -> true). | |
400 | det_solution_for_constant_was_stored(Var) :- det_solution_for_constant_packed(Var,_). | |
401 | ||
402 | :- use_module(avl_tools,[avl_height_less_than/2]). | |
403 | value_too_large(avl_set(A)) :- | |
404 | preference(allow_incomplete_partial_setup_constants,false), %if true we always store the value | |
405 | (preference(provide_trace_information,false) -> MaxH=7 ; MaxH=9), | |
406 | \+ avl_height_less_than(A,MaxH). | |
407 | % TO DO: it could be a small set but include large subsets ! | |
408 | value_too_large((A,B)) :- (value_too_large(A) -> true ; value_too_large(B)). | |
409 | value_too_large(rec(F)) :- member(field(_,FVal),F), value_too_large(FVal). | |
410 | % TODO: detect large symbolic closures | |
411 | ||
412 | :- use_module(tools_printing,[print_value_summary/1]). | |
413 | reset_observe_state :- retractall(det_solution_for_constant_packed(_,_)). | |
414 | observe_state(Env,WF,ComponentNr) :- | |
415 | get_wait_flag0(WF,WF0), get_wait_flag1(observe_state,WF,WF1), | |
416 | (preferences:get_preference(provide_trace_information,true) | |
417 | -> when((ground(Env);nonvar(WF0)),print_success(WF0,ComponentNr,Env,WF)) | |
418 | %% ,when(nonvar(WF1),(nl, print('Starting Phase 1'),nl, portray_waitflags(WF))) | |
419 | ; true), | |
420 | observe_state2(Env,WF0,WF1). | |
421 | %,when(nonvar(WF0),(print(wf0),nl,portray_waitflags(WF))), when(nonvar(WF1),(print(wf1),nl)). | |
422 | ||
423 | :- use_module(debug,[debug_format/3]). | |
424 | print_success(WF0,ComponentNr,_,_WF) :- nonvar(WF0),!, | |
425 | debug_format(19,'~n-->> WF0 for component ~w grounded.~n',[ComponentNr]). | |
426 | print_success(_,ComponentNr,Env,_WF) :- | |
427 | (Env=[] | |
428 | -> | |
429 | format('~n-->> SUCCESS; processed component ~w (no identifiers)~n',[ComponentNr]) | |
430 | ; length(Env,NrVal), | |
431 | format('~n-->> SUCCESS; all ~w identifier(s) valued in component ~w~n',[NrVal,ComponentNr]) | |
432 | ), | |
433 | (debug_mode(on) | |
434 | -> findall(V,member(typedval(_,_,V,_),Env),Vars), | |
435 | statistics(walltime,[W,_]), format('-->> (walltime: ~w ms) : identifiers = ~w~n',[W,Vars]) | |
436 | ; true), | |
437 | %%,check_for_multiple_solutions(WF,ComponentNr) %% comment in to check for multiple solutions | |
438 | nl. | |
439 | ||
440 | observe_state2([],_,_). | |
441 | observe_state2([Binding|T],WF0,WF1) :- get_binding_value(Binding,VarID,Val), | |
442 | observe_variable(VarID,Val,WF0,WF1),observe_state2(T,WF0,WF1). | |
443 | ||
444 | get_binding_value(bind(Id,Value),Id,Value). | |
445 | get_binding_value(typedval(Value,_Type,Id,_Trigger),Id,Value). | |
446 | ||
447 | % print a warning message if we find multiple solutions *after* all constants have been valued | |
448 | %:- public check_for_multiple_solutions/2. | |
449 | %check_for_multiple_solutions(WF,ComponentNr) :- get_enumeration_finished_wait_flag(WF,EWF), | |
450 | % retractall(solution_found(ComponentNr,_)), | |
451 | % add_solution(EWF,ComponentNr). | |
452 | %:- volatile solution_found/2. | |
453 | %:- dynamic solution_found/2. | |
454 | %:- block add_solution(-,?). | |
455 | %add_solution(_,ComponentNr) :- retract(solution_found(ComponentNr,Nr)),!, | |
456 | % print('*** Multiple solutions found *after valuation* for component '), print(ComponentNr),nl, | |
457 | % N1 is Nr+1, | |
458 | % print('*** Solution: '),print(N1),nl, | |
459 | % assertz(solution_found(ComponentNr,N1)). | |
460 | %add_solution(_,ComponentNr) :- | |
461 | % assertz(solution_found(ComponentNr,1)). | |
462 | ||
463 | observe_variable(Var,Val,WF0,_WF1) :- preferences:get_preference(provide_trace_information,false),!, | |
464 | observe_variable_no_trace(Var,Val,WF0). | |
465 | observe_variable(Var,Val,WF0,WF1) :- | |
466 | ground_value_check(Val,GrVal), | |
467 | observe_variable0_block(Var,Val,GrVal,WF0,WF1). | |
468 | :- block observe_variable0_block(?,?,-,-,?). | |
469 | observe_variable0_block(Var,Val,GrVal,WF0,WF1) :- | |
470 | (var(GrVal) -> write(' :?: '), write(Var), write(' '), print_value_summary(Val), | |
471 | observe_variable1(Var,Val,WF1) | |
472 | ; (var(WF0) -> write('-->> ') | |
473 | ; write('--0-->> ')), % WF0/GrVal grounded at same time probably does not happen (often) | |
474 | write(Var),nl, write(' '),print_value_summary(Val),print_walltime,nl, | |
475 | assert_det_solution_for_constant(Var,Val) | |
476 | ). | |
477 | :- use_module(kernel_tools,[ground_value/1,ground_value_check/2]). | |
478 | :- block observe_variable_no_trace(?,-,-). | |
479 | observe_variable_no_trace(Var,Val,WF0) :- nonvar(WF0),!, % important e.g. for test 1368 | |
480 | (ground_value(Val) -> assert_det_solution_for_constant(Var,Val) ; true). | |
481 | observe_variable_no_trace(Var,Val,WF0) :- ground_value_check(Val,GV), | |
482 | %tools_printing:print_term_summary(gr_val_check(Var,Val,GV)),nl, | |
483 | observe_variable_no_trace4(Var,GV,Val,WF0). | |
484 | :- block observe_variable_no_trace4(?,-,?,-). | |
485 | observe_variable_no_trace4(_,GV,_,_) :- var(GV),!. | |
486 | observe_variable_no_trace4(Var,_,Val,_) :- assert_det_solution_for_constant(Var,Val). % this could be expensive !? | |
487 | ||
488 | print_walltime :- statistics(walltime,[Tot,Delta]), | |
489 | (debug_mode(on) -> print(' '),tools:print_memory_used_wo_gc ; true), | |
490 | format(' ~w ms (Delta ~w ms) ',[Tot,Delta]). | |
491 | ||
492 | observe_variable1(Var,Val,WF1) :- ground_value_check(Val,GV), | |
493 | observe_variable1_block(Var,Val,WF1,GV). | |
494 | :- block observe_variable1_block(?,?,-,-). | |
495 | observe_variable1_block(Var,Val,_WF1,GV):- | |
496 | (nonvar(GV) | |
497 | -> write('--1-->> '), write(Var),nl, write(' '),print_value_summary(Val), | |
498 | assert_det_solution_for_constant(Var,Val) | |
499 | ; write(' :?1?: '), write(Var), write(' '), print_value_summary(Val) | |
500 | %% , when(ground(Val), (print('--ground-->> '),print(Var),print(' '), print_value_summary(Val))) % comment in to see grounding | |
501 | %% , external_functions:observe_state([bind(Var,Val)]) % comment in to observe values | |
502 | %% , translate:print_bstate([bind(Var,Val)]),nl % comment in to print full value with CLP(FD) info | |
503 | ). | |
504 | ||
505 | ||
506 | % -------------------- | |
507 | ||
508 | construct_optimized_exists(Parameters,Body,Pred) :- | |
509 | construct_optimized_exists(Parameters,Body,Pred,true,_). | |
510 | construct_optimized_exists(Parameters,Body,Pred,Simplify) :- | |
511 | construct_optimized_exists(Parameters,Body,Pred,Simplify,_). | |
512 | ||
513 | % we could also partition inside b_interpreter ? | |
514 | construct_optimized_exists(Parameters,Body,Pred,Simplify,NrComponents) :- | |
515 | % we can actually do more: first project out all conjuncts which do not have any variables in common with Parameters | |
516 | % #x.(P(x) & Q) <=> #x.(P(x)) & Q | |
517 | % we can also use a stronger version of predicate components #(x,y).( P(x,v) & Q(v,y)) <=> #(x).P(x,v) & #(y).Q(v,y) | |
518 | get_texpr_ids(Parameters,PIDs), | |
519 | %print(constructing_optimized_exists(PIDs)),nl, | |
520 | LocalVars = PIDs, | |
521 | predicate_components_with_restriction(Body,LocalVars,PIDs,Components), % we focus partition decision on PIDs, not on all identifiers | |
522 | %length(Components,Len), print(nr_of_components_for_exists(Len,Components)),nl, | |
523 | conjunct_components(Components,Parameters,Pred,Simplify,NrComponents). | |
524 | % print('* EXISTS: '),translate:print_bexpr(Pred),nl. | |
525 | ||
526 | :- use_module(bsyntaxtree). | |
527 | conjunct_components(C,Parameters,Res,Simplify,NrComponents) :- | |
528 | conjunct_components2(C,Parameters,List,Simplify,0,NrComponents), | |
529 | conjunct_predicates_with_pos_info(List,Res). | |
530 | ||
531 | conjunct_components2([],_Parameters,[],_,Nr,Nr). % :- (Parameters=[] -> true ; print(unused_existential_var(Parameters)),nl). | |
532 | conjunct_components2([component(Pred,ComponentVars)|T],Parameters,Res,Simplify,InNr,OutNr) :- | |
533 | augment_ids(ComponentVars,CV), % translate atomic id names into b(identifier(... | |
534 | tools:list_intersection(CV,Parameters,ExistParas), % TO DO: use ordsets | |
535 | (Simplify=true | |
536 | -> create_and_simplify_exists(ExistParas,Pred,EP) % no use in recursively calling construct_optimized_exists | |
537 | ; Simplify= no_cleanup_and_simplify | |
538 | -> create_exists(ExistParas,Pred,EP0), % avoid loops when called from ast_cleanup | |
539 | get_texpr_info(EP0,AllInfos0), | |
540 | (nonmember(nodeid(_),AllInfos0),ExistParas=[Par1|_] | |
541 | -> get_texpr_info(Par1,AllInfos1),extract_pos_infos(AllInfos1,PIs) % try and get position from ids | |
542 | ; PIs=[]), % we already have a position info | |
543 | add_texpr_infos(EP0,[partitioned_exists|PIs],EP) % add ,removed_typing ?? | |
544 | ; create_unsimplified_exists(ExistParas,Pred,EP) | |
545 | ), | |
546 | (EP=b(truth,pred,[]) % or should we allow _ for Info field ?? | |
547 | -> Res=TRes | |
548 | ; Res=[EP|TRes]), | |
549 | In1 is InNr+1, | |
550 | conjunct_components2(T,Parameters,TRes,Simplify,In1,OutNr). | |
551 | ||
552 | ||
553 | % translate a list of atomic ides into ids with the b/3 wrapper | |
554 | augment_ids([],[]). | |
555 | augment_ids([ID|T],[b(identifier(ID),_,_)|TT]) :- augment_ids(T,TT). | |
556 | ||
557 | % extract and inline simple equalities to remove quantified variables; useful for exists and forall | |
558 | % TO DO: move to b_quantifier_optimizations.pl or similar | |
559 | extract_equalities_in_quantifier(Parameters,Pred, ReducedParas,OutPred) :- | |
560 | extract_equalities2(Pred,Parameters,ReducedParas,NewPred,[],Subst), | |
561 | %sort(Subst,SortedSubst), | |
562 | %print(extracted(Subst)),nl, | |
563 | apply_subst(Subst,NewPred,OutPred). | |
564 | % apply equality inside expressions: note: this may duplicate expressions ! | |
565 | % However, it also works if the equalities contain parameters | |
566 | ||
567 | :- use_module(bsyntaxtree,[is_equality/3]). | |
568 | ||
569 | extract_equalities2(b(conjunct(A,B),pred,Info),Ids,RemIds,Res) --> !, | |
570 | {Res=b(conjunct(PA,PB),pred,Info)}, | |
571 | extract_equalities2(A, Ids,RemIds1,PA), | |
572 | extract_equalities2(B,RemIds1,RemIds,PB). | |
573 | extract_equalities2(TEqual,Ids,RemIds,NewPred,InSubst,OutSubst) :- | |
574 | is_equality(TEqual,ID,E), | |
575 | % TODO: we could try and split equalities if possible; usually this is done by ast_cleanup though? | |
576 | %(bsyntaxtree:split_equality(TEqual,A,B) -> nl,print('COULD BE SPLIT: '),translate:print_bexpr(TEqual),nl ; true), | |
577 | same_id_is_member(ID,Ids,SID,RemIds), | |
578 | %\+ occurs_in_expr(SID,E), % not cyclic; we check it again after applyng InSubst to E below | |
579 | \+ in_subst_dom(SID,InSubst), % ensure we don't already have an equation for the same ID | |
580 | compose_with_subst(InSubst,SID,E,OutSubst), % we can compose with existing substitution without occurs-check problem | |
581 | always_well_defined_or_disprover_mode(E), % otherwise we may move evaluation of E forward ! | |
582 | !, | |
583 | NewPred=b(truth,pred,[]). | |
584 | extract_equalities2(X,Ids,Ids,X) --> []. | |
585 | ||
586 | ||
587 | ||
588 | % compose a new binding Var/Expr with existing substitution Subst; where Subst was not yet applied to Expr | |
589 | compose_with_subst(Subst,Var,Expr,[Var/NewExpr|ModSubst]) :- | |
590 | apply_subst(Subst,Expr,NewExpr), | |
591 | \+ occurs_in_expr(Var,NewExpr), % otherwise cyclic | |
592 | apply_binding_to_substitution(Subst,Var,NewExpr,ModSubst). | |
593 | apply_binding_to_substitution([],_,_,[]). | |
594 | apply_binding_to_substitution([TV/TE|T],Var,Expr,[TV/TE2|NT]) :- | |
595 | \+ occurs_in_expr(TV,Expr), % otherwise we get a cyclic substitution --> fail | |
596 | replace_id_by_expr(TE,Var,Expr,TE2), | |
597 | apply_binding_to_substitution(T,Var,Expr,NT). | |
598 | ||
599 | apply_subst([],X,X). | |
600 | apply_subst([Var/Expr|T],E,NewE) :- | |
601 | (replace_id_by_expr(E,Var,Expr,E2) % replace identifier Var by expression Expr | |
602 | -> %apply_to_tail(T,Var,Expr,NT), % apply binding to tail of substitution | |
603 | apply_subst(T,E2,NewE) | |
604 | ; add_internal_error('Call failed: ',apply_subst([Var/Expr|T],E,NewE)),NewE=E). | |
605 | ||
606 | ||
607 | in_subst_dom(X,[I/_|T]) :- (X=I -> true ; in_subst_dom(X,T)). | |
608 | ||
609 | same_id_is_member(X,[H|T],SID,Rest) :- | |
610 | (same_id(X,H,SID) -> Rest=T ; Rest=[H|TR],same_id_is_member(X,T,SID,TR)). | |
611 | ||
612 | % TO DO: investigate what is the exact difference with create_exists_opt; partition into components is only done by construct_optimized_exists/3 | |
613 | create_and_simplify_exists(Paras,Pred,ResultingPred) :- | |
614 | extract_equalities_in_quantifier(Paras,Pred,NewParas,NewPred), | |
615 | create_and_simplify_exists2(NewParas,NewPred,ResultingPred). | |
616 | ||
617 | %:- use_module(b_interpreter_check,[arithmetic_op/4]). % TODO REFACTOR and move this and code below to separate module | |
618 | create_and_simplify_exists2([],Pred,R) :- !,R=Pred. | |
619 | % simplify #ID.(ID:E1 & ID:E2) <=> E1 /\ E2 /= {} , etc... now done in ast_cleanup | |
620 | % simplify #ID.(ID/:E) <=> E /= FullType also done in ast_cleanup | |
621 | % simplify #SID.(SID > Expr) <=> truth now done in ast_cleanup | |
622 | create_and_simplify_exists2(Parameters,Body,Res) :- create_unsimplified_exists(Parameters,Body,Res). | |
623 | % TO DO: treat nested exists | |
624 | ||
625 | ||
626 | ||
627 | :- use_module(b_ast_cleanup,[clean_up_pred/3]). | |
628 | :- use_module(bsyntaxtree,[add_texpr_info_if_new/3]). | |
629 | create_unsimplified_exists(Parameters,Body,Res) :- | |
630 | maplist(mark_generated_exists,Parameters,Para2), % mark that this is an artificially constructed; we now mark the exists | |
631 | create_exists(Para2,Body,Res1), | |
632 | add_texpr_info_if_new(Res1,removed_typing,Res2), % unconditionally add this info, avoid generating warnings in exists_body_warning, see test 625 | |
633 | % and avoid useless_let_message | |
634 | % previously removed_typing was only added for disjuncts or implications | |
635 | clean_up_pred(Res2,[],Res). % also computes used_ids, | |
636 | % and performs some existential quantifier optimisations like replace_exists_by_not_empty | |
637 | ||
638 | mark_generated_exists(TID1,TID2) :- add_texpr_info_if_new(TID1,generated_exists_parameter,TID2). |