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