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