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