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