1		% (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5
6		:- module(kernel_waitflags,
7		[init_wait_flags/1, waitflag0_is_set/1,
8		get_wait_flag_infos/2, get_wait_flag_info/2, is_wait_flag_info/2,
9		add_wait_flag_info/3,
10		get_wait_flag/3, get_wait_flag/4, get_bounded_wait_flag/4,
11		block_get_wait_flag/4,
12		get_wait_flag0/2,
13		get_wait_flag1/2, get_wait_flag1/3, % deterministic wait flag
14		get_middle_wait_flag/3, get_last_wait_flag/3,
15		get_idle_wait_flag/3,
16		get_binary_choice_wait_flag/3,
17		get_pow2_binary_choice_priority/2,
18		get_binary_choice_wait_flag_exp_backoff/3, get_binary_choice_wait_flag_exp_backoff/4,
19		%refresh_wait_flag/4,
20		add_fd_variable_for_labeling/3, add_fd_variable_for_labeling/2, add_fd_variables_for_labeling/2,
21		get_new_subsidiary_wait_flag/4,
22		update_waitflag/4,
23		ground_constraintprop_wait_flags/1,
24		check_is_wait_flag/1,
25		no_pending_waitflags/1,
26		create_inner_wait_flags/3, copy_wf01e_wait_flags/2,
27		copy_wf_start/2, copy_wf_finish/2,
28		copy_waitflag_store/2,
29
30		clone_wait_flags_from1/2, clone_wait_flags_from1_finish/2,
31		ground_wait_flag0/1,
32		%create_wdguarded_wait_flags/4,
33		%get_abort_error_flag/2,
34		get_large_finite_wait_flag/3,
35		get_enumeration_starting_wait_flag/3, ground_wait_flag_to_enumeration/1,
36		get_enumeration_finished_wait_flag/2,
37		get_integer_enumeration_wait_flag/3,
38		ground_det_wait_flag/1, ground_wait_flag_to/2,
39		ground_wait_flags/1, ground_inner_wait_flags/1,
40
41		add_abort_error_span/5,
42		add_wd_error_span/4,
43		add_wd_error/3, add_wd_error_set_result/6,
44		pending_abort_error/1, pending_abort_error/4,
45		%add_wd_error_span_now/3,
46		assert_must_abort_wf/2,
47
48		get_minimum_waitflag_prio/3,
49		portray_waitflags/1, quick_portray_waitflags/1, quick_portray_waitflags_store/1,
50		find_waitflag_info/4,
51
52		integer_priority/1, large_finite_priority/1, integer_pow2_priority/1,
53
54		my_get_kodkod_predicates/3, my_add_predicate_to_kodkod/3,
55		my_get_satsolver_predicates/3, my_add_predicate_to_satsolver/3,
56
57		set_silent/1]).
58		/* File: kernel_waitflags.pl */
59		/* Created: 17/3/06 by Michael Leuschel */
60
61		/*
62		Phases of the ProB Kernel:
63
64		-> all Waitflags unbound
65
66		* Phase 0: propagation of completely known ground values in a deterministic fashion
67
68		-> WF0 is bound
69
70		* Phase 1: deterministic propagation (not necessarily of completely known full values)
71
72		-> WF1 is bound
73
74		* Phase 2: boolean propagation (e.g., P or Q will now try P or Q)
75
76		-> WF2 is bound
77
78		* Phase 3: non-deterministic propagation (e.g, x: {1,2,3})
79
80		-> Enumeration Starting WF is bound
81
82		* Enumeration Phase: (later to be split into enumeration of finite and infinite types (e.g., integer)
83
84		-> Enumeration Finished Waitflag bound
85
86		* Error Generation Phase: errors for, e.g., division by zero, f(x) with x outside domain of f,... are generated
87		* This phase should not create choice points and should not detect failure
88		(e.g., in the
89		case of negated existential quantifiers the Enumeration Finished Waitflag will be set outside of delay_not)
90
91
92		We now distinguish
93		- Enumeration Wait Flags for Decision Variables with estimated enumeration domain size as priority
94		- Binary Choice Point Wait Flags (stemming e.g. from disjunctions)
95
96		Note: all floats like 1.0, 1.5, 2.0 ... are dealt with before all integers (even 1) !
97
98		*/
99
100		:- use_module(error_manager).
101		:- use_module(self_check).
102		:- use_module(typechecker).
103		:- use_module(library(clpfd),[labeling/2, fd_size/2, fd_degree/2]).
104		:- use_module(tools).
105		:- use_module(coverage_tools_annotations,['$NOT_COVERED'/1]).
106		:- use_module(preferences,[preference/2]).
107
108		:- use_module(module_information,[module_info/2]).
109		:- module_info(group,kernel).
110		:- module_info(description,'This module manages the various choice points and enumerators of ProB, by maintaining the kernel Waitflags store.').
111
112		:- type wait_flag +--> (var ; wfx(any,var,any,list(any)) ; no_wf_available).
113
114		:- use_module(library(avl)).
115		:- use_module(library(atts)).
116
117		:- attribute wf_store/1,wf_fdvars/1, wf_kodkod/2, wf_satsolver/2, wf_abort_pending/0.
118
119		% the Call must succeed and generate one abort_error
120		:- meta_predicate assert_must_abort_wf(0,*).
121		%:- meta_predicate assert_must_abort2_wf(0,-).
122		assert_must_abort_wf(M:Call,WF) :- assert_must_succeed_any(M:(kernel_waitflags:assert_must_abort2_wf(M:Call,WF))).
123
124		assert_must_abort2_wf(_,_) :- get_error(well_definedness_error,M),
125		add_internal_error('Abort error prior to call in assert_must_abort: ',M),fail.
126		assert_must_abort2_wf(Call,WF) :- (real_error_occurred -> RE=true ; RE=false),
127		init_wait_flags(WF),
128		call(Call), %print(called(Call)),nl,
129		(ground_wait_flags(WF)
130		-> add_internal_error('Call did not fail after grounding WF: ',assert_must_abort2_wf(Call,WF)),fail
131		; (get_error(well_definedness_error,_), % we have 1 abort_error
132		print(got_expected_well_definedness_error),nl,
133		(RE=false -> reset_real_error_occurred ; true)
134		)
135		).
136
137		:- assert_must_succeed(( kernel_waitflags:init_wait_flags(WF), kernel_waitflags:check_is_wait_flag(WF) )).
138
139		check_is_wait_flag(WFX) :- var(WFX),!,
140		add_internal_error('Variable as waitflag: ',check_is_wait_flag(WFX)).
141		check_is_wait_flag(WFX) :-
142		WFX = wfx(_,Store,_,_)
143		-> (get_atts(Store,+wf_store(_))
144		-> true
145		; print('WF does not yet contain heap: '), print(WFX),nl)
146		%add_internal_error('WF does not contain heap: ',check_is_wait_flag(WFX)))
147		; add_internal_error('Illegal WF Format: ',check_is_wait_flag(WFX)).
148
149		verify_attributes(Var, Value, [] ) :- get_atts(Var,+wf_abort_pending),!,
150		% we are unifying the EWF enumeration finished waitflag, not the store
151		(nonvar(Value) -> true ; print(verify_attributes),nl).
152		verify_attributes(Var, Value, [] ) :-
153		nonvar(Value) -> print('Trying to unify waitflag_heap_store'),nl
154		; print(verify_attributes(Var,Value)),nl.
155
156		init_wait_flags(wfx(_,_,_,[])).
157		%init_wait_flags(wfx(_,Store,_,[])) :- init_wait_flags_store(Store).
158		% we no longer do this because of performance, (see, e.g., LotsOfInvariants.mch) :
159		init_wait_flags_store(_).
160		%init_wait_flags_store(Store) :-
161		% empty_avl(Heap),
162		% put_atts(Store,+wf_store(Heap)),
163		% put_atts(Store,+wf_fdvars([])).
164
165
166		:- assert_must_succeed(( kernel_waitflags:init_wait_flags(WF),
167		kernel_waitflags:ground_wait_flag0(WF), kernel_waitflags:waitflag0_is_set(WF) )).
168		:- assert_must_fail(( kernel_waitflags:init_wait_flags(WF), kernel_waitflags:waitflag0_is_set(WF) )).
169		waitflag0_is_set(wfx(WF0,_Store,_EF,_INFOS)) :- ground(WF0).
170		waitflag0_is_set(no_wf_available).
171
172		get_new_subsidiary_wait_flag(OldWF,Info,WFX,NewWF) :-
173		(ground(OldWF) /* then we have created a choice point with the old WF: double new WF prio */
174		-> NewPrio is OldWF*2, get_wait_flag(NewPrio,Info,WFX,NewWF)
175		; NewWF = OldWF
176		).
177
178		% not used at the moment:
179		%refresh_wait_flag(OldWF,Info,WFX,NewWF) :-
180		% (ground(OldWF) /* then we have created a choice point with the old WF: double new WF prio */
181		% -> get_wait_flag(OldWF,Info,WFX,NewWF)
182		% ; NewWF = OldWF
183		% ).
184
185		:- volatile silent/0.
186		:- dynamic silent/0.
187		set_silent(true) :- !,(silent -> true ; assert(silent)).
188		set_silent(false) :- retractall(silent).
189		%waitflag_not_init :- silent -> true ; print('waitflag-store not initialised'),nl, '$NOT_COVERED'('This should not happen').
190
191		:- use_module(eventhandling,[register_event_listener/3]).
192		:- register_event_listener(start_unit_tests,set_silent(true),'Allow wf not to be set up without printing a warning').
193		:- register_event_listener(stop_unit_tests, set_silent(false), 'Printing wf warnings again').
194
195		:- use_module(library(lists),[maplist/2]).
196		add_fd_variables_for_labeling(Vars,WF) :- WF==no_wf_available,!,
197		add_internal_error('Cannot add FDVars to waitflag store: ',Vars).
198		add_fd_variables_for_labeling(Vars,WF) :-
199		WF=wfx(_,Store,_EnumFinished,_INFOS),
200		!,
201		my_get_fdvars_atts(Store,FDVARS),
202		l_add_fd_var_to_FDVARS(Vars,FDVARS,NewFDVARS),
203		put_atts(Store,+wf_fdvars(NewFDVARS)).
204		add_fd_variables_for_labeling(Vars,WF) :-
205		add_internal_error('Illegal waitflag store: ',add_fd_variables_for_labeling(Vars,WF)).
206
207		l_add_fd_var_to_FDVARS([],Acc,Acc).
208		l_add_fd_var_to_FDVARS([Var|VT],FDVARS,NewFDVARS) :-
209		(nonvar(Var) -> F2=FDVARS; add_fd_var_to_FDVARS(Var,FDVARS,F2)),
210		l_add_fd_var_to_FDVARS(VT,F2,NewFDVARS).
211
212		% adds a CLP(FD) variable with given domain Size, will be enumerated by labeling (even if clpfd_solver preference is false !)
213		% Size could be computed by fd_size(FDVariable,Size)
214		add_fd_variable_for_labeling(FDVariable,WF) :-
215		add_fd_variable_for_labeling_aux(FDVariable,WF).
216		add_fd_variable_for_labeling(FDVariable,Size,WF) :- Size = not_used_anymore,
217		add_fd_variable_for_labeling_aux(FDVariable,WF).
218
219
220		add_fd_variable_for_labeling_aux(FDVariable,_WF) :- nonvar(FDVariable),!.
221		add_fd_variable_for_labeling_aux(FDVariable,WF) :-
222		% otherwise: store the FDVariable in the separate list of FD Variables (all mixed together)
223		WF=wfx(_,Store,_EnumFinished,_),
224		my_get_fdvars_atts(Store,FDVARS),
225		add_fd_var_to_FDVARS(FDVariable,FDVARS,NewFDVARS),
226		%% fd_size(FDVariable,Size),print(added(FDVariable,Size,NewFDVARS,old(FDVARS))),nl,
227		%% print(added_fd_variable(FDVariable,_Size,NewFDVARS)),nl,portray_waitflags_store(Store),nl,nl,%%
228		put_atts(Store,+wf_fdvars(NewFDVARS)).
229
230		add_fd_var_to_FDVARS(FDVariable,FDVARS,NewFDVARS) :-
231		%insert_fd_var(FDVARS,FDVariable,Size,LWF,NewFDVARS),
232		(FDVARS=[HH|_],HH==FDVariable -> NewFDVARS = FDVARS % variable already in list [cheap check at front]
233		; NewFDVARS = [FDVariable|FDVARS]). %% this adds new variables at front; will be given priority over older ones
234		%% add_fd_var(FDVARS,FDVariable,NewFDVARS), %% this adds new variables at the end and does more thorough duplicate check
235
236
237		% a bit like append: but cleans up list: removes numbers + checks if var already in list
238		% runtimes for tests: 349 stays at 220ms, test 1088 4660 -> 5040ms
239		%add_fd_var([],Var,[Var]).
240		%add_fd_var([V|T],Var,Res) :-
241		% (V==Var -> Res = [V|T] %,print(dup(V)),nl,
242		% ; nonvar(V) -> add_fd_var(T,Var,Res) %,print(nonvar(V)),nl
243		% ; Res = [V|RT], add_fd_var(T,Var,RT)).
244
245		my_get_fdvars_atts(Store,FDVARS) :-
246		(get_atts(Store,+wf_fdvars(FDVARS)) -> true
247		; var(Store),FDVARS=[]
248		).
249		/* store not initialised; initialise it below but print msg */
250		% ,waitflag_not_init).
251
252		:- use_module(library(random),[random_select/3]).
253		% reverse the list at each step; alternating taking from end and front; makes no sense with randomise_enumeration_order
254		%my_get_next_fdvar_to_enumerate_rev(FDVARS,NextFDVar,RemainingFDVARS) :- lists:reverse(FDVARS,RevFDVARS),
255		% my_get_next_fdvar_to_enumerate(RevFDVARS,NextFDVar,RemainingFDVARS).
256
257		my_get_next_fdvar_to_enumerate([],_NextFDVar,_RemainingFDVARS) :- !,fail.
258		my_get_next_fdvar_to_enumerate([V1|FDVARS],NextFDVar,RemainingFDVARS) :-
259		nonvar(V1),
260		!, % 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 !
261		my_get_next_fdvar_to_enumerate(FDVARS,NextFDVar,RemainingFDVARS).
262		my_get_next_fdvar_to_enumerate(FDVARS,NextFDVar,RemainingFDVARS) :-
263		preferences:preference(randomise_enumeration_order,true),
264		!,
265		get_min_fd_size_elements(FDVARS,MinFDVars),
266		random_select(NextFDVar,MinFDVars,_),
267		%print(random_enum(NextFDVar,FDVARS,MinFDVars)),nl,
268		RemainingFDVARS=FDVARS. % still contains variable; but no problem as it will be discarded later
269		my_get_next_fdvar_to_enumerate(FDVARS,NextFDVar,RemainingFDVARS) :-
270		%clpfd_interface:clpfd_get_next_variable_to_label_ffc(FDVARS,NextFDVar,RemainingFDVARS).
271		clpfd_interface:clpfd_get_next_variable_to_label(FDVARS,NextFDVar),
272		% print(enumerating(NextFDVar,FDVARS)),nl, maplist(tools_printing:print_arg,FDVARS),nl,
273		RemainingFDVARS=FDVARS.
274		% ((FDVARS=[H|T],H==NextFDVar) -> RemainingFDVARS=T ; RemainingFDVARS=FDVARS).% does not seem to buy any speed
275
276		get_min_fd_size_elements([V1|FDVARS],MinFDVars) :- my_get_fd_size(V1,Size),
277		get_min_aux(FDVARS,Size,[V1],MinFDVars).
278
279		get_min_aux([],_,MinFDVars,MinFDVars).
280		get_min_aux([V1|FDVARS],Size,MAcc,MinFDVars) :- number(V1),!,
281		get_min_aux(FDVARS,Size,MAcc,MinFDVars).
282		get_min_aux([V1|FDVARS],Size,MAcc,MinFDVars) :-
283		my_get_fd_size(V1,Size1),
284		(lt_size(Size1,Size)
285		-> get_min_aux(FDVARS,Size1,[V1],MinFDVars)
286		; Size1=Size -> get_min_aux(FDVARS,Size,[V1|MAcc],MinFDVars)
287		; get_min_aux(FDVARS,Size,MAcc,MinFDVars)
288		).
289
290		lt_size(X,Y) :- number(X),(Y=sup -> true ; X<Y).
291
292		% -------------
293
294		% using this is relevant for e.g. tests 415, 416, 1096 : to give variables without frozen goals a lower priority
295		% TO DO: we could filter out those before we call clpfd_get_next_variable_to_label !?
296		fd_priority_leq_limit(FDVAR,Prio,Limit) :-
297		my_get_fd_size(FDVAR,Size),
298		number(Size), % not =sup or =inf
299		geq_limit(Limit,Size), % the calculation below will only increase the Size
300		(Size < 2 -> Prio = Size
301		; geq_limit(Limit,Size*4) -> Prio = Size % avoid calling frozen and fd_degree, Priority only used for warnings and bisect decisions
302		; %print(sz(Size,Limit)),nl,
303		(enumeration_only_fdvar(FDVAR) -> Prio is Size*4, Prio =< Limit
304		; Prio = Size)
305		).
306
307		my_get_fd_size(FDVAR,ResSize) :- fd_size(FDVAR,Size),!, ResSize=Size.
308		%(Size=sup -> ResSize = 10000000 /* same as for inf */ ; ResSize=Size).
309		my_get_fd_size(FDVAR,Size) :- add_internal_error('Could not get fd_size: ',my_get_fd_size(FDVAR,Size)), Size=sup.
310
311		gt_limit(inf,_) :- !.
312		gt_limit(sup,_) :- !.
313		gt_limit(X,Limit) :- X > Limit.
314
315		geq_limit(inf,_) :- !.
316		geq_limit(sup,_) :- !.
317		geq_limit(X,Limit) :- X >= Limit.
318
319
320
321		% -------------
322
323
324		enumeration_only_fdvar(FDVAR) :- var(FDVAR),fd_degree(FDVAR,D),!,
325		D=0,
326		frozen(FDVAR,Goal), %print(frozen(FDVAR,D,Goal)),nl,
327		enum_only_frozen_goal(Goal,FDVAR).
328		enumeration_only_fdvar(_).
329
330		% TO DO: maybe use enumeration_only_goal in b_enumerate
331		enum_only_frozen_goal((A,B),Var) :- !, enum_only_frozen_goal(A,Var), enum_only_frozen_goal(B,Var).
332		enum_only_frozen_goal(clpfd:_,_) :- !.
333		enum_only_frozen_goal(kernel_objects:G,V) :- !, enum_only_frozen_goal_k_obj(G,V).
334		enum_only_frozen_goal(true,_).
335
336		enum_only_frozen_goal_k_obj(safe_less_than_equal(_,X,Y),_) :- (number(X);number(Y)), !.
337		enum_only_frozen_goal_k_obj(call_enumerate_int(X,_,_,_),Var) :- Var==X,!.
338		enum_only_frozen_goal_k_obj(enumerate_int_wf(X,_,_),Var) :- Var==X,!.
339		enum_only_frozen_goal_k_obj(true,_).
340
341
342		% get a wait-flag that will be triggered first next time;
343		% can be used to ensure that all pending co-routines complete
344		get_idle_wait_flag(Info,wfx(WF0,Store,EnumFinished,_),LWF) :- !,
345		(var(WF0) -> LWF=WF0
346		; nonvar(EnumFinished) -> LWF=1 % waitflag store already grounded to completion; nobody may drive it anymore
347		; get_waitflag_from_store(0.9,Info,Store,LWF)).
348		get_idle_wait_flag(_Info,no_wf_available,1).
349
350
351		get_wait_flag(Prio,Store,WF) :- get_wait_flag(Prio,'??',Store,WF).
352		get_wait_flag(0,_Info,wfx(WF0,_Store,_EnumFinished,_),WF) :- !, WF=WF0.
353		get_wait_flag(1.0,Info,wfx(WF0,Store,_EnumFinished,_),WF) :- !,
354		(var(WF0) -> get_waitflag_from_store(1.0,Info,Store,WF) ; WF=1).
355		get_wait_flag(Prio,Info,wfx(_,Store,EnumFinished,_),WF) :- !,
356		(ground(EnumFinished) -> WF=Prio /* enumeration has finished: return a ground WF */
357		; get_waitflag_from_store(Prio,Info,Store,WF)).
358		get_wait_flag(Prio,Info,Store,WF) :-
359		(Store=no_wf_available -> WF=Prio ;
360		Store=none -> print(get_wait_flag_deprecated(Prio,Info,Store,WF)),nl, WF=Prio ;
361		add_internal_error('Illegal call: ',get_wait_flag(Prio,Info,Store,WF))).
362
363		get_waitflag_from_store(Prio,Info,Store,WF) :-
364		%get_debug_info(Info0,Info),
365		% print(get_waitflag_from_store(Prio,Info,Store,WF)),nl,
366		(Prio=inf -> integer_priority(X), RealPrio = float(X)
367		% , print(infinite_priority(Prio,Info)),nl %%
368		% ; (Prio>10, Prio<10000) -> RealPrio = float(100) % perform left-to-right enumeration in that range
369		; RealPrio=float(Prio)),
370		my_get_wf_store_atts(Store,Heap),
371		(avl_fetch(RealPrio,Heap,wf(WFs,_OldInfo))
372		-> (is_finite_priority(RealPrio) % TO DO: investigate performance if reduce the threshold
373		-> WF1 = WFs % here we re-use the waitflag instead of storing a new one
374		; (var(WFs) -> WFs2 = [WF1,WFs] ; WFs2 = [WF1|WFs]), % else: store waitflags as list; important for test 1194
375		%print(not_reusing(WFs2)),nl,
376		avl_store(RealPrio,Heap,wf(WFs2,Info),NewHeap),
377		put_atts(Store,+wf_store(NewHeap))
378		)
379		; avl_store(RealPrio,Heap,wf(WF1,Info),NewHeap),
380		put_atts(Store,+wf_store(NewHeap))
381		),!,
382		%avl_size(NewHeap,Sz),
383		%(Sz=10 -> print(heap_size(10)),nl ; true),
384		%(Sz=1000 -> print(heap_size(1000)),nl, portray_avl(NewHeap) ; true),
385		WF=WF1.
386		get_waitflag_from_store(Prio,Info,Store,WF) :-
387		add_internal_error('Error getting Waitflag: ', get_waitflag_from_store(Prio,Info,Store,WF)),fail.
388
389		% a version which delays getting a waitflag until the Prio is known:
390		:- block block_get_wait_flag(-,?,?,?).
391		block_get_wait_flag(Prio,Info,WFX,WF) :- get_wait_flag(Prio,Info,WFX,WF).
392
393		% check if there are no waitflags and no FD variables; note: there could be pending co-routines on WF0
394		no_pending_waitflags(no_wf_available).
395		no_pending_waitflags(wfx(_WF0,Store,_WFE,_)) :-
396		my_get_wf_store_atts(Store,Heap), empty_avl(Heap), % no waitflags pending
397		(get_atts(Store,+wf_fdvars(FDVars)) -> FDVars == [] ; true). % and no FD Variables either
398
399		% -------------------
400
401		my_get_wf_store_atts(Store,Heap) :-
402		(get_atts(Store,+wf_store(Heap)) -> true
403		; var(Store),empty_avl(Heap)
404		).
405		%, /* store not initialised; initialise it below but print msg */
406		% waitflag_not_init).
407
408		% -------------------
409
410		% storing Predicates for Kodkod external function:
411		my_get_kodkod_predicates(wfx(_,Store,_,_),ID,PredicateList) :- my_get_wf_kodkod(Store,ID,PredicateList).
412		my_get_wf_kodkod(Store,ID,PredicateList) :-
413		(get_atts(Store,+wf_kodkod(ID,PredicateList)) -> true
414		; var(Store),PredicateList = []
415		).
416		%my_store_wf_kodkod(Store,ID,PredicateList) :- put_atts(Store,+wf_kodkod(ID,PredicateList)).
417		my_add_predicate_to_kodkod(wfx(_,Store,_,_),ID,Predicate) :-
418		my_get_wf_kodkod(Store,ID,PredicateList),
419		put_atts(Store,+wf_kodkod(ID,[Predicate|PredicateList])).
420
421		% -------------------
422
423		% storing Predicates for external function calling satsolver:
424		my_get_satsolver_predicates(wfx(_,Store,_,_),ID,PredicateList) :- my_get_wf_satsolver(Store,ID,PredicateList).
425		my_get_wf_satsolver(Store,ID,PredicateList) :-
426		(get_atts(Store,+wf_satsolver(ID,PredicateList)) -> true
427		; var(Store),PredicateList = []
428		).
429		my_add_predicate_to_satsolver(wfx(_,Store,_,_),ID,Predicate) :-
430		my_get_wf_satsolver(Store,ID,PredicateList),
431		put_atts(Store,+wf_satsolver(ID,[Predicate|PredicateList])).
432
433		% -------------------
434
435
436		ground_wait_flag0(wfx(WF0,_,_,_)) :- grd_wf0(WF0).
437
438	?	ground_wait_flags(wfx(WF0,Store,EnumFinish,_)) :- !,
439	?	grd_wf0(WF0),
440	?	ground_waitflags_store_clpfd(Store),
441		grd_ef(EnumFinish).
442		ground_wait_flags(no_wf_available) :- !.
443		ground_wait_flags(W) :-
444		add_internal_error('Waitflags in wrong format: ',ground_wait_flags(W)).
445
446	?	grd_wf0(E) :- var(E) -> E=0 %%,print(grd_wf0_done),nl
447		; (E==0 -> true ; add_internal_error('Illegal WF0 Waitflag value: ',grd_wf0(E))).
448		grd_ef(E) :- var(E) -> E=0
449		; ((E==0;E==wd_guarded) -> true ; add_internal_error('Illegal EF Waitflag value: ',grd_ef(E))).
450
451		/* currently unused:
452		create_wdguarded_wait_flags(wfx(WF0,Store,EnumFinish,Info),Res,Expected,
453		wfx(WF0,Store,LocalEnumFinish,Info)) :-
454		%% if Res=Expected then the computations of the inner waitflags should be well-defined;
455		%% otherwise they may not
456		copy_wfe(EnumFinish,Res,Expected,LocalEnumFinish).
457		:- block copy_wfe(-,?,?,?), copy_wfe(?,-,?,?).
458		copy_wfe(EnumFinish,Res,Expected,LocalEnumFinish) :-
459		(Res==Expected -> LocalEnumFinish=EnumFinish
460		; LocalEnumFinish=wd_guarded %% branch is pruned by well-definedness condition
461		).
462		*/
463
464		% will not set WFE flag
465		ground_constraintprop_wait_flags(wfx(WF0,Store,_WFE,_Infos)) :-
466		%% print(ground_constraintprop_wait_flags(WF0,Store,_WFE)),nl, %%
467	?	!,grd_wf0(WF0),% print(finished_grounding_wf0),nl,portray_waitflags_store(Store),
468	?	ground_waitflags_store_clpfd(Store).
469		ground_constraintprop_wait_flags(no_wf_available) :- !.
470		ground_constraintprop_wait_flags(W) :-
471		add_internal_error('Waitflags in wrong format',ground_constraintprop_wait_flags(W)).
472
473		:- use_module(clpfd_interface,[clpfd_in_domain/1, clpfd_labeling/2]).
474		:- use_module(library(lists),[reverse/2]).
475
476		%ground_wf(Prio,WF) :- nl,print(ground(WF,Prio)),nl,WF=Prio, print(done_ground(WF,Prio)),nl.
477		% ground_wf(Prio,WF) :- Prio=WF.
478	?	ground_wf(Prio,WF) :- (var(WF) -> WF=Prio ; if(WF=Prio,true,add_internal_error('Illegal waitflag: ',ground_wf(Prio,WF)))).
479
480		ground_prio(Prio,WF,Info) :- %print(ground_prio(Prio,WF,Info)),nl,
481	?	nonvar(WF),!,
482	?	(WF=[H|T] -> % we have a list of waitflags; ground one-by one; TO DO: only ground one and store remaining list in wfx Heap
483	?	reverse([H|T],Ls), %print(list(Ls)),nl,
484	?	maplist(ground_wf(Prio),Ls)
485		; ground(WF) -> true % already grounded by somebody else
486		; add_internal_error('Waitflag already partially grounded: ',ground_prio(Prio,WF,Info))).
487		%ground_prio(Prio,WF,Info) :- debug_kernel_waitflags(Cntr),!,
488		% print(ground_prio(Cntr,Prio,WF,Info)),nl, WF=Prio, print(grounded_prio(Cntr,Prio,WF,Info)),nl.
489		ground_prio(Prio,WF,_Info) :-
490		%external_functions:indent_format(user_output,'~w (~w)~n',[Prio,Info],no_trace),portray_attached_goals(WF),nl,
491		%% (debug:debug_mode(on) -> external_functions:indent_format(user_output,'~w (~w)~n',[Prio,Info],no_trace) ; true),
492		% print(ground(Prio,WF,Info)),nl, translate:print_frozen_info(WF),nl,
493	?	WF = Prio. % ground waitflag
494		% print(grounded(Prio,Info)),nl,nl, %%
495
496		%:- use_module(kernel_objects,[enum_warning_large/3]).
497	?	label_clpfd_variable(Variable) :- label_clpfd_variable(2097153,Variable).
498		label_clpfd_variable(Prio,Variable) :-
499	?	(gt_limit(Prio,2097152), % note Prio > test also works with float(X) terms !
500		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
501		-> %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
502	?	performance_messages:perfmessage(enumerating_large_integer_variable(RANGE)),
503	?	(number(Size)
504	?	-> clpfd_labeling([Variable],[bisect]) % ffc no longer required: just a single variable
505		; add_warning(label_clpfd_variable,'Trying to enumerate FD Variable with infinite domain (possibly due to WD error) ',RANGE)
506		)
507		% 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)
508		% Note: test 1099 tests this
509		% TO DO: investigate whether it makes sense to use bisect for smaller values already
510	?	; preferences:preference(randomise_enumeration_order,true) -> clpfd_interface:clpfd_randomised_in_domain(Variable)
511	?	; clpfd_in_domain(Variable)). % TO DO: use random ?
512
513		check_if_labeling_domain_large(H,Limit,Size,Res) :-
514		my_get_fd_size(H,Size),
515		gt_limit(Size,Limit),
516		clpfd_interface:clpfd_domain(H,From,To),
517		Res=From:To.
518
519		%check_if_labeling_domain_finite(H) :-
520		% my_get_fd_size(H,Size), number(Size).
521
522		% mix ProB labeling with CLP(FD) labeling
523		ground_waitflags_store_clpfd(Store) :-
524	?	my_get_wf_store_atts(Store,Heap),!,
525	?	ground_waitflags_store_clpfd_aux(Store,Heap).
526		ground_waitflags_store_clpfd(Store) :-
527		add_internal_error('Illegal Waitflag: ',ground_waitflags_store_clpfd(Store)),fail.
528
529		ground_waitflags_store_clpfd_aux(Store,Heap) :-
530		%my_get_fdvars_atts(Store,FDVars),
531	?	get_atts(Store,+wf_fdvars(FDVars)), % there is a list of FD vars available
532	?	!,
533	?	( avl_del_min(Heap,Prio,wf(WF,Info),NewHeap) -> % we have non-ground waitflags with a matching priority
534	?	(my_get_next_fdvar_to_enumerate(FDVars,NextFDVar,RemainingFDVARS),
535		fd_priority_leq_limit(NextFDVar,FDPrio,Prio)
536	?	-> enum_fd_variable_store(FDPrio,Store,NextFDVar,RemainingFDVARS)
537	?	; put_atts(Store,+wf_store(NewHeap)), % write the modified heap back
538		% debug:hit_counter(XXX),print(grounding(XXX,Prio,_Info)),nl, (XXX=16556->trace ; true),
539		%WF = Prio, % ground waitflag
540		% print(grounding(Prio,Info)),nl,
541	?	ground_prio(Prio,WF,Info),
542	?	ground_waitflags_store_clpfd(Store) % continue recursively
543		)
544		; /* otherwise -> */ %print(empty_store),nl,
545	?	(my_get_next_fdvar_to_enumerate(FDVars,NextFDVar,RemainingFDVARS)
546	?	-> enum_fd_variable_store(Store,NextFDVar,RemainingFDVARS)
547		; true % heap and FDVars list is empty, nothing more to do
548		)
549		).
550		ground_waitflags_store_clpfd_aux(Store,Heap) :- % no FDVars are available to enumerate
551	?	avl_del_min(Heap,Prio,wf(WF,Info),NewHeap), !,
552	?	put_atts(Store,+wf_store(NewHeap)), % write the modified heap back
553		% debug:hit_counter(XXX),print(grounding(XXX,Prio,_Info)),nl, (XXX=16556->trace ; true),
554	?	ground_prio(Prio,WF,Info), % ground waitflag
555	?	ground_waitflags_store_clpfd(Store). % continue recursively
556		ground_waitflags_store_clpfd_aux(_Store,_Heap). % heap and FDVars list is empty, nothing more to do
557
558		%:- use_module(library(lists),[exclude/3]).
559		enum_fd_variable_store(Store,NextFDVar,RemainingFDVARS) :-
560		%exclude(nonvar,RemainingFDVARS,RemainingFDVARS2),
561	?	put_atts(Store,+wf_fdvars(RemainingFDVARS)),
562		%% print(labeling(NextFDVar,RemainingFDVARS)),nl, portray_fd_vars([NextFDVar|RemainingFDVARS]),nl,nl,
563	?	label_clpfd_variable(NextFDVar),
564	?	ground_waitflags_store_clpfd(Store).
565		% a version of the above where we know the priority
566		enum_fd_variable_store(FDPrio,Store,NextFDVar,RemainingFDVARS) :-
567		%exclude(nonvar,RemainingFDVARS,RemainingFDVARS2), % does not seem to buy a lot
568	?	put_atts(Store,+wf_fdvars(RemainingFDVARS)),
569		%% print(labeling(NextFDVar,RemainingFDVARS)),nl, portray_fd_vars([NextFDVar|RemainingFDVARS]),nl,nl,
570	?	label_clpfd_variable(FDPrio,NextFDVar),
571	?	ground_waitflags_store_clpfd(Store).
572
573		:- if(false).
574		% small utility to trace through waitflag enumeration
575		:- dynamic spying_on/1.
576		spying_on(1).
577		spy_waitflags(_,_) :- \+ spying_on(_) , !.
578		spy_waitflags(Msg,Store) :- retract(spying_on(Nr)),print(Msg),nl,
579		(Nr=1
580		-> assert(spying_on(Nr)),
581		print(' (j,t,p,q) ==> '),read_term(T,[]),
582		action(T,Store)
583		; N1 is Nr-1, assert(spying_on(N1))
584		).
585		action(t,_Store) :- !,trace.
586		action(p,Store) :- !,portray_waitflags_store(Store), spy_waitflags('',Store).
587		action(q,_Store) :- !,retractall(spying_on).
588		action(Nr,_) :- number(Nr),!, retractall(spying_on(_)), assert(spying_on(Nr)).
589		action(_,_).
590		:- endif.
591
592		:- assert_must_succeed(( kernel_waitflags:init_wait_flags(WF), kernel_waitflags:portray_waitflags(WF),
593		kernel_waitflags:get_wait_flag(2,'Test',WF,WF2), when(nonvar(WF2),print(wf2)),
594		clpfd:in(FD,'..'(1,2)),kernel_waitflags:add_fd_variable_for_labeling(FD,WF),
595		kernel_waitflags:portray_waitflags(WF), kernel_waitflags:ground_wait_flags(WF) )).
596		% PORTRAYING Waitflags
597		portray_waitflags(wfx(WF0,Store,WFE,Infos)) :- flush_output,
598		print('*WAITFLAG STORE: '),print(wfx(WF0,Store,WFE,Infos)),nl,
599		(var(WF0) -> print('> WF0 :: '), portray_attached_goals(WF0),nl ; true),
600		portray_waitflags_store(Store),!,
601		(var(WFE) -> print('> WFE :: '), portray_attached_goals(WFE),nl ; true),
602		print('*END WAITFLAG STORE'),nl.
603		%my_portray_avl(Heap),nl.
604		portray_waitflags(none) :- !, print('*WAITFLAG STORE: none'),nl.
605		portray_waitflags(no_wf_available) :- !, print('*WAITFLAG STORE: none'),nl.
606		portray_waitflags(Store) :-
607		add_internal_error('Illegal Waitflag: ',portray_waitflags(Store)),flush_output.
608
609		portray_fd_vars([]) :- !, '$NOT_COVERED'('This is debugging code!').
610		portray_fd_vars([V|T]) :- print('> '), print(V), nonvar(V),!, nl,
611		portray_fd_vars(T), '$NOT_COVERED'('This is debugging code!').
612		portray_fd_vars([V|T]) :- my_get_fd_size(V,Size), !, print(' : '), print(Size),
613		portray_attached_goals(V),
614		portray_fd_vars(T),
615		'$NOT_COVERED'('This is debugging code!').
616		portray_fd_vars(X) :- print('> *** UNKNOWN FDVARS: '), print(X), nl,
617		'$NOT_COVERED'('This is debugging code!').
618
619		portray_waitflags_store(Store) :-
620		my_get_fdvars_atts(Store,FDList),
621		(FDList=[] -> true ; print('FDVARS:'),nl,portray_fd_vars(FDList),nl),
622		my_get_wf_store_atts(Store,Heap),
623		avl_to_list(Heap,List), portray_avl_els(List).
624
625		portray_avl_els([]).
626		portray_avl_els([Prio-wf(LWF,Info)|T]) :-
627		print('> '),print(Prio), print(' : '), print(LWF), print(' : '), portray_info(Info),nl,
628		portray_attached_goals(LWF),
629		portray_avl_els(T).
630
631		portray_info(label_clpfd_vars(Vars)) :- print('label_clpfd_vars :: '),
632		translate:l_print_frozen_info(Vars).
633		portray_info(I) :- print(I).
634
635		portray_attached_goals(V) :- V==[],!.
636		portray_attached_goals(LWF) :- nonvar(LWF),LWF=[H|T],!,
637		portray_attached_goals(H),portray_attached_goals(T).
638		portray_attached_goals(LWF) :- frozen(LWF,Goal), print(' :: '), portray_goal(Goal),nl.
639
640		:- use_module(tools_printing,[print_term_summary/1]).
641		portray_goal((A,B)) :- !, portray_goal(A), print(','), print(' '), portray_goal(B).
642		portray_goal(A) :- print_term_summary(A).
643
644		:- public my_portray_avl/1.
645		my_portray_avl(V) :- var(V), !, add_internal_error('Variable: ',my_portray_avl(V)).
646		my_portray_avl(V) :- portray_avl(V).
647
648
649		quick_portray_waitflags(wfx(WF0,Store,WFE,_)) :-
650		my_get_fdvars_atts(Store,FDList),
651		my_get_wf_store_atts(Store,Heap),
652		avl_domain(Heap,List),
653		format('% Waitflags-Store WF0=~w,WFE=~w, Flags=~w, FDVars=~w~n',[WF0,WFE,List,FDList]).
654		quick_portray_waitflags_store(Store) :-
655		my_get_fdvars_atts(Store,FDList),
656		my_get_wf_store_atts(Store,Heap),
657		avl_domain(Heap,List),
658		format('% Waitflags-Store Flages=~w, FDVars=~w~n',[List,FDList]).
659
660		:- assert_must_succeed(( kernel_waitflags:init_wait_flags(WF),
661		kernel_waitflags:get_wait_flag1(WF,WF1), when(ground(WF1),X=a),
662		kernel_waitflags:ground_wait_flags(WF), X==a )).
663
664		% create a copy of the waitflags with WF0 and WF0 as variable; should be finished with copy_wf_finish
665		% can be used if you temporarily want to disable non-deterministic enumeration, ...
666		copy_wf_start(wfx(_,WF,_,Infos),wfx(_,WF,_,Infos)).
667		copy_wf_start(no_wf_available,no_wf_available).
668
669		% just copy WF0 and WFE over to new waitflag
670		copy_wf_finish(wfx(WF0,_,WFE,_),wfx(WF0,_,WFE,_)).
671		copy_wf_finish(no_wf_available,no_wf_available).
672
673
674		/* create a copy where the enumeration_finished waitflag is shared;
675		the inner enumeration_finished wait flags should normally not be grounded */
676		%create_inner_wait_flags(wfx(_,_,WFE),wfx(WF0Inner,S,WFE)) :- !,init_wait_flags_store(S). % old version
677		create_inner_wait_flags(wfx(_,_,WFE,Infos),Info,wfx(WF0Inner,S,WFEInner,Infos)) :-
678		init_wait_flags_store(S),
679		get_inner_enumeration_over_wait_flag(wfx(WF0Inner,S,WFEInner,Infos),Info,LastWF),
680		copy_wfe_to_inner(LastWF,WFE,WFEInner). % delay copying WFE at least until inner enumeration has been run
681		create_inner_wait_flags(no_wf_available,_,no_wf_available).
682		:- block copy_wfe_to_inner(-,?,?).
683		copy_wfe_to_inner(_,WFE,WFE).
684
685		ground_inner_wait_flags(wfx(WF0,Store,_EWF,_)) :- !,
686		% does not ground enumeration finished waitflag
687		grd_wf0(WF0),
688		ground_waitflags_store_clpfd(Store).
689		ground_inner_wait_flags(no_wf_available) :- !.
690		ground_inner_wait_flags(W) :-
691		add_internal_error('Inner waitflags in wrong format: ',ground_inner_wait_flags(W)).
692
693		% copy WF0 and WFE, set up a new store for the rest
694		copy_wf01e_wait_flags(wfx(WF0,WFX,WFE,Infos),wfx(WF0,S,WFE,Infos)) :-
695		init_wait_flags_store(S),
696		get_waitflag_from_store(1,copy_wf01e,WFX,WF1), % now ground wait flag 1 if it is grounded in the orginal WF store
697		copy_wf01e_wait_flags_aux(WF1,S).
698		copy_wf01e_wait_flags(no_wf_available,no_wf_available).
699
700		:- block copy_wf01e_wait_flags_aux(-,?).
701		copy_wf01e_wait_flags_aux(_,S) :- ground_waitflags_store_up_to_no_clpfd(1,S). % no CLPFD - labeling required until prio 1
702
703
704		clone_wait_flags_from1(wfx(_WF0,S,WFE,Infos),wfx(_NewWF0,S,WFE,Infos)).
705		clone_wait_flags_from1(no_wf_available,no_wf_available).
706		% creates a copy of the wait_flags, except for WF0; this needs to be grounded separately with grd_wf0/1
707		clone_wait_flags_from1_finish(wfx(WF0,_,_,_),wfx(WF0,_,_,_)). % finish copying by copying over WF0
708		clone_wait_flags_from1_finish(no_wf_available,no_wf_available).
709
710		get_wait_flag0(wfx(WF0,_,_,_),WF0).
711		get_wait_flag0(no_wf_available,0).
712
713		%get_wait_flag0(WFX,WF0) :- get_wait_flag(0,WFX,WF0). /* when this is ground you can do det. propagatons */
714		get_wait_flag1(WFX,WF1) :- get_wait_flag(1.0,WFX,WF1). /* when this is ground you can do det. propagatons */
715		get_wait_flag1(Info,WFX,WF1) :- get_wait_flag(1.0,Info,WFX,WF1).
716
717		get_binary_choice_wait_flag(Info,WFX,WF2) :- !, get_binary_choice_wait_flag_exp_backoff(4,Info,WFX,WF2).
718		%get_binary_choice_wait_flag(Info,WFX,WF2) :- % use 3 rather than 2 to give priority over enumeration choicepoints
719		% get_wait_flag(4,Info,WFX,WF2). /* when this is ground you can do binary propagatons */
720
721		get_middle_wait_flag(Info,WFX,WFn) :- get_wait_flag(10,Info,WFX,WFn).
722
723		get_last_wait_flag(Info,WFX,Res) :- last_finite_priority(P),get_wait_flag(P,Info,WFX,Res).
724
725		% ------------------------
726		get_wait_flag_infos(wfx(_,_,_,Infos),Infos).
727		get_wait_flag_infos(no_wf_available,[]).
728
729		:- use_module(library(ordsets),[ord_member/2,ord_add_element/3]).
730		get_wait_flag_info(wfx(_,_,_,Infos),Info) :- member(Info,Infos).
731
732		% use if the Info field is known, requires ordered/sorted Infos list
733		is_wait_flag_info(wfx(_,_,_,Infos),Info) :-
734		(nonvar(Infos) -> ord_member(Info,Infos) ; print(var_waitflag),nl,fail).
735
736		%set_wait_flag_infos(wfx(WF0,Store,WFE,_),Infos,wfx(WF0,Store,WFE,Infos)).
737		%set_wait_flag_infos(no_wf_available,_,no_wf_available).
738
739		add_wait_flag_info(wfx(WF0,Store,WFE,Infos),Info,wfx(WF0,Store,WFE,NewInfos)) :-
740		ord_add_element(Infos,Info,NewInfos). %, print(added_wf_infos(NewInfos)),nl.
741		add_wait_flag_info(no_wf_available,_,no_wf_available).
742
743		% ------------------------
744
745		% BINARY CHOICE WAITFLAGS
746
747		:- use_module(tools,[max_tagged_pow2/1]).
748		% last power of 2 exponent that is still a finite priority
749		last_finite_pow2_prio_exponent(Lim) :- tools:max_tagged_pow2(Pow),
750		Lim is Pow-1. % stay below last_finite_priority, i.e., max_tagged_integer-1024
751
752		% utility to get power of two priority:
753		get_pow2_binary_choice_priority(Exp,Prio) :- last_finite_pow2_prio_exponent(Lim),
754		(Exp =< Lim -> Prio is integer(2**Exp)
755		; Prio is integer(2**Lim)).
756
757		% get a binary choice wait flag, start with 2 but for every further call double the priority (exponential backoff)
758		% idea: give priority to data enumerations when too many choice points arise
759		get_binary_choice_wait_flag_exp_backoff(Info,WFX,WF2) :-
760		get_binary_choice_wait_flag_exp_backoff(2,Info,WFX,WF2).
761		get_binary_choice_wait_flag_exp_backoff(_,_Info,no_wf_available,WF2) :- !, WF2=2.
762
763		% StartPrio should be a power of 2:
764		get_binary_choice_wait_flag_exp_backoff(StartPrio,Info,wfx(_,Store,_,_),WF2) :-
765		my_get_wf_store_atts(Store,Heap),
766		last_finite_pow2_prio_exponent(Lim),
767		get_bin_aux(StartPrio,Lim,Info,Heap,NewHeap,WF2),
768		put_atts(Store,+wf_store(NewHeap)).
769
770		% to do : maybe store attribute of current exponential ??
771		get_bin_aux(Prio,Lim,Info,Heap,NewHeap,WF2) :- avl_fetch(float(Prio),Heap,wf(WFs,OldInfo)),
772		!,
773		(Prio >= Lim -> WF2 = WFs, NewHeap=Heap /* for finite priorities single waitflag stored */
774		; OldInfo = '$binary'(_) -> P2 is Prio*2, get_bin_aux(P2,Lim,Info,Heap,NewHeap,WF2)
775		; otherwise -> WF2=WFs, avl_store(float(Prio),Heap,wf(WFs,'$binary'(Info)),NewHeap) % just update Info; so that next time we double
776		).
777		get_bin_aux(Prio,_,Info,Heap,NewHeap,WF2) :- % we have found an unused power of 2
778		%print(get_bin(Prio,Info)),nl,
779		avl_store(float(Prio),Heap,wf(WF2,'$binary'(Info)),NewHeap).
780
781		% ------------------------
782
783		get_enumeration_finished_wait_flag(wfx(_,_,WFE,_),WFE) :- !.
784		get_enumeration_finished_wait_flag(no_wf_available,WFE) :- !,WFE=1.
785		get_enumeration_finished_wait_flag(W,E) :-
786		add_internal_error('Waitflags in wrong format: ',get_enumeration_finished_wait_flag(W,E)).
787
788
789	?	ground_det_wait_flag(wfx(WF0,Store,_,_)) :- !, %% print(ground_det_wait_flag),nl,
790	?	grd_wf0(WF0),
791		ground_waitflags_store_up_to_no_clpfd(1,Store). % no CLPFD labeling required for prio until 1
792		ground_det_wait_flag(no_wf_available) :- !.
793		ground_det_wait_flag(W) :-
794		add_internal_error('Waitflags in wrong format: ',ground_det_wait_flag(W)).
795
796	?	ground_wait_flag_to(wfx(WF0,Store,_,_),Limit) :- !,%% print(ground_det_wait_flag),nl,
797	?	grd_wf0(WF0),
798	?	ground_waitflags_store_clpfd_up_to(Limit,Store).
799		ground_wait_flag_to(no_wf_available,_) :- !.
800		ground_wait_flag_to(W,Limit) :-
801		add_internal_error('Waitflags in wrong format: ',ground_wait_flag_to(W,Limit)).
802
803		ground_waitflags_store_up_to_no_clpfd(Prio,Store) :- % print(prio(Prio)),nl,
804		my_get_wf_store_atts(Store,Heap), % portray_waitflags_store(Store), %
805		( avl_min(Heap,Min,wf(WF,Info)) -> % heap is non-empty, first element is WF with priority Min
806		( Min =< Prio -> % we have non-ground waitflags with a matching priority
807		(avl_del_min(Heap,AMin,_,NewHeap),AMin==Min % remove the first element
808		-> true
809		; add_internal_error('Could not remove min. in ground_waitflags_store_up_to_no_clpfd: ',Min:Info:Heap), fail
810		),
811		put_atts(Store,+wf_store(NewHeap)), % write the modified heap back
812		%% print(grounding2(Prio,_Info)),nl, %%
813		ground_prio(Min,WF,Info),
814		ground_waitflags_store_up_to_no_clpfd(Prio,Store) % continue recursively
815		; /* otherwise -> */ % no more matching waitflags present
816		true) % stop here
817		; /* otherwise -> */ % heap is empty, nothing more to do
818		true). % stop here
819
820		ground_waitflags_store_clpfd_up_to(Limit,Store) :-
821	?	my_get_wf_store_atts(Store,Heap),
822	?	my_get_fdvars_atts(Store,FDVars),!,
823	?	( avl_del_min(Heap,Prio,wf(WF,Info),NewHeap) -> % we have non-ground waitflags with a matching priority
824	?	( my_get_next_fdvar_to_enumerate(FDVars,NextFDVar,RemainingFDVARS),
825		fd_priority_leq_limit(NextFDVar,FDPrio,Limit)
826	?	-> (FDPrio > Limit -> true
827	?	; enum_fd_variable_store(FDPrio,Store,NextFDVar,RemainingFDVARS))
828	?	; (Prio > Limit -> true
829	?	; put_atts(Store,+wf_store(NewHeap)), % write the modified heap back
830		%print(grounding(Prio,_Info)),nl,
831	?	ground_prio(Prio,WF,Info), % ground waitflag
832	?	ground_waitflags_store_clpfd_up_to(Limit,Store) % continue recursively
833		)
834		)
835		; ((my_get_next_fdvar_to_enumerate(FDVars,NextFDVar,RemainingFDVARS),
836		fd_priority_leq_limit(NextFDVar,FDPrio,Limit))
837		-> enum_fd_variable_store(FDPrio,Store,NextFDVar,RemainingFDVARS)
838		; true % heap and FDVars list is empty, nothing more to do
839		)
840		).
841		ground_waitflags_store_clpfd_up_to(Limit,Store) :-
842		add_internal_error('Illegal Waitflag: ',ground_waitflags_store_clpfd_up_to(Limit,Store)),fail.
843
844
845		update_waitflag(Prio,CurrentWaitflag,NewWaitFlag,WF) :-
846		/* if the CurrentWaitflag is already ground and now a new WF with lower priority has been added to the store:
847		create a new non-ground waitflag to give priority to new WF with lower priority value */
848		(var(CurrentWaitflag) -> NewWaitFlag=CurrentWaitflag
849		; WF=wfx(_WF0,Store,_,_),my_get_wf_store_atts(Store,Heap),
850		((avl_min(Heap,Min,wf(_NewerWF,_Info)),(Prio=inf;Min<Prio))
851		-> get_waitflag_from_store(Prio,updated_wf,Store,NewWaitFlag) % could be optimized
852		% ,print(updating_wf(Prio,CurrentWaitflag,NewWaitFlag,Min)),nl
853		; fdvar_with_higher_prio_exists(Store,Prio) -> get_waitflag_from_store(Prio,updated_wf,Store,NewWaitFlag)
854		; NewWaitFlag=CurrentWaitflag
855		)
856		).
857
858		fdvar_with_higher_prio_exists(Store,Limit) :-
859		my_get_fdvars_atts(Store,FDVars),
860		my_get_next_fdvar_to_enumerate(FDVars,NextFDVar,_),
861		fd_priority_leq_limit(NextFDVar,_,Limit).
862
863		% get the minimum waitflag, if it exists
864		get_minimum_waitflag_prio(wfx(_,Store,_,_),MinPrio,Info) :-
865		my_get_wf_store_atts(Store,Heap),
866		avl_min(Heap,MinPrio,wf(_LWF,Info)).
867
868
869		% currently not used:
870		%/* same as get_enumeration_finished_wait_flag, but will fail if user does not want
871		% to look for abort errors */
872		%get_abort_error_flag(wfx(_,_,WFE,_),WFE) :- !, \+ preferences:preference(find_abort_values,false).
873		%get_abort_error_flag(W,_) :-
874		% add_internal_error(get_abor_error_flag,'Waitflags in wrong format: ',W).
875
876
877		add_wd_error(Msg,Term,WF) :- add_wd_error_span(Msg,Term,unknown,WF).
878		add_wd_error_set_result(Msg,Term,Result,ResultValue,Span,WF) :-
879		is_wd_guarded_result(Result), % just dummy co-routine to detect variables which have WD assignments pending on them; should not be enumerated
880		% add well-definedness error but also set Result Variable to ResultValue to trigger pending co-routines if wd_guarded
881		add_abort_error7(well_definedness_error,Msg,Term,Result,ResultValue,Span,WF).
882		add_wd_error_span(Msg,Term,Span,WF) :- add_abort_error_span(well_definedness_error,Msg,Term,Span,WF).
883
884		:- block is_wd_guarded_result(-).
885		is_wd_guarded_result(_).
886
887		add_abort_error_span(ErrType,Msg,Term,Span,WF) :- add_abort_error7(ErrType,Msg,Term,0,0,Span,WF).
888
889		:- use_module(tools_printing,[print_error/1]).
890		add_abort_error7(_ErrType,_Msg,_Term,_Result,_ResultValue,_Span,_WF) :-
891		preference(disprover_mode,true),
892		!, % When Disproving we can assume well-definedness of the PO; sometimes the relevant hypotheses will be filtered out
893		fail.
894		add_abort_error7(ErrType,Msg,Term,Result,ResultValue,Span,WF) :-
895		preference(raise_abort_immediately,F), F \= false,
896		!,
897		(F=full -> AWF=1 % really raise immediately; may entail more spurious messages, particularly in WF0
898		; get_idle_wait_flag(add_abort_error7,WF,AWF), %get_wait_flag0(WF,AWF),
899		mark_pending_abort_error(WF,Msg,Term,Span)
900		),
901		%when(nonvar(AWF),
902
903		%(print_error('Raising error immediately without checking rest of predicate for unsatisfiability (because RAISE_ABORT_IMMEDIATELY set to TRUE): error could be spurious!'),true)),
904		string_concatenate('Raising error immediately without checking rest of predicate for unsatisfiability (because RAISE_ABORT_IMMEDIATELY set to TRUE): error could be spurious!~n! ',Msg,NewMsg),
905		add_abort_error2(AWF,ErrType,NewMsg,Term,Result,ResultValue,Span).
906		add_abort_error7(ErrType,Msg,Term,Result,ResultValue,Span,WF) :-
907		%nl,print(possible_wd_error(WF,Msg)),nl,
908		mark_pending_abort_error(WF),
909		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:
910		%integer_priority(P), get_wait_flag(P,add_abort_error7,WF,AWF), % causes problem for test 1122
911		add_abort_error2(AWF,ErrType,Msg,Term,Result,ResultValue,Span).
912
913
914		% no longer used:
915		%add_wd_error_span_now(Msg,Term,Span) :- add_abort_error2(true,well_definedness_error,Msg,Term,0,0,Span).
916
917		:- use_module(state_space,
918		[store_abort_error_for_context_state_if_possible/4]).
919		:- block add_abort_error2(-,?,?,?,?,?,?).
920		add_abort_error2(wd_guarded,_Err,_Msg,_Term,Result,ResultValue,_Span) :- !,% ignoring error message; no-wd problem
921		% set Result to default ResultValue; useful to get rid of pending co-routines; result will not be used
922		(Result=ResultValue -> true ; print(add_abort_error_failure(Result,ResultValue)),nl).
923		add_abort_error2(_AWF,ErrType,Msg,Term,_,_,Span) :- % print(adding_abort_error(Msg)),nl,trace,
924		% add_error(abort_error,Msg,Term),
925		(store_abort_error_for_context_state_if_possible(ErrType,Msg,Term,Span)
926		-> true
927		; add_error(add_abort_error2,'Could not store error: ',(Msg,Term),Span)),
928		% print(done),nl,
929		fail.
930
931		/*
932		ground_wait_flags_catch_enumeration_warnings(WF) :-
933		on_exception(enumeration_warning(A,B,C,D,E),
934		ground_wait_flags(WF),
935		(pending_abort_error(WF,Msg,Term,Span),
936		format('WD-Error may be causing Enumeration Warning : ~w~n',[Msg]),
937		fail
938		;
939		throw(enumeration_warning(A,B,C,D,E)))).
940		*/
941
942		% check whether an abort error is pending.
943		pending_abort_error(wfx(_WF0,_WFX,WFE,_)) :- var(WFE),
944		get_atts(WFE,+wf_abort_pending).
945		% succeed once for every pending abort error in Waitflag store
946		pending_abort_error(wfx(_WF0,_WFX,WFE,_),Msg,Term,Span) :-
947		frozen(WFE,Goal), %print(goal(Goal)),nl,
948		pending_abort_error_aux(Goal,Msg,Term,Span).
949
950		pending_abort_error_aux(kernel_waitflags:add_abort_error2(_,_ErrType,Msg,Term,_Result,_ResultValue,Span), Msg,Term,Span).
951		pending_abort_error_aux(add_abort_error2(_,_ErrType,Msg,Term,_Result,_ResultValue,Span), Msg,Term,Span).
952		pending_abort_error_aux(kernel_waitflags:mark_pending_abort_error2(_,Msg,Term,Span), Msg,Term,Span).
953		pending_abort_error_aux((A,B),Msg,Term,Span) :-
954		(pending_abort_error_aux(A,Msg,Term,Span) ;
955		pending_abort_error_aux(B,Msg,Term,Span) ).
956
957		% explicitly mark that an abort error is pending
958		mark_pending_abort_error(wfx(_WF0,_WFX,WFE,_)) :-
959		(var(WFE) -> put_atts(WFE,+wf_abort_pending)
960		; true).
961		% explicitly mark that an abort error is pending with storing information
962		mark_pending_abort_error(wfx(_WF0,_WFX,WFE,_),Msg,Term,Span) :-
963		(var(WFE) -> put_atts(WFE,+wf_abort_pending),
964		mark_pending_abort_error2(WFE,Msg,Term,Span)
965		; true).
966		mark_pending_abort_error(no_wf_available,_Msg,_Term,_Span).
967
968		:- block mark_pending_abort_error2(-,?,?,?).
969		mark_pending_abort_error2(_,_,_,_).
970		% ---------------------------------------------
971
972		ground_wait_flag_to_enumeration(WF) :-
973	?	last_finite_priority(P),
974	?	ground_wait_flag_to(WF,P).
975
976		get_large_finite_wait_flag(Info,WFX,WF2) :-
977		large_finite_priority(P),
978		get_wait_flag(P,Info,WFX,WF2).
979
980		get_enumeration_starting_wait_flag(Info,WFX,WF2) :-
981		last_finite_priority(P),
982		get_wait_flag(P,enumeration_starting(Info),WFX,WF2).
983
984		get_inner_enumeration_over_wait_flag(WFX,Info,WF2) :-
985		tools:max_tagged_integer(P), % a bit of a hack; what if inf_type_prio generates something higher ? TO DO : bound get_max_cardinality_as_priority/inf_type_prio result
986		get_wait_flag(P,inner_enumeration(Info),WFX,WF2).
987
988		get_integer_enumeration_wait_flag(Info,WFX,WF2) :-
989		integer_priority(Prio),
990		get_wait_flag(Prio,Info,WFX,WF2).
991
992		% A few hardcoded priorities
993		large_finite_priority(P) :- integer_priority(I), P is I-1000.
994		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
995		%integer_priority(10000000). % old value
996		integer_priority(Prio) :- % priority for X : INTEGER enumerations
997		tools:max_tagged_integer(P),
998		Prio is P - 1024.
999		% note inf_type_prio sets some priorities such as seq(INTEGER) ... higher
1000
1001		% priority for sets of infinite type (POW(INTEGER)...)
1002		integer_pow2_priority(Prio) :- % was 10000010
1003		integer_priority(P), Prio is P+10.
1004
1005
1006		is_finite_priority(P) :-
1007		P < 100000, % TO DO: put max_tagged_integer for 32-bit system minus 1026 or so (see above)
1008		last_finite_priority(LFP),
1009		P =< LFP.
1010
1011		%integer_pow_priority(10000020) :- tools:max_tagged_integer(MAX).
1012
1013		% ensure that we do not exceed priority of type enumeration or use too big numbers
1014		get_bounded_wait_flag(Prio,Info,WF,LWF) :-
1015		bound_prio(Prio,P),
1016		get_wait_flag(P,Info,WF,LWF).
1017
1018		bound_prio(Prio,P) :- number(Prio),
1019		Prio>268435452, % 268435455 is max_tagged_integer on 32 bit platforms
1020		last_finite_priority(MAX),
1021		Prio>MAX,
1022		!, P=MAX.
1023		bound_prio(P,P).
1024
1025		% -------------
1026
1027		% copy waitflags from one waitflag store to another; warning: can ground WF0 from outer store
1028		copy_waitflag_store(wfx(WF0,Store1,WFE1,_),wfx(WF0,Store2,WFE2,Info2)) :-
1029		%print(copy_wf(WF0,Store1,Store2,WFE1,WFE2)),nl,
1030		my_get_fdvars_atts(Store1,FDList1),
1031		(FDList1 = [] -> true
1032		; my_get_fdvars_atts(Store2,FDList2),
1033		append(FDList1,FDList2,NewFDList),
1034		put_atts(Store2,+wf_fdvars(NewFDList))),
1035		my_get_wf_store_atts(Store1,Heap),
1036		avl_to_list(Heap,WF_List),
1037		%print(copying(FDList1,WF_List)),nl,
1038		maplist(add_wf(wfx(WF0,Store2,WFE2,Info2)),WF_List), % we could do this faster
1039		clear_store(Store1), Store1=Store2, % ensure that calls which add waitflags now get-redirected to waitflag store 2
1040		%portray_waitflags(wfx(WF0,Store2,WFE2,Info2)),
1041		WFE1=WFE2.
1042
1043		clear_store(Store) :- put_atts(Store,-wf_store(_)), put_atts(Store,-wf_fdvars(_)).
1044
1045		add_wf(WF,Prio-wf(WFlag,Info)) :- % purpose: copy waitflag WFlag to WF
1046		(Prio=float(P) -> true ; P=Prio),
1047		(var(WFlag) -> get_wait_flag(P,Info,WF,WFlag) % we just have a single waitflag
1048		; maplist(get_wait_flag(P,Info,WF),WFlag)). % we have a list of waitflags
1049
1050
1051		% try and find an exact match for a waitflag info; this is linear in size of waitflag store !
1052		find_waitflag_info(wfx(_WF0,Store,_WFE1,_),Info,Prio,WF1) :-
1053		my_get_wf_store_atts(Store,Heap),
1054		avl_member(Prio,Heap,wf(WF1,Info)).
1055		% --------------------------
1056		% DEBUGGING UTILITIES:
1057
1058		% you also need to comment in code above using it
1059
1060		:- dynamic debug_kernel_waitflags/1.
1061		set_debug_kernel_waitflags :- (debug_kernel_waitflags(_) -> true ; assert(debug_kernel_waitflags(0))).
1062
1063		% the counter allows to set trace points
1064		debug_kernel_waitflags(Counter) :- retract(debug_kernel_waitflags(C)), C1 is C+1,
1065		assert(debug_kernel_waitflags(C1)), Counter=C1.
1066
1067		get_debug_info(Info,Res) :- debug_kernel_waitflags(Counter),!,
1068		(Counter==39 -> trace ; true),
1069		Res=info(Counter,Info).
1070		get_debug_info(Info,Info).
1071
1072		% --------------------------
1073
1074		:- assert_must_succeed(( kernel_waitflags:test_waitflags(1) )).
1075		:- assert_must_succeed(( kernel_waitflags:test_waitflags(2) )).
1076
1077		test_waitflags(1) :-
1078		init_wait_flags(Waitflags),
1079		get_wait_flag(10,Waitflags,WF1),
1080		when(nonvar(WF1),print('WF1 - Prio 10\n')),
1081		get_wait_flag(5,Waitflags,WF2),
1082		when(nonvar(WF2),(print('WF2 - Prio 5\n'),
1083		get_wait_flag(6,Waitflags,WF4),
1084		when(nonvar(WF4),print('WF4 - Prio 6\n')),
1085		get_wait_flag(2,Waitflags,WF5),
1086		when(nonvar(WF5),print('WF5 - Prio2\n')))),
1087		get_wait_flag(5,Waitflags,WF3),
1088		when(nonvar(WF3),print('WF3 - Prio 5\n')),
1089		ground_wait_flags(Waitflags),nl.
1090
1091		test_waitflags(2) :-
1092		init_wait_flags(Waitflags),
1093		get_wait_flag(10,Waitflags,WF1),
1094		when(nonvar(WF1),print('WF1 Prio 10\n')),
1095		get_wait_flag(5,Waitflags,WF2),
1096		when(nonvar(WF2),(print('WF2 - Prio 5\n'),
1097		get_wait_flag(6,Waitflags,WF4),
1098		when(nonvar(WF4),print('WF4 - Prio 6\n')),
1099		get_wait_flag(2,Waitflags,WF5),
1100		when(nonvar(WF5),print('WF5 - Prio2\n')))),
1101		get_wait_flag(5,Waitflags,WF3),
1102		when(nonvar(WF3),print('WF3 - Prio 5\n')),
1103		ground_wait_flags(Waitflags),nl.