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