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