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
6 :- module(kernel_waitflags,
7 [init_wait_flags/1, init_wait_flags/2,
8 waitflag0_is_set/1,
9 get_wait_flag_infos/2, get_wait_flag_info/2, is_wait_flag_info/2,
10 add_wait_flag_info/3, portray_wait_flag_infos/1,
11 push_wait_flag_call_stack_info/3, opt_push_wait_flag_call_stack_info/3, debug_opt_push_wait_flag_call_stack_info/3,
12 opt_push_wait_flag_call_stack_quantifier_info/6,
13 copy_wait_flag_call_stack_info/3,
14 init_quantifier_wait_flag/6,
15 init_wait_flags_and_push_call_stack/3, init_wait_flags_and_push_call_stack/4,
16 init_wait_flags_with_call_stack/2,
17 add_call_stack_to_span/3,
18 add_error_wf/5, add_warning_wf/5, add_message_wf/5, add_internal_error_wf/5,
19 add_state_error_wf/5,
20 portray_call_stack/1, get_call_stack/2,
21 get_wait_flag/3, get_wait_flag/4,
22 get_bounded_wait_flag/4, get_bounded_priority/2,
23 block_get_wait_flag/4,
24 get_wait_flag0/2,
25 get_wait_flag1/2, get_wait_flag1/3, % deterministic wait flag
26 get_last_wait_flag/3,
27 get_idle_wait_flag/3,
28 get_binary_choice_wait_flag/3,
29 get_pow2_binary_choice_priority/2,
30 get_binary_choice_wait_flag_exp_backoff/3, get_binary_choice_wait_flag_exp_backoff/4,
31 %refresh_wait_flag/4,
32 add_fd_variable_for_labeling/3, add_fd_variable_for_labeling/2, add_fd_variables_for_labeling/2,
33 get_new_subsidiary_wait_flag/4,
34 update_waitflag/4,
35 ground_constraintprop_wait_flags/1,
36 check_is_wait_flag/1,
37 no_pending_waitflags/1,
38 create_inner_wait_flags/3, copy_wf01e_wait_flags/2,
39 copy_wfe_from_inner_if_necessary/2,
40 %copy_wf_start/2,
41 copy_wf_start/3,
42 copy_wf_finish/2,
43 copy_waitflag_store/2,
44
45 clone_wait_flags_from1/3, clone_wait_flags_from1_finish/3,
46 ground_wait_flag0/1,
47 %create_wdguarded_wait_flags/4,
48 get_large_finite_wait_flag/3,
49 get_enumeration_starting_wait_flag/3,
50 %get_enumeration_almost_finished_wait_flag/3,
51 get_enumeration_finished_wait_flag/2, % get_wfe
52 grd_ef/1, % ground enumeration finished waitflag
53 get_integer_enumeration_wait_flag/3,
54 ground_det_wait_flag/1, ground_wait_flag_to/2,
55 ground_wait_flags/1, ground_inner_wait_flags/1,
56 ground_inner_wait_flags_in_context/2,
57 start_attach_inner_abort_errors/2, re_attach_pending_inner_abort_errors/3,
58 deref_wf/2,
59
60 add_abort_error_span/5,
61 add_wd_error_span/4,
62 add_wd_error/3, add_wd_error_set_result/6,
63 pending_abort_error/1, pending_abort_error/4,
64 get_wait_flags_context_msg/2,
65 add_wd_error_span_now/4,
66 assert_must_abort_wf/2,
67
68 get_minimum_waitflag_prio/3,
69 portray_waitflags/1, quick_portray_waitflags/1, quick_portray_waitflags_store/1,
70 get_waitflags_phase/2,
71 find_waitflag_info/4,
72
73 integer_priority/1, large_finite_priority/1, integer_pow2_priority/1, last_priority/1,
74
75 my_get_kodkod_predicates/3, my_add_predicate_to_kodkod/3,
76 my_get_satsolver_predicates/3, my_add_predicate_to_satsolver/3,
77
78 get_wf_dynamic_info/3, put_wf_dynamic_info/3, % these infos are stored together with the Kodkod preds
79 % they can always be added and do not require updating the WF term like add_wait_flag_info does
80 % add_wait_flag_info are static/lexical scoping infos; these are dynamic infos
81
82 set_silent/1]).
83 /* File: kernel_waitflags.pl */
84 /* Created: 17/3/06 by Michael Leuschel */
85
86 :- meta_predicate assert_must_abort_wf(0,*).
87 %:- meta_predicate assert_must_abort2_wf(0,-).
88
89 /*
90 Phases of the ProB Kernel:
91
92 -> all Waitflags unbound
93
94 * Phase 0: propagation of completely known ground values in a deterministic fashion
95
96 -> WF0 is bound (first to s(VAR) and then to s(0))
97 when WF0 is not ground one knows that the WF0 phase is still ongoing
98 (relevant for getting 1.0 waitflag)
99
100 * Phase 1: deterministic propagation (not necessarily of completely known full values)
101
102 -> WF1 is bound (1.0)
103
104 * Phase 2: boolean propagation (e.g., P or Q will now try P or Q)
105
106 -> WF2 is bound
107
108 * Phase 3: non-deterministic propagation (e.g, x: {1,2,3})
109
110 -> Enumeration Starting WF is bound
111
112 * Enumeration Phase: (later to be split into enumeration of finite and infinite types (e.g., integer)
113
114 -> Enumeration Finished Waitflag bound
115
116 * Error Generation Phase: errors for, e.g., division by zero, f(x) with x outside domain of f,... are generated
117 * This phase should not create choice points and should not detect failure
118 (e.g., in the
119 case of negated existential quantifiers the Enumeration Finished Waitflag will be set outside of delay_not)
120
121
122 We now distinguish
123 - Enumeration Wait Flags for Decision Variables with estimated enumeration domain size as priority
124 - Binary Choice Point Wait Flags (stemming e.g. from disjunctions)
125
126 Note: all floats like 1.0, 1.5, 2.0 ... are dealt with before all integers (even 1) !
127
128 There are three ways to create a waitflag store:
129 - init_wait_flags : to create a fresh empty store
130 - create_inner_wait_flags: the inner WFE should not be instantiated and will be instantiated from the outside
131 useful for a nested quantifier where well-definedness errors should only be raised when the outer quantifier
132 is set and where you want to enumerate the inner quantifier in isolation (e.g., for exists to be able to use the Prolog cut)
133 - copy_wf_start to create a temporary copy with WF0 unset, which will be unified with copy_wf_finish
134 useful for adding a new predicate to the constraint solver and ensure that WF0 is not set until
135 predicate has been fully interpreted, to avoid enumerations/inefficient computations (e.g., there
136 could be an obvious inconsistency at the end of the predicate)
137 */
138
139 :- use_module(error_manager).
140 :- use_module(self_check).
141 :- use_module(typechecker).
142 :- use_module(library(clpfd),[fd_size/2, fd_degree/2, (in/2)]).
143 :- use_module(tools).
144 :- use_module(tools_portability, [exists_source/1]).
145 :- use_module(covsrc(coverage_tools_annotations),['$NOT_COVERED'/1]).
146 :- use_module(preferences,[preference/2, get_preference/2]).
147 :- use_module(debug,[debug_format/3]).
148
149 :- use_module(module_information,[module_info/2]).
150 :- module_info(group,kernel).
151 :- module_info(description,'This module manages the various choice points and enumerators of ProB, by maintaining the kernel Waitflags store.').
152
153 :- type wait_flag +--> (var ; wfx(simple,mutable,simple,list(any)) ; no_wf_available).
154 % a mutable either contains:
155 % wfm_store(AVLWaitflagHeap,NewFDVARS,KodSatPredicateList)
156 % wfm_ref(Mutable) a reference pointing to another Mutable which should be used to store waitflags
157
158 :- use_module(library(lists),[is_list/1, delete/3, last/2]).
159 :- use_module(library(avl)).
160
161 % -------------- ATTRIBUTES ------------------
162
163 % Portable attributed variable handling.
164 % Use SICStus-style library(atts) and verify_attributes/3 if available,
165 % otherwise the SWI/hProlog-style attr builtins and attr_unify_hook/2.
166 :- if(\+ exists_source(library(atts))).
167
168
169 is_wf_abort_pending(Var) :- get_attr(Var,kernel_waitflags,wf_abort_pending).
170 is_not_wf_abort_pending(Var) :- \+ get_attr(Var,kernel_waitflags,wf_abort_pending).
171 put_wf_abort_pending(Var) :- put_attr(Var,kernel_waitflags,wf_abort_pending).
172
173 attr_unify_hook(wf_abort_pending, Value) :-
174 % we are unifying the EWF enumeration finished waitflag, not the store
175 (nonvar(Value) -> true % EWF bound, enumeration finished
176 ; get_attr(Value,kernel_waitflags,wf_abort_pending) -> true % other EWF Value already has same attribute
177 ; put_attr(Value,kernel_waitflags,wf_abort_pending)
178 ).
179
180 :- else.
181
182 :- use_module(library(atts)).
183 :- attribute %wf_store/1,wf_fdvars/1, wf_kodkod/2, wf_satsolver/2, % now stored in mutable
184 wf_abort_pending/0.
185
186 is_wf_abort_pending(Var) :- get_atts(Var,+wf_abort_pending).
187 is_not_wf_abort_pending(Var) :- get_atts(Var,-wf_abort_pending).
188 put_wf_abort_pending(Var) :- put_atts(Var,+wf_abort_pending).
189
190 % verify_attributes is called whenever a variable Var that might have attributes is about to be bound to Value (it might have none).
191 % verify(VariableBeforeUnification, ValueWithWhichVariableUnifies, GoalWhichSICStusShouldCallAfterUnif)
192 verify_attributes(Var, Value, [] ) :- get_atts(Var,+wf_abort_pending),!,
193 % we are unifying the EWF enumeration finished waitflag, not the store
194 (nonvar(Value) -> true % EWF bound, enumeration finished
195 ; get_atts(Value,+wf_abort_pending) -> true % other EWF Value already has same attribute
196 ; put_atts(Value,+wf_abort_pending)
197 ).
198 verify_attributes(Var, Value, [] ) :-
199 (nonvar(Value) -> print('Trying to unify WFE flags'),nl
200 ; print(verify_attributes(Var,Value)),nl).
201 % The SICStus documentation is not entirely clear: it seems we only have to copy attributes from Var to Value, not the other way around
202
203 :- endif.
204
205 % -------------- MUTABLES ------------------
206
207 % Should we use several mutables?
208 put_mutable_other_attr(Store,wf_preds(ID,Type,PredList)) :- !,
209 get_mutable_store_for_update(Store,S,FD,KodSat,StoreToUpdate),
210 update_preds(KodSat,ID,Type,PredList,KodSat2),
211 update_mutable(wfm_store(S,FD,KodSat2),StoreToUpdate).
212 put_mutable_other_attr(Store,wf_info(ID,Val)) :- !, % Store other infos in the wf_preds list
213 get_mutable_store_for_update(Store,S,FD,KodSat,StoreToUpdate),
214 (select(wf_info(ID,_),KodSat,Rest) -> true ; Rest=KodSat),
215 update_mutable(wfm_store(S,FD,[wf_info(ID,Val)|Rest]),StoreToUpdate).
216 put_mutable_other_attr(Store,New) :-
217 add_internal_error('Uncovered put_mutable_other_attr',put_mutable_other_attr(Store,New)).
218
219 % update AVL WF heap in WF Store
220 % faster version of put_mutable_attr(Store,wf_store(NewHeap))
221 put_mutable_wf_store_attr(Store,NewHeap) :-
222 get_mutable_store_for_update(Store,_,FD,KodSat,StoreToUpdate),
223 update_mutable(wfm_store(NewHeap,FD,KodSat),StoreToUpdate).
224
225 % update FD Variables List in WF Store
226 % faster version of put_mutable_attr(Store,wf_fdvars(NewFDVARS))
227 put_mutable_wf_fdvars_attr(Store,NewFDVARS) :-
228 get_mutable_store_for_update(Store,Heap,_,KodSat,StoreToUpdate),
229 update_mutable(wfm_store(Heap,NewFDVARS,KodSat),StoreToUpdate).
230
231 % TO DO: improve my_get_wf_store_fdvars_atts / put_mutable_attr pairs of calls to make them more efficient
232
233 % update Kodkod or Satsolver predicates attached in store:
234 update_preds([],ID,Type,PredList,[wf_preds(ID,Type,PredList)]).
235 update_preds([wf_preds(ID,Type,_)|T],ID,Type,PredList,Res) :- !,
236 Res = [wf_preds(ID,Type,PredList)|T].
237 update_preds([H|T],ID,Type,PredList,[H|RT]) :-
238 update_preds(T,ID,Type,PredList,RT).
239
240 % a utility predicate that always returns a mutable with wfm attribute
241 get_mutable_store_for_update(Store, S,FD,KodSat, MutableToUpdate) :- mutable(Store),!,
242 get_mutable(MutableInfo,Store),
243 (get_mutable_infos__for_update_aux(MutableInfo,S,FD,KodSat,Store,MutableToUpdate) -> true
244 ; add_internal_error('get_mutable_infos__for_update_aux failed for:',Store),fail).
245 get_mutable_store_for_update(Store, S,[],[], Res) :- var(Store),!, Res=Store,
246 empty_avl(S),
247 create_mutable(wfm_store(S,[],[]),Store).
248 get_mutable_store_for_update(Store, _,_,_, _) :-
249 add_internal_error('get_mutable_store_for_update failed for:',Store),fail.
250
251 get_mutable_infos__for_update_aux(wfm_store(S,FD,KodSat),S,FD,KodSat,Store,Store).
252 get_mutable_infos__for_update_aux(wfm_ref(OuterStore),S,FD,KodSat,_,MutableToUpdate) :-
253 get_mutable_store_for_update(OuterStore,S,FD,KodSat,MutableToUpdate).
254
255 % follow links of wfm_ref to get access to proper mutable store to update
256 deref_store(Store,MutableToUpdate) :- mutable(Store), !,
257 (Store=wfm_ref(Store2) -> deref_store(Store2,MutableToUpdate)
258 ; MutableToUpdate=Store).
259 deref_store(Store,MutableToUpdate) :- var(Store),!, MutableToUpdate=Store,
260 empty_avl(S),
261 create_mutable(wfm_store(S,[],[]),Store).
262 deref_store(Store, _) :-
263 add_internal_error('deref_store failed for:',Store),fail.
264
265 % get the associated infos for a mutable store; follow chain of wfm_ref's:
266 get_mutable_infos(S,FD,KodSat,Store) :- mutable(Store),
267 get_mutable(MutableInfo,Store),
268 get_mutable_infos_aux(MutableInfo,S,FD,KodSat).
269 get_mutable_infos_aux(wfm_store(S,FD,KodSat),S,FD,KodSat).
270 get_mutable_infos_aux(wfm_ref(OuterStore),S,FD,KodSat) :- get_mutable_infos(S,FD,KodSat,OuterStore).
271
272 my_get_wf_store_att(Store,Heap) :- get_mutable_infos(S,_,_,Store),!,
273 Heap=S.
274 my_get_wf_store_att(_,E) :- empty_avl(E).
275
276 my_get_wf_preds_att(Store,ID,Type,PredList) :- get_mutable_infos(_,_,KodSat,Store),!,
277 (member(wf_preds(ID,Type,R),KodSat) -> PredList=R).
278
279 my_get_wf_info_att(Store,ID,Value) :- get_mutable_infos(_,_,KodSat,Store),!,
280 (member(wf_info(ID,V),KodSat) -> Value=V).
281
282 my_get_all_wf_info_atts(Store,List) :- get_mutable_infos(_,_,KodSat,Store),!,
283 findall(wf_info(ID,V),member(wf_info(ID,V),KodSat),List).
284 my_get_all_wf_info_atts(_,List) :-
285 %init_wait_flags/1 will not initialise a mutable and get_mutable_infos will fail
286 List=[].
287
288 my_get_fdvars_att(Store,FDList) :- get_mutable_infos(_,FD,_,Store),!,
289 FDList=FD.
290 my_get_fdvars_att(_,[]).
291
292 my_get_wf_store_fdvars_atts(Store,Heap,FDList) :- get_mutable_infos(S,FD,_,Store),!,
293 Heap=S, FDList=FD.
294 my_get_wf_store_fdvars_atts(_,E,[]) :- empty_avl(E).
295
296 % Mutable store should now point to another mutable store (OuterStore)
297 % ensures that calls which add waitflags to Store now get-redirected to OuterStore
298 set_mutable_ref(Store,OuterStore) :- mutable(Store),
299 !,
300 update_mutable(wfm_ref(OuterStore),Store).
301 set_mutable_ref(Store,OuterStore) :- % not instantiated yet, we can simply unify
302 Store=OuterStore.
303
304
305 % -------------------------
306
307 % the Call must succeed and generate one abort_error
308 assert_must_abort_wf(M:Call,WF) :- assert_must_succeed_any(M:(kernel_waitflags:assert_must_abort2_wf(M:Call,WF))).
309
310 :- use_module(tools_printing,[format_with_colour_nl/4]).
311 assert_must_abort2_wf(_,_) :-
312 get_error(well_definedness_error,M),
313 add_internal_error('Abort error prior to call in assert_must_abort: ',M),fail.
314 assert_must_abort2_wf(Call,WF) :-
315 (real_error_occurred -> RE=true ; RE=false),
316 init_wait_flags(WF,[assert_must_abort2_wf]),
317 ? call(Call),
318 (ground_wait_flags(WF)
319 -> add_internal_error('Call did not fail after grounding WF: ',assert_must_abort2_wf(Call,WF)),fail
320 ; get_error(well_definedness_error,_), % we have 1 abort_error
321 format_with_colour_nl(user_output,[blue],'Got expected well-definedness error',[]),
322 (RE=false -> reset_real_error_occurred ; true)
323 ).
324
325
326 :- assert_must_succeed(( kernel_waitflags:init_wait_flags(WF), kernel_waitflags:check_is_wait_flag(WF) )).
327
328 check_is_wait_flag(WFX) :- var(WFX),!,
329 add_internal_error('Variable as waitflag: ',check_is_wait_flag(WFX)).
330 check_is_wait_flag(no_wf_available) :- !.
331 check_is_wait_flag(WFX) :-
332 WFX = wfx(WF0,Store,WFE,Infos)
333 -> (get_mutable_infos(_,_,_,Store)
334 -> true
335 ; print('WF does not yet contain heap: '), print(WFX),nl),
336 %add_internal_error('WF does not contain heap: ',check_is_wait_flag(WFX)))
337 (var(WF0) -> true ; WF0 = s(WF00), \+compound(WF00) -> true
338 ; compound(WF0) -> add_internal_error('WF0 is compound: ',WF0) ; true
339 ),
340 (compound(WFE) -> add_internal_error('WFE is compound: ',WFE) ; true),
341 (nonvar(Infos),is_list(Infos) -> true ; add_internal_error('WF Infos not list: ',Infos))
342 ; add_internal_error('Illegal WF Format: ',check_is_wait_flag(WFX)).
343
344
345 % initialise a new waitflag store
346 init_wait_flags(WF,Info) :-
347 (nonvar(Info) -> true ; add_internal_error('Illegal WF Format: ',init_wait_flags(WF,Info))),
348 init_debug_wait_flag_info(Info,Infos),
349 WF=wfx(_,_Store,_,Infos).
350 init_wait_flags(wfx(_,_Store,_,[])). % no_expansion_context_available
351 init_wait_flags_with_infos(wfx(_,_Store,_,Infos),Infos). % infos copied as is without checking
352 init_wait_flags_with_sd_infos(wfx(_,Store,_,StaticInfos),StaticInfos,DynamicInfos) :-
353 init_wait_flags_store_with_dynamic_infos(Store,DynamicInfos).
354
355 %init_wait_flags(wfx(_,Store,_,[])) :- init_wait_flags_store(Store).
356 % we no longer do this because of performance, (see, e.g., LotsOfInvariants.mch) :
357 init_wait_flags_store(Store) :- empty_avl(Heap),
358 create_mutable(wfm_store(Heap,[],[]),Store).
359 init_wait_flags_store_with_dynamic_infos(Store,KodkodDynInfos) :- empty_avl(Heap),
360 create_mutable(wfm_store(Heap,[],KodkodDynInfos),Store).
361 %init_wait_flags_store(Store) :-
362 % empty_avl(Heap),
363 % put_atts(Store,wf_store(Heap)),
364 % put_atts(Store,wf_fdvars([])).
365
366
367 :- assert_must_succeed(( kernel_waitflags:init_wait_flags(WF),
368 kernel_waitflags:ground_wait_flag0(WF), kernel_waitflags:waitflag0_is_set(WF) )).
369 :- assert_must_fail(( kernel_waitflags:init_wait_flags(WF), kernel_waitflags:waitflag0_is_set(WF) )).
370 waitflag0_is_set(wfx(WF0,_Store,_EF,_INFOS)) :- ground(WF0).
371 waitflag0_is_set(no_wf_available).
372
373 get_new_subsidiary_wait_flag(OldWF,Info,WFX,NewWF) :-
374 (ground(OldWF) /* then we have created a choice point with the old WF: double new WF prio */
375 -> double_prio(OldWF,NewPrio), get_wait_flag(NewPrio,Info,WFX,NewWF)
376 ; NewWF = OldWF
377 ).
378
379 double_prio(OldPrio,NewPrio) :- number(OldPrio),!, NewPrio is OldPrio*2.
380 double_prio(s(_),2) :- !. % for things like s(0) created for WF0
381 double_prio(Old,New) :- add_internal_error('Unknown priority: ',double_prio(Old,New)), New=2.
382
383 % not used at the moment:
384 %refresh_wait_flag(OldWF,Info,WFX,NewWF) :-
385 % (ground(OldWF) /* then we have created a choice point with the old WF: double new WF prio */
386 % -> get_wait_flag(OldWF,Info,WFX,NewWF)
387 % ; NewWF = OldWF
388 % ).
389
390 :- volatile silent/0.
391 :- dynamic silent/0.
392 set_silent(true) :- !,(silent -> true ; assertz(silent)).
393 set_silent(false) :- retractall(silent).
394 %waitflag_not_init :- silent -> true ; print('waitflag-store not initialised'),nl, '$NOT_COVERED'('This should not happen').
395
396 :- use_module(eventhandling,[register_event_listener/3]).
397 :- register_event_listener(start_unit_tests,set_silent(true),'Allow wf not to be set up without printing a warning').
398 :- register_event_listener(stop_unit_tests, set_silent(false), 'Printing wf warnings again').
399
400 :- use_module(library(lists),[maplist/2]).
401 add_fd_variables_for_labeling(Vars,WF) :- WF==no_wf_available,!,
402 add_internal_error('Cannot add FDVars to waitflag store: ',Vars).
403 add_fd_variables_for_labeling(Vars,WF) :-
404 WF=wfx(_,Store,_EnumFinished,_INFOS),
405 !,
406 my_get_fdvars_att(Store,FDVARS),
407 l_add_fd_var_to_FDVARS(Vars,FDVARS,NewFDVARS),
408 put_mutable_wf_fdvars_attr(Store,NewFDVARS).
409 add_fd_variables_for_labeling(Vars,WF) :-
410 add_internal_error('Illegal waitflag store: ',add_fd_variables_for_labeling(Vars,WF)).
411
412 l_add_fd_var_to_FDVARS([],Acc,Acc).
413 l_add_fd_var_to_FDVARS([Var|VT],FDVARS,NewFDVARS) :-
414 (nonvar(Var) -> F2=FDVARS; add_fd_var_to_FDVARS(Var,FDVARS,F2)),
415 l_add_fd_var_to_FDVARS(VT,F2,NewFDVARS).
416
417 % adds a CLP(FD) variable with given domain Size, will be enumerated by labeling (even if clpfd_solver preference is false !)
418 % Size could be computed by fd_size(FDVariable,Size)
419 add_fd_variable_for_labeling(FDVariable,WF) :-
420 add_fd_variable_for_labeling_aux(FDVariable,WF).
421 add_fd_variable_for_labeling(FDVariable,Size,WF) :- Size = not_used_anymore,
422 add_fd_variable_for_labeling_aux(FDVariable,WF).
423
424
425 add_fd_variable_for_labeling_aux(FDVariable,_WF) :- nonvar(FDVariable),!.
426 add_fd_variable_for_labeling_aux(FDVariable,WF) :-
427 % otherwise: store the FDVariable in the separate list of FD Variables (all mixed together)
428 WF=wfx(_,Store,_EnumFinished,_),
429 my_get_fdvars_att(Store,FDVARS),
430 add_fd_var_to_FDVARS(FDVariable,FDVARS,NewFDVARS),
431 %% fd_size(FDVariable,Size),print(added(FDVariable,Size,NewFDVARS,old(FDVARS))),nl,
432 %% print(added_fd_variable(FDVariable,_Size,NewFDVARS)),nl,portray_waitflags_store(Store),nl,nl,%%
433 put_mutable_wf_fdvars_attr(Store,NewFDVARS).
434
435 add_fd_var_to_FDVARS(FDVariable,FDVARS,NewFDVARS) :-
436 %print_term_summary(add_fd_var_to_FDVARS(FDVariable)),nl,
437 %(fd_size(FDVariable,Sz), Sz=sup -> trace ; true),
438 (FDVARS=[HH|_],HH==FDVariable -> NewFDVARS = FDVARS % variable already in list [cheap check at front]
439 ; NewFDVARS = [FDVariable|FDVARS]). %% this adds new variables at front; will be given priority over older ones
440 %% add_fd_var(FDVARS,FDVariable,NewFDVARS), %% this adds new variables at the end and does more thorough duplicate check
441
442
443 % a bit like append: but cleans up list: removes numbers + checks if var already in list
444 % runtimes for tests: 349 stays at 220ms, test 1088 4660 -> 5040ms
445 %add_fd_var([],Var,[Var]).
446 %add_fd_var([V|T],Var,Res) :-
447 % (V==Var -> Res = [V|T] %,print(dup(V)),nl,
448 % ; nonvar(V) -> add_fd_var(T,Var,Res) %,print(nonvar(V)),nl
449 % ; Res = [V|RT], add_fd_var(T,Var,RT)).
450
451
452 :- use_module(library(random),[random_select/3]).
453 % reverse the list at each step; alternating taking from end and front; makes no sense with randomise_enumeration_order
454 %my_get_next_fdvar_to_enumerate_rev(FDVARS,NextFDVar,RemainingFDVARS) :- lists:reverse(FDVARS,RevFDVARS),
455 % my_get_next_fdvar_to_enumerate(RevFDVARS,NextFDVar,RemainingFDVARS).
456
457 my_get_next_fdvar_to_enumerate([],_NextFDVar,_RemainingFDVARS) :- !,fail.
458 my_get_next_fdvar_to_enumerate([V1|FDVARS],NextFDVar,RemainingFDVARS) :-
459 nonvar(V1),
460 !, % skip over non-variables (numbers); clpfd_get_next_variable_to_label does not delete variable from list and may crash with leading non-variable terms !
461 my_get_next_fdvar_to_enumerate(FDVARS,NextFDVar,RemainingFDVARS).
462 my_get_next_fdvar_to_enumerate(FDVARS,NextFDVar,RemainingFDVARS) :-
463 preferences:preference(randomise_enumeration_order,true),
464 !,
465 get_min_fd_size_elements(FDVARS,MinFDVars),
466 random_select(NextFDVar,MinFDVars,_),
467 %print(random_enum(NextFDVar,FDVARS,MinFDVars)),nl,
468 RemainingFDVARS=FDVARS. % still contains variable; but no problem as it will be discarded later
469 my_get_next_fdvar_to_enumerate(FDVARS,NextFDVar,RemainingFDVARS) :-
470 %clpfd_interface:clpfd_get_next_variable_to_label_ffc(FDVARS,NextFDVar,RemainingFDVARS).
471 clpfd_interface:clpfd_get_next_variable_to_label(FDVARS,NextFDVar),
472 % print(enumerating(NextFDVar,FDVARS)),nl, maplist(tools_printing:print_arg,FDVARS),nl,
473 RemainingFDVARS=FDVARS.
474 % ((FDVARS=[H|T],H==NextFDVar) -> RemainingFDVARS=T ; RemainingFDVARS=FDVARS).% does not seem to buy any speed
475
476 get_min_fd_size_elements([V1|FDVARS],MinFDVars) :- clpfd_size(V1,Size),
477 get_min_aux(FDVARS,Size,[V1],MinFDVars).
478
479 get_min_aux([],_,MinFDVars,MinFDVars).
480 get_min_aux([V1|FDVARS],Size,MAcc,MinFDVars) :- number(V1),!,
481 get_min_aux(FDVARS,Size,MAcc,MinFDVars).
482 get_min_aux([V1|FDVARS],Size,MAcc,MinFDVars) :-
483 clpfd_size(V1,Size1),
484 (lt_size(Size1,Size)
485 -> get_min_aux(FDVARS,Size1,[V1],MinFDVars)
486 ; Size1=Size -> get_min_aux(FDVARS,Size,[V1|MAcc],MinFDVars)
487 ; get_min_aux(FDVARS,Size,MAcc,MinFDVars)
488 ).
489
490 lt_size(X,Y) :- number(X),(Y=sup -> true ; X<Y).
491
492 % -------------
493
494 % using this is relevant for e.g. tests 415, 416, 1096 : to give variables without frozen goals a lower priority
495 % TO DO: we could filter out those before we call clpfd_get_next_variable_to_label !?
496 fd_priority_leq_limit(FDVAR,Prio,Limit) :-
497 clpfd_size(FDVAR,Size),
498 number(Size), % not =sup or =inf
499 geq_limit(Limit,Size), % the calculation below will only increase the Size
500 (Size < 2 -> Prio = Size
501 ; geq_limit(Limit,Size*4) -> Prio = Size % avoid calling frozen and fd_degree, Priority only used for warnings and bisect decisions
502 ; (enumeration_only_fdvar(FDVAR) -> Prio is Size*4, Prio =< Limit
503 ; Prio = Size)
504 ).
505
506 gt_limit(inf,_) :- !.
507 gt_limit(inf_overflow,_) :- !.
508 gt_limit(sup,_) :- !.
509 gt_limit(X,Limit) :- X > Limit.
510
511 geq_limit(inf,_) :- !.
512 geq_limit(inf_overflow,_) :- !.
513 geq_limit(sup,_) :- !.
514 geq_limit(X,Limit) :- X >= Limit.
515
516
517
518 % -------------
519
520
521 enumeration_only_fdvar(FDVAR) :- var(FDVAR),fd_degree(FDVAR,D),!,
522 D=0,
523 frozen(FDVAR,Goal), % print(frozen(FDVAR,D,Goal)),nl,
524 enum_only_frozen_goal(Goal,FDVAR).
525 enumeration_only_fdvar(_).
526
527 % TO DO: maybe use enumeration_only_goal in b_enumerate
528 enum_only_frozen_goal((A,B),Var) :- !, enum_only_frozen_goal(A,Var), enum_only_frozen_goal(B,Var).
529 enum_only_frozen_goal(true,_).
530 enum_only_frozen_goal(Module:Call,Var) :- enum_only_frozen_goal_m(Module,Call,Var).
531
532 enum_only_frozen_goal_m(clpfd,_,_) :- !.
533 enum_only_frozen_goal_m(kernel_objects,G,V) :- !, enum_only_frozen_goal_k_obj(G,V).
534 enum_only_frozen_goal_m(b_interpreter_components,observe_variable_block(_,_,_,_,_),_).
535 enum_only_frozen_goal_m(b_interpreter_components,observe_variable1_block(_,_,_,_),_).
536 enum_only_frozen_goal_m(custom_explicit_sets,block_copy_waitflag_store(_,_,_,_,_),_).
537
538 enum_only_frozen_goal_k_obj(safe_less_than_equal(_,X,Y),_) :- (number(X);number(Y)), !.
539 enum_only_frozen_goal_k_obj(call_enumerate_int(X,_,_,_),Var) :- Var==X,!.
540 enum_only_frozen_goal_k_obj(enumerate_int_wf(X,_,_,_,_),Var) :- Var==X,!.
541 enum_only_frozen_goal_k_obj(true,_).
542
543
544 % get a wait-flag that will be triggered first next time;
545 % can be used to ensure that all pending co-routines complete
546 get_idle_wait_flag(Info,wfx(WF0,Store,EnumFinished,_),LWF) :- !,
547 (var(WF0) -> LWF=WF0
548 ; WF0=s(WF00), var(WF00) -> LWF=WF00
549 ; nonvar(EnumFinished) -> LWF=1 % waitflag store already grounded to completion; nobody may drive it anymore
550 ; get_waitflag_from_store(0.9,Info,Store,LWF)
551 ).
552 get_idle_wait_flag(_Info,no_wf_available,1).
553
554
555 get_wait_flag(Prio,Store,WF) :- get_wait_flag(Prio,'??',Store,WF).
556 get_wait_flag(Prio,_Info,wfx(WF0,_Store,EnumFinished,_),WF) :- (Prio=0 ; ground(EnumFinished)),
557 !, % if EnumFinished is ground nothing will drive the Waitflag store anymore
558 % WF0 can be set to a variable by clone_wait_flags_from1
559 WF=WF0.
560 get_wait_flag(1.0,Info,wfx(WF0,Store,_EnumFinished,_),WF) :-
561 % WF for deterministic computations, not guaranteed to generate efficient representations
562 % (those are triggered in WF0 phase)
563 !,
564 %used to b: (var(WF0) -> get_waitflag_from_store(1.0,Info,Store,WF) ; WF=1).
565 (ground(WF0) % if WF0 is ground the WF0 phase is completed fully;
566 -> WF=1 % we can return this waitflag immediately;
567 % good idea also if we are already in the later stages of propagation
568 % so as not to delay the attached deterministic propagations (see test 383, SudokuHexAsConstant.mch)
569 ; get_waitflag_from_store(1.0,Info,Store,WF)).
570 get_wait_flag(Prio,Info,wfx(_,Store,EnumFinished,_),WF) :- !,
571 (ground(EnumFinished) -> WF=Prio /* enumeration has finished: return a ground WF */
572 ; get_waitflag_from_store(Prio,Info,Store,WF)).
573 get_wait_flag(Prio,Info,Store,WF) :- check_is_wait_flag(Store),
574 (Store=no_wf_available -> WF=Prio ;
575 Store=none -> print(get_wait_flag_deprecated(Prio,Info,Store,WF)),nl, WF=Prio ;
576 add_internal_error('Illegal call: ',get_wait_flag(Prio,Info,Store,WF))).
577
578 :- use_module(kernel_card_arithmetic,[is_inf_or_overflow_card/1]).
579 % get Waitflag with Priority Prio, additional information Info from Store
580 get_waitflag_from_store(Prio,Info,Store,WF) :-
581 % print(get_waitflag_from_store(Prio,Info,Store,WF)),nl,
582 (is_inf_or_overflow_card(Prio) -> integer_priority(RealPrio)
583 ; RealPrio=Prio),
584 my_get_wf_store_att(Store,Heap),
585 (avl_fetch(RealPrio,Heap,wf(WFs,_OldInfo)) %,print(fetch(RealPrio,WFs,_OldInfo)),nl
586 -> ((RealPrio < 2 %is_finite_priority(RealPrio)
587 ; Info = allow_reuse(_))
588 %RealPrio < 100000 % TO DO: investigate performance if reduce the threshold
589 % here we re-use the waitflag instead of storing a new one
590 -> (var(WFs) -> WF1 = WFs %, print(reusing_wf(RealPrio,WF1,Info)),nl
591 ; WFs = [WF1|_]-_ -> true % add_wf has constructed a difference list
592 ; print(wf_already_grounded(Prio,Info,WFs)),nl,
593 WFs = WF1
594 )
595 ; push_waitflag(WFs,WF1,WFs2) ->
596 % poses problems for 1003, possibly 1194; keep WFs as a FIFO stack to have localised enumeration
597 %(RealPrio<100000 -> test_runner:inc_test_target_coverage ; true),
598 avl_store(RealPrio,Heap,wf(WFs2,Info),NewHeap),
599 put_mutable_wf_store_attr(Store,NewHeap)
600 ; add_internal_error('Pushing waitflag failed:',RealPrio:WFs)
601 )
602 ; avl_store(RealPrio,Heap,wf(WF1,Info),NewHeap), % print(storing_fresh_wf(RealPrio,WF1,Info)),nl,
603 put_mutable_wf_store_attr(Store,NewHeap) % put_atts seems to be expensive
604 ),!,
605 WF=WF1.
606 get_waitflag_from_store(Prio,Info,Store,WF) :-
607 add_internal_error('Error getting Waitflag: ', get_waitflag_from_store(Prio,Info,Store,WF)),fail.
608
609 % ----------------
610
611 % utilities for managing difference lists of waitflag variables for a particular priority:
612
613 % for each priority we store wf(WFQueue,Info)
614 % WFQueue is either a free variable (aka waitflag), or a difference list of free variables (waitflags)
615
616 % push new waitflag NextWF onto an existing WF list for a priority
617 push_waitflag(WFs,NextWF,NewWFs) :- var(WFs),!, NewWFs = [WFs,NextWF|TAIL]-TAIL. % create difference list
618 push_waitflag(Head-TAIL,NextWF,NewWFs) :- !, TAIL = [NextWF|NewTAIL], NewWFs = Head-NewTAIL.
619 push_waitflag(WFs,_,WFs) :- add_internal_error('Illegal waitflag list:',WFs).
620
621 % pop the next waitflag NextWF from a list of waitflags associated with some priority
622 pop_waitflag(WFs,NextWF,Tail) :- var(WFs),!, NextWF=WFs,Tail=[].
623 pop_waitflag(Head-Tail,NextWF,NextTail) :- Head \== Tail, % should always succeed
624 !,
625 Head = [NextWF|NextHead],
626 (NextHead==Tail -> NextTail=[] ; NextTail = NextHead-Tail).
627 pop_waitflag(WFs,_,_) :- add_internal_error('Illegal waitflag list, cannot pop:',WFs),fail.
628
629 % merge_waitflag_queues(InnerWF,OuterWF,MergedWF)
630 merge_waitflag_queues(WF1,WFs,MergedWFs) :- var(WFs),!,
631 push_waitflag(WF1,WFs,MergedWFs).
632 merge_waitflag_queues(WF1,Head2-Tail2,MergedWFs) :- var(WF1),!,
633 MergedWFs = [WF1|Head2]-Tail2. % add WF1 at front
634 merge_waitflag_queues(Head1-Tail1,Head2-Tail2,MergedWFs) :- !, % concatenation of difference lists
635 Tail1=Head2,
636 MergedWFs = Head1-Tail2.
637 merge_waitflag_queues(WF1,WFs,MergedWFs) :-
638 add_internal_error('Illegal WF list:',merge_waitflag_queues(WF1,WFs,MergedWFs)),
639 MergedWFs = WFs.
640
641
642 % ------------------------
643
644 % a version which delays getting a waitflag until the Prio is known:
645 :- block block_get_wait_flag(-,?,?,?).
646 block_get_wait_flag(Prio,Info,WFX,WF) :- get_wait_flag(Prio,Info,WFX,WF).
647
648 % check if there are no waitflags and no FD variables; note: there could be pending co-routines on WF0
649 no_pending_waitflags(no_wf_available).
650 no_pending_waitflags(wfx(_WF0,Store,_WFE,_)) :-
651 my_get_wf_store_fdvars_atts(Store,Heap,FDList),
652 FDList=[], % no FD Variables
653 empty_avl(Heap). % no waitflags pending
654 % Note grounding could still be in progress
655 % TO DO: we could add attribute before grounding and remove after grounding !?
656
657
658 % -------------------
659
660 % storing Predicates for Kodkod external function:
661 my_get_kodkod_predicates(wfx(_,Store,_,_),ID,PredicateList) :- my_get_wf_preds(Store,ID,kodod,PredicateList).
662 my_get_wf_preds(Store,ID,Type,PredicateList) :-
663 (my_get_wf_preds_att(Store,ID,Type,PredicateList)
664 -> true
665 ; PredicateList = []
666 ).
667 %my_store_wf_kodkod(Store,ID,PredicateList) :- put_atts(Store,+wf_kodkod(ID,PredicateList)).
668 my_add_predicate_to_kodkod(wfx(_,Store,_,_),ID,Predicate) :-
669 my_add_predicate_aux(wfx(_,Store,_,_),ID,kodod,Predicate).
670 my_add_predicate_aux(wfx(_,Store,_,_),ID,Type,Predicate) :-
671 my_get_wf_preds(Store,ID,Type,PredicateList),
672 %length(PredicateList,Len), format('Adding pred to ~w of len ~w~n',[ID,Len]),
673 put_mutable_other_attr(Store,wf_preds(ID,Type,[Predicate|PredicateList])).
674
675 % -------------------
676
677 % storing Predicates for external function calling satsolver:
678 my_get_satsolver_predicates(wfx(_,Store,_,_),ID,PredicateList) :-
679 my_get_wf_preds(Store,ID,satsolver,PredicateList).
680 my_add_predicate_to_satsolver(wfx(_,Store,_,_),ID,Predicate) :-
681 my_add_predicate_aux(wfx(_,Store,_,_),ID,satsolver,Predicate).
682
683 % -------------------
684
685 % allow to store and update other information entries
686 % they are mixed in with the Kodkod predicate list
687
688 get_wf_all_dynamic_infos(no_wf_available,[]).
689 get_wf_all_dynamic_infos(wfx(_,Store,_,_),List) :- my_get_all_wf_info_atts(Store,List).
690
691 get_wf_dynamic_info(wfx(_,Store,_,_),ID,Val) :- my_get_wf_info_att(Store,ID,Val).
692
693 put_wf_dynamic_info(no_wf_available,_,_).
694 put_wf_dynamic_info(wfx(_,Store,_,_),ID,Val) :- put_mutable_other_attr(Store,wf_info(ID,Val)).
695
696 % -------------------
697
698
699 ground_wait_flag0(wfx(WF0,_,_,_)) :- grd_wf0(WF0).
700
701 ground_wait_flags(wfx(WF0,Store,EnumFinish,WFInfos)) :- !,
702 ? grd_wf0(WF0),
703 deref_store(Store,DStore),
704 init_wf_infos_for_grounding(WFInfos,WFInfos2),
705 %nl,print(' ground_wait_flags:'),nl,portray_waitflags_store(Store), portray_call_stack(wfx(WF0,Store,EnumFinish,WFInfos)),nl,
706 ? ground_waitflags_store_clpfd(DStore,WFInfos2),
707 grd_ef(EnumFinish).
708 ground_wait_flags(no_wf_available) :- !.
709 ground_wait_flags(W) :-
710 add_internal_error('Waitflags in wrong format: ',ground_wait_flags(W)).
711
712 grd_wf0(E) :- %print(start_grd_wf0(E)),nl,
713 (var(E) ->
714 E=s(E2), % first make nonvar, and then ground (separate call to avoid merging unifications)
715 ? grd_wf01(E2) %%,print(grd_wf0_done),nl
716 ; E=s(E2) -> (nonvar(E2),E2 \== 0 -> add_internal_error('Illegal WF0 Waitflag value: ',grd_wf0(E))
717 ; grd_wf01(E2))
718 ; add_internal_error('Illegal WF0 Waitflag value functor: ',grd_wf0(E))
719 ).
720 grd_wf01(0).
721
722 grd_ef(E) :- var(E) -> E=0
723 ; ((E==0;E==wd_guarded) -> true ; add_internal_error('Illegal EF Waitflag value: ',grd_ef(E))).
724
725 /* currently unused:
726 create_wdguarded_wait_flags(wfx(WF0,Store,EnumFinish,Info),Res,Expected,
727 wfx(WF0,Store,LocalEnumFinish,Info)) :-
728 %% if Res=Expected then the computations of the inner waitflags should be well-defined;
729 %% otherwise they may not
730 copy_wfe(EnumFinish,Res,Expected,LocalEnumFinish).
731 :- block copy_wfe(-,?,?,?), copy_wfe(?,-,?,?).
732 copy_wfe(EnumFinish,Res,Expected,LocalEnumFinish) :-
733 (Res==Expected -> LocalEnumFinish=EnumFinish
734 ; LocalEnumFinish=wd_guarded %% branch is pruned by well-definedness condition
735 ).
736 */
737
738 % ground_constraintprop_wait_flags will not ground WFE flag
739
740 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
741 :- if(environ(prob_safe_mode,true)).
742 ground_constraintprop_wait_flags(W) :- check_is_wait_flag(W),fail.
743 :- endif.
744 ground_constraintprop_wait_flags(wfx(WF0,Store,_WFE,WFInfos)) :-
745 %% print(ground_constraintprop_wait_flags(WF0,Store,_WFE)),nl, %%
746 !,grd_wf0(WF0),% print(finished_grounding_wf0),nl,portray_waitflags_store(Store),
747 deref_store(Store,DStore),
748 init_wf_infos_for_grounding(WFInfos,WFInfos2),
749 ? ground_waitflags_store_clpfd(DStore,WFInfos2).
750 ground_constraintprop_wait_flags(no_wf_available) :- !.
751 ground_constraintprop_wait_flags(W) :-
752 add_internal_error('Waitflags in wrong format',ground_constraintprop_wait_flags(W)).
753
754
755
756 :- use_module(clpfd_interface,[clpfd_in_domain/1, clpfd_labeling/2]).
757 :- use_module(library(lists),[reverse/2]).
758
759 % deprecated:
760 ground_wf(Prio,WF) :-
761 (var(WF) -> WF=Prio ; if(WF=Prio,true,add_internal_error('Illegal waitflag: ',ground_wf(Prio,WF)))).
762
763 :- if(environ(debug_waitflags,true)).
764 % provide feedback about waitflag grounding
765 init_wf_infos_for_grounding(Infos,NewInfos) :-
766 %print(start_wf_grounding(Infos)),nl,
767 ord_add_element(Infos,wf_indent(_),NewInfos).
768
769 % provided indentation to see scope of grounding
770 indent_wf(WFInfos) :- member(wf_indent(Var),WFInfos),!,indent_var(Var).
771 indent_wf(_).
772 % indent based upon a shared variable and increment it
773 indent_var(X) :- var(X),!, X=s(_).
774 indent_var(s(X)) :- !,print('.'), indent_var(X).
775 indent_var(_) :- print('***').
776
777 :- use_module(library(terms),[term_hash/3]).
778 ground_prio(Prio,WFMin,Info,WFInfos) :- WFInfos \= '$debug_done',
779 (member(IM,WFInfos),get_info_context_description(IM,Msg) -> true ; Msg=''),
780 nl,indent_wf(WFInfos),
781 term_hash(Info,[if_var(ignore)],Hash),
782 format(' -> ~w --> #~w# ~w :: ~w ~w~n',[Prio,Hash,Info,WFMin,Msg]),
783 !,
784 ground_prio(Prio,WFMin,Info,'$debug_done'). % recursive, but this time normal clauses will apply
785 :- else.
786 init_wf_infos_for_grounding(I,I).
787 :- endif.
788 ground_prio(Prio,WF,Info,WFInfos) :- %print(ground_prio(Prio,WF,Info)),nl,
789 nonvar(WF),!,
790 (WF=[H|T] -> % we used sometimes to have a list of waitflags; ground one-by one;
791 add_internal_error('Deprecated grounding of lists:',ground_prio(Prio,WF,Info,WFInfos)),
792 reverse([H|T],Ls),
793 maplist(ground_wf(Prio),Ls)
794 ; ground(WF) -> true % already grounded by somebody else
795 ; add_internal_error('Waitflag already partially grounded: ',ground_prio(Prio,WF,Info))).
796 %ground_prio(Prio,WF,Info,WFInfos) :- get_debug_kernel_waitflags(Cntr),!,
797 % print(ground_prio(Cntr,Prio,WF,Info)),nl, WF=Prio, print(grounded_prio(Cntr,Prio,WF,Info)),nl.
798 ground_prio(Prio,WF,_Info,_WFInfos) :-
799 %external_functions:indent_format(user_output,'~w (~w)~n',[Prio,Info],no_trace),portray_attached_goals(WF),nl,
800 %% (debug:debug_mode(on) -> external_functions:indent_format(user_output,'~w (~w)~n',[Prio,Info],no_trace) ; true),
801 % print(ground(Prio,WF,Info)),nl, translate:print_frozen_info(WF),nl,
802 WF = Prio. % ground waitflag
803 % print(grounded(Prio,Info)),nl,nl, %%
804
805 %:- use_module(kernel_objects,[enum_warning_large/3]).
806 ?label_clpfd_variable(Variable) :- label_clpfd_variable(2097153,Variable).
807 label_clpfd_variable(Prio,Variable) :-
808 %print(label_clpfd_variable(Prio,Variable)),nl,
809 (gt_limit(Prio,2097152), % note Prio > test also works with float(X) terms !
810 check_if_labeling_domain_large(Variable,2097152,Size,RANGE) % {x|x:1..2**23 & x mod 2 = x mod 1001} takes about 2 minutes; {x|x:1..2**21 & x mod 2 = x mod 1001} takes about 30 seconds; 2**21 = 2097152, 2**23 = 8388608
811 -> %kernel_objects:enum_warning_large(Variable,'INTEGER VARIABLE',RANGE), % could in principle also be enumerated set; but extremely unlikely given size; enum_warning will generate virtual time-outs, ... -> we no longer do this; for AMASS scheduler.mch there is a time-out after step 301 otherwise
812 performance_messages:perfmessage(enumerating_large_integer_variable(RANGE)),
813 (number(Size)
814 -> clpfd_labeling([Variable],[bisect]) % ffc no longer required: just a single variable
815 ; add_warning(label_clpfd_variable,'Trying to enumerate FD Variable with infinite domain (possibly due to WD error) ',RANGE)
816 % or due to clpfd_tables element/3 adding unbounded variables for labeling (add_fd_variables_for_labeling)
817 )
818 % we use bisecting rather than default enumeration; e.g., x:1..8388610 & y:1..8388610 & x*x*x = y*y + y + 10 is relatively quickly determined to be unsatisfiable (380 ms)
819 % Note: test 1099 tests this
820 % TO DO: investigate whether it makes sense to use bisect for smaller values already
821 ; preferences:preference(randomise_enumeration_order,true) -> clpfd_interface:clpfd_randomised_in_domain(Variable)
822 ? ; clpfd_in_domain(Variable)). % TO DO: use random ?
823
824 :- use_module(clpfd_interface,[ clpfd_size/2]).
825 check_if_labeling_domain_large(H,Limit,Size,Res) :-
826 clpfd_size(H,Size),
827 gt_limit(Size,Limit),
828 clpfd_interface:clpfd_domain(H,From,To),
829 Res=From:To.
830
831 %check_if_labeling_domain_finite(H) :-
832 % clpfd_size(H,Size), number(Size).
833
834 % mix ProB labeling with CLP(FD) labeling
835 ground_waitflags_store_clpfd(Store,WFInfos) :-
836 my_get_wf_store_fdvars_atts(Store,Heap,FD),!,
837 ? ground_waitflags_store_clpfd_aux(Store,Heap,FD,WFInfos).
838 ground_waitflags_store_clpfd(Store,WFInfos) :-
839 add_internal_error('Illegal Waitflag: ',ground_waitflags_store_clpfd(Store,WFInfos)),fail.
840
841 ground_waitflags_store_clpfd_aux(Store,Heap,FDVars,WFInfos) :- FDVars \= [],
842 %my_get_fdvars_att(Store,FDVars),
843 %get_atts(Store,wf_fdvars(FDVars)), % there is a list of FD vars available
844 !,
845 ( avl_del_min_waitflag(Heap,Prio,wf(WFMin,Info),NewHeap)
846 -> % we have non-ground waitflags with a matching priority
847 (my_get_next_fdvar_to_enumerate(FDVars,NextFDVar,RemainingFDVARS),
848 fd_priority_leq_limit(NextFDVar,FDPrio,Prio)
849 ? -> enum_fd_variable_store(FDPrio,Store,NextFDVar,RemainingFDVARS,WFInfos)
850 ; put_mutable_wf_store_attr(Store,NewHeap), % write the modified heap back
851 % debug:hit_counter(XXX),print(grounding(XXX,Prio,_Info)),nl, (XXX=16556->trace ; true),
852 ? ground_prio(Prio,WFMin,Info,WFInfos),
853 ? ground_waitflags_store_clpfd(Store,WFInfos) % continue recursively
854 )
855 ; % there are no pending waitflag
856 (my_get_next_fdvar_to_enumerate(FDVars,NextFDVar,RemainingFDVARS)
857 ? -> enum_fd_variable_store(Store,NextFDVar,RemainingFDVARS,WFInfos)
858 ; true % heap and FDVars list is empty, nothing more to do
859 )
860 ).
861 ground_waitflags_store_clpfd_aux(Store,Heap,[],WFInfos) :- % no FDVars are available to enumerate
862 avl_del_min_waitflag(Heap,Prio,wf(WFMin,Info),NewHeap),
863 !,
864 put_mutable_wf_store_attr(Store,NewHeap), % write the modified heap back
865 % debug:hit_counter(XXX),print(grounding(XXX,Prio,_Info)),nl, (XXX=16556->trace ; true),
866 ? ground_prio(Prio,WFMin,Info,WFInfos), % ground waitflag
867 ? ground_waitflags_store_clpfd(Store,WFInfos). % continue recursively
868 ground_waitflags_store_clpfd_aux(_Store,_Heap,[],_). % heap and FDVars list is empty, nothing more to do
869
870 %:- use_module(library(lists),[exclude/3]).
871 enum_fd_variable_store(Store,NextFDVar,RemainingFDVARS,WFInfos) :-
872 %exclude(nonvar,RemainingFDVARS,RemainingFDVARS2),
873 put_mutable_wf_fdvars_attr(Store,RemainingFDVARS),
874 %% print(labeling(NextFDVar,RemainingFDVARS)),nl, portray_fd_vars([NextFDVar|RemainingFDVARS]),nl,nl,
875 ? label_clpfd_variable(NextFDVar),
876 ? ground_waitflags_store_clpfd(Store,WFInfos).
877 % a version of the above where we know the priority
878 enum_fd_variable_store(FDPrio,Store,NextFDVar,RemainingFDVARS,WFInfos) :-
879 %exclude(nonvar,RemainingFDVARS,RemainingFDVARS2), % does not seem to buy a lot
880 put_mutable_wf_fdvars_attr(Store,RemainingFDVARS),
881 %% print(labeling(NextFDVar,RemainingFDVARS)),nl, portray_fd_vars([NextFDVar|RemainingFDVARS]),nl,nl,
882 ? label_clpfd_variable(FDPrio,NextFDVar),
883 ? ground_waitflags_store_clpfd(Store,WFInfos).
884
885 :- if(false).
886 % small utility to trace through waitflag enumeration
887 :- dynamic spying_on/1.
888 spying_on(1).
889 spy_waitflags(_,_) :- \+ spying_on(_) , !.
890 spy_waitflags(Msg,Store) :- retract(spying_on(Nr)),print(Msg),nl,
891 (Nr=1
892 -> assertz(spying_on(Nr)),
893 print(' (j,t,p,q) ==> '),read_term(T,[]),
894 action(T,Store)
895 ; N1 is Nr-1, assertz(spying_on(N1))
896 ).
897 action(t,_Store) :- !,trace.
898 action(p,Store) :- !,portray_waitflags_store(Store), spy_waitflags('',Store).
899 action(q,_Store) :- !,retractall(spying_on).
900 action(Nr,_) :- number(Nr),!, retractall(spying_on(_)), assertz(spying_on(Nr)).
901 action(_,_).
902 :- endif.
903
904 :- assert_must_succeed(( kernel_waitflags:init_wait_flags(WF), kernel_waitflags:portray_waitflags(WF),
905 kernel_waitflags:get_wait_flag(2,'Test',WF,WF2), when(nonvar(WF2),print(wf2)),
906 FD in 1..2,kernel_waitflags:add_fd_variable_for_labeling(FD,WF),
907 kernel_waitflags:portray_waitflags(WF), kernel_waitflags:ground_wait_flags(WF) )).
908 % PORTRAYING Waitflags
909 portray_waitflags(wfx(WF0,Store,WFE,Infos)) :- flush_output,
910 delete(Infos,call_stack(_),Infos2),
911 print('*WAITFLAG STORE: '),print(wfx(WF0,'STORE',WFE,Infos2)),nl,
912 portray_wait_flag_infos(Infos),nl,
913 (var(WF0) -> print('> WF0 :: '), portray_attached_goals(WF0),nl ; true),
914 portray_waitflags_store(Store),!,
915 (var(WFE) -> print('> WFE :: '), portray_attached_goals(WFE),nl ; true),
916 print('*END WAITFLAG STORE'),nl.
917 %my_portray_avl(Heap),nl.
918 portray_waitflags(none) :- !, print('*WAITFLAG STORE: none'),nl.
919 portray_waitflags(no_wf_available) :- !, print('*WAITFLAG STORE: none'),nl.
920 portray_waitflags(Store) :-
921 add_internal_error('Illegal Waitflag: ',portray_waitflags(Store)),flush_output.
922
923 portray_fd_vars([]) :- !, '$NOT_COVERED'('This is debugging code!').
924 portray_fd_vars([V|T]) :- print('> '), print(V), nonvar(V),!, nl,
925 portray_fd_vars(T), '$NOT_COVERED'('This is debugging code!').
926 portray_fd_vars([V|T]) :- clpfd_size(V,Size), !, print(' : '), print(Size),
927 portray_attached_goals(V),
928 portray_fd_vars(T),
929 '$NOT_COVERED'('This is debugging code!').
930 portray_fd_vars(X) :- print('> *** UNKNOWN FDVARS: '), print(X), nl,
931 '$NOT_COVERED'('This is debugging code!').
932
933 portray_waitflags_store(Store) :-
934 my_get_fdvars_att(Store,FDList),
935 (FDList=[] -> true ; print('FDVARS:'),nl,portray_fd_vars(FDList),nl),
936 my_get_wf_store_att(Store,Heap),
937 avl_to_list(Heap,List), portray_avl_els(List).
938
939 portray_avl_els([]).
940 portray_avl_els([Prio-wf(LWF,Info)|T]) :-
941 print('> '),print(Prio), print(' : '), print(LWF), print(' : '), portray_info(Info),nl,
942 portray_attached_goals(LWF),
943 portray_avl_els(T).
944
945 portray_info(label_clpfd_vars(Vars)) :- print('label_clpfd_vars :: '),
946 translate:l_print_frozen_info(Vars).
947 portray_info(I) :- print(I).
948
949 portray_attached_goals(V) :- V==[],!.
950 portray_attached_goals(LWF) :- nonvar(LWF),LWF=[H|T],!,
951 portray_attached_goals(H),
952 portray_attached_goals(T).
953 portray_attached_goals(LWF) :- frozen(LWF,Goal), print(' :: '), portray_goal(Goal),nl.
954
955 :- use_module(tools_printing,[print_term_summary/1]).
956 portray_goal((A,B)) :- !, portray_goal(A), print(','), print(' '), portray_goal(B).
957 portray_goal(A) :- print_term_summary(A).
958
959
960 :- public my_portray_avl/1.
961 my_portray_avl(V) :- var(V), !, add_internal_error('Variable: ',my_portray_avl(V)).
962 my_portray_avl(V) :- portray_avl(V).
963
964
965 quick_portray_waitflags(wfx(WF0,Store,WFE,_)) :-
966 my_get_wf_store_fdvars_atts(Store,Heap,FDList),
967 avl_domain(Heap,List),
968 format('% Waitflags-Store WF0=~w,WFE=~w, Flags=~w, FDVars=~w~n',[WF0,WFE,List,FDList]).
969 quick_portray_waitflags(no_wf_available) :-
970 format('% Waitflags-Store no_wf_available~n',[]).
971 quick_portray_waitflags_store(Store) :-
972 my_get_wf_store_fdvars_atts(Store,Heap,FDList),
973 avl_domain(Heap,List),
974 format('% Waitflags-Store Flages=~w, FDVars=~w~n',[List,FDList]).
975
976 % get information about the phase a Waitflag store is in
977 get_waitflags_phase(no_wf_available,Phase) :- Phase=no_wf_available.
978 get_waitflags_phase(wfx(WF0,_,WFE,_),Phase) :-
979 (var(WF0) -> Phase=phase0
980 ; \+ ground(WF0) -> Phase=phase1
981 ; ground(WFE) -> Phase=enumeration_finished
982 ; Phase = grounding). % TODO: get avl_min
983
984 :- assert_must_succeed(( kernel_waitflags:init_wait_flags(WF),
985 kernel_waitflags:get_wait_flag1(WF,WF1), when(ground(WF1),X=a),
986 kernel_waitflags:ground_wait_flags(WF), X==a )).
987
988 % create a copy of the waitflags with WF0 and WFE as variable; should be finished with copy_wf_finish
989 % can be used if you temporarily want to disable non-deterministic enumeration, ...
990 % This is typically used within e.g., a local scope where a conjunction of predicates is added
991 % we start 1) by doing copy_wf_start(OuterWF,LocalWF), 2) assert all predicates,
992 % and then 3) call copy_wf_finish at the end of the block
993 % This ensures that during assertion of the predicates only efficient deterministic computations occur
994 copy_wf_start(wfx(_,WFStore,_,Infos),Info,wfx(_,WFStore,_,NewInfos)) :-
995 add_debug_wait_flag_info(Infos,wf_copy(Info),NewInfos).
996 copy_wf_start(no_wf_available,_,no_wf_available).
997
998 % just copy WF0 and WFE over to new waitflag
999 copy_wf_finish(wfx(WF0,_,WFE,_),wfx(WF0,Store,WFE2,Info)) :-
1000 (var(WFE) -> WFE2 = WFE
1001 ; % the outer WF is already fully grounded and will not be driven anymore
1002 % so now we ground all the constraints that have been set-up since copy_wf_start
1003 ? ground_wait_flags(wfx(WF0,Store,WFE2,Info))
1004 ).
1005 copy_wf_finish(no_wf_available,no_wf_available).
1006
1007
1008 /* create a copy where the enumeration_finished waitflag is shared;
1009 the inner enumeration_finished wait flags should normally not be grounded */
1010 create_inner_wait_flags(wfx(_,OuterStore,WFE,Infos),Info,wfx(_WF0Inner,S,WFEInner,NewInfos)) :-
1011 add_debug_wait_flag_info(Infos,Info,NewInfos),
1012 copy_wfe_to_inner(WFE,WFEInner),
1013 my_get_all_wf_info_atts(OuterStore,DynInfos), % copy dynamic wf_infos from outer to inner store
1014 init_wait_flags_store_with_dynamic_infos(S,DynInfos).
1015
1016 create_inner_wait_flags(no_wf_available,_,no_wf_available).
1017
1018 % was using: get_inner_enumeration_over_wait_flag/get_enumeration_almost_finished_wait_flag
1019 %:- block copy_wfe_to_inner(-,?,?).
1020 %copy_wfe_to_inner(_,WFE,WFE).
1021
1022 :- block copy_wfe_to_inner(-,-).
1023 copy_wfe_to_inner(WFE,_) :- var(WFE),!. % inner was grounded before outer
1024 copy_wfe_to_inner(WFE,WFE).
1025 % copy enumeration finished waitflag from inner computation if WFE was not grounded there
1026 % assumes inner WF enumeration is finished
1027 copy_wfe_from_inner_if_necessary(wfx(_,_,WFEInner,_),wfx(_,_,WFE,_)) :- var(WFEInner),!, WFE=WFEInner.
1028 copy_wfe_from_inner_if_necessary(_,_).
1029
1030 % is very similar to ground_constraintprop_wait_flags, but will also ground EF if no abort is pending
1031 ground_inner_wait_flags(WF) :-
1032 ? ground_constraintprop_wait_flags(WF),
1033 ground_ef_wait_flag_unless_abort_pending(WF).
1034
1035 % copy WF0 and WFE, set up a new store for the rest
1036 copy_wf01e_wait_flags(wfx(WF0,WFX,WFE,Infos),wfx(WF0,S,WFE,Infos)) :-
1037 init_wait_flags_store(S),
1038 get_waitflag_from_store(1,copy_wf01e,WFX,WF1), % now ground wait flag 1 if it is grounded in the orginal WF store
1039 copy_wf01e_wait_flags_aux(WF1,S).
1040 copy_wf01e_wait_flags(no_wf_available,no_wf_available).
1041
1042 :- block copy_wf01e_wait_flags_aux(-,?).
1043 copy_wf01e_wait_flags_aux(_,S) :-
1044 ground_waitflags_store_up_to_no_clpfd(1,S,[]). % no CLPFD - labeling required until prio 1
1045
1046 %--------------
1047
1048 % the following is useful when new predicates are checked during enumeration
1049 % creates a copy of the wait_flags, except for WF0; this needs to be grounded separately with grd_wf0/1 or clone_finish
1050 % thanks to the copy, WF0 is a variable again and we give priority to propagations that create avl_sets
1051 clone_wait_flags_from1(wfx(_WF0,S,WFE,Infos),Ground,wfx(_NewWF0,S2,NewWFE,Infos)) :-
1052 (nonvar(WFE)
1053 -> Ground=ground_upon_finish,
1054 add_debug_message(clone_wait_flags_from1,'Cloning WF store whose enumeration is finished: ',Infos)
1055 ; Ground=no_grounding,
1056 NewWFE=WFE % waitflag store still being driven by enumerator, no need to ground/enumerate afterwards
1057 ),
1058 deref_store(S,S2).
1059 clone_wait_flags_from1(no_wf_available,no_grounding,no_wf_available).
1060
1061 % call after clone_wait_flags_from1, after you have set up all predicates/constraints
1062 clone_wait_flags_from1_finish(wfx(WF0,_,_,_),Ground,wfx(WF0,S2,NewWFE,Infos)) :- % finish copying by copying over WF0
1063 (Ground=no_grounding -> true
1064 ; ground_wait_flags(wfx(WF0,S2,NewWFE,Infos)) % the cloned store is not being enumerated anymore; do it ourselves
1065 ).
1066 clone_wait_flags_from1_finish(no_wf_available,_,no_wf_available).
1067
1068 %--------------
1069
1070 get_wait_flag0(wfx(WF0,_,_,_),WF0).
1071 get_wait_flag0(no_wf_available,0).
1072
1073 %get_wait_flag0(WFX,WF0) :- get_wait_flag(0,WFX,WF0). /* when this is ground you can do det. propagatons */
1074 get_wait_flag1(WFX,WF1) :- get_wait_flag(1.0,WFX,WF1). /* when this is ground you can do det. propagatons */
1075 get_wait_flag1(Info,WFX,WF1) :- %print(getwf1(Info)),nl, portray_waitflags(WFX),nl,
1076 get_wait_flag(1.0,Info,WFX,WF1).
1077
1078 get_binary_choice_wait_flag(_,no_wf_available,WF2) :- !, WF2=2.
1079 get_binary_choice_wait_flag(Info,WF,WF2) :- get_preference(data_validation_mode,true),!,
1080 get_binary_choice_wait_flag_exp_backoff(1048576,Info,WF,WF2).
1081 % in DV mode we do not want to enumerate bool(.) or similar; we want to wait for data enumeration to decide those
1082 % prio was 1048576, caused slowdown for TYPES_AUTORISES_RVF3_GEN__MRGA.mch before improvement to b_check_exists_wfwd
1083 get_binary_choice_wait_flag(Info,WFX,WF2) :- !, get_binary_choice_wait_flag_exp_backoff(4,Info,WFX,WF2).
1084 %get_binary_choice_wait_flag(Info,WFX,WF2) :- % use 3 rather than 2 to give priority over enumeration choicepoints
1085 % get_wait_flag(4,Info,WFX,WF2). /* when this is ground you can do binary propagatons */
1086
1087 %get_middle_wait_flag(Info,WFX,WFn) :- get_wait_flag(10,Info,WFX,WFn).
1088
1089 ?get_last_wait_flag(Info,WFX,Res) :- last_finite_priority(P), get_wait_flag(P,Info,WFX,Res).
1090
1091 % ------------------------
1092 get_wait_flag_infos(wfx(_,_,_,Infos),Infos).
1093 get_wait_flag_infos(no_wf_available,[]).
1094
1095 portray_wait_flag_infos(wfx(_,_,_,Infos)) :- !, portray_wait_flag_infos(Infos).
1096 portray_wait_flag_infos(no_wf_available) :- !.
1097 portray_wait_flag_infos(List) :- maplist(portray_wait_flag_info,List).
1098
1099 portray_wait_flag_info(call_stack(CallStack)) :- !, translate_call_stack(CallStack,TS), write(TS).
1100 portray_wait_flag_info(X) :- write(X),nl.
1101
1102
1103 :- use_module(library(ordsets),[ord_member/2,ord_add_element/3]).
1104 get_wait_flag_info(wfx(_,_,_,Infos),Info) :- member(Info,Infos).
1105
1106 % use if the Info field is known, requires ordered/sorted Infos list
1107 % used for wfx_no_enumeration information, see test 1368
1108 is_wait_flag_info(wfx(_,_,_,Infos),Info) :-
1109 (nonvar(Infos) -> ord_member(Info,Infos) ; print(var_waitflag),nl,fail).
1110
1111 %set_wait_flag_infos(wfx(WF0,Store,WFE,_),Infos,wfx(WF0,Store,WFE,Infos)).
1112 %set_wait_flag_infos(no_wf_available,_,no_wf_available).
1113
1114 % add new Info entry to WF store's info list
1115 add_wait_flag_info(wfx(WF0,Store,WFE,Infos),Info,wfx(WF0,Store,WFE,NewInfos)) :-
1116 (ord_add_element(Infos,Info,NewInfos) -> true %, print(added_wf_infos(NewInfos)),nl
1117 ; add_internal_error('Could not add_wait_flag_info:',(Info,Infos)),
1118 NewInfos = [Info|Infos]).
1119 add_wait_flag_info(no_wf_available,_,no_wf_available).
1120
1121
1122 % CALL STACK related predicates
1123 % --------------
1124 :- use_module(tools_lists,[ord_update_nonvar/4]).
1125 % push call stack information into the WF info field
1126 push_wait_flag_call_stack_info(no_wf_available,_,WF2) :- !, WF2=no_wf_available.
1127 push_wait_flag_call_stack_info(wfx(WF0,Store,WFE,Infos),CallInfo,wfx(WF0,Store,WFE,NewInfos)) :-
1128 ord_update_nonvar(call_stack(Stack),Infos,call_stack([CallInfo|Stack]),NewInfos),!,
1129 %print(push_call_stack(CallInfo,Stack)),nl,
1130 (var(Stack) -> Stack=[] % no call stack available yet
1131 ; true).
1132 push_wait_flag_call_stack_info(WF,CallInfo,WF) :- add_internal_error('Pushing call stack failed: ',CallInfo).
1133
1134 % only push in TRACE_INFO mode to avoid performance hit in regular mode
1135 opt_push_wait_flag_call_stack_info(WF,_,WF2) :- preference(provide_trace_information,false),!, WF2=WF.
1136 opt_push_wait_flag_call_stack_info(WF,CallInfo,WF2) :-
1137 push_wait_flag_call_stack_info(WF,CallInfo,WF2).
1138
1139 debug_opt_push_wait_flag_call_stack_info(WF,CallInfo,WF2) :-
1140 (debug_mode(off) -> WF2=WF
1141 ; opt_push_wait_flag_call_stack_info(WF,CallInfo,WF2)
1142 ).
1143
1144 :- use_module(tools_lists,[ord_member_nonvar_chk/2]).
1145 add_call_stack_to_span(Span,wfx(_,_,_,Infos),NewSpan) :-
1146 (var(Infos) -> write(illegal_wfx),nl,fail ; true),
1147 ord_member_nonvar_chk(call_stack(CallStack),Infos),
1148 !,
1149 (Span = pos_context(Span1,call_stack(OldStack),Span2), % we already have a call_stack
1150 merge_call_stack(OldStack,CallStack,NewStack)
1151 -> NewSpan = pos_context(Span1,call_stack(NewStack),Span2)
1152 ; % we do not already have merged in a call-stack
1153 NewSpan = pos_context(Span,call_stack(CallStack),unknown)
1154 ).
1155 add_call_stack_to_span(Span,_,Span).
1156
1157 merge_call_stack(OldStack,AddStack,NewStack) :-
1158 reverse(OldStack,OR), OR=[FirstOld|_],
1159 reverse(AddStack,AR), AR=[FirstAdd|_],
1160 (FirstOld \= FirstAdd % we use \= and not \== as entries can contain different Prolog variables
1161 -> append(OldStack,AddStack,NewStack) % we have not yet incorporated the outer stack
1162 ; append(AR,_,OR) -> NewStack = OldStack % old stack incorporates new one; this is often (always?) the case
1163 ; NewStack = AddStack).
1164
1165 % a variation of add_error/4
1166 add_error_wf(Src,Msg,V,Span,WF) :-
1167 add_call_stack_to_span(Span,WF,NewSpan),
1168 add_error(Src,Msg,V,NewSpan).
1169
1170 add_internal_error_wf(Src,Msg,V,Span,WF) :-
1171 add_call_stack_to_span(Span,WF,NewSpan),
1172 add_internal_error(Src,Msg,V,NewSpan).
1173
1174 % a variation of add_error/4
1175 add_warning_wf(Src,Msg,V,Span,WF) :-
1176 add_call_stack_to_span(Span,WF,NewSpan),
1177 add_warning(Src,Msg,V,NewSpan).
1178
1179 % a variation of add_message/4
1180 add_message_wf(Src,Msg,V,Span,WF) :-
1181 add_call_stack_to_span(Span,WF,NewSpan),
1182 add_message(Src,Msg,V,NewSpan).
1183
1184 :- use_module(translate,[translate_call_stack/2]).
1185 portray_call_stack(Var) :- var(Var),!,
1186 add_internal_error('Illegal var WF:',portray_call_stack(Var)).
1187 portray_call_stack(wfx(_,_,_,Infos)) :-
1188 ord_member_nonvar_chk(call_stack(CallStack),Infos),!,
1189 translate_call_stack(CallStack,TS),!,write(TS),nl.
1190 portray_call_stack(_) :- write(no_call_stack_available),nl.
1191
1192 % copy call stack info from one wait flag to another
1193 copy_wait_flag_call_stack_info(wfx(_,_,_,FromInfos),wfx(WF0,Store,WFE,Infos),wfx(WF0,Store,WFE,NewInfos)) :-
1194 ord_member_nonvar_chk(call_stack(CallStack),FromInfos),!,
1195 ord_add_element(Infos,call_stack(CallStack),NewInfos).
1196 % Note: we do not copy expect_explicit_value (but we use this in b_trace_test_components only)
1197 copy_wait_flag_call_stack_info(_,WF,WF).
1198
1199 % get call stack, empty list if none available
1200 get_call_stack(wfx(_,_,_,FromInfos),Stack) :-
1201 ord_member_nonvar_chk(call_stack(CallStack),FromInfos),!,
1202 Stack=CallStack.
1203 get_call_stack(_,[]).
1204
1205 :- use_module(library(lists),[select/3]).
1206 init_quantifier_wait_flag(OuterWF,_QK,Paras,ParaValues,Pos,WF) :-
1207 ? select(QK,Pos,Pos1),
1208 detect_quantifier_kind(QK,QuantKind),!, % see if we have position infos which indicate the origin of the comprehension_set / quantifier
1209 simplify_span(Pos1,SPos),
1210 init_wait_flags_and_push_call_stack(OuterWF,quantifier_call(QuantKind,Paras,ParaValues,SPos),WF).
1211 init_quantifier_wait_flag(OuterWF,QuantKind,Paras,ParaValues,Pos,WF) :-
1212 simplify_span(Pos,SPos),
1213 init_wait_flags_and_push_call_stack(OuterWF,quantifier_call(QuantKind,Paras,ParaValues,SPos),WF).
1214
1215 % check grounding of WFE flag occurs after everything else
1216 :- public observe_wait_flags_wfe/1. % debugging utility
1217 observe_wait_flags_wfe(wfx(WF0,WFX,WFE,Infos)) :- !, obs(WF0,WFX,WFE,Infos).
1218 observe_wait_flags_wfe(_).
1219 :- block obs(?,?,-,?).
1220 obs(WF0,WFX,WFE,Infos) :-
1221 add_message_wf(kernel_waitflags,'WFE grounded:',WFE,unknown,wfx(WF0,WFX,WFE,Infos)),
1222 var(WF0),!,
1223 add_error_wf(kernel_waitflags,'WF0 not grounded before WFE:',WF0,unknown,wfx(WF0,WFX,WFE,Infos)).
1224 obs(WF0,WFX,WFE,Infos) :- my_get_fdvars_att(WFX,FDList), FDList \= [], !,
1225 add_error_wf(kernel_waitflags,'FDVars not grounded before WFE:',FDList,unknown,wfx(WF0,WFX,WFE,Infos)).
1226 obs(WF0,WFX,WFE,Infos) :- my_get_wf_store_att(WFX,Heap), avl_to_list(Heap,List), List \= [], !,
1227 add_error_wf(kernel_waitflags,'Waitflags not grounded before WFE:',List,unknown,wfx(WF0,WFX,WFE,Infos)).
1228 obs(_WF0,_WFX,_WFE,_Infos).
1229
1230 % a version of opt_push_wait_flag_call_stack_info for quantifiers
1231 opt_push_wait_flag_call_stack_quantifier_info(WF,_,_,_,_,WF2) :-
1232 preference(provide_trace_information,false),!, WF2=WF.
1233 opt_push_wait_flag_call_stack_quantifier_info(no_wf_available,_,_,_,_,WF2) :- !, WF2=no_wf_available.
1234 opt_push_wait_flag_call_stack_quantifier_info(WF,QuantKind,Paras,ParaValues,Pos,WF2) :-
1235 simplify_span(Pos,SPos),
1236 opt_push_wait_flag_call_stack_info(WF,quantifier_call(QuantKind,Paras,ParaValues,SPos),WF2).
1237
1238 detect_quantifier_kind(prob_annotation('LAMBDA'),lambda).
1239 detect_quantifier_kind(quantifier_kind(QK),QK).
1240
1241 %init_wait_flags_and_push_call_stack(_,_,WF) :- !, init_wait_flags(WF). % comment in to disable tracking quantifiers
1242 % makes a difference for memoize test 1968 with recursive calls
1243 init_wait_flags_and_push_call_stack(OuterWF,CallStackTerm,WF) :-
1244 init_wait_flags_and_push_call_stack(OuterWF,CallStackTerm,[],WF).
1245 init_wait_flags_and_push_call_stack(OuterWF,CallStackTerm,OtherWFInfos,WF) :-
1246 get_call_stack(OuterWF,OuterCallStack),
1247 %print(init_quantifier(QuantKind,Paras,OuterCallStack)),nl,
1248 CallStack = [CallStackTerm|OuterCallStack],
1249 get_wf_all_dynamic_infos(OuterWF,DynInfos),
1250 copy_new_important_wf_infos(OuterWF,OtherWFInfos,NewWFInfos),
1251 init_wait_flags_with_sd_infos(WF,[call_stack(CallStack)|NewWFInfos],DynInfos).
1252
1253 init_wait_flags_with_call_stack(WF,CallStack) :-
1254 init_wait_flags_with_infos(WF,[call_stack(CallStack)]).
1255
1256 % the following is optimised for the fact that expect_explicit_value is the only important info
1257 % other than call_stack which is dealt with separately:
1258 copy_new_important_wf_infos(OuterWF,OtherWFInfos,NewWFInfos) :-
1259 (get_wait_flag_infos(OuterWF,OuterWFInfos),
1260 ? member(expect_explicit_value,OuterWFInfos),
1261 nonmember(expect_explicit_value,OtherWFInfos)
1262 -> NewWFInfos = [expect_explicit_value|OtherWFInfos]
1263 ; NewWFInfos = OtherWFInfos).
1264
1265 % :- use_module(library(lists),[include/3]).
1266 % get important static WF infos other than call-stack
1267 % call stack dealt with separately
1268 %get_important_wf_infos(WF,ImportantInfos) :-
1269 % get_wait_flag_infos(WF,Infos),
1270 % include(is_important,Infos,ImportantInfos).
1271 %is_important(expect_explicit_value).
1272
1273 % --------------
1274
1275 :- if((environ(prob_safe_mode,true) ; environ(prob_src_profile,true) ; environ(prob_profile,true))).
1276 % TODO: should this be controlled also by prob_profiling_on preference
1277 add_debug_wait_flag_info(Infos,Info,NewInfos) :- ord_add_element(Infos,Info,NewInfos).
1278 init_debug_wait_flag_info([],Infos) :- !, Infos=[].
1279 init_debug_wait_flag_info([H|T],Infos) :- !, Infos=[H|T].
1280 init_debug_wait_flag_info(Info,[Info]).
1281 :- else.
1282 add_debug_wait_flag_info(Infos,_,Infos).
1283 init_debug_wait_flag_info(_,[]).
1284 :- endif.
1285 % ------------------------
1286
1287 % BINARY CHOICE WAITFLAGS
1288
1289 :- use_module(tools_platform, [max_tagged_integer/1, max_tagged_pow2/1]).
1290 % last power of 2 exponent that is still a finite priority
1291 last_finite_pow2_prio_exponent(Lim) :- max_tagged_pow2(Pow),
1292 Lim is Pow-1. % stay below last_finite_priority, i.e., max_tagged_integer-1024
1293
1294 % utility to get power of two priority:
1295 get_pow2_binary_choice_priority(Exp,Prio) :- last_finite_pow2_prio_exponent(Lim),
1296 (Exp =< Lim -> Prio is floor(2**Exp)
1297 ; Prio is floor(2**Lim)).
1298
1299 % get a binary choice wait flag, start with 2 but for every further call double the priority (exponential backoff)
1300 % idea: give priority to data enumerations when too many choice points arise
1301 % TO DO: when triggering: keep the WF info with an empty trigger or store in separate info field
1302 get_binary_choice_wait_flag_exp_backoff(Info,WFX,WF2) :-
1303 get_binary_choice_wait_flag_exp_backoff(2,Info,WFX,WF2).
1304 get_binary_choice_wait_flag_exp_backoff(_,_Info,no_wf_available,WF2) :- !, WF2=2.
1305
1306 % StartPrio should normally be a power of 2:
1307 get_binary_choice_wait_flag_exp_backoff(MinPrio,Info,wfx(WF0,Store,WFE,_II),WF2) :-
1308 (nonvar(WFE) -> add_message(kernel_waitflags,'Getting waitflag from grounded store: ',Info),
1309 % probably a good idea to use clone_wait_flags_from1 if this happens
1310 WF2=WF0 % use at least WF0 for WF2, maybe it is still being enumerated
1311 ; my_get_wf_store_att(Store,Heap),
1312 large_finite_priority(Lim), % avoid creating too big numbers and stay in finite area
1313 (MinPrio < 1 -> StartPrio=1 ; StartPrio=MinPrio),
1314 get_bin_aux(StartPrio,Lim,Info,Heap,NewHeap,WF2),
1315 put_mutable_wf_store_attr(Store,NewHeap)
1316 ).
1317
1318 % to do : maybe store attribute of current exponential ??
1319 get_bin_aux(Prio,Lim,Info,Heap,NewHeap,WF2) :-
1320 avl_fetch(Prio,Heap,wf(WFs,OldInfo)),
1321 !,
1322 (%Prio >= Lim -> pop_waitflag(WFs,WF2,_), % should we get last waitflag or simply push
1323 % NewHeap=Heap ; /* for large finite priorities single waitflag stored */
1324 Prio<Lim, OldInfo = '$binary'(_)
1325 -> double_prio(Prio,P2), get_bin_aux(P2,Lim,Info,Heap,NewHeap,WF2)
1326 ; push_waitflag(WFs,WF2,WFs2),
1327 avl_store(Prio,Heap,wf(WFs2,'$binary'(Info)),NewHeap) % just update Info; so that next time we double
1328 ).
1329 get_bin_aux(Prio,_,Info,Heap,NewHeap,WF2) :- % we have found an unused power of 2
1330 avl_store(Prio,Heap,wf(WF2,'$binary'(Info)),NewHeap).
1331
1332 % ------------------------
1333
1334 get_enumeration_finished_wait_flag(wfx(_,_,WFE,_),Res) :- !,Res=WFE.
1335 get_enumeration_finished_wait_flag(no_wf_available,WFE) :- !,WFE=1.
1336 get_enumeration_finished_wait_flag(W,E) :-
1337 add_internal_error('Waitflags in wrong format: ',get_enumeration_finished_wait_flag(W,E)).
1338
1339
1340 ground_det_wait_flag(wfx(WF0,Store,_,WFInfos)) :- !, %% print(ground_det_wait_flag),nl,
1341 ? grd_wf0(WF0),
1342 deref_store(Store,DStore),
1343 init_wf_infos_for_grounding(WFInfos,WFInfos2),
1344 ? ground_waitflags_store_up_to_no_clpfd(1,DStore,WFInfos2). % no CLPFD labeling required for prio until 1
1345 ground_det_wait_flag(no_wf_available) :- !.
1346 ground_det_wait_flag(W) :-
1347 add_internal_error('Waitflags in wrong format: ',ground_det_wait_flag(W)).
1348
1349 ground_wait_flag_to(wfx(WF0,Store,_,WFInfos),Limit) :- !,%% print(ground_det_wait_flag),nl,
1350 grd_wf0(WF0),
1351 deref_store(Store,DStore),
1352 init_wf_infos_for_grounding(WFInfos,WFInfos2),
1353 ? ground_waitflags_store_clpfd_up_to(Limit,DStore,WFInfos2).
1354 ground_wait_flag_to(no_wf_available,_) :- !.
1355 ground_wait_flag_to(W,Limit) :-
1356 add_internal_error('Waitflags in wrong format: ',ground_wait_flag_to(W,Limit)).
1357
1358 useless_wait_flag(treat_next_integer(_VarID,Val,Rest)) :- Rest==[],
1359 kernel_tools:ground_value(Val).
1360 useless_wait_flag(tighter_enum(_VarID,Val,_Type)) :- %ground(Val).
1361 kernel_tools:ground_value(Val).
1362 %nonvar(Val), quick_ground(Val).
1363 %quick_ground(int(N)) :- integer(N).
1364 %quick_ground(string(S)) :- atom(S).
1365
1366 % show which waitflags are actually useless
1367 % TODO: think about pruning the WF store; e.g., when calling deref_store ??
1368 :- public portray_useless_waitflags_in_store/1.
1369 portray_useless_waitflags_in_store(Store) :-
1370 my_get_wf_store_att(Store,Heap),
1371 avl_member(AMin,Heap,wf(_,Info)),
1372 useless_wait_flag(Info),
1373 format(' useless waitflag ~w --> ~w~n',[AMin,Info]),
1374 fail.
1375 portray_useless_waitflags_in_store(_).
1376
1377
1378
1379 ground_waitflags_store_up_to_no_clpfd(Prio,Store,WFInfos) :- % print(prio(Prio)),nl,
1380 my_get_wf_store_att(Store,Heap), % portray_waitflags_store(Store), %
1381 ( avl_min(Heap,Min,_) -> % heap is non-empty, first element is WF with priority Min
1382 ( Min =< Prio -> % we have non-ground waitflags with a matching priority
1383 (avl_del_min_waitflag(Heap,AMin,wf(WFMin,Info),NewHeap),AMin==Min % remove the first element
1384 -> true
1385 ; add_internal_error('Could not remove min. in ground_waitflags_store_up_to_no_clpfd: ',Min:Info:Heap), fail
1386 ),
1387 put_mutable_wf_store_attr(Store,NewHeap), % write the modified heap back
1388 %% print(grounding2(Prio,_Info)),nl, %%
1389 ? ground_prio(Min,WFMin,Info,WFInfos),
1390 ground_waitflags_store_up_to_no_clpfd(Prio,Store,WFInfos) % continue recursively
1391 ; % no more matching waitflags present
1392 true) % stop here
1393 ; % heap is empty, nothing more to do
1394 true). % stop here
1395
1396 ground_waitflags_store_clpfd_up_to(Limit,Store,WFInfos) :-
1397 my_get_wf_store_fdvars_atts(Store,Heap,FDVars),
1398 !,
1399 ( avl_del_min_waitflag(Heap,Prio,wf(WFMin,Info),NewHeap),
1400 Prio =< Limit
1401 -> % we have non-ground waitflags with a matching priority
1402 ( my_get_next_fdvar_to_enumerate(FDVars,NextFDVar,RemainingFDVARS),
1403 fd_priority_leq_limit(NextFDVar,FDPrio,Limit)
1404 -> (FDPrio > Limit -> true
1405 ; enum_fd_variable_store(FDPrio,Store,NextFDVar,RemainingFDVARS,WFInfos))
1406 ; put_mutable_wf_store_attr(Store,NewHeap), % write the modified heap back
1407 ? ground_prio(Prio,WFMin,Info,WFInfos), % ground waitflag
1408 ground_waitflags_store_clpfd_up_to(Limit,Store,WFInfos) % continue recursively
1409 )
1410 ; % no pending waitflag
1411 my_get_next_fdvar_to_enumerate(FDVars,NextFDVar,RemainingFDVARS),
1412 fd_priority_leq_limit(NextFDVar,FDPrio,Limit)
1413 -> enum_fd_variable_store(FDPrio,Store,NextFDVar,RemainingFDVARS,WFInfos)
1414 ; true % heap and FDVars list is empty, nothing more to do
1415 ).
1416 ground_waitflags_store_clpfd_up_to(Limit,Store,WFInfos) :-
1417 add_internal_error('Illegal Waitflag: ',ground_waitflags_store_clpfd_up_to(Limit,Store,WFInfos)),fail.
1418
1419 % --------------------
1420
1421 :- assert_must_succeed(( kernel_waitflags:init_wait_flags(WF),
1422 kernel_waitflags:get_wait_flag(10001,test1,WF,WF1),
1423 kernel_waitflags:get_wait_flag(10001,test2,WF,WF2),
1424 check_eq(WF,wfx(_,Store,_,_)),
1425 kernel_waitflags:my_get_wf_store_fdvars_atts(Store,Heap,_FDVars),
1426 kernel_waitflags:avl_del_min_waitflag(Heap,Prio1,wf(WFMin1,_Info1),Heap2),
1427 check_eqeq(Prio1,10001), check_eqeq(WFMin1,WF1),
1428 kernel_waitflags:avl_del_min_waitflag(Heap2,Prio2,wf(WFMin2,_Info2),_),
1429 check_eqeq(Prio2,10001), check_eqeq(WFMin2,WF2)
1430 )).
1431
1432 % a conditional version of avl_del_min: where we either delete or update the minimal element
1433
1434 :- if(current_prolog_flag(dialect, swi)).
1435 avl_del_min_waitflag(AVL0, Key, wf(NextWF,Info), AVL) :-
1436 avl_del_min(AVL0,Key,Val0,AVL1),
1437 Val0 = wf(WFMin,Info),
1438 pop_waitflag(WFMin,NextWF,RemainingWFMin),
1439 (RemainingWFMin==[] -> AVL=AVL1
1440 ; avl_store(Key,AVL1,wf(RemainingWFMin,Info),AVL)
1441 ).
1442
1443 :- else.
1444 % optimized code to delete and update in one traversal; requires access to inner predicates of library(avl)
1445
1446 avl_del_min_waitflag(AVL0, Key, Val, AVL) :-
1447 avl_del_min_wf_aux(AVL0, Key, Val, AVL, _).
1448
1449 avl_del_min_wf_aux(node(K,V,B,L,R), Key, Val, AVL, Delta) :-
1450 ( L == empty ->
1451 Key = K,
1452 V = wf(WFMin,Info),
1453 pop_waitflag(WFMin,NextWF,RemainingWFMin),
1454 Val = wf(NextWF,Info),
1455 (RemainingWFMin==[] -> % single waitflag
1456 %print(single_wf(Key,WFMin,Info)),nl,
1457 AVL = R, Delta=1 % we delete the minimal element
1458 ; % there are multiple waitflags for the same priority
1459 % print(multiple_wf(Key,WFMin,Info)),nl,
1460 AVL = node(K,wf(RemainingWFMin,Info),B,L,R), % update AVL with remaining waitflags
1461 Delta = 0 % we do not delete the node, but update it
1462 )
1463 ; avl_del_min_wf_aux(L, Key, Val, L1, D1),
1464 B1 is B+D1,
1465 avl:avl(B1, K, V, L1, R, AVL),
1466 avl:avl_shrinkage(AVL, D1, Delta)
1467 ).
1468
1469 :- endif.
1470
1471 % -------------------
1472
1473 update_waitflag(Prio,CurrentWaitflag,NewWaitFlag,WF) :-
1474 /* if the CurrentWaitflag is already ground and now a new WF with lower priority has been added to the store:
1475 create a new non-ground waitflag to give priority to new WF with lower priority value */
1476 (var(CurrentWaitflag) -> NewWaitFlag=CurrentWaitflag
1477 ; WF=wfx(_WF0,Store,_,_),my_get_wf_store_att(Store,Heap),
1478 (avl_min(Heap,Min,wf(_NewerWF,_Info)),
1479 (is_inf_or_overflow_card(Prio) ; Min<Prio)
1480 -> get_waitflag_from_store(Prio,updated_wf,Store,NewWaitFlag) % could be optimized
1481 % ,print(updating_wf(Prio,CurrentWaitflag,NewWaitFlag,Min)),nl
1482 ; fdvar_with_higher_prio_exists(Store,Prio) -> get_waitflag_from_store(Prio,updated_wf,Store,NewWaitFlag)
1483 ; NewWaitFlag=CurrentWaitflag
1484 )
1485 ).
1486
1487 fdvar_with_higher_prio_exists(Store,Limit) :-
1488 my_get_fdvars_att(Store,FDVars),
1489 my_get_next_fdvar_to_enumerate(FDVars,NextFDVar,_),
1490 fd_priority_leq_limit(NextFDVar,_,Limit).
1491
1492 % get the minimum waitflag, if it exists
1493 get_minimum_waitflag_prio(wfx(WF0,Store,_,_),MinPrio,Info) :-
1494 (var(WF0) -> MinPrio=0, Info=wf0
1495 ; WF0=s(WF00), var(WF00) -> MinPrio = 1, Info=wf0_nonvar
1496 ; my_get_wf_store_att(Store,Heap),
1497 avl_min(Heap,MinPrio,wf(_LWF,Info))).
1498
1499
1500 add_wd_error(Msg,Term,WF) :-
1501 try_extract_span(Term,Span), % try extract span if possible;
1502 % e.g., for {x|x>10 } = res & card(res)=10 we have a closure/3 as Term
1503 add_wd_error_span(Msg,Term,Span,WF).
1504
1505 try_extract_span(closure(_,_,B),Span) :- !, Span=B.
1506 try_extract_span(b(_,_,Infos),Span) :- !, Span=Infos.
1507 try_extract_span(_,unknown).
1508
1509 add_wd_error_set_result(Msg,Term,Result,ResultValue,Span,WF) :-
1510 is_wd_guarded_result(Result), % just dummy co-routine to detect variables which have WD assignments pending on them; should not be enumerated
1511 % add well-definedness error but also set Result Variable to ResultValue to trigger pending co-routines if wd_guarded
1512 add_abort_error7(well_definedness_error,Msg,Term,Result,ResultValue,Span,WF).
1513
1514 add_wd_error_span(Msg,Term,Span,WF) :-
1515 add_abort_error_span(well_definedness_error,Msg,Term,Span,WF).
1516 % the same but adding a WD error directly, without any delay:
1517 add_wd_error_span_now(Msg,Term,Span,WF) :-
1518 add_abort_error2(true,well_definedness_error,Msg,Term,0,0,Span,WF).
1519
1520 % mark a variable as being wd_guarded
1521 % TODO: use put_wf_abort_pending(X).
1522 :- block is_wd_guarded_result(-).
1523 is_wd_guarded_result(string(X)) :- !, is_wd_guarded_result(X).
1524 is_wd_guarded_result(int(X)) :- !, is_wd_guarded_result(X).
1525 is_wd_guarded_result(fd(X,_)) :- !, is_wd_guarded_result(X).
1526 is_wd_guarded_result(_).
1527
1528 add_abort_error_span(ErrType,Msg,Term,Span,WF) :- add_abort_error7(ErrType,Msg,Term,0,0,Span,WF).
1529
1530
1531 :- use_module(probsrc(debug), [debug_mode/1]).
1532 add_abort_error7(_ErrType,_Msg,_Term,_Result,_ResultValue,_Span,_WF) :-
1533 preference(disprover_mode,true),
1534 !, % When Disproving we can assume well-definedness of the PO; sometimes the relevant hypotheses will be filtered out
1535 fail.
1536 add_abort_error7(ErrType,Msg,Term,Result,ResultValue,Span,WF) :-
1537 preference(raise_abort_immediately,F), F \= false,
1538 !,
1539 (F=full -> AWF=1 % really raise immediately; may entail more spurious messages, particularly in WF0
1540 ; get_idle_wait_flag(add_abort_error7,WF,AWF), %get_wait_flag0(WF,AWF),
1541 (var(AWF),debug_mode(on) ->
1542 (pending_abort_error(WF)
1543 -> format(user_output,'Additional WD Error pending:~n',[]) % TODO: no use in calling add_abort_error2 below
1544 ; true),
1545 add_message(wd_error_pending,Msg,Term,Span)
1546 ; true),
1547 mark_pending_abort_error(WF,Msg,Term,Span)
1548 ),
1549 %when(nonvar(AWF),
1550
1551 %(tools_printing:print_error('Raising error immediately without checking rest of predicate for unsatisfiability (because RAISE_ABORT_IMMEDIATELY set to TRUE): error could be spurious!'),true)),
1552 string_concatenate('Raising error immediately without checking rest of predicate for unsatisfiability (because RAISE_ABORT_IMMEDIATELY set to TRUE or full): error could be spurious!\n! ',Msg,NewMsg),
1553 add_abort_error2(AWF,ErrType,NewMsg,Term,Result,ResultValue,Span,WF).
1554 add_abort_error7(ErrType,Msg,Term,Result,ResultValue,Span,WF) :-
1555 %add_message_wf(add_abort_error,'Possible WD Error: ',Term,Span,WF), % happens a lot in test 1886
1556 mark_pending_abort_error(WF),
1557 get_enumeration_finished_wait_flag(WF,AWF), % infinite enumeration will never result in failure ? and thus never discard a WD error ? --> better to activate WD/abort error earlier, but the following does not fully work:
1558 %integer_priority(P), get_wait_flag(P,add_abort_error7,WF,AWF), % causes problem for test 1122
1559 add_abort_error2(AWF,ErrType,Msg,Term,Result,ResultValue,Span,WF).
1560
1561
1562 :- use_module(error_manager,[add_new_event_in_error_scope/1]).
1563 :- use_module(state_space,
1564 [store_abort_error_for_context_state_if_possible/4]).
1565 :- block add_abort_error2(-,?,?,?,?,?,?,?).
1566 add_abort_error2(wd_guarded,_Err,_Msg,_Term,Result,ResultValue,_Span,_WF) :- !,% ignoring error message; no-wd problem
1567 % set Result to default ResultValue; useful to get rid of pending co-routines; result will not be used
1568 (Result=ResultValue -> true ; print(add_abort_error_failure(Result,ResultValue)),nl).
1569 add_abort_error2(_AWF,ErrType,Msg,Term,_,_,Span,WF) :-
1570 add_call_stack_to_span(Span,WF,Span2),
1571 (register_abort_errors_in_error_scope(Level)
1572 -> (get_preference(provide_trace_information,false)
1573 -> format('Registering WD Error in error scope (~w): ~w~n',[Level,Msg])
1574 ; add_message_wf(wd_error,'Registering WD Error in error scope: ',Msg,Span,WF)
1575 ),
1576 assert(pending_inner_abort_error(Level,ErrType,Msg,Term,Span2))
1577 % ,trace,write(level(Level,ErrType)),nl,get_enumeration_finished_wait_flag(WF,WFE), when(nonvar(WFE),(write(abewf(Level,Msg)),nl,trace))
1578 % add_new_event_in_error_scope(abort_error(ErrType)) % do not register as error yet; we will copy it to the outer WF
1579 ; store_abort_error_for_context_state_if_possible(ErrType,Msg,Term,Span2)
1580 -> true
1581 ; add_error(add_abort_error2,'Could not store error: ',(Msg,Term),Span2)),
1582 % TODO: think about: throw(enumeration_warning('WD ERROR',ErrType,'','',throwing)), % TODO: throw and recognise as special error and treat e.g., in Keeping comprehension-set symbolic messages
1583 fail.
1584
1585 :- dynamic register_abort_errors_in_error_scope/0, pending_inner_abort_error/5.
1586
1587
1588 :- use_module(eventhandling,[register_event_listener/3]).
1589 :- register_event_listener(clear_specification,reset_waitflags, 'Reset kernel_waitflags.').
1590
1591 reset_waitflags :-
1592 retractall(register_abort_errors_in_error_scope),
1593 retractall(pending_inner_abort_error(_,_,_,_,_)),
1594 bb_put(wf_findall_nesting_level,0).
1595
1596 % clear pending inner abort errors
1597 % there is still a potential issue if a time-out appears just in the middle
1598 start_attach_inner_abort_errors(NewLevel,_PP) :-
1599 (bb_get(wf_findall_nesting_level,L) -> Level=L ; Level=0),
1600 NewLevel is Level+1,
1601 bb_put(wf_findall_nesting_level,NewLevel),
1602 %write(enter(NewLevel,PP)),nl,
1603 retractall(pending_inner_abort_error(NewLevel,_,_,_,_)).
1604
1605 % succeeds when abort errors should be asserted for later copying (at the end of a findall) to the outer WF
1606 register_abort_errors_in_error_scope(Level) :-
1607 register_abort_errors_in_error_scope,
1608 get_wf_findall_nesting_level(Level).
1609
1610 get_wf_findall_nesting_level(Level) :-
1611 (bb_get(wf_findall_nesting_level,L) -> Level=L
1612 ; write(missing_wf_findall_nesting_level),nl, Level=0).
1613
1614 % extract all pending inner abort errors and attach them to the outer WF store
1615 % should be called after ground_inner_wait_flags_in_context
1616 re_attach_pending_inner_abort_errors(Level,OuterWF,SomePending) :-
1617 get_wf_findall_nesting_level(L),
1618 %write(exit(L)),nl,
1619 (Level=L -> true
1620 ; write(unexpected_wf_findall_nesting(L,expected(Level))),nl
1621 % could happen if a time-out occured in middle of updating wf_findall_nesting_level info
1622 ),
1623 LL1 is Level-1, bb_put(wf_findall_nesting_level,LL1),
1624 findall(pending(ErrType,Msg,Term,Span),
1625 retract(pending_inner_abort_error(Level,ErrType,Msg,Term,Span)), PendingList),
1626 (PendingList=[]
1627 -> SomePending=none_pending
1628 ; SomePending=pending_abort_errors,
1629 % the next is useless when we call re_attach_pending_abort_errors in call_cleanup when the call failed
1630 maplist(re_add_pending_aux(OuterWF,LL1),PendingList)
1631 ).
1632
1633 re_add_pending_aux(WF,OuterLevel,pending(ErrType,Msg,Term,Span)) :-
1634 (get_preference(provide_trace_information,true), debug_mode(on)
1635 -> add_message_wf(wd_error,'Reattaching WD Error to outer WF: ',Msg,Span,WF)
1636 ; format('Reattaching error ~w in outer WF (~w)~n',[ErrType,OuterLevel])
1637 ),
1638 add_abort_error_span(ErrType,Msg,Term,Span,WF).
1639
1640 portray_pending :- pending_inner_abort_error(_Level,ErrType,Msg,Term,Span),
1641 add_message(ErrType,Msg,Term,Span),fail.
1642 portray_pending.
1643
1644 % add abort / state error directly (now), but do not fail unlike add_wd_error_span_now
1645 add_state_error_wf(ErrType,Msg,Term,Span,WF) :-
1646 add_call_stack_to_span(Span,WF,Span2),
1647 (store_abort_error_for_context_state_if_possible(ErrType,Msg,Term,Span2) -> true
1648 ; add_error_wf(ErrType,Msg,Term,Span2,WF)
1649 ).
1650
1651
1652 % ground enumeration finished waitflag unless abort is pending
1653 % useful inside of exists, ... to complete all pending co-routines
1654 ground_ef_wait_flag_unless_abort_pending(wfx(_WF0,_WFX,WFE,_)) :-
1655 var(WFE), %print(check_abort_pending(_WF0,_WFX,WFE)),nl,
1656 is_not_wf_abort_pending(WFE),
1657 !, %print(grd_ef(WFE)),nl,
1658 grd_ef(WFE).
1659 ground_ef_wait_flag_unless_abort_pending(_).
1660
1661 % special grounding of inner waitflags taking context (all_solutions, positive, negative) into account
1662 % one should call re_attach_pending_inner_abort_errors on the OuterWF after the forall/negation
1663 % in order to retract pending_inner_abort_error and re-attach the WD errors to the OuterWF
1664 ground_inner_wait_flags_in_context(all_solutions,WF) :-
1665 WF = wfx(_WF0,_WFX,WFE,_),!,
1666 ? ground_constraintprop_wait_flags(WF),
1667 (var(WFE),
1668 is_wf_abort_pending(WFE)
1669 -> !, % cut, we have found a WD error, whole findall result is useless anyway; cut
1670 % happens in tests 629, 1921, 1966, 2224
1671 debug_format(19,'WD Error(s) pending, could be spurious ~n',[]),
1672 assert(register_abort_errors_in_error_scope),
1673 call_cleanup(grd_ef(WFE), % will not raise WD errors but store them for OuterWF
1674 retract(register_abort_errors_in_error_scope))
1675 ; grd_ef(WFE)
1676 ).
1677 ground_inner_wait_flags_in_context(negative,WF) :- !,
1678 ground_inner_wait_flags_in_context(all_solutions,WF).
1679 ground_inner_wait_flags_in_context(_,WF) :-
1680 ground_wait_flags(WF). % TODO: do not ground WFE, ensure it is shared;
1681 % but currently positive context only used in external funs with wf_not_available
1682
1683
1684 % try and get a user-readable description of the context in which the WF store was created
1685 get_wait_flags_context_msg(wfx(_WF0,_WFX,_WFE,Infos),Msg) :-
1686 member(Info,Infos),
1687 get_info_context_description(Info,Msg).
1688
1689 :- use_module(bsyntaxtree, [get_texpr_ids/2]).
1690 get_info_context_description(call_stack(CS),Msg) :- translate_call_stack(CS,Msg).
1691 % TODO: do we need expansion_context anymore?
1692 get_info_context_description(expansion_context(Type,Parameters),Msg) :-
1693 (Parameters=[b(identifier(_),_,_)|_]
1694 -> get_texpr_ids(Parameters,Ids),
1695 get_msg_aux(Type,Ids,Parameters,Msg)
1696 ; get_msg_aux(Type,Parameters,[],Msg)
1697 ).
1698 get_info_context_description(expansion_context_with_pos(Type,Parameters,Info),Msg) :-
1699 get_msg_aux(Type,Parameters,Info,Msg).
1700 % also deal with : check_element_of_function_closure_nowf(MemoID)
1701
1702 get_msg_aux(Type,Parameters,Info,Msg) :-
1703 extract_span_description(Info,PosMsg),!, % we could do this only if preference trace_info set ?
1704 ajoin_with_sep(['expanding', Type, 'at', PosMsg, 'over ids'|Parameters],' ',Msg).
1705 get_msg_aux(Type,[],_Info,Msg) :- !,
1706 ajoin(['expanding ', Type],Msg).
1707 get_msg_aux(Type,Parameters,_Info,Msg) :-
1708 ajoin_with_sep(['expanding', Type, 'over ids'|Parameters],' ',Msg).
1709
1710
1711 % check whether an abort error is pending.
1712 pending_abort_error(wfx(_WF0,_WFX,WFE,_)) :- var(WFE),
1713 is_wf_abort_pending(WFE). %print(got_abort_pending),nl.
1714 % succeed once for every pending abort error in Waitflag store
1715 pending_abort_error(wfx(_WF0,_WFX,WFE,_),Msg,Term,Span) :- var(WFE),
1716 is_wf_abort_pending(WFE),
1717 frozen(WFE,Goal), %print(goal(Goal)),nl,
1718 pending_abort_error_aux(Goal,Msg,Term,Span).
1719
1720 pending_abort_error_aux(kernel_waitflags:add_abort_error2(_,_ErrType,Msg,Term,_Result,_ResultValue,Span,_), Msg,Term,Span).
1721 pending_abort_error_aux(add_abort_error2(_,_ErrType,Msg,Term,_Result,_ResultValue,Span,_), Msg,Term,Span).
1722 pending_abort_error_aux(kernel_waitflags:mark_pending_abort_error2(_,Msg,Term,Span), Msg,Term,Span).
1723 pending_abort_error_aux((A,B),Msg,Term,Span) :-
1724 (pending_abort_error_aux(A,Msg,Term,Span) ;
1725 pending_abort_error_aux(B,Msg,Term,Span) ).
1726
1727 % explicitly mark that an abort error is pending
1728 mark_pending_abort_error(wfx(_WF0,_WFX,WFE,_)) :- !, % print(mark_abort_pending(_WFX)),nl,
1729 (var(WFE) -> put_wf_abort_pending(WFE)
1730 ; true).
1731 mark_pending_abort_error(no_wf_available).
1732
1733 % explicitly mark that an abort error is pending with storing information
1734 mark_pending_abort_error(wfx(_WF0,_WFX,WFE,_),Msg,Term,Span) :-
1735 (var(WFE) -> put_wf_abort_pending(WFE),
1736 mark_pending_abort_error2(WFE,Msg,Term,Span)
1737 ; true).
1738 mark_pending_abort_error(no_wf_available,_Msg,_Term,_Span).
1739
1740 :- block mark_pending_abort_error2(-,?,?,?).
1741 mark_pending_abort_error2(_,_,_,_).
1742 % ---------------------------------------------
1743
1744
1745 get_large_finite_wait_flag(Info,WFX,WF2) :-
1746 large_finite_priority(P),
1747 get_wait_flag(P,Info,WFX,WF2).
1748
1749 get_enumeration_starting_wait_flag(Info,WFX,WF2) :-
1750 last_finite_priority(P),
1751 get_wait_flag(P,enumeration_starting(Info),WFX,WF2).
1752 %get_enumeration_almost_finished_wait_flag(Info,WFX,WF2) :-
1753 % max_tagged_integer(P), % largest tagged value
1754 % get_wait_flag(P,enumeration_starting(Info),WFX,WF2).
1755
1756
1757 get_integer_enumeration_wait_flag(Info,WFX,WF2) :-
1758 integer_priority(Prio),
1759 get_wait_flag(Prio,Info,WFX,WF2).
1760
1761 % A few hardcoded priorities
1762 large_finite_priority(P) :- integer_priority(I), P is I-1000.
1763 last_finite_priority(P) :- integer_priority(I), P is I-2. % Note: enumerate_integer_with_min_range_wf did set its priority to I-1
1764 %integer_priority(10000000). % old value
1765 integer_priority(Prio) :- % priority for X : INTEGER enumerations
1766 max_tagged_integer(P),
1767 Prio is P - 1024.
1768 % note inf_type_prio sets some priorities such as seq(INTEGER) ... higher
1769
1770 % priority for sets of infinite type (POW(INTEGER)...)
1771 integer_pow2_priority(Prio) :- % was 10000010
1772 integer_priority(P), Prio is P+10.
1773
1774 last_priority(P) :- % was 10000010
1775 max_tagged_integer(P).
1776
1777 % ensure that we do not exceed priority of type enumeration or use too big numbers
1778 get_bounded_wait_flag(Prio,Info,WF,LWF) :-
1779 get_bounded_priority(Prio,P),
1780 ? get_wait_flag(P,Info,WF,LWF).
1781
1782 get_bounded_priority(Prio,P) :- number(Prio),
1783 Prio>268435452, % 268435455 is max_tagged_integer on 32 bit platforms
1784 last_finite_priority(MAX),
1785 Prio>MAX,
1786 !, P=MAX.
1787 get_bounded_priority(P,P).
1788
1789 % -------------
1790
1791 % copy waitflags from one waitflag store to another; warning: can ground WF0 from outer store
1792 % the assumption is that the outer store will be grounded/enumerated
1793 % the inner store 1 will now point to the outer store 2 in case some co-routines still add waitflags
1794 copy_waitflag_store(wfx(WF0,Store1,WFE1,_),wfx(WF0,Store2,WFE2,_Info2)) :-
1795 %print(copy_wf(WF0,Store1,Store2,WFE1,WFE2)),nl,
1796 my_get_wf_store_fdvars_atts(Store1,Heap,FDList1),
1797 (FDList1 = [] -> true
1798 ; my_get_fdvars_att(Store2,FDList2),
1799 %append(FDList1,FDList2,NewFDList), % used to be like this
1800 append_wf(FDList2,FDList1,NewFDList), % now we add inner FD variables to end
1801 put_mutable_wf_fdvars_attr(Store2,NewFDList)
1802 ),
1803 avl_to_list(Heap,WF_List),
1804 %print(copying(FDList1,WF_List)),nl,
1805 my_get_wf_store_att(Store2,Heap2),
1806 add_wf(WF_List,Heap2,NewHeap2),
1807 put_mutable_wf_store_attr(Store2,NewHeap2),
1808 set_mutable_ref(Store1,Store2),
1809 % ensures that calls which add waitflags now get-redirected to waitflag store 2
1810 % get_ef from Store2 and add trigger to enumerate Store1?
1811 %portray_waitflags(wfx(WF0,Store2,WFE2,Info2)),
1812 WFE1=WFE2.
1813
1814 append_wf([],FDL,FDL).
1815 append_wf([H|T],FDL2,Res) :-
1816 (ground(H) -> append_wf(T,FDL2,Res) ; Res=[H|RT], append_wf(T,FDL2,RT)).
1817
1818 % Note: add_wf will construct multiple WF variables also for finite_priorities,
1819 % get_waitflag_from_store will only keep multiple entries for infinite ones
1820 add_wf([],Heap,Heap).
1821 add_wf([Prio-wf(WF1,Info)|T],Heap,NewHeap) :-
1822 % purpose: copy waitflag WFlag to WF store; if same priority exists it will be appended at end
1823 P=Prio,
1824 (avl_fetch(P,Heap,wf(WFs,_OldInfo))
1825 -> % priority waitflag(s) exist; add inner store WF1 at end
1826 merge_waitflag_queues(WF1,WFs,MergedWFs), % TO DO: just unify WF 1 and 0.9 or smaller ?
1827 avl_store(P,Heap,wf(MergedWFs,Info),Heap2)
1828 ; % this priority does not yet exist in outer store
1829 avl_store(P,Heap,wf(WF1,Info),Heap2)
1830 ),
1831 add_wf(T,Heap2,NewHeap).
1832
1833
1834 % try and find an exact match for a waitflag info; this is linear in size of waitflag store !
1835 find_waitflag_info(wfx(_WF0,Store,_WFE1,_),Info,Prio,WF1) :-
1836 my_get_wf_store_att(Store,Heap),
1837 avl_member(Prio,Heap,wf(WF1,Info)).
1838
1839 % dereference the waitflag store, see SICStus for SPRM-20503
1840 % should be called e.g., in WHILE loops of interpreter to prevent degradation of put_atts performance
1841 deref_wf(wfx(WF0,S,EF,I),R) :- !, R=wfx(WF0,S2,EF,I), deref_store(S,S2).
1842 deref_wf(WF,WF).
1843
1844 % D is the dereferenced value of V.
1845 % see email by SICStus for SPRM-20503; gets rid of variable chains; was useful for old Waitflag store with attributes
1846 %deref(V,D) :- var(V), !, D = V.
1847 %deref(X,X).
1848
1849 % --------------------------
1850 % DEBUGGING UTILITIES:
1851
1852 % you also need to comment in code above using it
1853 /*
1854 :- dynamic debug_kernel_waitflags/1.
1855 set_debug_kernel_waitflags :- (debug_kernel_waitflags(_) -> true ; assertz(debug_kernel_waitflags(0))).
1856
1857 % the counter allows to set trace points
1858 get_debug_kernel_waitflags(Counter) :- retract(debug_kernel_waitflags(C)), C1 is C+1,
1859 assertz(debug_kernel_waitflags(C1)), Counter=C1.
1860
1861 get_debug_info(Info,Res) :- debug_kernel_waitflags(Counter),!,
1862 (Counter==39 -> trace ; true),
1863 Res=info(Counter,Info).
1864 get_debug_info(Info,Info).
1865 */
1866
1867 % check that a WF is grounded before EWF is grounded:
1868 :- public check_grounding/3. %debugging predicate
1869 check_grounding(WF,Info,LWF) :- get_enumeration_finished_wait_flag(WF,EWF), check_grounding_of_wf(WF,Info,LWF,EWF).
1870 :- block check_grounding_of_wf(?,?,-,-).
1871 check_grounding_of_wf(_,_,LWF,_) :- nonvar(LWF),!.
1872 check_grounding_of_wf(WF,Info,LWF,_EWF) :- add_internal_error('Waitflag not grounded: ',check_grounding(WF,Info,LWF)),
1873 portray_waitflags(WF),nl.
1874
1875 % --------------------------
1876
1877 :- assert_must_succeed(( kernel_waitflags:test_waitflags(1) )).
1878 :- assert_must_succeed(( kernel_waitflags:test_waitflags(2) )).
1879
1880 test_waitflags(1) :-
1881 init_wait_flags(Waitflags,[test_waitflags]),
1882 get_wait_flag(10,Waitflags,WF1),
1883 when(nonvar(WF1),print('WF1 - Prio 10\n')),
1884 get_wait_flag(5,Waitflags,WF2),
1885 when(nonvar(WF2),(print('WF2 - Prio 5\n'),
1886 get_wait_flag(6,Waitflags,WF4),
1887 when(nonvar(WF4),print('WF4 - Prio 6\n')),
1888 get_wait_flag(2,Waitflags,WF5),
1889 when(nonvar(WF5),print('WF5 - Prio2\n')))),
1890 get_wait_flag(5,Waitflags,WF3),
1891 when(nonvar(WF3),print('WF3 - Prio 5\n')),
1892 ground_wait_flags(Waitflags),nl.
1893
1894 test_waitflags(2) :-
1895 init_wait_flags(Waitflags,[test_waitflags]),
1896 get_wait_flag(10,Waitflags,WF1),
1897 when(nonvar(WF1),print('WF1 Prio 10\n')),
1898 get_wait_flag(5,Waitflags,WF2),
1899 when(nonvar(WF2),(print('WF2 - Prio 5\n'),
1900 get_wait_flag(6,Waitflags,WF4),
1901 when(nonvar(WF4),print('WF4 - Prio 6\n')),
1902 get_wait_flag(2,Waitflags,WF5),
1903 when(nonvar(WF5),print('WF5 - Prio2\n')))),
1904 get_wait_flag(5,Waitflags,WF3),
1905 when(nonvar(WF3),print('WF3 - Prio 5\n')),
1906 ground_wait_flags(Waitflags),nl.
1907
1908
1909 /*
1910
1911 bench_waitflags(N) :-
1912 statistics(walltime,[Tot1,_]),
1913 init_wait_flags(Waitflags),
1914 getwf(N,Waitflags),
1915 ground_wait_flags(Waitflags),nl,statistics(walltime,[Tot2,_]), Tot is Tot2-Tot1,
1916 format('Waitflag test for size ~w : ~w ms walltime (wf=~w)]~n',[N,Tot,Waitflags]).
1917 getwf(0,_).
1918 getwf(N,Waitflags) :- N>0, N1 is N-1, get_wait_flag(N,bench(N),Waitflags,_), getwf(N1,Waitflags).
1919
1920 % old attribute based:
1921 | ?- kernel_waitflags:bench_waitflags(1000).
1922
1923 Waitflag test for size 1000 : 37 ms walltime (wf=wfx(0,_205205,0,[]))]
1924 yes
1925 | ?- kernel_waitflags:bench_waitflags(10000).
1926
1927 Waitflag test for size 10000 : 5859 ms walltime (wf=wfx(0,_2512071,0,[]))]
1928 yes
1929
1930 % new mutable based:
1931 | ?- kernel_waitflags:bench_waitflags(1000).
1932
1933 Waitflag test for size 1000 : 4 ms walltime (wf=wfx(0,$mutable(wfm_store(empty,[],[]),3008),0,[]))]
1934 yes
1935 | ?- kernel_waitflags:bench_waitflags(10000).
1936
1937 Waitflag test for size 10000 : 24 ms walltime (wf=wfx(0,$mutable(wfm_store(empty,[],[]),30008),0,[]))]
1938 yes
1939 | ?- kernel_waitflags:bench_waitflags(100000).
1940
1941 Waitflag test for size 100000 : 497 ms walltime (wf=wfx(0,$mutable(wfm_store(empty,[],[]),9),0,[]))]
1942 yes
1943
1944 */