1 % (c) 2009-2023 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- 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_all_values/2,
12 b_tighter_enumerate_values/3,
13 b_tighter_enumerate_values_in_ctxt/3,
14 b_tighter_enumerate_single_value/5,
15
16 b_extract_typedvalc/5,
17 construct_typedval_infos/4,
18
19 extract_do_not_enum_ids_from_predicate/2
20 %enumerate_integer_with_min_range_wf/4 % no longer used
21 ]).
22
23
24 :- use_module(self_check).
25 :- use_module(debug).
26 :- use_module(kernel_objects).
27 :- use_module(kernel_waitflags).
28 :- use_module(error_manager,[add_internal_error/2]).
29
30 :- use_module(module_information,[module_info/2]).
31 :- module_info(group,interpreter).
32 :- module_info(description,'This module takes care of enumerating B variables.').
33
34 /* ------------------------------------------ */
35
36
37 /* can be used to apply the result of
38 b_getVarTypes_from_boolean_expression to a store */
39
40
41 :- use_module(typechecker,[type_check/2]).
42 :- assert_pre(b_enumerate:b_type_values_in_store(V,T,S),
43 (typechecker:type_check(V,list(variable_id)),
44 typechecker:type_check(T,list(basic_type_descriptor)),typechecker:type_check(S,store))).
45 :- assert_post(b_enumerate:b_type_values_in_store(_,_,_), true).
46
47 b_type_values_in_store([],[],_).
48 b_type_values_in_store([Variable|VT],[Type|TT],Store) :-
49 ? b_type_value_in_store(Variable,Type,Store),
50 ? b_type_values_in_store(VT,TT,Store).
51
52 :- use_module(store,[lookup_value_for_existing_id/3]).
53 b_type_value_in_store(Var,Type,Store) :-
54 (Var = 'Identifier'(VarID)
55 -> add_internal_error('Variable not in proper form: ',b_type_value_in_store(Var,Type,_))
56 ; VarID = Var),
57 lookup_value_for_existing_id(VarID,Store,Val),
58 (Val==fail
59 -> add_internal_error('Variable has not been given value: ',b_type_value_in_store(Var,Type,Store))
60 ? ; kernel_objects:basic_type(Val,Type)).
61
62
63
64
65 /* ------------------------------------------ */
66
67
68 :- assert_pre(b_enumerate:b_enumerate_values_in_store(V,T,_,S,_WF),
69 (typechecker:type_check(V,list(variable_id)),
70 typechecker:type_check(T,list(basic_type_descriptor)),typechecker:type_check(S,store))).
71 :- assert_post(b_enumerate:b_enumerate_values_in_store(_,_,_,_,_), true).
72
73 % note: assumes no lambda_result variables in scope
74 b_enumerate_values_in_store(Variables,Types,Values,Store,WF) :-
75 generate_typed_var_list(Variables,Types,Store,Values,TypedValues),
76 b_tighter_enumerate_all_values(TypedValues,WF).
77
78 :- block generate_typed_var_list(-,?,?,?,?).
79 generate_typed_var_list([],[],_,[],[]).
80 generate_typed_var_list([VarID|VT],[Type|TT],Store,Values,Res) :-
81 (store:lookup_value_for_existing_id(VarID,Store,Val), Val \== fail
82 -> construct_typedval_infos(VarID,[],trigger_true(VarID),TINFO),
83 Res = [typedval(Val,Type,VarID,TINFO)|Rest], % always trigger enumeration warning
84 Values=[Val|ValT]
85 ; add_internal_error('Variable has not been given value: ',VarID),
86 Res=Rest,Values=ValT
87 ),
88 generate_typed_var_list(VT,TT,Store,ValT,Rest).
89
90
91 /* ------------------------------------------ */
92
93 b_enumerate_typed_values(Values,Types,WF) :- % called by b_execute_eventb_action(becomes_element_of, ...
94 b_generate_typed_values(Values,Types,TypedVals),
95 b_tighter_enumerate_all_values(TypedVals,WF).
96
97 % generated typed values trigger the enumeration warning
98 b_generate_typed_values([],[],[]).
99 b_generate_typed_values([Val|Vrest],[Type|Trest],[typedval(Val,Type,'$UNKNOWN_ID',TINFO)|TVrest]) :-
100 construct_typedval_infos('$unknown',[],trigger_true(unknown),TINFO),
101 b_generate_typed_values(Vrest,Trest,TVrest).
102
103 :- use_module(library(ordsets),[ord_member/2]).
104 is_lambda_result_or_useless(ID,TINFO,DoNotEnumIds) :-
105 (is_lambda_result_id(ID) -> true
106 ; is_lambda_result_annotated(ID,TINFO) -> true
107 ; ord_member(ID,DoNotEnumIds)).
108
109 is_lambda_result_id('_lambda_result_'). % TO DO: use lambda_result info field ?
110 %is_lambda_result_id(caval__msg__all). is_lambda_result_id(data_verified__index__0). is_lambda_result_id(data_verified__index__1). is_lambda_result_id(status).
111 is_lambda_result_annotated(ID,lambda_result(Trigger)) :-
112 (var(Trigger) -> add_internal_error('Illegal trigger for enumeration variable:',ID),fail
113 ; true).
114
115 % store relevant infos from AST info list for use in typedval(_,_,_,INFO) field
116 construct_typedval_infos(VarID,Infos,Trigger,Res) :-
117 ? member(Info,Infos),
118 lambda_result_info(Info,VarID),
119 !,
120 Res = lambda_result(Trigger).
121 construct_typedval_infos(_,_,Trigger,Trigger).
122
123 lambda_result_info(lambda_result(VarID),VarID).
124 lambda_result_info(prob_annotation('DO_NOT_ENUMERATE'(VarID)),VarID).
125 % TO DO: merge into one sorted info field: lambda_result(SortedIds)
126
127 % extract enumeration warning from Trigger Info field
128 get_enum_warning_info(lambda_result(Trigger),Res) :- !, Res=Trigger.
129 get_enum_warning_info(Trigger,Trigger).
130
131 % add enum_Warning wrapper to trigger if not already there
132 add_enum_warning_info(lambda_result(Trigger),Res) :- !, Res=lambda_result(Trigger).
133 add_enum_warning_info(Trigger,lambda_result(Trigger)).
134
135
136 % only called by b_not_test_closure_enum:
137 b_extract_typedvalc([],[],_,_,[]).
138 b_extract_typedvalc([Variable|VT],[Type|TT],Infos,Store,Res) :-
139 (is_lambda_result_or_useless(Variable,Infos,[]) % TO DO: check if we can pass DO_NOT_ENUMERATE Infos
140 % TO DO: use lambda_result info field ?; Note the check is repeated below in sort_typed_values
141 -> b_extract_typedvalc(VT,TT,Infos,Store,Res)
142 % lambda result does not need to be enumerated; will be computed from rest
143 % TO DO: should we also deal specially with _lambda_result_ below in b_tighter_enumerate_values;
144 % or even infer in ANY statements, ... which variables are simply defined by equalities from the others
145 ; Res=[ExtractedH|ET],
146 b_extract_typedvalc_var(Variable,Type,Infos,Store,ExtractedH),
147 b_extract_typedvalc(VT,TT,Infos,Store,ET)).
148
149 b_extract_typedvalc_var(Var,Type,Infos,Store,typedval(Val,Type,VarID,TINFO)) :-
150 (Var = 'Identifier'(VarID)
151 -> print(b_tighter_enumerate_value_in_store(Var,Type)),print(' variable not in proper form'),nl
152 ; VarID = Var),
153 construct_typedval_infos(VarID,Infos,trigger_true(VarID),TINFO),
154 (store:lookup_value_for_existing_id(VarID,Store,Val), Val \== fail
155 -> true
156 ; add_internal_error('Variable has not been given value: ',VarID)
157 ).
158
159 % update priority for certain types
160 % TO DO: we should probably group all infinite integer values together and take the variable with the smallest size
161
162 :- use_module(kernel_tools,[ground_value/1]).
163 b_tighter_enumerate_sorted_values([],_WF).
164 b_tighter_enumerate_sorted_values([typedvalc(Val,Type,VarID,EnumWarningInfos,Card)|Rest],WF) :-
165 (ground_value(Val)
166 -> check_reached(Val,Type,VarID,Card,det,WF), %% <-----
167 b_tighter_enumerate_sorted_values(Rest,WF) %% no need to enumerate this value
168 ; treat_next_typed_valc(Type,Val,VarID,EnumWarningInfos,Card,Rest,WF)).
169
170 :- use_module(library(lists)).
171 :- use_module(clpfd_interface,[ clpfd_size/2]).
172 :- use_module(kernel_waitflags,[large_finite_priority/1]).
173 treat_next_typed_valc(integer,Val,VarID,EnumWarningInfos,_Card,Rest,WF) :-
174 nonvar(Val), Val=int(FD),
175 clpfd_size(FD,Size), % will return sup if no bounds + also works in non-CLPFD mode
176 number(Size),!,
177 treat_next_typed_valc_normal(integer,Val,VarID,EnumWarningInfos,Size,Rest,WF).
178 treat_next_typed_valc(integer,Val,VarID,EnumWarningInfos,Card,Rest,WF) :-
179 !,
180 large_finite_priority(LP),
181 treat_next_integer(first_iteration,[LP],Val,VarID,EnumWarningInfos,Card,Rest,WF). % TO DO: maybe do several iterations 1000,LP
182 % however: test 1003 with plavis-TransData_SP_13.prob fails in this case; to do: investigate
183 treat_next_typed_valc(Type,Val,VarID,EnumWarningInfos,Card,Rest,WF) :- % TO DO: also look for finite values in Rest if Type is infinite but not integer
184 treat_next_typed_valc_normal(Type,Val,VarID,EnumWarningInfos,Card,Rest,WF).
185
186 % compute current priority of typedvalc; to be compared with @<
187 get_typedvalc_priority(typedvalc(Val,Type,_,Enum,_Prio),Res) :- %Type=integer,
188 (Enum = lambda_result(_) -> Res=sup(1) % do not give priority to lambda_result
189 ? ; get_typedvalc_finite_size(Type,Val,Size)
190 -> Res=Size % we have a finite value: use size
191 ; degree_value(Type,Val,Dg)
192 -> NDg is -Dg, Res=sup(NDg) % use negative number of degree, so that larger degrees get priority
193 % relevant for e.g. test 1484: res=x*x+4*x+14
194 ; Res = sup(1)
195 ).
196 get_typedvalc_finite_size(Type,Val,Size) :-
197 ? finite_value(Type,Val,Size),
198 (Size=1 -> true ;
199 \+ currently_useless_variable(Val)). % ,print(finite(Val,Size)),nl.
200
201 :- use_module(library(clpfd),[fd_degree/2]).
202 % try and get degree of a value
203 degree_value(integer,Val,Dg) :- %translate:print_value_variable(Val),nl,
204 nonvar(Val), Val=int(FD), fd_degree(FD,Dg), number(Dg).
205
206 :- use_module(b_global_sets,[b_global_set_cardinality/2]).
207 finite_value(integer,Val,Size) :- nonvar(Val), Val=int(FD), clpfd_size(FD,Size), number(Size).
208 finite_value(boolean,Val,Size) :- (ground(Val) -> Size = 1 ; Size =2).
209 finite_value(string(_),Val,Size) :- ground(Val), Size=1.
210 finite_value(real(_),Val,Size) :- ground(Val), Size=1.
211 finite_value(global(G),Val,Size) :- (ground(Val) -> Size = 1 ; b_global_set_cardinality(G,Size)).
212 ?finite_value(set(T),Val,Size) :- nonvar(Val), l_finite_value(T,Val,Size).
213 finite_value(couple(T1,T2),Val,Size) :- nonvar(Val), Val = (V1,V2),
214 finite_value(T1,V1,Size1),
215 ? finite_value(T2,V2,Size2),
216 kernel_objects:safe_mul(Size1,Size2,Size), number(Size).
217 finite_value(record(Fields),Val,Size) :-
218 nonvar(Val), Val=rec(FVals),
219 finite_fields(Fields,FVals,Size), nl,print(finite_field(Val,Size)),nl,nl.
220 % TO DO: missing freetypes
221
222 l_finite_value(_Type,Val,_) :- var(Val),!,fail.
223 l_finite_value(_,avl_set(_),1).
224 l_finite_value(_Type,[],1).
225 ?l_finite_value(Type,[H|T],Size) :- l_finite_value(Type,T,SizeT), finite_value(Type,H,SizeH),
226 kernel_objects:safe_mul(SizeT,SizeH,Size), number(Size).
227
228 finite_fields(_Type,Val,_) :- var(Val),!,fail.
229 finite_fields([],[],1).
230 finite_fields([HType|TTypes],[H|T],Size) :- finite_fields(TTypes,T,SizeT), finite_value(HType,H,SizeH),
231 kernel_objects:safe_mul(SizeT,SizeH,Size), number(Size).
232
233 % find the typedvalc (Selected) with the smallest value (Prio) and return other (Rest) typedvalc-values
234 smallest_value([H|T],Selected,Rest,Prio) :-
235 get_typedvalc_priority(H,HPrio),
236 smallest_value_aux(T,H,HPrio,Selected,Rest,Prio).
237
238 smallest_value_aux([],H,HPrio,H,[],HPrio).
239 smallest_value_aux([H|T],Acc,AccPrio,Selected,Rest,SelPrio) :-
240 get_typedvalc_priority(H,HPrio),
241 (HPrio=1 -> smallest_value_aux(T,Acc,AccPrio,Selected,Rest,SelPrio) % remove this TC from list; does not need to be enumerated anymore
242 ; HPrio @< AccPrio
243 -> Rest = [Acc|TRest],
244 smallest_value_aux(T,H,HPrio,Selected,TRest,SelPrio)
245 ; Rest = [H|TRest],
246 smallest_value_aux(T,Acc,AccPrio,Selected,TRest,SelPrio)
247 ).
248
249 % we try again and see if the domain is now finite
250 % 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
251 :- block treat_next_integer(-,?,?,?,?,?,?,?).
252 treat_next_integer(LWF,_,Val,VarID,EnumWarning,_Card,Rest,WF) :- LWF \== first_iteration, % print(treat(Val,VarID,Rest)),nl,
253 nonvar(Val), Val=int(FD),
254 clpfd_size(FD,Size), % will return sup if no bounds + also works in non-CLPFD mode
255 %print(treat_next_integer(VarID,Val,Size,_Card,Rest)),nl,
256 number(Size),!,
257 (Size = 1 % for Size=1 no enumeration is necessary anyway
258 -> b_tighter_enumerate_sorted_values(Rest,WF) % no enumeration required
259 ; treat_next_typed_valc_normal(integer,Val,VarID,EnumWarning,Size,Rest,WF)).
260 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
261 CurTC = typedvalc(Val,integer,VarID,EnumWarning,Card),
262 smallest_value([CurTC|OtherTCs],TC,Rest,Size),
263 (number(Size) % finite domain found
264 ;
265 Prios = [] % no more delaying; we have to enumerate an unbounded value
266 ),
267 !,
268 (Size == 1 % no enumeration required for this variable
269 -> b_tighter_enumerate_sorted_values(Rest,WF)
270 ; treat_next_typed_valc_normal4(TC,Size,Rest,WF)
271 ).
272 treat_next_integer(_,[NextPrio|Prios],Val,VarID,EnumWarning,Card,Rest,WF) :- !, % for test 1161 this clause causes a considerable slowdown
273 get_wait_flag(NextPrio,treat_next_integer(VarID,Val),WF,LWF),
274 treat_next_integer(LWF,Prios,Val,VarID,EnumWarning,Card,Rest,WF).
275 treat_next_integer(_,_,Val,VarID,EnumWarning,Card,Rest,WF) :-
276 treat_next_typed_valc_normal(integer,Val,VarID,EnumWarning,Card,Rest,WF). % we have already delayed; no need to delay further
277
278 treat_next_typed_valc_normal4(typedvalc(Val,Type,VarID,EnumWarning,Card),Size,Rest,WF) :-
279 (number(Size) -> NewCard=Size ; NewCard=Card), % use narrowed down card if possible
280 treat_next_typed_valc_normal(Type,Val,VarID,EnumWarning,NewCard,Rest,WF).
281 treat_next_typed_valc_normal(Type,Val,VarID,EnumWarning,Card,Rest,WF) :-
282 get_wait_flag(Card,tighter_enum(VarID,Val,Type),WF,LWF),
283 b_tighter_enumerate_sorted_value_and_continue(LWF,Val,Type,VarID,EnumWarning,Card,Rest,WF).
284
285 :- block b_tighter_enumerate_sorted_value_and_continue(-,?,?,?,?,?,?,?).
286 b_tighter_enumerate_sorted_value_and_continue(_LWF,Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
287 (Rest = [] -> true ; get_minimum_waitflag_prio(WF,Prio,_), Prio < 20000),
288 % only check for useless if there are either other variables to chose from or other WF goals
289 currently_useless_variable(Val),
290 !,
291 ? b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF).
292 b_tighter_enumerate_sorted_value_and_continue(_LWF,Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
293 check_reached(Val,Type,VarID,Card,WF), %% <-----
294 %% tools:print_bt_message(enumerate(VarID,Val)), %%
295 ? enum_tight_with_wf(Val,Type,EnumWarning,WF),
296 %% tools:print_bt_message(after_enumerate(VarID,Val)),
297 %(VarID=='VS_NOERRORCOND' -> print(done_enum(VarID,Val)),nl ; true),
298 b_tighter_enumerate_sorted_values(Rest,WF).
299
300 b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
301 get_next_useful_variable(Rest,RVal,RType,RVarID,REnumWarning,RCard,RRest), % ,print(using(RVarID,RVal,RType)),nl
302 !,
303 %debug_println(9,skipping(Val,VarID,Card,new(RVal,RType,RVarID,RCard))),
304 (RCard =< Card /* we can enumerate straight away */
305 -> check_reached(RVal,RType,RVarID,RCard,WF), %% <------
306 ? enum_tight_with_wf(RVal,RType,EnumWarning,WF),
307 b_tighter_enumerate_sorted_values([typedvalc(Val,Type,VarID,EnumWarning,Card)|RRest],WF)
308 ; b_tighter_enumerate_sorted_values([typedvalc(RVal,RType,RVarID,REnumWarning,RCard),
309 typedvalc(Val,Type,VarID,EnumWarning,Card)|RRest],WF)
310 ).
311 b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
312 %debug_println(19,all_variables_useless(Val,Card)),
313 get_minimum_waitflag_prio(WF,Prio,_Info),
314 Prio < 20000, % avoid infinite enumeration ... TO DO: improve check
315 %debug_println(19,all_variables_useless_info(Prio,Info)),
316 !,
317 ? ground_wait_flag_to(WF,Prio),
318 % Now try again:
319 ? b_tighter_enumerate_sorted_value_and_continue(1,Val,Type,VarID,EnumWarning,Card,Rest,WF).
320 b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
321 check_reached(Val,Type,VarID,Card,WF), %% <-----
322 %% tools:print_bt_message(enumerate(VarID,Val)), %%
323 ? enum_tight_with_wf(Val,Type,EnumWarning,WF),
324 %% tools:print_bt_message(after_enumerate(VarID,Val)),
325 %(VarID=='VS_NOERRORCOND' -> print(done_enum(VarID,Val)),nl ; true),
326 b_tighter_enumerate_sorted_values(Rest,WF).
327
328 % --------------------
329
330
331 :- use_module(kernel_objects,[enumerate_tight_type_wf/4]).
332 enum_tight_with_wf(Val,Type,EnumWarningInfos,WF) :-
333 get_enum_warning_info(EnumWarningInfos,EnumWarning),
334 ? enumerate_tight_type_wf(Val,Type,EnumWarning,WF).
335
336
337 % ---------------------
338
339 get_next_useful_variable([typedvalc(Val,Type,VarID,EnumWarning,Card)|Rest],RVal,RType,RVarID,REnumWarning,RCard,RRest) :-
340 (currently_useless_variable(Val)
341 -> RRest=[typedvalc(Val,Type,VarID,EnumWarning,Card)|TRRest],
342 get_next_useful_variable(Rest,RVal,RType,RVarID,REnumWarning,RCard,TRRest)
343 ; RRest=Rest, RVal=Val, RType=Type, RVarID=VarID, REnumWarning = EnumWarning, RCard=Card
344 ).
345
346
347 /* purpose: check if an enumeration is useful or not and give priority to useful variables ? */
348 % relevant for tests 1368 and 1492
349 %:- use_module(library(clpfd),[fd_dom/2]).
350 currently_useless_variable(Val) :- var(Val),!,frozen(Val,Goal), % this can be expensive when Goal is large !
351 (enumeration_only_goal(Goal,Val) -> true).
352 currently_useless_variable(int(Val)) :- currently_useless_variable(Val).
353 currently_useless_variable(fd(Val,_)) :- currently_useless_variable(Val).
354 currently_useless_variable(string(Val)) :- currently_useless_variable(Val).
355
356 :- use_module(clpfd_interface,[clpfd_degree/2]).
357 enumeration_only_goal(true,_).
358 enumeration_only_goal((A,B),Val) :-
359 ? (enumeration_only_goal(A,Val) -> enumeration_only_goal(B,Val)
360 ; % we have not detected A as enumeration only: check if we can find an annotation not to enumerate
361 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 ?
362 ).
363 enumeration_only_goal(dif(A,B),Var) :- (Var==A ; Var==B). % SWI
364 ?enumeration_only_goal(Module:Call,Val) :- enumeration_only_goal_m(Module,Call,Val).
365
366 %enumeration_only_goal_m(fd_utils_clpfd:delayed_enum_fd(V,_,_,_),Val) :- V==Val.
367 enumeration_only_goal_m(kernel_objects,call_enumerate_int(V,_,_,_),Val) :- !, V==Val.
368 enumeration_only_goal_m(kernel_objects,enumerate_int_wf(V,_,_),Val) :- !, V==Val.
369 enumeration_only_goal_m(kernel_objects,enumerate_natural(V,_,_,_),Val) :- !, V==Val.
370 enumeration_only_goal_m(prolog,dif(A,B),Var) :- !, (Var==A ; Var==B).
371 enumeration_only_goal_m(clpfd,(X in _),Var) :- !, Var==X,
372 clpfd_degree(X,0). % only goal is the enumerator itself;
373 % but CLPFD constraints are ***NOT*** shown in frozen(...) so we need to call clpfd_degree
374 enumeration_only_goal_m(bsets_clp,is_sequence_wf_ex(V,GS,_,_),Val) :- V==Val,
375 nonvar(GS),GS=global_set(_). % only constraint: we should generate a sequence
376 enumeration_only_goal_m(external_functions,string_to_int2(_,V,_,_),Val) :- !, V==Val.
377 enumeration_only_goal_m(external_functions,printf(_,V,_,_),Val) :-!, V==Val.
378 enumeration_only_goal_m(external_functions,block_print_value(_,_,_V,_,_),_Val) :- !. % from observe
379 enumeration_only_goal_m(external_functions,block_print_value_complete(_,_,_,_,_),_Val). % from observe
380 enumeration_only_goal_m(b_interpreter_components,observe_variable_block(_,_,_,_,_),_) :- !. % in -p TRACE_INFO TRUE mode
381 enumeration_only_goal_m(b_interpreter_components,observe_variable1_block(_,_,_,_),_).
382 enumeration_only_goal_m(prolog,trig_ground(A1,_,_,_,Trigger),Val) :- Val==A1,
383 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
384
385 force_enumeration_only_goal((A,B),Val) :-
386 (force_enumeration_only_goal(A,Val) -> true ; force_enumeration_only_goal(B,Val) ).
387 force_enumeration_only_goal(external_functions:'DO_NOT_ENUMERATE'(V,_,_),Val) :- V==Val.
388
389 % check if Trigger either triggers a better enumerator or just debugging code
390 triggers_better_enumeration(Trigger,Val,Depth) :- Depth>0, D1 is Depth-1,
391 frozen(Trigger,TrigGoal),
392 ( better_enum(TrigGoal,Trigger,Val,D1) -> true).
393
394 better_enum((A,B),Trigger,Val,Depth) :- better_enum(A,Trigger,Val,Depth), better_enum(B,Trigger,Val,Depth).
395 better_enum(prolog:trig_and(_,_,_,_,Trigger1),Trigger,Val,Depth) :- !,
396 (Trigger1==Trigger -> true ; triggers_better_enumeration(Trigger1,Val,Depth)).
397 better_enum(prolog:trig_or(_,Trigger1,_),Trigger,Val,Depth) :- !,
398 (Trigger1==Trigger -> true ; triggers_better_enumeration(Trigger1,Val,Depth)).
399 better_enum(prolog:trig_ground(VV,_,_,Trigger1,_),Trigger,Val,Depth) :- !,
400 (Trigger1==Trigger -> true ; VV=Val -> true ; triggers_better_enumeration(Trigger1,Val,Depth)).
401 better_enum(prolog:when(WT,_,G), Trigger,Val,Depth) :- !,
402 Trigger==WT, better_enum(G,Trigger,Val,Depth).
403 better_enum(custom_explicit_sets:couple_element_of_avl_set(_X,_Y,_AVL,_WF1,_WF),_,_Val,_Depth) :- !,
404 % TO DO: add more enumerators of Val
405 % TO DO: VAL occurs in _X !!
406 true.
407 better_enum(external_functions:G,_,_Val,_Depth) :- external_debug_function(G).
408
409 external_debug_function(fprintf2(_,_,_,_)). % TO DO: add more
410
411
412
413 b_tighter_enumerate_single_value(Val,Type,Infos,VarID,WF) :-
414 construct_typedval_infos(VarID,Infos,trigger_true(VarID),TINFO),
415 b_tighter_enumerate_all_values([typedval(Val,Type,VarID,TINFO)],WF).
416
417 b_tighter_enumerate_all_values(TypedValues,WF) :-
418 b_tighter_enumerate_values(TypedValues,enum_info([],[]),WF).
419
420 % a variation of b_tighter_enumerate_values/2 which obtains a context predicate
421 % which may contain DO_NOT_ENUMERATE annotations
422 % and which is analysed if some ids are better enumerated inside the predicate itself
423 % (the latter was previously done by project_away_useless_enumeration_values)
424 b_tighter_enumerate_values_in_ctxt(TypedValues,ContextPred,WF) :-
425 extract_do_not_enum_ids_from_predicate(ContextPred,UselessIds),
426 b_tighter_enumerate_values(TypedValues,UselessIds,WF).
427
428 % enumerate given a list of useless ids (marked e.g. by DO_NOT_ENUMERATE)
429 b_tighter_enumerate_values(TypedValues,enum_info(UselessIds,DelayedIds),WF) :- !,
430 %print(sort_typed(UselessIds,DelayedIds)),nl,
431 sort_typed_values(TypedValues,[],UselessIds,DelayedIds,SortedValues),
432 b_tighter_enumerate_sorted_values(SortedValues,WF).
433 b_tighter_enumerate_values(TV,EI,WF) :-
434 add_internal_error('Illegal call: ',b_tighter_enumerate_values(TV,EI,WF)),
435 fail.
436
437 % -------------------------------
438
439 % extract identifiers which are either marked as DO_NOT_ENUMERATED or
440 % whose enumeration is pointless given the predicate body
441 extract_do_not_enum_ids_from_predicate(b(Pred,_,Infos),enum_info(SortedUselessIds,DelayedIds)) :- !,
442 findall(ID,member(prob_annotation('DO_NOT_ENUMERATE'(ID)),Infos),UselessIds1),
443 findall(ID,find_useless_enumeration_id(Pred,ID),UselessIds,UselessIds1),
444 findall(delay_enum(PosNr,ID),member(prob_annotation('DELAY_ENUMERATION'(PosNr,ID)),Infos),DelayedIds),
445 sort(UselessIds,SortedUselessIds).
446 extract_do_not_enum_ids_from_predicate(P,Res) :-
447 add_internal_error('Illegal call: ',extract_do_not_enum_ids_from_predicate(P,Res)),
448 Res=enum_info([],[]).
449
450 :- use_module(bsyntaxtree, [get_texpr_expr/2]).
451 :- use_module(preferences, [get_preference/2]).
452 % TO DO: try and generalize this treatment (applicable for SLOT-PERFORMANCE2 at the moment)
453 % i.e. also treat (x,y):AVL & OTHERPRED not just in CLPFD off or data validation mode
454 % see e.g. test 1162 with predicate:
455 % eq1 |-> et |-> es : #5775:{(0|->0|->97),,...,(524|->10|->-1)} & es /= -1 & er |-> es : #1497:{(0|->97),...,(1496|->1959)} & RANGE_LAMBDA__ = eq1 |-> er
456 find_useless_enumeration_id(member(LHS,b(value(V),_,_)),UselessID) :-
457 % we enumerate the identifier using memberships of avl_sets which will be more precise than naive enumeration
458 nonvar(V), V=avl_set(_),
459 ? extract_useless(LHS,UselessID).
460 find_useless_enumeration_id(conjunct(TA,TB),UselessID) :-
461 (get_preference(use_clpfd_solver,false) -> true
462 ; get_preference(data_validation_mode,true)),
463 % only look deeper if CLPFD is off; useful for test 1945, 1162
464 % in general it could be better to enumerate a variable if it occurs in multiple sets and we using CLPFD intersection we can narrow down the interval
465 % e.g., x: 1..100 & x:99..1000 --> we can narrow down x to 99..100 and it would be better to enumerate x
466 (get_texpr_expr(TA,P) ; get_texpr_expr(TB,P)),
467 ? find_useless_enumeration_id(P,UselessID).
468
469 extract_useless(b(couple(A,B),_,_),UselessID) :-
470 ? (extract_useless(A,UselessID) ; extract_useless(B,UselessID)).
471 extract_useless(b(identifier(UselessID),_,_),UselessID) :-
472 % the identifier is bound by the member test; we do not need to enumerate it
473 debug_println(9,not_enum_inside_closure(UselessID)).
474
475 % -------------------------------
476
477
478 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
479 :- if(environ(prob_debug_watch_flag,true)).
480 :- dynamic reached/4, enumerated/2,enum_edge/3.
481 check_reached(_Val,_Type,_VarID,_Card,_WF) :- check_reached(_Val,_Type,_VarID,_Card,enum,_WF).
482 check_reached(_Val,_Type,VarID,_Card,Info,_WF) :-
483 (retract(reached(VarID,RR,Info)) -> true ; RR=0),
484 R1 is RR+1,
485 assertz(reached(VarID,R1,Info)),
486 (enumerated(TopVar,Level) -> add_edge(TopVar,VarID,Level),L1 is Level+1 ; L1=0),
487 asserta(enumerated(VarID,L1)).
488 check_reached(_Val,_Type,VarID,_Card,_Info,_WF) :-
489 retract(enumerated(VarID,_)),fail.
490 add_edge(TopVar,VarID,Level) :-
491 (enum_edge(TopVar,VarID,Level) -> true ; assertz(enum_edge(TopVar,VarID,Level))).
492
493 % b_enumerate:print_enum_stats.
494 print_enum_stats :- findall( enum(Count,VarID,Info), reached(VarID,Count,Info),L),
495 sort(L,SL),
496 print('Enumeration Frequency'),nl,
497 member(enum(C,ID,I),SL), format(' ~w ~w ~w~n',[C, ID, I]),
498 fail.
499 print_enum_stats :-
500 enum_edge(TopVar,VarID,0), format('~w ---> ~w~n',[TopVar,VarID]),
501 print_edges(VarID,1),
502 fail.
503 print_enum_stats :- nl.
504 print_edges(VarID,Level) :- enum_edge(VarID,NxtId,Level),
505 format(' ~w -(~w)--> ~w~n',[VarID,Level,NxtId]),
506 fail.
507 print_edges(_,_).
508 :- else.
509 check_reached(Val,Type,Var,Card,_WF) :- is_lambda_result_id(Var),
510 Card \= det, \+ ground_value(Val), !,
511 format('~n*** Enumerating lambda result ~w : ~w (Type=~w, Card=~w)~n~n',[Var,Val,Type,Card]).
512 check_reached(_Val,_Type,_VarID,_Card,_WF). % :- format('Enumerating ~w (~w) : ~w~n',[_VarID,_Card,_Val]).
513 check_reached(_Val,_Type,_VarID,_Card,_Info,_WF). % :- format('Enumerating ~w (~w:~w) : ~w~n',[_VarID,_Card,_Info,_Val]).
514 :- endif.
515
516 /* comment in for debugging :
517 % dummy call to register variable name with free Prolog variables:
518 % can be obtained using frozen()
519 :- public register_prolog_variable_name/3. % Debugging tool
520 :- block register_prolog_variable_name(-,?,?).
521 register_prolog_variable_name(int(Val),Name,Type) :- !,
522 register_prolog_variable_name(Val,Name,Type).
523 register_prolog_variable_name(fd(Val,_),Name,Type) :- !,
524 register_prolog_variable_name(Val,Name,Type).
525 register_prolog_variable_name(string(Val),Name,Type) :- !,
526 register_prolog_variable_name(Val,Name,Type).
527 register_prolog_variable_name((A,B),Name,Type) :- !,
528 register_prolog_variable_name(A,left(Name,mapto(B)),Type),
529 register_prolog_variable_name(B,right(Name,mapfrom(A)),Type).
530 register_prolog_variable_name([A|T],Name,Type) :- !,
531 register_prolog_variable_name(A,el(Name),Type),
532 register_prolog_variable_name(T,Name,Type).
533 register_prolog_variable_name(_,_,_).
534 % TO DO: something that pretty prints the path information for the average user
535
536 % a tool to get variable name if it was registered
537 :- public get_prolog_variable_name/3. % Debugging tool
538 get_prolog_variable_name(X,Name,Type) :- var(X),
539 frozen(X,Goal), print(goal(X,Goal)),nl,
540 goal_member(Goal,b_enumerate:register_prolog_variable_name(_,ID,T)),
541 Name=ID, Type=T.
542 goal_member(X,X).
543 goal_member((A,B),X) :- goal_member(A,X) ; goal_member(B,X).
544 ------- */
545
546 sort_typed_values([],R,_,_,R).
547 sort_typed_values([typedval(Val,Type,VarID,EnumWarningInfo)|Rest],SortedSoFar,UselessIds,DelayedIds,Res) :-
548 %% comment in next line to keep track of variable names for enumeration warnings, etc...
549 %% register_prolog_variable_name(Val,VarID,Type), % dummy call to register variable name with free Prolog variables
550 (is_lambda_result_or_useless(VarID,EnumWarningInfo,UselessIds) -> % DO_NOT_ENUMERATE
551 (%Rest=[],SortedSoFar=[], % we used to check it is the only non-ground value to enumerate
552 \+ ground_value(Val)
553 % could be relevant if a variable was annotated as do_not_enumerate and there is a WD error in
554 % the expression defining it, e.g. in test 2337: {id19,id20|id19 : BOOL & id20 <: INTEGER}(id1) = x
555 -> % Note: we can have a construct {lambda_result| #x.( P(x) & lambda_result=E(x))},
556 % we want to enumerate it after trying to solve the existential quantifier
557 last_priority(Prio), % important that it is higher than existential quantifier prio, cf test 1492
558 add_enum_warning_info(EnumWarningInfo,NewInfo),
559 insert_val(SortedSoFar,Val,Type,VarID,NewInfo,Prio,NewSorted),
560 (debug:debug_level_active_for(9),
561 Rest\=[], SortedSoFar \= [] % then it is the only variable anyway
562 -> format('~n*** Possibly enumerating lambda result ~w : ~w (~w:~w)~n~n',[VarID,Val,Type,Prio])
563 ; true)
564 % was triggered in test 1093 and 1161, but seems no longer necessary there
565 ; NewSorted=SortedSoFar % completely skip enumeration
566 )
567 ; ground_value(Val) -> NewSorted=SortedSoFar
568 ; get_max_cardinality_as_priority(Type,CardPrio),
569 ? (member(delay_enum(PosNr,VarID),DelayedIds),
570 integer_pow2_priority(Prio), P2 is Prio+PosNr,
571 P2>CardPrio
572 -> debug_println(9,'DELAY_ENUMERATION'(VarID,PosNr,P2,CardPrio)),
573 get_bounded_priority(P2,EnumPrio)
574 ; EnumPrio=CardPrio),
575 %% TO DO: maybe also take shape of Val into account; e.g. if cardinality of a set already fixed...
576 insert_val(SortedSoFar,Val,Type,VarID,EnumWarningInfo,EnumPrio,NewSorted)
577 ),
578 sort_typed_values(Rest,NewSorted,UselessIds,DelayedIds,Res).
579
580 get_max_cardinality_as_priority(integer,Prio) :- !, integer_priority(Prio).
581 get_max_cardinality_as_priority(Type,Prio) :-
582 ? max_cardinality(Type,Card), !,
583 (Card \= inf
584 -> %Prio=Card
585 get_bounded_priority(Card,Prio)
586 ; inf_type_prio(Type,Prio)
587 ).
588 get_max_cardinality_as_priority(Type,Prio) :-
589 add_internal_error('Failed: ',max_cardinality(Type,_)),
590 integer_priority(Prio).
591
592 % Try to give priority to simpler infinite types (such as integer over seq(_) ,...)
593 % TO DO: to a full-blown analysis ...
594 inf_type_prio(integer,Prio) :- !, integer_priority(Prio).
595 inf_type_prio(real,Prio) :- !, integer_priority(P1), Prio is P1+11.
596 inf_type_prio(seq(X),Prio) :- !, inf_type_prio(X,P1), Prio is P1+11.
597 inf_type_prio(set(X),Prio) :- !, inf_type_prio(X,P1), Prio is P1+10.
598 %inf_type_prio(couple(_,_),Prio) :- !, TO DO check if both args are infinite or not ...
599 inf_type_prio(_,Prio) :- !, integer_priority(P), Prio is P+1.
600
601 :- public portray_typed_values/1.
602 portray_typed_values(List) :- maplist(print_typedvalc,List),nl.
603 print_typedvalc(typedvalc(_Val,_Type,VarID,_EnumWarning,Card)) :-
604 format('~w (card:~w) ',[VarID,Card]).
605
606 %typedvalc = typedval + cardinality information
607 insert_val([],Val,Type,VarID,EnumWarning,Card,[typedvalc(Val,Type,VarID,EnumWarning,Card)]).
608 insert_val([TC|T], Val,Type, VarID, EnumWarning, Card, Res) :-
609 TC = typedvalc(V1,_T1,_Var1,_W1,C1),
610 ? (cardval_greater_than(C1,V1,Card,Val)
611 -> Res = [typedvalc(Val,Type,VarID,EnumWarning,Card),TC|T]
612 ; Res = [TC|RT],
613 insert_val(T,Val,Type,VarID,EnumWarning,Card,RT)
614 ).
615
616
617 :- use_module(library(random)).
618 cardval_greater_than(C1,_,Card,_) :- Card \== inf, (C1=inf -> true ; C1>Card).
619 cardval_greater_than(Card,V1,Card,Val) :-
620 var(V1), nonvar(Val). % if card equal give priority to nonvariable values
621 cardval_greater_than(Card,_,Card,_) :-
622 preferences:preference(randomise_enumeration_order,true),
623 % TO DO: maybe we even want to change the order if cardinality different ?
624 % this also does not really generate random permutation of variables with same cardinality
625 random(1,3,1).
626
627 /*
628 % call to enumerate an integer ensuring that you go at least from MinFrom to MinTo
629 %:- block enumerate_integer_with_min_range_wf(-,?,?,?).
630 enumerate_integer_with_min_range_wf(int(X),MinFrom,MinTo,WF) :-
631 integer_priority(Prio), P1 is Prio-1,
632 ... removed ...
633 */