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 :- 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(kernel_card_arithmetic,[safe_mul/3]).
207 :- use_module(b_global_sets,[b_global_set_cardinality/2]).
208 finite_value(integer,Val,Size) :- nonvar(Val), Val=int(FD), clpfd_size(FD,Size), number(Size).
209 finite_value(boolean,Val,Size) :- (ground(Val) -> Size = 1 ; Size =2).
210 finite_value(string(_),Val,Size) :- ground(Val), Size=1.
211 finite_value(real(_),Val,Size) :- ground(Val), Size=1.
212 finite_value(global(G),Val,Size) :- (ground(Val) -> Size = 1 ; b_global_set_cardinality(G,Size)).
213 finite_value(set(T),Val,Size) :- nonvar(Val), l_finite_value(T,Val,Size).
214 finite_value(couple(T1,T2),Val,Size) :- nonvar(Val), Val = (V1,V2),
215 finite_value(T1,V1,Size1),
216 finite_value(T2,V2,Size2),
217 safe_mul(Size1,Size2,Size), number(Size). % can also be inf_overflow !
218 finite_value(record(Fields),Val,Size) :-
219 nonvar(Val), Val=rec(FVals),
220 finite_fields(Fields,FVals,Size), nl,print(finite_field(Val,Size)),nl,nl.
221 % TO DO: missing freetypes
222
223 l_finite_value(_Type,Val,_) :- var(Val),!,fail.
224 l_finite_value(_,avl_set(_),1).
225 l_finite_value(_Type,[],1).
226 l_finite_value(Type,[H|T],Size) :- l_finite_value(Type,T,SizeT), finite_value(Type,H,SizeH),
227 safe_mul(SizeT,SizeH,Size), number(Size).
228
229 finite_fields(_Type,Val,_) :- var(Val),!,fail.
230 finite_fields([],[],1).
231 finite_fields([HType|TTypes],[H|T],Size) :- finite_fields(TTypes,T,SizeT), finite_value(HType,H,SizeH),
232 safe_mul(SizeT,SizeH,Size), number(Size).
233
234 % find the typedvalc (Selected) with the smallest value (Prio) and return other (Rest) typedvalc-values
235 smallest_value([H|T],Selected,Rest,Prio) :-
236 get_typedvalc_priority(H,HPrio),
237 smallest_value_aux(T,H,HPrio,Selected,Rest,Prio).
238
239 smallest_value_aux([],H,HPrio,H,[],HPrio).
240 smallest_value_aux([H|T],Acc,AccPrio,Selected,Rest,SelPrio) :-
241 get_typedvalc_priority(H,HPrio),
242 (HPrio=1 -> smallest_value_aux(T,Acc,AccPrio,Selected,Rest,SelPrio) % remove this TC from list; does not need to be enumerated anymore
243 ; HPrio @< AccPrio
244 -> Rest = [Acc|TRest],
245 smallest_value_aux(T,H,HPrio,Selected,TRest,SelPrio)
246 ; Rest = [H|TRest],
247 smallest_value_aux(T,Acc,AccPrio,Selected,TRest,SelPrio)
248 ).
249
250 % we try again and see if the domain is now finite
251 % 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
252 :- block treat_next_integer(-,?,?,?,?,?,?,?).
253 treat_next_integer(LWF,_,Val,VarID,EnumWarning,_Card,Rest,WF) :- LWF \== first_iteration, % print(treat(Val,VarID,Rest)),nl,
254 nonvar(Val), Val=int(FD),
255 clpfd_size(FD,Size), % will return sup if no bounds + also works in non-CLPFD mode
256 %print(treat_next_integer(VarID,Val,Size,_Card,Rest)),nl,
257 number(Size),!,
258 (Size = 1 % for Size=1 no enumeration is necessary anyway
259 -> b_tighter_enumerate_sorted_values(Rest,WF) % no enumeration required
260 ; treat_next_typed_valc_normal(integer,Val,VarID,EnumWarning,Size,Rest,WF)).
261 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
262 CurTC = typedvalc(Val,integer,VarID,EnumWarning,Card),
263 smallest_value([CurTC|OtherTCs],TC,Rest,Size),
264 (number(Size) % finite domain found
265 ;
266 Prios = [] % no more delaying; we have to enumerate an unbounded value
267 ),
268 !,
269 (Size == 1 % no enumeration required for this variable
270 -> b_tighter_enumerate_sorted_values(Rest,WF)
271 ; treat_next_typed_valc_normal4(TC,Size,Rest,WF)
272 ).
273 treat_next_integer(_,[NextPrio|Prios],Val,VarID,EnumWarning,Card,Rest,WF) :- !, % for test 1161 this clause causes a considerable slowdown
274 get_wait_flag(NextPrio,treat_next_integer(VarID,Val),WF,LWF),
275 treat_next_integer(LWF,Prios,Val,VarID,EnumWarning,Card,Rest,WF).
276 treat_next_integer(_,_,Val,VarID,EnumWarning,Card,Rest,WF) :-
277 treat_next_typed_valc_normal(integer,Val,VarID,EnumWarning,Card,Rest,WF). % we have already delayed; no need to delay further
278
279 treat_next_typed_valc_normal4(typedvalc(Val,Type,VarID,EnumWarning,Card),Size,Rest,WF) :-
280 (number(Size) -> NewCard=Size ; NewCard=Card), % use narrowed down card if possible
281 treat_next_typed_valc_normal(Type,Val,VarID,EnumWarning,NewCard,Rest,WF).
282 treat_next_typed_valc_normal(Type,Val,VarID,EnumWarning,Card,Rest,WF) :-
283 get_wait_flag(Card,tighter_enum(VarID,Val,Type),WF,LWF),
284 b_tighter_enumerate_sorted_value_and_continue(LWF,Val,Type,VarID,EnumWarning,Card,Rest,WF).
285
286 :- block b_tighter_enumerate_sorted_value_and_continue(-,?,?,?,?,?,?,?).
287 b_tighter_enumerate_sorted_value_and_continue(_LWF,Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
288 (Rest = [] -> true ; get_minimum_waitflag_prio(WF,Prio,_), Prio < 20000),
289 % only check for useless if there are either other variables to chose from or other WF goals
290 currently_useless_variable(Val),
291 !,
292 ? b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF).
293 b_tighter_enumerate_sorted_value_and_continue(_LWF,Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
294 check_reached(Val,Type,VarID,Card,WF), %% <-----
295 %% tools:print_bt_message(enumerate(VarID,Val)), %%
296 ? enum_tight_with_wf(Val,Type,EnumWarning,WF),
297 %% tools:print_bt_message(after_enumerate(VarID,Val)),
298 %(VarID=='VS_NOERRORCOND' -> print(done_enum(VarID,Val)),nl ; true),
299 b_tighter_enumerate_sorted_values(Rest,WF).
300
301 b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
302 get_next_useful_variable(Rest,RVal,RType,RVarID,REnumWarning,RCard,RRest),
303 !,
304 %debug_println(9,skipping(Val,VarID,Card,new(RVal,RType,RVarID,RCard))),
305 (RCard =< Card /* we can enumerate straight away */
306 -> check_reached(RVal,RType,RVarID,RCard,WF), %% <------
307 enum_tight_with_wf(RVal,RType,EnumWarning,WF),
308 b_tighter_enumerate_sorted_values([typedvalc(Val,Type,VarID,EnumWarning,Card)|RRest],WF)
309 ; b_tighter_enumerate_sorted_values([typedvalc(RVal,RType,RVarID,REnumWarning,RCard),
310 typedvalc(Val,Type,VarID,EnumWarning,Card)|RRest],WF)
311 ).
312 b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
313 %debug_println(19,all_variables_useless(Val,Card)),
314 get_minimum_waitflag_prio(WF,Prio,_Info),
315 Prio < 20000, % avoid infinite enumeration ... TO DO: improve check
316 %debug_println(19,all_variables_useless_info(Prio,Info)),
317 !,
318 ? ground_wait_flag_to(WF,Prio),
319 % Now try again:
320 b_tighter_enumerate_sorted_value_and_continue(1,Val,Type,VarID,EnumWarning,Card,Rest,WF).
321 b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
322 check_reached(Val,Type,VarID,Card,WF), %% <-----
323 %% tools:print_bt_message(enumerate(VarID,Val)), %%
324 ? enum_tight_with_wf(Val,Type,EnumWarning,WF),
325 %% tools:print_bt_message(after_enumerate(VarID,Val)),
326 %(VarID=='VS_NOERRORCOND' -> print(done_enum(VarID,Val)),nl ; true),
327 b_tighter_enumerate_sorted_values(Rest,WF).
328
329 % --------------------
330
331
332 :- use_module(kernel_objects,[enumerate_tight_type_wf/4]).
333 enum_tight_with_wf(Val,Type,EnumWarningInfos,WF) :-
334 get_enum_warning_info(EnumWarningInfos,EnumWarning),
335 ? enumerate_tight_type_wf(Val,Type,EnumWarning,WF).
336
337
338 % ---------------------
339
340 get_next_useful_variable([typedvalc(Val,Type,VarID,EnumWarning,Card)|Rest],RVal,RType,RVarID,REnumWarning,RCard,RRest) :-
341 (currently_useless_variable(Val)
342 -> RRest=[typedvalc(Val,Type,VarID,EnumWarning,Card)|TRRest],
343 get_next_useful_variable(Rest,RVal,RType,RVarID,REnumWarning,RCard,TRRest)
344 ; RRest=Rest, RVal=Val, RType=Type, RVarID=VarID, REnumWarning = EnumWarning, RCard=Card
345 ).
346
347
348 /* purpose: check if an enumeration is useful or not and give priority to useful variables ? */
349 % relevant for tests 1368 and 1492
350 %:- use_module(library(clpfd),[fd_dom/2]).
351 currently_useless_variable(Val) :- var(Val),!,frozen(Val,Goal), % this can be expensive when Goal is large !
352 (enumeration_only_goal(Goal,Val) -> true).
353 currently_useless_variable(int(Val)) :- currently_useless_variable(Val).
354 currently_useless_variable(fd(Val,_)) :- currently_useless_variable(Val).
355 currently_useless_variable(string(Val)) :- currently_useless_variable(Val).
356
357 :- use_module(clpfd_interface,[clpfd_degree/2]).
358 enumeration_only_goal(true,_).
359 enumeration_only_goal((A,B),Val) :-
360 (enumeration_only_goal(A,Val) -> enumeration_only_goal(B,Val)
361 ; % we have not detected A as enumeration only: check if we can find an annotation not to enumerate
362 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 ?
363 ).
364 enumeration_only_goal(dif(A,B),Var) :- (Var==A ; Var==B). % SWI
365 enumeration_only_goal(Module:Call,Val) :- enumeration_only_goal_m(Module,Call,Val).
366
367 %enumeration_only_goal_m(fd_utils_clpfd:delayed_enum_fd(V,_,_,_),Val) :- V==Val.
368 enumeration_only_goal_m(kernel_objects,call_enumerate_int(V,_,_,_),Val) :- !, V==Val.
369 enumeration_only_goal_m(kernel_objects,enumerate_int_wf(V,_,_),Val) :- !, V==Val.
370 enumeration_only_goal_m(kernel_objects,enumerate_natural(V,_,_,_),Val) :- !, V==Val.
371 enumeration_only_goal_m(prolog,dif(A,B),Var) :- !, (Var==A ; Var==B).
372 enumeration_only_goal_m(clpfd,(X in _),Var) :- !, Var==X,
373 clpfd_degree(X,0). % only goal is the enumerator itself;
374 % but CLPFD constraints are ***NOT*** shown in frozen(...) so we need to call clpfd_degree
375 enumeration_only_goal_m(bsets_clp,is_sequence_wf_ex(V,GS,_,_),Val) :- V==Val,
376 nonvar(GS),GS=global_set(_). % only constraint: we should generate a sequence
377 enumeration_only_goal_m(external_functions,string_to_int2(_,V,_,_),Val) :- !, V==Val.
378 enumeration_only_goal_m(external_functions,printf(_,V,_,_),Val) :-!, V==Val.
379 enumeration_only_goal_m(external_functions,block_print_value(_,_,_V,_,_),_Val) :- !. % from observe
380 enumeration_only_goal_m(external_functions,block_print_value_complete(_,_,_,_,_),_Val). % from observe
381 enumeration_only_goal_m(b_interpreter_components,observe_variable_block(_,_,_,_,_),_) :- !. % in -p TRACE_INFO TRUE mode
382 enumeration_only_goal_m(b_interpreter_components,observe_variable1_block(_,_,_,_),_).
383 enumeration_only_goal_m(prolog,trig_ground(A1,_,_,_,Trigger),Val) :- Val==A1,
384 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
385
386 force_enumeration_only_goal((A,B),Val) :-
387 (force_enumeration_only_goal(A,Val) -> true ; force_enumeration_only_goal(B,Val) ).
388 force_enumeration_only_goal(external_functions:'DO_NOT_ENUMERATE'(V,_,_),Val) :- V==Val.
389
390 % check if Trigger either triggers a better enumerator or just debugging code
391 triggers_better_enumeration(Trigger,Val,Depth) :- Depth>0, D1 is Depth-1,
392 frozen(Trigger,TrigGoal),
393 ( better_enum(TrigGoal,Trigger,Val,D1) -> true).
394
395 better_enum((A,B),Trigger,Val,Depth) :- better_enum(A,Trigger,Val,Depth), better_enum(B,Trigger,Val,Depth).
396 better_enum(prolog:trig_and(_,_,_,_,Trigger1),Trigger,Val,Depth) :- !,
397 (Trigger1==Trigger -> true ; triggers_better_enumeration(Trigger1,Val,Depth)).
398 better_enum(prolog:trig_or(_,Trigger1,_),Trigger,Val,Depth) :- !,
399 (Trigger1==Trigger -> true ; triggers_better_enumeration(Trigger1,Val,Depth)).
400 better_enum(prolog:trig_ground(VV,_,_,Trigger1,_),Trigger,Val,Depth) :- !,
401 (Trigger1==Trigger -> true ; VV=Val -> true ; triggers_better_enumeration(Trigger1,Val,Depth)).
402 better_enum(prolog:when(WT,_,G), Trigger,Val,Depth) :- !,
403 Trigger==WT, better_enum(G,Trigger,Val,Depth).
404 better_enum(custom_explicit_sets:couple_element_of_avl_set(_X,_Y,_AVL,_WF1,_WF),_,_Val,_Depth) :- !,
405 % TO DO: add more enumerators of Val
406 % TO DO: VAL occurs in _X !!
407 true.
408 better_enum(external_functions:G,_,_Val,_Depth) :- external_debug_function(G).
409
410 external_debug_function(fprintf2(_,_,_,_)). % TO DO: add more
411
412
413
414 b_tighter_enumerate_single_value(Val,Type,Infos,VarID,WF) :-
415 construct_typedval_infos(VarID,Infos,trigger_true(VarID),TINFO),
416 b_tighter_enumerate_all_values([typedval(Val,Type,VarID,TINFO)],WF).
417
418 b_tighter_enumerate_all_values(TypedValues,WF) :-
419 b_tighter_enumerate_values(TypedValues,enum_info([],[]),WF).
420
421 % a variation of b_tighter_enumerate_values/2 which obtains a context predicate
422 % which may contain DO_NOT_ENUMERATE annotations
423 % and which is analysed if some ids are better enumerated inside the predicate itself
424 % (the latter was previously done by project_away_useless_enumeration_values)
425 b_tighter_enumerate_values_in_ctxt(TypedValues,ContextPred,WF) :-
426 extract_do_not_enum_ids_from_predicate(ContextPred,UselessIds),
427 b_tighter_enumerate_values(TypedValues,UselessIds,WF).
428
429 % enumerate given a list of useless ids (marked e.g. by DO_NOT_ENUMERATE)
430 b_tighter_enumerate_values(TypedValues,enum_info(UselessIds,DelayedIds),WF) :- !,
431 %print(sort_typed(UselessIds,DelayedIds)),nl,
432 sort_typed_values(TypedValues,[],UselessIds,DelayedIds,SortedValues),
433 b_tighter_enumerate_sorted_values(SortedValues,WF).
434 b_tighter_enumerate_values(TV,EI,WF) :-
435 add_internal_error('Illegal call: ',b_tighter_enumerate_values(TV,EI,WF)),
436 fail.
437
438 % -------------------------------
439
440 % extract identifiers which are either marked as DO_NOT_ENUMERATED or
441 % whose enumeration is pointless given the predicate body
442 extract_do_not_enum_ids_from_predicate(b(Pred,_,Infos),enum_info(SortedUselessIds,DelayedIds)) :- !,
443 findall(ID,member(prob_annotation('DO_NOT_ENUMERATE'(ID)),Infos),UselessIds1),
444 findall(ID,find_useless_enumeration_id(Pred,ID),UselessIds,UselessIds1),
445 findall(delay_enum(PosNr,ID),member(prob_annotation('DELAY_ENUMERATION'(PosNr,ID)),Infos),DelayedIds),
446 sort(UselessIds,SortedUselessIds).
447 extract_do_not_enum_ids_from_predicate(P,Res) :-
448 add_internal_error('Illegal call: ',extract_do_not_enum_ids_from_predicate(P,Res)),
449 Res=enum_info([],[]).
450
451 :- use_module(bsyntaxtree, [get_texpr_expr/2]).
452 :- use_module(preferences, [get_preference/2]).
453 % TO DO: try and generalize this treatment (applicable for SLOT-PERFORMANCE2 at the moment)
454 % i.e. also treat (x,y):AVL & OTHERPRED not just in CLPFD off or data validation mode
455 % see e.g. test 1162 with predicate:
456 % eq1 |-> et |-> es : #5775:{(0|->0|->97),,...,(524|->10|->-1)} & es /= -1 & er |-> es : #1497:{(0|->97),...,(1496|->1959)} & RANGE_LAMBDA__ = eq1 |-> er
457 find_useless_enumeration_id(member(LHS,b(value(V),_,_)),UselessID) :-
458 % we enumerate the identifier using memberships of avl_sets which will be more precise than naive enumeration
459 nonvar(V), V=avl_set(_),
460 extract_useless(LHS,UselessID).
461 find_useless_enumeration_id(conjunct(TA,TB),UselessID) :-
462 (get_preference(use_clpfd_solver,false) -> true
463 ; get_preference(data_validation_mode,true)),
464 % only look deeper if CLPFD is off; useful for test 1945, 1162
465 % 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
466 % e.g., x: 1..100 & x:99..1000 --> we can narrow down x to 99..100 and it would be better to enumerate x
467 (get_texpr_expr(TA,P) ; get_texpr_expr(TB,P)),
468 find_useless_enumeration_id(P,UselessID).
469
470 extract_useless(b(couple(A,B),_,_),UselessID) :-
471 (extract_useless(A,UselessID) ; extract_useless(B,UselessID)).
472 extract_useless(b(identifier(UselessID),_,_),UselessID) :-
473 % the identifier is bound by the member test; we do not need to enumerate it
474 debug_println(9,not_enumerating_inside_closure(UselessID)).
475
476 % -------------------------------
477
478
479 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
480 :- if(environ(prob_debug_watch_flag,true)).
481 :- dynamic reached/4, enumerated/2,enum_edge/3.
482 check_reached(_Val,_Type,_VarID,_Card,_WF) :- check_reached(_Val,_Type,_VarID,_Card,enum,_WF).
483 check_reached(_Val,_Type,VarID,_Card,Info,_WF) :-
484 (retract(reached(VarID,RR,Info)) -> true ; RR=0),
485 R1 is RR+1,
486 assertz(reached(VarID,R1,Info)),
487 (enumerated(TopVar,Level) -> add_edge(TopVar,VarID,Level),L1 is Level+1 ; L1=0),
488 asserta(enumerated(VarID,L1)).
489 check_reached(_Val,_Type,VarID,_Card,_Info,_WF) :-
490 retract(enumerated(VarID,_)),fail.
491 add_edge(TopVar,VarID,Level) :-
492 (enum_edge(TopVar,VarID,Level) -> true ; assertz(enum_edge(TopVar,VarID,Level))).
493
494 % b_enumerate:print_enum_stats.
495 print_enum_stats :- findall( enum(Count,VarID,Info), reached(VarID,Count,Info),L),
496 sort(L,SL),
497 print('Enumeration Frequency'),nl,
498 member(enum(C,ID,I),SL), format(' ~w ~w ~w~n',[C, ID, I]),
499 fail.
500 print_enum_stats :-
501 enum_edge(TopVar,VarID,0), format('~w ---> ~w~n',[TopVar,VarID]),
502 print_edges(VarID,1),
503 fail.
504 print_enum_stats :- nl.
505 print_edges(VarID,Level) :- enum_edge(VarID,NxtId,Level),
506 format(' ~w -(~w)--> ~w~n',[VarID,Level,NxtId]),
507 fail.
508 print_edges(_,_).
509 :- else.
510 check_reached(Val,Type,Var,Card,_WF) :- is_lambda_result_id(Var),
511 Card \= det, \+ ground_value(Val), !,
512 format('~n*** Enumerating lambda result ~w : ~w (Type=~w, Card=~w)~n~n',[Var,Val,Type,Card]).
513 check_reached(_Val,_Type,_VarID,_Card,_WF). % :- format('Enumerating ~w (~w) : ~w~n',[_VarID,_Card,_Val]).
514 check_reached(_Val,_Type,_VarID,_Card,_Info,_WF). % :- format('Enumerating ~w (~w:~w) : ~w~n',[_VarID,_Card,_Info,_Val]).
515 :- endif.
516
517 /* comment in for debugging :
518 % dummy call to register variable name with free Prolog variables:
519 % can be obtained using frozen()
520 :- public register_prolog_variable_name/3. % Debugging tool
521 :- block register_prolog_variable_name(-,?,?).
522 register_prolog_variable_name(int(Val),Name,Type) :- !,
523 register_prolog_variable_name(Val,Name,Type).
524 register_prolog_variable_name(fd(Val,_),Name,Type) :- !,
525 register_prolog_variable_name(Val,Name,Type).
526 register_prolog_variable_name(string(Val),Name,Type) :- !,
527 register_prolog_variable_name(Val,Name,Type).
528 register_prolog_variable_name((A,B),Name,Type) :- !,
529 register_prolog_variable_name(A,left(Name,mapto(B)),Type),
530 register_prolog_variable_name(B,right(Name,mapfrom(A)),Type).
531 register_prolog_variable_name([A|T],Name,Type) :- !,
532 register_prolog_variable_name(A,el(Name),Type),
533 register_prolog_variable_name(T,Name,Type).
534 register_prolog_variable_name(_,_,_).
535 % TO DO: something that pretty prints the path information for the average user
536
537 % a tool to get variable name if it was registered
538 :- public get_prolog_variable_name/3. % Debugging tool
539 get_prolog_variable_name(X,Name,Type) :- var(X),
540 frozen(X,Goal), print(goal(X,Goal)),nl,
541 goal_member(Goal,b_enumerate:register_prolog_variable_name(_,ID,T)),
542 Name=ID, Type=T.
543 goal_member(X,X).
544 goal_member((A,B),X) :- goal_member(A,X) ; goal_member(B,X).
545 ------- */
546
547 sort_typed_values([],R,_,_,R).
548 sort_typed_values([typedval(Val,Type,VarID,EnumWarningInfo)|Rest],SortedSoFar,UselessIds,DelayedIds,Res) :-
549 %% comment in next line to keep track of variable names for enumeration warnings, etc...
550 %% register_prolog_variable_name(Val,VarID,Type), % dummy call to register variable name with free Prolog variables
551 (is_lambda_result_or_useless(VarID,EnumWarningInfo,UselessIds) -> % DO_NOT_ENUMERATE
552 (%Rest=[],SortedSoFar=[], % we used to check it is the only non-ground value to enumerate
553 \+ ground_value(Val)
554 % could be relevant if a variable was annotated as do_not_enumerate and there is a WD error in
555 % the expression defining it, e.g. in test 2337: {id19,id20|id19 : BOOL & id20 <: INTEGER}(id1) = x
556 -> % Note: we can have a construct {lambda_result| #x.( P(x) & lambda_result=E(x))},
557 % we want to enumerate it after trying to solve the existential quantifier
558 last_priority(Prio), % important that it is higher than existential quantifier prio, cf test 1492
559 add_enum_warning_info(EnumWarningInfo,NewInfo),
560 insert_val(SortedSoFar,Val,Type,VarID,NewInfo,Prio,NewSorted),
561 (debug:debug_level_active_for(9),
562 Rest\=[], SortedSoFar \= [] % then it is the only variable anyway
563 -> format('~n*** Possibly enumerating lambda result ~w : ~w (~w:~w)~n~n',[VarID,Val,Type,Prio])
564 ; true)
565 % was triggered in test 1093 and 1161, but seems no longer necessary there
566 ; NewSorted=SortedSoFar % completely skip enumeration
567 )
568 ; ground_value(Val) -> NewSorted=SortedSoFar
569 ; get_max_cardinality_as_priority(Type,CardPrio),
570 (member(delay_enum(PosNr,VarID),DelayedIds),
571 integer_pow2_priority(Prio), P2 is Prio+PosNr,
572 P2>CardPrio
573 -> debug_println(9,'DELAY_ENUMERATION'(VarID,PosNr,P2,CardPrio)),
574 get_bounded_priority(P2,EnumPrio)
575 ; EnumPrio=CardPrio),
576 %% TO DO: maybe also take shape of Val into account; e.g. if cardinality of a set already fixed...
577 insert_val(SortedSoFar,Val,Type,VarID,EnumWarningInfo,EnumPrio,NewSorted)
578 ),
579 sort_typed_values(Rest,NewSorted,UselessIds,DelayedIds,Res).
580
581 get_max_cardinality_as_priority(integer,Prio) :- !, integer_priority(Prio).
582 get_max_cardinality_as_priority(Type,Prio) :-
583 ? max_cardinality(Type,Card), !,
584 (number(Card) % \= inf or inf_overflow
585 -> %Prio=Card
586 get_bounded_priority(Card,Prio)
587 ; inf_type_prio(Type,Prio)
588 ).
589 get_max_cardinality_as_priority(Type,Prio) :-
590 add_internal_error('Failed: ',max_cardinality(Type,_)),
591 integer_priority(Prio).
592
593 % Try to give priority to simpler infinite types (such as integer over seq(_) ,...)
594 % TO DO: to a full-blown analysis ...
595 inf_type_prio(integer,Prio) :- !, integer_priority(Prio).
596 inf_type_prio(real,Prio) :- !, integer_priority(P1), Prio is P1+11.
597 inf_type_prio(seq(X),Prio) :- !, inf_type_prio(X,P1), Prio is P1+11.
598 inf_type_prio(set(X),Prio) :- !, inf_type_prio(X,P1), Prio is P1+10.
599 %inf_type_prio(couple(_,_),Prio) :- !, TO DO check if both args are infinite or not ...
600 inf_type_prio(_,Prio) :- !, integer_priority(P), Prio is P+1.
601
602 :- public portray_typed_values/1.
603 portray_typed_values(List) :- maplist(print_typedvalc,List),nl.
604 print_typedvalc(typedvalc(_Val,_Type,VarID,_EnumWarning,Card)) :-
605 format('~w (card:~w) ',[VarID,Card]).
606
607 %typedvalc = typedval + cardinality information
608 insert_val([],Val,Type,VarID,EnumWarning,Card,[typedvalc(Val,Type,VarID,EnumWarning,Card)]).
609 insert_val([TC|T], Val,Type, VarID, EnumWarning, Card, Res) :-
610 TC = typedvalc(V1,_T1,_Var1,_W1,C1),
611 ? (cardval_greater_than(C1,V1,Card,Val)
612 -> Res = [typedvalc(Val,Type,VarID,EnumWarning,Card),TC|T]
613 ; Res = [TC|RT],
614 insert_val(T,Val,Type,VarID,EnumWarning,Card,RT)
615 ).
616
617 :- use_module(inf_arith,[infgreater/2]).
618 :- use_module(library(random)).
619 cardval_greater_than(C1,_,Card,_) :- infgreater(C1,Card). %Card \== inf, (C1=inf -> true ; C1>Card).
620 cardval_greater_than(Card,V1,Card,Val) :-
621 var(V1), nonvar(Val). % if card equal give priority to nonvariable values
622 cardval_greater_than(Card,_,Card,_) :-
623 preferences:preference(randomise_enumeration_order,true),
624 % TO DO: maybe we even want to change the order if cardinality different ?
625 % this also does not really generate random permutation of variables with same cardinality
626 random(1,3,1).
627
628 /*
629 % call to enumerate an integer ensuring that you go at least from MinFrom to MinTo
630 %:- block enumerate_integer_with_min_range_wf(-,?,?,?).
631 enumerate_integer_with_min_range_wf(int(X),MinFrom,MinTo,WF) :-
632 integer_priority(Prio), P1 is Prio-1,
633 ... removed ...
634 */