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