1 % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(b_enumerate, [
6 b_type_values_in_store/3,
7 b_enumerate_values_in_store/5,
8 %b_enumerate_values/2,
9 b_enumerate_typed_values/3,
10 %b_tighter_enumerate_values_in_store/4,
11 b_tighter_enumerate_values/2, b_tighter_enumerate_single_value/4,
12 b_trace_tighter_enumerate_values/2,
13
14 b_extract_typedvalc/4
15
16 %enumerate_integer_with_min_range_wf/4 % no longer used
17 ]).
18
19
20 :- use_module(self_check).
21 :- use_module(debug).
22 :- use_module(kernel_objects).
23 :- use_module(kernel_waitflags).
24 :- use_module(error_manager,[add_internal_error/2]).
25
26 :- use_module(module_information,[module_info/2]).
27 :- module_info(group,interpreter).
28 :- module_info(description,'This module takes care of enumerating B variables.').
29
30 /* ------------------------------------------ */
31
32
33 /* can be used to apply the result of
34 b_getVarTypes_from_boolean_expression to a store */
35
36
37 :- use_module(typechecker,[type_check/2]).
38 :- assert_pre(b_enumerate:b_type_values_in_store(V,T,S),
39 (typechecker:type_check(V,list(variable_id)),
40 typechecker:type_check(T,list(basic_type_descriptor)),typechecker:type_check(S,store))).
41 :- assert_post(b_enumerate:b_type_values_in_store(_,_,_), true).
42
43 b_type_values_in_store([],[],_).
44 b_type_values_in_store([Variable|VT],[Type|TT],Store) :-
45 b_type_value_in_store(Variable,Type,Store),
46 b_type_values_in_store(VT,TT,Store).
47
48 :- use_module(store,[lookup_value_for_existing_id/3]).
49 b_type_value_in_store(Var,Type,Store) :-
50 (Var = 'Identifier'(VarID)
51 -> add_internal_error('Variable not in proper form: ',b_type_value_in_store(Var,Type,_))
52 ; VarID = Var),
53 lookup_value_for_existing_id(VarID,Store,Val),
54 (Val==fail
55 -> add_internal_error('Variable has not been given value: ',b_type_value_in_store(Var,Type,Store))
56 ; kernel_objects:basic_type(Val,Type)).
57
58
59
60
61 /* ------------------------------------------ */
62
63
64 :- assert_pre(b_enumerate:b_enumerate_values_in_store(V,T,_,S,_WF),
65 (typechecker:type_check(V,list(variable_id)),
66 typechecker:type_check(T,list(basic_type_descriptor)),typechecker:type_check(S,store))).
67 :- assert_post(b_enumerate:b_enumerate_values_in_store(_,_,_,_,_), true).
68
69 b_enumerate_values_in_store(Variables,Types,Values,Store,WF) :-
70 generate_typed_var_list(Variables,Types,Store,Values,TypedValues),
71 b_tighter_enumerate_values(TypedValues,WF).
72
73 :- block generate_typed_var_list(-,?,?,?,?).
74 generate_typed_var_list([],[],_,[],[]).
75 generate_typed_var_list([VarID|VT],[Type|TT],Store,Values,Res) :-
76 (store:lookup_value_for_existing_id(VarID,Store,Val), Val \== fail
77 -> Res = [typedval(Val,Type,VarID,trigger_true(VarID))|Rest], Values=[Val|ValT] % always trigger enumeration warning
78 ; add_internal_error('Variable has not been given value: ',VarID),
79 Res=Rest,Values=ValT
80 ),
81 generate_typed_var_list(VT,TT,Store,ValT,Rest).
82
83
84 /* ------------------------------------------ */
85
86 b_enumerate_typed_values(Values,Types,WF) :- % called by b_execute_eventb_action(becomes_element_of, ...
87 b_generate_typed_values(Values,Types,TypedVals),
88 b_tighter_enumerate_values(TypedVals,WF).
89
90 % generated typed values trigger the enumeration warning
91 b_generate_typed_values([],[],[]).
92 b_generate_typed_values([Val|Vrest],[Type|Trest],[typedval(Val,Type,'$UNKNOWN_ID',trigger_true(unknown))|TVrest]) :-
93 b_generate_typed_values(Vrest,Trest,TVrest).
94
95
96 b_extract_typedvalc([],[],_,[]).
97 b_extract_typedvalc([Variable|VT],[Type|TT],Store,Res) :-
98 (Variable = '_lambda_result_' % TO DO: use lambda_result info field ?; Note the check is repeated below in sort_typed_values
99 -> b_extract_typedvalc(VT,TT,Store,Res) % lambda result does not need to be enumerated; will be computed from rest
100 % TO DO: should we also deal specially with _lambda_result_ below in b_tighter_enumerate_values;
101 % or even infer in ANY statements, ... which variables are simply defined by equalities from the others
102 ; Res=[ExtractedH|ET],
103 b_extract_typedvalc_var(Variable,Type,Store,ExtractedH),
104 b_extract_typedvalc(VT,TT,Store,ET)).
105
106 b_extract_typedvalc_var(Var,Type,Store,typedval(Val,Type,VarID,trigger_true(VarID))) :-
107 (Var = 'Identifier'(VarID)
108 -> print(b_tighter_enumerate_value_in_store(Var,Type)),print(' variable not in proper form'),nl
109 ; VarID = Var),
110 (store:lookup_value_for_existing_id(VarID,Store,Val), Val \== fail
111 -> true
112 ; add_internal_error('Variable has not been given value: ',VarID)
113 ).
114
115 % update priority for certain types
116 % TO DO: we should probably group all infinite integer values together and take the variable with the smallest size
117
118 :- use_module(kernel_tools,[ground_value/1]).
119 b_tighter_enumerate_sorted_values([],_WF).
120 b_tighter_enumerate_sorted_values([typedvalc(Val,Type,VarID,EnumWarning,Card)|Rest],WF) :-
121 (ground_value(Val)
122 -> check_reached(Val,Type,VarID,Card,det,WF), %% <-----
123 b_tighter_enumerate_sorted_values(Rest,WF) %% no need to enumerate this value
124 ; treat_next_typed_valc(Type,Val,VarID,EnumWarning,Card,Rest,WF)).
125
126 :- use_module(library(lists)).
127 :- use_module(library(clpfd),[fd_size/2]).
128 :- use_module(kernel_waitflags,[large_finite_priority/1]).
129 treat_next_typed_valc(integer,Val,VarID,EnumWarning,_Card,Rest,WF) :-
130 nonvar(Val), Val=int(FD),
131 fd_size(FD,Size), % will return sup if no bounds + also works in non-CLPFD mode
132 number(Size),!,
133 treat_next_typed_valc_normal(integer,Val,VarID,EnumWarning,Size,Rest,WF).
134 treat_next_typed_valc(integer,Val,VarID,EnumWarning,Card,Rest,WF) :-
135 !,
136 large_finite_priority(LP),
137 treat_next_integer(first_iteration,[LP],Val,VarID,EnumWarning,Card,Rest,WF). % TO DO: maybe do several iterations 1000,LP
138 % however: test 1003 with plavis-TransData_SP_13.prob fails in this case; to do: investigate
139 treat_next_typed_valc(Type,Val,VarID,EnumWarning,Card,Rest,WF) :- % TO DO: also look for finite values in Rest if Type is infinite but not integer
140 treat_next_typed_valc_normal(Type,Val,VarID,EnumWarning,Card,Rest,WF).
141
142 % compute current priority of typedvalc; to be compared with @<
143 get_typedvalc_priority(typedvalc(Val,Type,_,_,_),Res) :- %Type=integer,
144 (get_typedvalc_finite_size(Type,Val,Size)
145 -> Res=Size % we have a finite value: use size
146 ; degree_value(Type,Val,Dg) -> NDg is -Dg, Res=sup(NDg) % use negative number of degree, so that larger degrees get priority
147 % relevant for e.g. test 1484: res=x*x+4*x+14
148 ; Res = sup(1)
149 ).
150 get_typedvalc_finite_size(Type,Val,Size) :-
151 finite_value(Type,Val,Size),
152 (Size=1 -> true ; \+ currently_useless_variable(Val)). % ,print(finite(Val,Size)),nl.
153
154 :- use_module(library(clpfd),[fd_degree/2]).
155 % try and get degree of a value
156 degree_value(integer,Val,Dg) :- %translate:print_value_variable(Val),nl,
157 nonvar(Val), Val=int(FD), fd_degree(FD,Dg), number(Dg).
158
159 :- use_module(b_global_sets,[b_global_set_cardinality/2]).
160 finite_value(integer,Val,Size) :- nonvar(Val), Val=int(FD), clpfd:fd_size(FD,Size), number(Size).
161 finite_value(boolean,Val,Size) :- (ground(Val) -> Size = 1 ; Size =2).
162 finite_value(string(_),Val,Size) :- ground(Val), Size=1.
163 finite_value(global(G),Val,Size) :- (ground(Val) -> Size = 1 ; b_global_set_cardinality(G,Size)).
164 finite_value(set(T),Val,Size) :- nonvar(Val), l_finite_value(T,Val,Size).
165 finite_value(couple(T1,T2),Val,Size) :- nonvar(Val), Val = (V1,V2),
166 finite_value(T1,V1,Size1),
167 finite_value(T2,V2,Size2),
168 kernel_objects:safe_mul(Size1,Size2,Size), number(Size).
169 finite_value(record(Fields),Val,Size) :- %print(fv(Fields,Val)),nl,
170 nonvar(Val), Val=rec(FVals),
171 finite_fields(Fields,FVals,Size), nl,print(finite_field(Val,Size)),nl,nl.
172 % TO DO: missing freetypes
173
174 l_finite_value(_Type,Val,_) :- var(Val),!,fail.
175 l_finite_value(_,avl_set(_),1).
176 l_finite_value(_Type,[],1).
177 l_finite_value(Type,[H|T],Size) :- l_finite_value(Type,T,SizeT), finite_value(Type,H,SizeH),
178 kernel_objects:safe_mul(SizeT,SizeH,Size), number(Size).
179
180 finite_fields(_Type,Val,_) :- var(Val),!,fail.
181 finite_fields([],[],1).
182 finite_fields([HType|TTypes],[H|T],Size) :- finite_fields(TTypes,T,SizeT), finite_value(HType,H,SizeH),
183 kernel_objects:safe_mul(SizeT,SizeH,Size), number(Size).
184
185 % find the typedvalc (Selected) with the smallest value (Prio) and return other (Rest) typedvalc-values
186 smallest_value([H|T],Selected,Rest,Prio) :-
187 get_typedvalc_priority(H,HPrio),
188 smallest_value_aux(T,H,HPrio,Selected,Rest,Prio).
189
190 smallest_value_aux([],H,HPrio,H,[],HPrio).
191 smallest_value_aux([H|T],Acc,AccPrio,Selected,Rest,SelPrio) :-
192 get_typedvalc_priority(H,HPrio),
193 %print(compare(HPrio,AccPrio)),nl, print((H,Acc)),nl,
194 (HPrio=1 -> smallest_value_aux(T,Acc,AccPrio,Selected,Rest,SelPrio) % remove this TC from list; does not need to be enumerated anymore
195 ; HPrio @< AccPrio
196 -> Rest = [Acc|TRest],
197 smallest_value_aux(T,H,HPrio,Selected,TRest,SelPrio)
198 ; Rest = [H|TRest],
199 smallest_value_aux(T,Acc,AccPrio,Selected,TRest,SelPrio)
200 ).
201
202 % we try again and see if the domain is now finite
203 % ideally we should register all integer variables in the kernel_waitflag FD list; maybe we should have a finite and infinite list? or use our own labeling get-next function clpfd_get_next_variable_to_label_ffc adapted for infinite domains
204 :- block treat_next_integer(-,?,?,?,?,?,?,?).
205 treat_next_integer(LWF,_,Val,VarID,EnumWarning,_Card,Rest,WF) :- LWF \== first_iteration, % print(treat(Val,VarID,Rest)),nl,
206 nonvar(Val), Val=int(FD),
207 clpfd:fd_size(FD,Size), % will return sup if no bounds + also works in non-CLPFD mode
208 %print(treat_next_integer(VarID,Val,Size,_Card,Rest)),nl,
209 number(Size),!,
210 (Size = 1 % for Size=1 no enumeration is necessary anyway
211 -> b_tighter_enumerate_sorted_values(Rest,WF) % no enumeration required
212 ; treat_next_typed_valc_normal(integer,Val,VarID,EnumWarning,Size,Rest,WF)).
213 treat_next_integer(_,Prios,Val,VarID,EnumWarning,Card,OtherTCs,WF) :- % ideally we should move this above the clause with NextPrio; but then test 412 fails
214 CurTC = typedvalc(Val,integer,VarID,EnumWarning,Card),
215 smallest_value([CurTC|OtherTCs],TC,Rest,Size),
216 % print(found_smallest(TC,Size,Rest)),nl,
217 ? (number(Size) % finite domain found
218 ;
219 Prios = [] % no more delaying; we have to enumerate an unbounded value
220 ),
221 !,
222 % print(prioritising(Size,TC,VarID,Card,Rest)),nl,
223 (Size == 1 % no enumeration required for this variable
224 -> b_tighter_enumerate_sorted_values(Rest,WF)
225 ; treat_next_typed_valc_normal4(TC,Size,Rest,WF)
226 ).
227 treat_next_integer(_,[NextPrio|Prios],Val,VarID,EnumWarning,Card,Rest,WF) :- !, % for test 1161 this clause causes a considerable slowdown (VarID == dz1 -> trace ; true),
228 % print(get_wait_flag_for(VarID,Val,NextPrio,Rest)),nl,
229 get_wait_flag(NextPrio,treat_next_integer(VarID,Val),WF,LWF),
230 treat_next_integer(LWF,Prios,Val,VarID,EnumWarning,Card,Rest,WF).
231 treat_next_integer(_,_,Val,VarID,EnumWarning,Card,Rest,WF) :-
232 treat_next_typed_valc_normal(integer,Val,VarID,EnumWarning,Card,Rest,WF). % we have already delayed; no need to delay further
233
234 treat_next_typed_valc_normal4(typedvalc(Val,Type,VarID,EnumWarning,Card),Size,Rest,WF) :-
235 (number(Size) -> NewCard=Size ; NewCard=Card), % use narrowed down card if possible
236 treat_next_typed_valc_normal(Type,Val,VarID,EnumWarning,NewCard,Rest,WF).
237 treat_next_typed_valc_normal(Type,Val,VarID,EnumWarning,Card,Rest,WF) :-
238 get_wait_flag(Card,tighter_enum(VarID,Val,Type),WF,LWF),
239 b_tighter_enumerate_sorted_value_and_continue(LWF,Val,Type,VarID,EnumWarning,Card,Rest,WF).
240
241 :- block b_tighter_enumerate_sorted_value_and_continue(-,?,?,?,?,?,?,?).
242 b_tighter_enumerate_sorted_value_and_continue(_LWF,Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
243 ? (Rest = [] -> true ; get_minimum_waitflag_prio(WF,Prio,_), Prio < 20000),
244 % only check for useless if there are either other variables to chose from or other WF goals
245 ? currently_useless_variable(Val),
246 ? !,
247 ? b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF).
248 b_tighter_enumerate_sorted_value_and_continue(_LWF,Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
249 ? check_reached(Val,Type,VarID,Card,WF), %% <-----
250 %% tools:print_bt_message(enumerate(VarID,Val)), %%
251 ? enum_tight_with_wf(Val,Type,EnumWarning,WF),
252 %% tools:print_bt_message(after_enumerate(VarID,Val)),
253 %(VarID=='VS_NOERRORCOND' -> print(done_enum(VarID,Val)),nl ; true),
254 b_tighter_enumerate_sorted_values(Rest,WF).
255
256 b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
257 get_next_useful_variable(Rest,RVal,RType,RVarID,REnumWarning,RCard,RRest), % ,print(using(RVarID,RVal,RType)),nl
258 !,
259 %debug_println(9,skipping(Val,VarID,Card,new(RVal,RType,RVarID,RCard))),
260 (RCard =< Card /* we can enumerate straight away */
261 -> check_reached(RVal,RType,RVarID,RCard,WF), %% <------
262 enum_tight_with_wf(RVal,RType,EnumWarning,WF),
263 b_tighter_enumerate_sorted_values([typedvalc(Val,Type,VarID,EnumWarning,Card)|RRest],WF)
264 ; b_tighter_enumerate_sorted_values([typedvalc(RVal,RType,RVarID,REnumWarning,RCard),
265 typedvalc(Val,Type,VarID,EnumWarning,Card)|RRest],WF)
266 ).
267 b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
268 %debug_println(19,all_variables_useless(Val,Card)),
269 ? get_minimum_waitflag_prio(WF,Prio,_Info),
270 ? Prio < 20000, % avoid infinite enumeration ... TO DO: improve check
271 %debug_println(19,all_variables_useless_info(Prio,Info)),
272 ? !,
273 ? ground_wait_flag_to(WF,Prio),
274 % Now try again:
275 ? b_tighter_enumerate_sorted_value_and_continue(1,Val,Type,VarID,EnumWarning,Card,Rest,WF).
276 b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
277 ? check_reached(Val,Type,VarID,Card,WF), %% <-----
278 %% tools:print_bt_message(enumerate(VarID,Val)), %%
279 ? enum_tight_with_wf(Val,Type,EnumWarning,WF),
280 %% tools:print_bt_message(after_enumerate(VarID,Val)),
281 %(VarID=='VS_NOERRORCOND' -> print(done_enum(VarID,Val)),nl ; true),
282 b_tighter_enumerate_sorted_values(Rest,WF).
283
284 % --------------------
285
286 % add WF information; so that we can provide better enumeration warning messages
287 add_wf_context(trigger_true(Info),WF,trigger_true(enum_wf_context(WF,Info))).
288 add_wf_context(trigger_false(Info),WF,trigger_false(enum_wf_context(WF,Info))).
289 add_wf_context(trigger_throw(Info),WF,trigger_throw(enum_wf_context(WF,Info))).
290
291 % TO DO: check whether we should not call enumerate_basic_type_wf instead
292
293 :- use_module(kernel_objects,[enumerate_tight_type/3]).
294 enum_tight_with_wf(Val,Type,EnumWarning,WF) :-
295 ? (add_wf_context(EnumWarning,WF,NewWarning) -> enumerate_tight_type(Val,Type,NewWarning)
296 ; enumerate_tight_type(Val,Type,EnumWarning)).
297
298
299
300 % ---------------------
301
302 get_next_useful_variable([typedvalc(Val,Type,VarID,EnumWarning,Card)|Rest],RVal,RType,RVarID,REnumWarning,RCard,RRest) :-
303 (currently_useless_variable(Val)
304 -> RRest=[typedvalc(Val,Type,VarID,EnumWarning,Card)|TRRest],
305 get_next_useful_variable(Rest,RVal,RType,RVarID,REnumWarning,RCard,TRRest)
306 ; RRest=Rest, RVal=Val, RType=Type, RVarID=VarID, REnumWarning = EnumWarning, RCard=Card
307 ).
308
309
310 /* purpose: check if an enumeration is useful or not and give priority to useful variables ? */
311 %:- use_module(library(clpfd),[fd_dom/2]).
312 currently_useless_variable(Val) :- var(Val),!,frozen(Val,Goal), % print(enum(Val,Goal)),nl,
313 ? (enumeration_only_goal(Goal,Val) -> true
314 ; % print(useful_val(Val,Goal)),nl,nl, %trace, enumeration_only_goal(Goal,Val),
315 fail).
316 currently_useless_variable(int(Val)) :- currently_useless_variable(Val).
317 currently_useless_variable(fd(Val,_)) :- currently_useless_variable(Val).
318 currently_useless_variable(string(Val)) :- currently_useless_variable(Val).
319 %fd_dom(Val,Dom),print(uselessfd(Val,Dom)),nl.
320
321 :- use_module(clpfd_interface,[clpfd_degree/2]).
322 enumeration_only_goal(true,_).
323 %enumeration_only_goal(fd_utils_clpfd:delayed_enum_fd(V,_,_,_),Val) :- V==Val.
324 enumeration_only_goal(kernel_objects:call_enumerate_int(V,_,_,_),Val) :- V==Val.
325 enumeration_only_goal(kernel_objects:enumerate_int_wf(V,_,_),Val) :- V==Val.
326 enumeration_only_goal(kernel_objects:enumerate_natural(V,_,_,_),Val) :- V==Val.
327 enumeration_only_goal((A,B),Val) :-
328 (enumeration_only_goal(A,Val) -> enumeration_only_goal(B,Val)
329 ; % we have not detected A as enumeration only: check if we can find an annotation not to enumerate
330 force_enumeration_only_goal(A,Val) % Note: we only check first component; on the assumption that these co-routines are added early and to avoid useless lookups; TO DO: is there a better solution ?
331 ).
332 enumeration_only_goal(clpfd:(X in _),Var) :- Var==X,
333 clpfd_degree(X,0). % only goal is the enumerator itself; but CLPFD constraints are ***NOT*** shown in frozen(...) so we need to call clpfd_degree
334 enumeration_only_goal(bsets_clp:is_sequence_wf_ex(V,GS,_,_),Val) :- V==Val, nonvar(GS),GS=global_set(_). % only constraint: we should generate a sequence
335 enumeration_only_goal(external_functions:string_to_int2(_,V,_,_),Val) :- V==Val.
336 enumeration_only_goal(external_functions:printf(_,V,_,_),Val) :- V==Val.
337 enumeration_only_goal(prolog:dif(A,B),Var) :- (Var==A ; Var==B).
338
339 enumeration_only_goal(prolog:trig_ground(A1,_,_,_,Trigger),Val) :- Val==A1,
340 triggers_better_enumeration(Trigger,Val,3). % if this only triggers an enumeration of Val itself; it is better to let the other variable trigger the enumeration
341
342 force_enumeration_only_goal((A,B),Val) :-
343 (force_enumeration_only_goal(A,Val) -> true ; force_enumeration_only_goal(B,Val) ).
344 force_enumeration_only_goal(external_functions:'DO_NOT_ENUMERATE'(V,_,_),Val) :- V==Val.
345
346 % check if Trigger either triggers a better enumerator or just debugging code
347 triggers_better_enumeration(Trigger,Val,Depth) :- Depth>0, D1 is Depth-1,
348 frozen(Trigger,TrigGoal),
349 %print(trig(TrigGoal,Val)),nl,trace,
350 ( better_enum(TrigGoal,Trigger,Val,D1) -> true).
351
352 better_enum((A,B),Trigger,Val,Depth) :- better_enum(A,Trigger,Val,Depth), better_enum(B,Trigger,Val,Depth).
353 better_enum(prolog:trig_and(_,_,_,_,Trigger1),Trigger,Val,Depth) :- !,
354 (Trigger1==Trigger -> true ; triggers_better_enumeration(Trigger1,Val,Depth)).
355 better_enum(prolog:trig_or(_,Trigger1,_),Trigger,Val,Depth) :- !,
356 (Trigger1==Trigger -> true ; triggers_better_enumeration(Trigger1,Val,Depth)).
357 better_enum(prolog:trig_ground(VV,_,_,Trigger1,_),Trigger,Val,Depth) :- !,
358 (Trigger1==Trigger -> true ; VV=Val -> true ; triggers_better_enumeration(Trigger1,Val,Depth)).
359 better_enum(prolog:when(WT,_,G), Trigger,Val,Depth) :- !,
360 Trigger==WT, better_enum(G,Trigger,Val,Depth).
361 better_enum(custom_explicit_sets:couple_element_of_avl_set(_X,_Y,_AVL,_WF1,_WF),_,_Val,_Depth) :- !,
362 % TO DO: add more enumerators of Val
363 % TO DO: VAL occurs in _X !!
364 true. %print(avl_trig(X,Y,Val,Depth)),nl.
365 better_enum(external_functions:G,_,_Val,_Depth) :- external_debug_function(G).
366
367 external_debug_function(fprintf2(_,_,_,_)). % TO DO: add more
368
369
370
371 b_tighter_enumerate_single_value(Val,Type,VarID,WF) :-
372 b_tighter_enumerate_values([typedval(Val,Type,VarID,trigger_true(VarID))],WF).
373
374 b_tighter_enumerate_values(TypedValues,WF) :-
375 ~~mnf(sort_typed_values(TypedValues,[],SortedValues)), % no longer required ??
376 b_tighter_enumerate_sorted_values(SortedValues,WF).
377
378 :- if(debug:global_debug_flag).
379 :- dynamic reached/4.
380 my_spy('P_Env_Output_TargetSpeed_Speed').
381 check_reached(Val,Type,VarID,Card,WF) :-
382 (my_spy(VarID) -> print(' SPY POINT : '), print(VarID), print(' = '), print(Val),nl,
383 portray_waitflags(WF), trace ; true),
384 (ground_value(Val) -> check_reached(Val,Type,VarID,Card,det,WF)
385 ; check_reached(Val,Type,VarID,Card,enum,WF)).
386 % findall(r(Card,VarID,Info),b_enumerate:reached(VarID,Card,Info),_A),sort(_A,_AS),reverse(_AS,RAS).
387 check_reached(Val,Type,VarID,Card,Info,WF) :-
388 (retract(reached(VarID,RR,Info)) -> true ; RR=0),
389 R1 is RR+1,
390 (RR mod 1000 < 1 -> (RR=0 -> print('REACHED : ') ; print(' AGAIN : ')), print(Info), print(' '),
391 print(VarID), print(' : '), print(Card),
392 print(' : '), print(Type), print(' : '), print(Val), print(' :: '), print(RR), nl,
393 (my_spy(VarID) %(RR>8000,RR<40001)
394 -> portray_waitflags(WF),trace ; portray_waitflags(WF))
395 %, (RR=1000 -> trace ; true)
396 ; true),
397 assert(reached(VarID,R1,Info)).
398 b_trace_tighter_enumerate_values(TypedValues,WF) :-
399 ~~mnf(sort_typed_values(TypedValues,[],SortedValues)),
400 print('ENUMERATING VALUES:'),nl,print_values(SortedValues), %%
401 nl, portray_waitflags(WF),nl,
402 b_trace_tighter_enumerate_values2(SortedValues,WF),
403 print('FINISHED SETTING UP ENUMERATION'),nl, portray_waitflags(WF),nl.
404 b_trace_tighter_enumerate_values2(SortedValues,WF) :- retractall(reached(_,_,_)),
405 b_tighter_enumerate_sorted_values(SortedValues,WF).
406
407 print_values([]).
408 print_values([typedvalc(Val,Type,VarID,_EnumWarning,Card)|Rest]) :-
409 print_value(VarID,Card,Type,Val),
410 (ground_value(Val) -> true ; when(ground(Val),(nl,print('HAS BECOME GROUND: '),print_value(VarID,Card,Type,Val)))),
411 print_values(Rest).
412
413 print_value(VarID,Card,Type,Val) :-
414 print(' '),
415 print(VarID), print(' :card='), print(Card), print(' ('), print(Type), print(') = '), print(Val),nl.
416 :- elif(false).
417 :- dynamic reached/4, enumerated/2,enum_edge/3.
418 check_reached(_Val,_Type,_VarID,_Card,_WF) :- check_reached(_Val,_Type,_VarID,_Card,enum,_WF).
419 check_reached(_Val,_Type,VarID,_Card,Info,_WF) :-
420 (retract(reached(VarID,RR,Info)) -> true ; RR=0),
421 R1 is RR+1,
422 assert(reached(VarID,R1,Info)),
423 (enumerated(TopVar,Level) -> add_edge(TopVar,VarID,Level),L1 is Level+1 ; L1=0),
424 asserta(enumerated(VarID,L1)).
425 check_reached(_Val,_Type,VarID,_Card,_Info,_WF) :-
426 retract(enumerated(VarID,_)),fail.
427 add_edge(TopVar,VarID,Level) :-
428 (enum_edge(TopVar,VarID,Level) -> true ; assert(enum_edge(TopVar,VarID,Level))).
429
430 % b_enumerate:print_enum_stats.
431 print_enum_stats :- findall( enum(Count,VarID,Info), reached(VarID,Count,Info),L),
432 sort(L,SL),
433 print('Enumeration Frequency'),nl,
434 member(enum(C,ID,I),SL), format(' ~w ~w ~w~n',[C, ID, I]),
435 fail.
436 print_enum_stats :-
437 enum_edge(TopVar,VarID,0), format('~w ---> ~w~n',[TopVar,VarID]),
438 print_edges(VarID,1),
439 fail.
440 print_enum_stats :- nl.
441 print_edges(VarID,Level) :- enum_edge(VarID,NxtId,Level),
442 format(' ~w -(~w)--> ~w~n',[VarID,Level,NxtId]),
443 fail.
444 print_edges(_,_).
445 b_trace_tighter_enumerate_values(TypedValues,WF) :- b_tighter_enumerate_values(TypedValues,WF).
446 :- else.
447 check_reached(Val,Type,'_lambda_result_',Card,_WF) :- Card \= det, \+ ground_value(Val), !,
448 format('~n*** Enumerating lambda result : ~w (Type=~w, Card=~w)~n~n',[Val,Type,Card]).
449 check_reached(_Val,_Type,_VarID,_Card,_WF).
450 check_reached(_Val,_Type,_VarID,_Card,_Info,_WF).
451 b_trace_tighter_enumerate_values(TypedValues,WF) :- b_tighter_enumerate_values(TypedValues,WF).
452 :- endif.
453
454 /* comment in for debugging :
455 % dummy call to register variable name with free Prolog variables:
456 % can be obtained using frozen()
457 :- public register_prolog_variable_name/3. % Debugging tool
458 :- block register_prolog_variable_name(-,?,?).
459 register_prolog_variable_name(int(Val),Name,Type) :- !, %print(register_int(Val,Name,Type)),nl,
460 register_prolog_variable_name(Val,Name,Type).
461 register_prolog_variable_name(fd(Val,_),Name,Type) :- !,
462 register_prolog_variable_name(Val,Name,Type).
463 register_prolog_variable_name(string(Val),Name,Type) :- !,
464 register_prolog_variable_name(Val,Name,Type).
465 register_prolog_variable_name((A,B),Name,Type) :- !,
466 register_prolog_variable_name(A,left(Name,mapto(B)),Type),
467 register_prolog_variable_name(B,right(Name,mapfrom(A)),Type).
468 register_prolog_variable_name([A|T],Name,Type) :- !,
469 register_prolog_variable_name(A,el(Name),Type),
470 register_prolog_variable_name(T,Name,Type).
471 register_prolog_variable_name(_,_,_).
472 % TO DO: something that pretty prints the path information for the average user
473
474 % a tool to get variable name if it was registered
475 :- public get_prolog_variable_name/3. % Debugging tool
476 get_prolog_variable_name(X,Name,Type) :- var(X),
477 frozen(X,Goal), print(goal(X,Goal)),nl,
478 goal_member(Goal,b_enumerate:register_prolog_variable_name(_,ID,T)),
479 Name=ID, Type=T.
480 goal_member(X,X).
481 goal_member((A,B),X) :- goal_member(A,X) ; goal_member(B,X).
482 ------- */
483
484 sort_typed_values([],R,R).
485 sort_typed_values([typedval(Val,Type,VarID,EnumWarning)|Rest],SortedSoFar,Res) :-
486 %% comment in next line to keep track of variable names for enumeration warnings, etc...
487 %% register_prolog_variable_name(Val,VarID,Type), % dummy call to register variable name with free Prolog variables
488 (VarID = '_lambda_result_' ->
489 (Rest=[], SortedSoFar=[], \+ ground_value(Val)
490 % it is the only non-ground value to enumerate
491 -> get_max_cardinality_as_priority(Type,CardPrio),
492 insert_val(SortedSoFar,Val,Type,VarID,EnumWarning,CardPrio,NewSorted),
493 %format('~n*** Enumerating lambda result : ~w (~w:~w)~n~n',[Val,Type,CardPrio]),
494 debug_println(20,enumerate_lambda_result(Val)) % was triggered in test 1093 and 1161, but seems no longer necessary
495 ; NewSorted=SortedSoFar)
496 ; ground_value(Val) -> NewSorted=SortedSoFar
497 ; get_max_cardinality_as_priority(Type,CardPrio),
498 %% TO DO: maybe also take shape of Val into account; e.g. if cardinality of a set already fixed...
499 insert_val(SortedSoFar,Val,Type,VarID,EnumWarning,CardPrio,NewSorted)
500 ),
501 sort_typed_values(Rest,NewSorted,Res).
502
503 get_max_cardinality_as_priority(integer,Prio) :- !, integer_priority(Prio).
504 get_max_cardinality_as_priority(Type,Prio) :-
505 ~~mnf(kernel_objects:max_cardinality(Type,Card)),
506 (Card \= inf -> Prio=Card
507 ; inf_type_prio(Type,Prio)
508 ).
509
510 % Try to give priority to simpler infinite types (such as integer over seq(_) ,...)
511 % TO DO: to a full-blown analysis ...
512 inf_type_prio(integer,Prio) :- !, integer_priority(Prio).
513 inf_type_prio(seq(X),Prio) :- !, inf_type_prio(X,P1), Prio is P1+11.
514 inf_type_prio(set(X),Prio) :- !, inf_type_prio(X,P1), Prio is P1+10.
515 %inf_type_prio(couple(_,_),Prio) :- !, TO DO check if both args are infinite or not ...
516 inf_type_prio(_,Prio) :- !, integer_priority(P), Prio is P+1.
517
518
519 %typedvalc = typedval + cardinality information
520 insert_val([],Val,Type,VarID,EnumWarning,Card,[typedvalc(Val,Type,VarID,EnumWarning,Card)]).
521 insert_val([TC|T], Val,Type, VarID, EnumWarning, Card, Res) :-
522 TC = typedvalc(V1,_T1,_Var1,_W1,C1),
523 ? (cardval_greater_than(C1,V1,Card,Val)
524 -> Res = [typedvalc(Val,Type,VarID,EnumWarning,Card),TC|T]
525 ; Res = [TC|RT],
526 insert_val(T,Val,Type,VarID,EnumWarning,Card,RT)
527 ).
528
529
530 :- use_module(library(random)).
531 cardval_greater_than(C1,_,Card,_) :- Card \== inf, (C1=inf -> true ; C1>Card).
532 cardval_greater_than(Card,V1,Card,Val) :-
533 var(V1), nonvar(Val). % if card equal give priority to nonvariable values
534 cardval_greater_than(Card,_,Card,_) :-
535 preferences:preference(randomise_enumeration_order,true),
536 % TO DO: maybe we even want to change the order if cardinality different ?
537 % this also does not really generate random permutation of variables with same cardinality
538 random(1,3,1).
539
540 /*
541 % call to enumerate an integer ensuring that you go at least from MinFrom to MinTo
542 %:- block enumerate_integer_with_min_range_wf(-,?,?,?).
543 enumerate_integer_with_min_range_wf(int(X),MinFrom,MinTo,WF) :-
544 integer_priority(Prio), P1 is Prio-1,
545 ... removed ...
546 */