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 | | */ |