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