1 | | % (c) 2009-2019 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 | | unsat_component/2, unsat_component_enumeration_warning/1, |
9 | | unsat_or_unknown_component_exists/0, |
10 | | unsat_component_abort_error/1, |
11 | | unsat_conjunct_inside_component/4, |
12 | | det_solution_for_constant/2, |
13 | | b_tracetest_boolean_expression/5, |
14 | | observe_state/3, |
15 | | |
16 | | construct_optimized_exists/3, construct_optimized_exists/4 |
17 | | ]). |
18 | | |
19 | | :- use_module(b_interpreter,[b_test_boolean_expression/6]). |
20 | | :- use_module(preferences). |
21 | | :- use_module(kernel_waitflags). |
22 | | :- use_module(tools). |
23 | | :- use_module(translate). |
24 | | :- use_module(error_manager). |
25 | | :- use_module(library(lists)). |
26 | | :- use_module(b_enumerate, [b_trace_tighter_enumerate_values/2]). |
27 | | |
28 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
29 | | :- if(\+ environ(disable_chr, true)). |
30 | | :- use_module(chrsrc(chr_integer_inequality),[attach_chr_integer_inequality_to_wf_store/1]). |
31 | | :- else. |
32 | | attach_chr_integer_inequality_to_wf_store(_). |
33 | | :- endif. |
34 | | |
35 | | :- use_module(module_information,[module_info/2]). |
36 | | :- module_info(group,interpreter). |
37 | | :- module_info(description,'This module can be used to split a predicate into components and solving each component individually (with tracing feedback).'). |
38 | | |
39 | | /* -------------- */ |
40 | | /* dynamic bits */ |
41 | | /* -------------- */ |
42 | | |
43 | | :- dynamic skipped_unsat_conjunct/1, unsat_conjunct_inside_component/4. |
44 | | reset_unsat_conjunct_inside_component_info :- |
45 | | retractall(skipped_unsat_conjunct(_)), |
46 | | retractall(unsat_conjunct_inside_component(_,_,_,_)). |
47 | | reset_tracetest_for_component :- retractall(skipped_unsat_conjunct(_)). % to be called before trace checking a component |
48 | | |
49 | | % individual conjuncts which are directly unsatisfiable |
50 | | assert_skipped_failed_conjunct(ComponentNr,BE) :- assert_skipped_unsat_conjunct, |
51 | | assert(unsat_conjunct_inside_component(ComponentNr,BE,false,'')), |
52 | | (preferences:get_preference(provide_trace_information,false) -> true |
53 | | ; print(' *** INCONSISTENCY DETECTED, SKIPPING: '), |
54 | | (debug_mode(on) -> print_bexpr_with_limit(BE,500) ; print_bexpr_with_limit(BE,150)), |
55 | | nl, |
56 | | print(' *** COMPONENT NUMBER: '), print(ComponentNr),nl). |
57 | | assert_skipped_unknown_conjunct(ComponentNr,BE,Reason) :- assert_skipped_unknown_conjunct, |
58 | | assert(unsat_conjunct_inside_component(ComponentNr,BE,unknown,Reason)), |
59 | | (preferences:get_preference(provide_trace_information,false) -> true |
60 | | ; get_reason_msg(Reason,MSG),format(' *** Skipping predicate due to ~w:',[MSG]), |
61 | | print_bexpr_with_limit(BE,150),nl, |
62 | | format('~n *** Predicate is unknown~n *** COMPONENT NUMBER: ~w~n',[ComponentNr]) |
63 | | ). |
64 | | assert_skipped_unsat_conjunct :- |
65 | | (skipped_unsat_conjunct(false) -> true |
66 | | ; retractall(skipped_unsat_conjunct(_)), assert(skipped_unsat_conjunct(false))). |
67 | | assert_skipped_unknown_conjunct :- |
68 | | (skipped_unsat_conjunct(_) -> true ; assert(skipped_unsat_conjunct(unknown))). |
69 | | |
70 | | get_reason_msg(enumeration_warning,R) :- !, R='ENUMERATION WARNING'. |
71 | | get_reason_msg('prob-ignore',R) :- !, R='prob-ignore pragma'. |
72 | | get_reason_msg(M,M). |
73 | | |
74 | | |
75 | | :- dynamic unsat_component/2, unsat_component_enumeration_warning/1, unsat_component_abort_error/1. |
76 | | reset_unsat_component_info :- |
77 | | retractall(unsat_component(_,_)), |
78 | | retractall(unsat_component_enumeration_warning(_)), |
79 | | retractall(unsat_component_abort_error(_)). |
80 | | |
81 | | :- use_module(eventhandling,[register_event_listener/3]). |
82 | | :- register_event_listener(clear_specification,reset_unsat_component_info, |
83 | | 'Reset b_interpreter_components unsat component info.'). |
84 | | |
85 | | store_unsat_component_nr(X,FalseOrUnknown) :- debug_println(19,store_unsat_component_nr(X,FalseOrUnknown)), |
86 | | (unsat_component(X,false) -> true |
87 | | ; retractall(unsat_component(X,_)),assert(unsat_component(X,FalseOrUnknown)) |
88 | | ), |
89 | | (enumeration_warning_occured_in_error_scope, |
90 | | \+ unsat_component_enumeration_warning(X) |
91 | | -> assert(unsat_component_enumeration_warning(X)), |
92 | | debug_println(19,enumeration_warning_in_component(X)) |
93 | | ; true), |
94 | | (abort_error_occured_in_error_scope, |
95 | | \+ unsat_component_abort_error(X) |
96 | | -> assert(unsat_component_abort_error(X)), print(abort(X)),nl, |
97 | | debug_println(19,unsat_component_abort_error(X)) |
98 | | ; true). |
99 | ? | unsat_component_exists :- unsat_component(_,false),!. |
100 | | unsat_or_unknown_component_exists :- unsat_component(_,_),!. |
101 | | |
102 | | :- public nr_of_components/1. |
103 | | :- dynamic nr_of_components/1. |
104 | | :- dynamic allow_skipping_over_components/0. |
105 | | reset_component_info(AllowSkip) :- retractall(allow_skipping_over_components), |
106 | | (AllowSkip==true -> assert(allow_skipping_over_components) ; true), |
107 | | reset_unsat_component_info, |
108 | | reset_unsat_conjunct_inside_component_info. |
109 | | |
110 | | % 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 !! |
111 | | % TO DO: keep track of enumeration warnings per component |
112 | | |
113 | | /* -------------- */ |
114 | | |
115 | | |
116 | | :- use_module(library(avl)). |
117 | | % You can use the term one as ComponentNr if you don't know the number or it is not relevant |
118 | | b_tracetest_boolean_expression(BE,LS,S,WF,ComponentNr) :- |
119 | | empty_avl(Ai), |
120 | | b_tracetest_boolean_expression1(BE,LS,S,WF,ComponentNr,Ai,_Ao). |
121 | | |
122 | | |
123 | | b_tracetest_boolean_expression1(b(Expr,_,Infos),LS,S,WF,ComponentNr,Ai,Ao) :- !, |
124 | | b_tracetest_boolean_expression2(Expr,Infos,LS,S,WF,ComponentNr,Ai,Ao). |
125 | | |
126 | | :- use_module(bsyntaxtree,[info_has_ignore_pragma/1]). |
127 | | |
128 | | b_tracetest_boolean_expression2(BE,Infos,_LS,_S,_WF,ComponentNr,Ai,Ao) :- |
129 | | get_preference(use_ignore_pragmas,true), |
130 | | info_has_ignore_pragma(Infos),!, |
131 | | format('~n ==IGNORING==> (~w) ',[ComponentNr]),print_bexpr_with_limit(BE,250),nl, |
132 | | assert_skipped_unknown_conjunct(ComponentNr,b(BE,pred,Infos),'prob-ignore'), |
133 | | Ai=Ao. |
134 | | b_tracetest_boolean_expression2(conjunct(LHS,RHS),_Info,LocalState,State,WF,ComponentNr,Ai,Ao) :- |
135 | | % \+(Info = [try_smt|_]), |
136 | | !, |
137 | | %% print('check lhs of conjunct: '), translate:print_bexpr(LHS),nl, |
138 | | b_tracetest_boolean_expression1(LHS,LocalState,State,WF,ComponentNr,Ai,Aii), |
139 | | %% print('check rhs of conjunct: '), translate:print_bexpr(RHS),nl, |
140 | | b_tracetest_boolean_expression1(RHS,LocalState,State,WF,ComponentNr,Aii,Ao). |
141 | | b_tracetest_boolean_expression2(BE,Infos,LS,S,WF,ComponentNr,Ai,Ao) :- |
142 | | (get_preference(provide_trace_information,true) |
143 | | -> format('~n ====> (~w) ',[ComponentNr]),print_bexpr_with_limit(BE,250),nl |
144 | | ; true), |
145 | | if(safe_b_test_boolean_expression(ComponentNr,b(BE,pred,Infos),LS,S,WF,Ai,Ao),true, %% b_det_test_boolean_expression2 |
146 | | (assert_skipped_failed_conjunct(ComponentNr,b(BE,pred,Infos)), |
147 | | Ai=Ao)). |
148 | | |
149 | | safe_b_test_boolean_expression(ComponentNr,BE,LS,S,WF,Ai,Ao) :- |
150 | | catch_enumeration_warning_exceptions( |
151 | | b_test_boolean_expression(BE,LS,S,WF,Ai,Ao), % this should not backtrack (without WF0 set); otherwise we may get problems with error blocks nesting |
152 | | (assert_skipped_unknown_conjunct(ComponentNr,BE,enumeration_warning),Ai=Ao), true). % true: add exceptions as event errors |
153 | | |
154 | | :- use_module(bsyntaxtree,[predicate_components_in_scope/3, |
155 | | predicate_identifiers/2,predicate_identifiers_in_scope/3]). |
156 | | |
157 | | get_typedval_id(typedval(_Val,_Type,ID,_),ID). |
158 | | b_trace_test_components(Properties,ConstantsState,TypedVals) :- |
159 | | %format('b_trace_test_components(~w,~w,~w)',[Properties,ConstantsState,TypedVals]), |
160 | ? | b_trace_test_components(Properties,ConstantsState,TypedVals,all). |
161 | | b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables) :- |
162 | ? | b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables,[]). |
163 | | % in constract to /3 and /4 b_trace_test_components/5 does not fail if the predicate is unsatisfiable. |
164 | | % instead it returns the unsatisfiable component as the last argument |
165 | | % the other predicates still fail because they expect to find an empty list there |
166 | | b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables,UnsatConjuncts) :- |
167 | | % we now treat all TypedVals as local variables: ensure that we count them in predicate_components/predicate_identifiers (in case they clash with global identifiers)! |
168 | ? | maplist(get_typedval_id,TypedVals,LocalVars), |
169 | ? | (preferences:get_preference(partition_predicates,true) |
170 | | -> predicate_components_in_scope(Properties,LocalVars,Components), |
171 | | length(Components,Len), print_trace_message(nr_of_components(Len)) |
172 | | ; predicate_identifiers_in_scope(Properties,LocalVars,PropVars), |
173 | | Components = [component(Properties,PropVars)], Len=1 |
174 | | ), |
175 | ? | retractall(nr_of_components(_)),assert(nr_of_components(Len)), |
176 | ? | reset_observe_state, |
177 | | % print(components(Components)),nl, |
178 | ? | b_trace_test_components2(Components,ConstantsState,TypedVals,RelevantVariables,1,WFList), |
179 | ? | get_unsat_component(WFList,Components,UnsatConjuncts). |
180 | | |
181 | | |
182 | | get_unsat_component(_,Components,UnsatConjuncts) :- |
183 | | unsat_component_exists, !, |
184 | | debug_println(9,unsatisfiable_predicate), |
185 | ? | unsat_component(UnsatComponentNr,false),!, |
186 | | nth0(UnsatComponentNr,Components,component(UnsatConjuncts,_)). |
187 | | get_unsat_component(WFList,Components,UnsatConjuncts) :- |
188 | ? | get_unsat_component_aux(WFList,Components,UnsatConjuncts). |
189 | | |
190 | | get_unsat_component_aux(WFList,Components,UnsatConjuncts) :- |
191 | ? | print_trace_message(grounding_wait_flags), % Note: for unknown components we continue grounding |
192 | ? | l_ground_wait_flags(WFList), |
193 | | (unsat_component(UnsatComponentNr,_) |
194 | | -> print(we_have_unsat(UnsatComponentNr)),nl, |
195 | | nth0(UnsatComponentNr,Components,component(UnsatConjuncts,_)) |
196 | | ; UnsatConjuncts=[]). |
197 | | get_unsat_component_aux(_,Components,UnsatConjuncts) :- |
198 | | unsat_component(UnsatComponentNr,_),!, |
199 | | nth0(UnsatComponentNr,Components,component(UnsatConjuncts,_)). |
200 | | |
201 | | |
202 | | :- use_module(b_ast_cleanup,[predicate_level_optimizations/2]). |
203 | | :- use_module(debug,[printsilent_message/1]). |
204 | | print_trace_message(Msg) :- |
205 | | (preference(provide_trace_information,false) -> true |
206 | | ; printsilent_message(Msg)). |
207 | | print_trace_message_with_typed_vals(Msg,TypedVals) :- |
208 | | (preference(provide_trace_information,false) -> true |
209 | | ; printsilent_message(Msg), |
210 | | maplist(get_typedval_id,TypedVals,IDs), |
211 | | printsilent_message(IDs) |
212 | | ). |
213 | | |
214 | | b_trace_test_components2([],_ConstantsState,TypedVals,_,Nr,ResWF) :- |
215 | | (TypedVals=[] -> print_trace_message(finished_processing_component_predicates), |
216 | | ResWF=[] |
217 | | ; print_trace_message_with_typed_vals('Enumerating Identifiers without constraints: ',TypedVals), |
218 | | init_wait_flags(WF), |
219 | | b_trace_tighter_enumerate_values(TypedVals,WF), ResWF=[wf_comp(WF,Nr)]). |
220 | | b_trace_test_components2([component(Pred,ComponentVars)|T],ConstantsState,TypedVals,RelevantVariables, |
221 | | Nr,ResWF) :- |
222 | | N1 is Nr+1, |
223 | | ((RelevantVariables\=all, ComponentVars\= all, |
224 | | lists_are_disjoint(RelevantVariables,ComponentVars)) |
225 | | -> print_trace_message(skipping_irrelevant_component(Nr,ComponentVars)), |
226 | | b_trace_test_components2(T,ConstantsState,TypedVals,RelevantVariables,N1,ResWF) |
227 | | ; debug_println(9,checking_component_properties(Nr,ComponentVars)), %% |
228 | | %% print(component(Nr)),nl, translate:nested_print_bexpr_as_classicalb(Pred),debug:nl_time, |
229 | | ResWF = [wf_comp(WF,Nr)|TWF], |
230 | | init_wait_flags(WF), |
231 | | attach_chr_integer_inequality_to_wf_store(WF), |
232 | | (ComponentVars=all -> InTypedVals=TypedVals, OutTypedVals=[], ProjectedState=ConstantsState |
233 | | ; project_typed_vals(TypedVals,ComponentVars,InTypedVals,OutTypedVals), |
234 | | project_state(ConstantsState,ComponentVars,ProjectedState) % relevant, e.g., for exists which may wait on state becoming ground |
235 | | ), |
236 | | observe_state(InTypedVals,WF,Nr), %% |
237 | | reset_tracetest_for_component, |
238 | | predicate_level_optimizations(Pred,OPred), |
239 | | %%nl,nl,print(component(Nr,ComponentVars,ProjectedState)),nl,nl,translate:print_bexpr(Pred),nl,nl, |
240 | | b_tracetest_boolean_expression(OPred,[],ProjectedState,WF,Nr), |
241 | | %print(done_comp(Nr,WF,ComponentVars)),nl, |
242 | | (skipped_unsat_conjunct(false) |
243 | | -> store_unsat_component_nr(Nr,false), |
244 | | allow_skipping_over_components % check if we allow skipping over unsat components to maybe find as many values for constants as possible ,... |
245 | | % Note: in Disprover mode we can stop and fail straightaway |
246 | | ; %print_bt_message(setup_enumerating_constants(Nr)), %%(TypedVals)), %% |
247 | | (skipped_unsat_conjunct(_) -> store_unsat_component_nr(Nr,unknown) ; true), % probably due to prob-ignore |
248 | | b_trace_tighter_enumerate_values(InTypedVals,WF), |
249 | | (preferences:get_preference(disprover_mode,false) -> true |
250 | | ; ground_wait_flag0(WF) % ensure that we give each component the chance to run WF0 inconsistency checks |
251 | | %, print(finished_wf0_grounding_in_disprover_mode(Nr)),nl |
252 | | ) |
253 | | ), |
254 | | % we could ground waitflag 1 (deterministic computations) ? |
255 | | b_trace_test_components2(T,ConstantsState,OutTypedVals,RelevantVariables,N1,TWF) |
256 | | ). |
257 | | |
258 | | :- use_module(debug,[debug_println/2, debug_mode/1]). |
259 | | :- use_module(tools,[start_ms_timer/1, stop_ms_timer_with_msg/2]). |
260 | | |
261 | | l_ground_wait_flags(WF) :- |
262 | ? | l_ground_wait_flags(WF,Result), |
263 | | (Result=false |
264 | | -> (!,fail) % Cut: to prevent backtracking to find other solutions for earlier components ! |
265 | | % 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 |
266 | | ; true). |
267 | | |
268 | | l_ground_wait_flags([],true). |
269 | | l_ground_wait_flags([wf_comp(WF,ComponentNr)|TWF],SatResult) :- %trace, |
270 | ? | (debug_mode(off) -> true ; print(grounding_component(ComponentNr)),nl, start_ms_timer(Timer)), |
271 | | % print_bt_message(grounding_component(ComponentNr)), portray_waitflags(WF),nl, %% |
272 | | % maybe we should set up new error scope ? <--- TO DO |
273 | ? | if(ground_wait_flags(WF), |
274 | | ((debug_mode(on) -> stop_ms_timer_with_msg(Timer,component(ComponentNr)) ; true), |
275 | | l_ground_wait_flags(TWF,SatResult) % continue with other components |
276 | | ), |
277 | | ((debug_mode(on) -> print(unsatisfiable_component(ComponentNr)),nl, |
278 | | stop_ms_timer_with_msg(Timer,component(ComponentNr)) ; true), |
279 | | store_unsat_component_nr(ComponentNr,false), |
280 | | SatResult=false)). |
281 | | |
282 | | project_typed_vals([],_,[],[]). |
283 | | project_typed_vals([typedval(Val,Type,VarID,EnumWarning)|Rest],ComponentVars,In,Out) :- |
284 | ? | (member(VarID,ComponentVars) |
285 | | -> In=[typedval(Val,Type,VarID,EnumWarning)|In2], Out2=Out |
286 | | ; Out=[typedval(Val,Type,VarID,EnumWarning)|Out2], In2=In |
287 | | ), project_typed_vals(Rest,ComponentVars,In2,Out2). |
288 | | project_state([],_,[]). |
289 | | project_state([bind(VarID,Value)|Rest],ComponentVars,Out) :- |
290 | ? | (member(VarID,ComponentVars) |
291 | | -> Out=[bind(VarID,Value)|Out2] |
292 | | ; Out=Out2 |
293 | | ), project_state(Rest,ComponentVars,Out2). |
294 | | |
295 | | |
296 | | :- use_module(state_packing,[pack_value/2,unpack_value/2]). |
297 | | :- volatile det_solution_for_constant_packed/2. |
298 | | :- dynamic det_solution_for_constant_packed/2. |
299 | | assert_det_solution_for_constant(Var,Val) :- %print(sol(Var)),tools:print_memory_used_wo_gc,nl,nl, |
300 | | (value_too_large(Val) -> PVal = '$TOO_LARGE' ,debug_println(4,not_storing(Var)) |
301 | | ; pack_value(Val,PVal)), |
302 | | assert(det_solution_for_constant_packed(Var,PVal)). |
303 | | %,tools:print_memory_used_wo_gc,nl. |
304 | ? | det_solution_for_constant(Var,Val) :- det_solution_for_constant_packed(Var,PVal), |
305 | | (PVal = '$TOO_LARGE' |
306 | | -> add_message(no_det_value_stored_for_constant,'Values were found for some constants but not stored. Set ALLOW_INCOMPLETE_SETUP_CONSTANTS to TRUE to store constants found, e.g.: ',Var), |
307 | | fail |
308 | | ; unpack_value(PVal,Val) |
309 | | ). |
310 | | |
311 | | :- use_module(avl_tools,[avl_height_less_than/2]). |
312 | | value_too_large(avl_set(A)) :- |
313 | | preference(allow_incomplete_partial_setup_constants,false), %if true we always store the value |
314 | | \+ avl_height_less_than(A,7). |
315 | | % TO DO: it could be a small set but include large subsets ! |
316 | | |
317 | | :- use_module(tools_printing,[print_term_summary/1]). |
318 | | reset_observe_state :- retractall(det_solution_for_constant_packed(_,_)). |
319 | | observe_state(Env,WF,ComponentNr) :- |
320 | | get_wait_flag0(WF,WF0), get_wait_flag1(observe_state,WF,WF1), |
321 | | (preferences:get_preference(provide_trace_information,true) |
322 | | -> when((ground(Env);nonvar(WF0)),print_success(WF0,ComponentNr,Env,WF)) |
323 | | %% ,when(nonvar(WF1),(nl, print('Starting Phase 1'),nl, portray_waitflags(WF))) |
324 | | ; true), |
325 | | observe_state2(Env,WF0,WF1). |
326 | | %,when(nonvar(WF0),(print(wf0),nl,portray_waitflags(WF))), when(nonvar(WF1),(print(wf1),nl)). |
327 | | |
328 | | :- use_module(debug,[debug_format/3]). |
329 | | print_success(WF0,ComponentNr,_,_WF) :- nonvar(WF0),!, |
330 | | debug_format(19,'~n-->> WF0 for component ~w grounded.~n',[ComponentNr]). |
331 | | print_success(_,ComponentNr,Env,_WF) :- |
332 | | format('~n-->> SUCCESS; all constants valued in component ~w~n',[ComponentNr]), |
333 | | (debug_mode(on) |
334 | | -> findall(V,member(typedval(_,_,V,_),Env),Vars), |
335 | | statistics(walltime,[W,_]), format('-->> (walltime: ~w ms) : variables = ~w~n',[W,Vars]) |
336 | | ; true), |
337 | | %%,check_for_multiple_solutions(WF,ComponentNr) %% comment in to check for multiple solutions |
338 | | nl. |
339 | | |
340 | | observe_state2([],_,_). |
341 | | observe_state2([typedval(Val,_Type,VarID,_EnumWarning)|T],WF0,WF1) :- |
342 | | observe_variable(VarID,Val,WF0,WF1),observe_state2(T,WF0,WF1). |
343 | | %observe_state2([bind(Var,Val)|T],WF0) :- observe_variable(Var,Val,WF0), observe_state2(T,WF0). |
344 | | |
345 | | % print a warning message if we find multiple solutions *after* all constants have been valued |
346 | | %:- public check_for_multiple_solutions/2. |
347 | | %check_for_multiple_solutions(WF,ComponentNr) :- get_enumeration_finished_wait_flag(WF,EWF), |
348 | | % retractall(solution_found(ComponentNr,_)), |
349 | | % add_solution(EWF,ComponentNr). |
350 | | %:- volatile solution_found/2. |
351 | | %:- dynamic solution_found/2. |
352 | | %:- block add_solution(-,?). |
353 | | %add_solution(_,ComponentNr) :- retract(solution_found(ComponentNr,Nr)),!, |
354 | | % print('*** Multiple solutions found *after valuation* for component '), print(ComponentNr),nl, |
355 | | % N1 is Nr+1, |
356 | | % print('*** Solution: '),print(N1),nl, |
357 | | % assert(solution_found(ComponentNr,N1)). |
358 | | %add_solution(_,ComponentNr) :- % print(add_sol(ComponentNr)),nl, |
359 | | % assert(solution_found(ComponentNr,1)). |
360 | | |
361 | | observe_variable(Var,Val,WF0,_WF1) :- preferences:get_preference(provide_trace_information,false),!, |
362 | | observe_variable_no_trace(Var,Val,WF0). |
363 | | observe_variable(Var,Val,WF0,WF1) :- ground_value_check(Val,GrVal), |
364 | | when((nonvar(GrVal);nonvar(WF0)), |
365 | | (var(WF0) -> print('-->> '),print(Var), nl,print(' '),print_term_summary(value(Val)),print_walltime,nl, |
366 | | assert_det_solution_for_constant(Var,Val) |
367 | | ; print(' :?: '),print(Var),print(' '), print_term_summary(value(Val)), |
368 | | observe_variable1(Var,Val,WF1) |
369 | | ) |
370 | | ). |
371 | | :- use_module(kernel_tools,[ground_value/1,ground_value_check/2]). |
372 | | :- block observe_variable_no_trace(?,-,-). |
373 | | observe_variable_no_trace(Var,Val,WF0) :- nonvar(WF0),!, % important e.g. for test 1368 |
374 | | (ground_value(Val) -> assert_det_solution_for_constant(Var,Val) ; true). |
375 | | observe_variable_no_trace(Var,Val,WF0) :- ground_value_check(Val,GV), |
376 | | %print_term_summary(gr_val_check(Var,Val,GV)),nl, |
377 | | observe_variable_no_trace4(Var,GV,Val,WF0). |
378 | | :- block observe_variable_no_trace4(?,-,?,-). |
379 | | observe_variable_no_trace4(_,GV,_,_) :- var(GV),!. |
380 | | observe_variable_no_trace4(Var,_,Val,_) :- assert_det_solution_for_constant(Var,Val). % this could be expensive !? |
381 | | |
382 | | print_walltime :- statistics(walltime,[Tot,Delta]), |
383 | | (debug_mode(on) -> print(' '),tools:print_memory_used_wo_gc ; true), |
384 | | format(' ~w ms (Delta ~w ms) ',[Tot,Delta]). |
385 | | |
386 | | observe_variable1(Var,Val,WF1) :- ground_value_check(Val,GV), |
387 | | when((nonvar(GV);nonvar(WF1)), |
388 | | (nonvar(GV) -> print('--1-->> '),print(Var), nl,print(' '),print_term_summary(value(Val)), |
389 | | assert_det_solution_for_constant(Var,Val) |
390 | | ; print(' :?1?: '),print(Var),print(' '), print_term_summary(value(Val)) |
391 | | %% , when(ground(Val), (print('--ground-->> '),print(Var),print(' '), print_term_summary(value(Val)))) % comment in to see grounding |
392 | | %% , external_functions:observe_state([bind(Var,Val)]) % comment in to observe values |
393 | | %% , translate:print_bstate([bind(Var,Val)]),nl % comment in to print full value with CLP(FD) info |
394 | | ) ). |
395 | | |
396 | | /* |
397 | | comment back in for finer-grained observation and uncomment call above |
398 | | :- block observe_instantiation(-,?,?). |
399 | | observe_instantiation(X,Var,Val) :- |
400 | | print(bind(X)),nl,translate:print_bstate([bind(Var,Val)]),nl, (debug_mode(on) -> trace ; true), |
401 | | X =.. [_|Args], |
402 | | observe2(Args,Var,Val). |
403 | | |
404 | | observe2([],_,_). |
405 | | observe2([H|T],Var,Val) :- (var(H) -> observe_instantiation(H,Var,Val) |
406 | | ; H=.. [_|Args], observe2(Args,Var,Val)), |
407 | | observe2(T,Var,Val). |
408 | | */ |
409 | | |
410 | | % -------------------- |
411 | | |
412 | | |
413 | | construct_optimized_exists(Parameters,Body,Pred) :- |
414 | | construct_optimized_exists(Parameters,Body,Pred,true). |
415 | | |
416 | | % we could also partition inside b_interpreter ? |
417 | | construct_optimized_exists(Parameters,Body,Pred,Simplify) :- |
418 | | % we can actually do more: first project out all conjuncts which do not have any variables in common with Parameters |
419 | | % #x.(P(x) & Q) <=> #x.(P(x)) & Q |
420 | | % 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) |
421 | | get_texpr_ids(Parameters,PIDs), |
422 | | %print(constructing_optimized_exists(PIDs)),nl, |
423 | | predicate_components_with_restriction(Body,[],PIDs,Components), % should we use LocalVars instead of [] ? |
424 | | %length(Components,Len), print(nr_of_components_for_exists(Len,Components)),nl, |
425 | | conjunct_components(Components,Parameters,Pred,Simplify). |
426 | | % print('* EXISTS: '),translate:print_bexpr(Pred),nl. |
427 | | |
428 | | :- use_module(bsyntaxtree). |
429 | | conjunct_components(C,Parameters,Res,Simplify) :- conjunct_components2(C,Parameters,List,Simplify), |
430 | | conjunct_predicates(List,Res). |
431 | | |
432 | | conjunct_components2([],_Parameters,[],_). % :- (Parameters=[] -> true ; print(unused_existential_var(Parameters)),nl). |
433 | | conjunct_components2([component(Pred,ComponentVars)|T],Parameters,Res,Simplify) :- |
434 | | augment_ids(ComponentVars,CV), % translate atomic id names into b(identifier(... |
435 | | tools:list_intersection(CV,Parameters,ExistParas), |
436 | | %print(ord_inter(CV,Parameters,ExistParas)),nl, |
437 | | (Simplify=true |
438 | | -> create_and_simplify_exists(ExistParas,Pred,EP) |
439 | | ; create_unsimplified_exists(ExistParas,Pred,EP)), |
440 | | (EP=b(truth,pred,[]) % or should we allow _ for Info field ?? |
441 | | -> Res=TRes |
442 | | ; Res=[EP|TRes]), |
443 | | conjunct_components2(T,Parameters,TRes,Simplify). |
444 | | |
445 | | % translate a list of atomic ides into ids with the b/3 wrapper |
446 | | augment_ids([],[]). |
447 | | augment_ids([ID|T],[b(identifier(ID),_,_)|TT]) :- augment_ids(T,TT). |
448 | | |
449 | | extract_equalities(Parameters,Pred, ReducedParas,OutPred) :- |
450 | | extract_equalities2(Pred,Parameters,ReducedParas,NewPred,[],Subst), |
451 | | %sort(Subst,SortedSubst), |
452 | | %print(extracted(Subst)),nl, |
453 | | apply_subst(Subst,NewPred,OutPred). |
454 | | % apply equality inside expressions: note: this may duplicate expressions ! |
455 | | % However, it also works if the equalities contain parameters |
456 | | |
457 | | extract_equalities2(b(conjunct(A,B),pred,Info),Ids,RemIds,Res) --> !, |
458 | | {Res=b(conjunct(PA,PB),pred,Info)}, |
459 | | extract_equalities2(A, Ids,RemIds1,PA), |
460 | | extract_equalities2(B,RemIds1,RemIds,PB). |
461 | | extract_equalities2(b(equal(ID,E),pred,_Info),Ids,RemIds,NewPred,InSubst,OutSubst) :- |
462 | | same_id_is_member(ID,Ids,SID,RemIds), |
463 | | %\+ occurs_in_expr(SID,E), % not cyclic; we check it again after applyng InSubst to E below |
464 | | \+ in_subst_dom(SID,InSubst), % ensure we don't already have an equation for the same ID |
465 | | compose_with_subst(InSubst,SID,E,OutSubst), % we can compose with existing substitution without occurs-check problem |
466 | | always_well_defined_or_disprover_mode(E), % otherwise we may move evaluation of E forward ! |
467 | | !, |
468 | | NewPred=b(truth,pred,[]). |
469 | | extract_equalities2(X,Ids,Ids,X) --> []. |
470 | | |
471 | | % compose a new binding Var/Expr with existing substitution Subst; where Subst was not yet applied to Expr |
472 | | compose_with_subst(Subst,Var,Expr,[Var/NewExpr|ModSubst]) :- |
473 | | apply_subst(Subst,Expr,NewExpr), |
474 | | \+ occurs_in_expr(Var,NewExpr), % otherwise cyclic |
475 | | apply_binding_to_substitution(Subst,Var,NewExpr,ModSubst). |
476 | | apply_binding_to_substitution([],_,_,[]). |
477 | | apply_binding_to_substitution([TV/TE|T],Var,Expr,[TV/TE2|NT]) :- |
478 | | \+ occurs_in_expr(TV,Expr), % otherwise we get a cyclic substitution --> fail |
479 | | replace_id_by_expr(TE,Var,Expr,TE2), |
480 | | apply_binding_to_substitution(T,Var,Expr,NT). |
481 | | |
482 | | apply_subst([],X,X). |
483 | | apply_subst([Var/Expr|T],E,NewE) :- |
484 | | (replace_id_by_expr(E,Var,Expr,E2) % replace identifier Var by expression Expr |
485 | | -> %apply_to_tail(T,Var,Expr,NT), % apply binding to tail of substitution |
486 | | apply_subst(T,E2,NewE) |
487 | | ; add_internal_error('Call failed: ',apply_subst([Var/Expr|T],E,NewE)),NewE=E). |
488 | | |
489 | | |
490 | | in_subst_dom(X,[I/_|T]) :- (X=I -> true ; in_subst_dom(X,T)). |
491 | | |
492 | | same_id_is_member(X,[H|T],SID,Rest) :- |
493 | | (same_id(X,H,SID) -> Rest=T ; Rest=[H|TR],same_id_is_member(X,T,SID,TR)). |
494 | | |
495 | | % TO DO: investigate what is the exact difference with create_exists_opt |
496 | | create_and_simplify_exists(Paras,Pred,ResultingPred) :- |
497 | | % print(exists(Paras)),nl, translate:print_bexpr(Pred),nl, |
498 | | extract_equalities(Paras,Pred,NewParas,NewPred), |
499 | | % translate:print_bexpr(NewPred),nl, |
500 | | %print(create_and_simplify_exists2(NewParas,NewPred)),nl, |
501 | | create_and_simplify_exists2(NewParas,NewPred,ResultingPred). |
502 | | |
503 | | %:- use_module(b_interpreter_check,[arithmetic_op/4]). % TODO REFACTOR and move this and code below to separate module |
504 | | create_and_simplify_exists2([],Pred,R) :- !,R=Pred. |
505 | | % simplify #ID.(ID:E1 & ID:E2) <=> E1 /\ E2 /= {} , etc... now done in ast_cleanup |
506 | | % simplify #ID.(ID/:E) <=> E /= FullType also done in ast_cleanup |
507 | | % simplify #SID.(SID > Expr) <=> truth now done in ast_cleanup |
508 | | create_and_simplify_exists2(Parameters,Body,Res) :- create_unsimplified_exists(Parameters,Body,Res). |
509 | | % TO DO: treat nested exists |
510 | | |
511 | | |
512 | | |
513 | | :- use_module(b_ast_cleanup,[clean_up_pred/3]). |
514 | | :- use_module(bsyntaxtree,[add_texpr_info_if_new/3]). |
515 | | create_unsimplified_exists(Parameters,Body,Res) :- |
516 | | % print(create_unsimplified_exists(Parameters,Body)),nl, |
517 | | create_exists(Parameters,Body,Res1), |
518 | | add_texpr_info_if_new(Res1,removed_typing,Res2), % unconditionally add this info, avoid generating warnings in exists_body_warning, see test 625 |
519 | | clean_up_pred(Res2,[],Res). % also computes used_ids, |
520 | | % and performs some existential quantifier optimisations like replace_exists_by_not_empty |
521 | | % previously removed_typing was only added for disjuncts or implications: |
522 | | % (bsyntaxtree:is_a_disjunct_or_implication(Body,_,_,_) |
523 | | % -> add_texpr_infos(Res2,[removed_typing],Res3) % avoid generating warnings in exists_body_warning; see, e.g., test 625 |
524 | | % ; Res3=Res2), |