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