1 | | % (c) 2014-2022 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(clpfd_lists,[ |
6 | | lazy_fd_value_check/4, |
7 | | try_in_fd_value_list_check/4, |
8 | | avl_fd_value_check/4, |
9 | | in_fd_value_list_wf/4, in_fd_value_list_wf/3, |
10 | | get_fd_value_list/5, |
11 | | try_get_fd_value_list/4, |
12 | | get_fd_value/3, |
13 | | |
14 | | get_fdset_information/2, get_finite_fdset_information/2, |
15 | | combine_fdset_information/3, |
16 | | assert_fdset_information/2 |
17 | | ]). |
18 | | |
19 | | :- use_module(preferences). |
20 | | :- use_module(error_manager). |
21 | | |
22 | | :- use_module(module_information,[module_info/2]). |
23 | | :- module_info(group,kernel). |
24 | | :- module_info(description,'This module provides a way to call the CLPFD clpfd_inlist and clpfd:element predicates for lists of FD values.'). |
25 | | |
26 | | % see clpfd_tables test category |
27 | | |
28 | | % ----------------------------------------------------- |
29 | | |
30 | | :- block complete_type(-). |
31 | | % check if we have a complete value type or if we extract only part of the value |
32 | | complete_type(global(_)). |
33 | | complete_type(integer). |
34 | | %complete_type(couple(A,B)) :- fail. % THIS IS NOT COMPLETE !! -> the element checks are done for each component in isolation ! (there is no guarantee that the pair is in the list of pairs) |
35 | | |
36 | | % ----------------------------------------------------- |
37 | | |
38 | | :- block try_in_fd_value_list_check(-,?,?,?). |
39 | | try_in_fd_value_list_check([],_,_,_) :- fail. |
40 | | try_in_fd_value_list_check([H|T],El,Type,WF) :- |
41 | | try_get_fd_value_type(El,H,Type), % print(fd_val_type(El,H,T)),nl, |
42 | | !, |
43 | | get_fd_value_list([H|T],Type,FDList,GroundList,El), |
44 | | get_fd_value(Type,El,ElFD), |
45 | | in_fd_value_list_wf(GroundList,ElFD,FDList,WF). |
46 | | try_in_fd_value_list_check(S,El,Type,WF) :- |
47 | | (S=[_|_] -> true |
48 | | ; add_internal_error('Illegal call: ',try_in_fd_value_list_check(S,El,Type,WF))). |
49 | | |
50 | | :- use_module(kernel_freetypes,[get_freeval_type/3]). |
51 | | |
52 | | % try get fd_value type from two values; one from element one from set |
53 | ? | try_get_fd_value_type(V1,V2,T) :- var(V1),!, try_get_fd_value(T,V2,_). |
54 | | try_get_fd_value_type((A1,_),(A2,_),T) :- nonvar(T),T=couple_left(TA),!, |
55 | | try_get_fd_value_type(A1,A2,TA). % useful for domain checks |
56 | | try_get_fd_value_type((A1,B1),(A2,B2),Type) :- !, |
57 | ? | (try_get_fd_value_type(A1,A2,TA) |
58 | | -> (try_get_fd_value_type(B1,B2,TB) |
59 | | -> Type = couple(TA,TB) % we have two values |
60 | | ; %print(failed_right(B1,B2,TB)),nl, |
61 | | Type = couple_left(TA)) |
62 | | ; Type = couple_right(TB), |
63 | | try_get_fd_value_type(B1,B2,TB)). |
64 | | try_get_fd_value_type(freeval(ID,Case,Val1),V2, freeval_case(ID,Case,Type)) :- !, |
65 | | nonvar(Case), ground(ID), |
66 | | (nonvar(V2),V2 = freeval(ID2,Case2,Val2), |
67 | | (ID,Case) == (ID2,Case2) |
68 | | -> try_get_fd_value_type(Val1,Val2,Type) |
69 | | ; % TO DO: if the cases do not match and if Val1 is a variable then we may miss FD values |
70 | | %print(case_mismatch(ID,Case,V2)),nl, |
71 | | get_freeval_type(ID,Case,_CaseType), |
72 | | %print(freeval_case_type(ID,Case,CaseType,Val1)),nl, |
73 | | % TO DO: use CaseType in case Val1 is not instantiated enough |
74 | | try_get_fd_value(Type,Val1,_)). |
75 | | try_get_fd_value_type(V1,V2,T) :- |
76 | ? | (var(V2) -> try_get_fd_value(T,V1,_) ; try_get_fd_value(T,V2,_)). |
77 | | |
78 | | % TO DO: merge both versions of try_get_fd_value |
79 | | try_get_fd_value(T,V,_) :- var(V),var(T),!,fail. |
80 | | try_get_fd_value(TV,(A,B),FD) :- var(TV),!, |
81 | ? | (try_get_fd_value(TA,A,FDA) |
82 | ? | -> (try_get_fd_value(TB,B,FDB) % What if this fails because B is still a variable !? --> ideally, typing info would help |
83 | | -> TV = couple(TA,TB), FD=fd_pair(FDA,FDB) % we have two values |
84 | | ; TV = couple_left(TA), FD=FDA) |
85 | | ; TV = couple_right(TB), |
86 | | try_get_fd_value(TB,B,FD)). |
87 | | try_get_fd_value(couple(TA,TB),(A,B),fd_pair(FDA,FDB)) :- |
88 | | try_get_fd_value(TA,A,FDA),try_get_fd_value(TB,B,FDB). |
89 | | try_get_fd_value(couple_left(T),(A,_),FDA) :- try_get_fd_value(T,A,FDA). % useful for domain checks |
90 | | % to do: try and get both and do multiple in_list/element calls later |
91 | | try_get_fd_value(couple_right(T),(_,A),FDA) :- try_get_fd_value(T,A,FDA). % useful for range checks |
92 | | try_get_fd_value(rec_fields(T),rec(Fields),fd_rec(FD)) :- |
93 | | try_get_field_fd_values(T,Fields,FD), |
94 | | T \= []. |
95 | | try_get_fd_value(global(GS),fd(X,GS),X). |
96 | | try_get_fd_value(integer,int(X),X). |
97 | | |
98 | | try_get_field_fd_values(_,Fields,_) :- var(Fields),!,fail. % we don't know all the fields; better do nothing |
99 | | try_get_field_fd_values(Types,[],FDVals) :- !,Types=[],FDVals=[]. |
100 | | try_get_field_fd_values(_,[FN|_],_) :- var(FN),!,fail. |
101 | | try_get_field_fd_values(_,[field(Name,_)|_],_) :- var(Name),!,fail. |
102 | | try_get_field_fd_values(Types,[field(Name,Value)|TF],FDVals) :- |
103 | ? | try_get_fd_value(T,Value,FDVal), |
104 | | !, |
105 | | Types = [field(Name,T)|TTypes], |
106 | | FDVals = [FDVal|TFD], |
107 | | try_get_field_fd_values(TTypes,TF,TFD). |
108 | | try_get_field_fd_values([field_no_fd(Name)|Types],[field(Name,_)|TF],FDVals) :- |
109 | | try_get_field_fd_values(Types,TF,FDVals). |
110 | | |
111 | | |
112 | | :- use_module(b_global_sets,[get_global_type_value/3]). |
113 | | |
114 | | get_fd_value(T,V,E) :- var(V),var(T),!, |
115 | | add_internal_error('Variable arguments: ',get_fd_value(V,T,E)),fail. |
116 | | get_fd_value(couple(TA,TB),(A,B),fd_pair(FDA,FDB)) :- |
117 | | get_fd_value(TA,A,FDA), get_fd_value(TB,B,FDB). |
118 | | get_fd_value(couple_left(T),(A,_),FDA) :- get_fd_value(T,A,FDA). |
119 | | get_fd_value(couple_right(T),(_,A),FDA) :- get_fd_value(T,A,FDA). |
120 | | get_fd_value(rec_fields(T),rec(Fields),fd_rec(FD)) :- get_field_fd_values(T,Fields,FD). |
121 | | get_fd_value(freeval_case(ID,Case,T),freeval(ID,Case,A),FDA) :- |
122 | | get_fd_value(T,A,FDA). |
123 | | get_fd_value(global(GS),FD,X) :- get_global_type_value(FD,GS,X). |
124 | | get_fd_value(integer,int(X),X). |
125 | | |
126 | | get_field_fd_values([],[],[]). |
127 | | get_field_fd_values([field_no_fd(Name)|TTypes],[field(Name,_)|TF],FDVals) :- |
128 | | get_field_fd_values(TTypes,TF,FDVals). |
129 | | get_field_fd_values([field(Name,T)|TTypes],[field(Name,Value)|TF],[FDVal|TFD]) :- |
130 | | get_fd_value(T,Value,FDVal), |
131 | | get_field_fd_values(TTypes,TF,TFD). |
132 | | |
133 | | :- use_module(library(lists),[maplist/2]). |
134 | | check_valid_fd_type(Type) :- |
135 | | (valid_type(Type) -> true |
136 | | ; add_internal_error('Illegal FD type:',check_valid_fd_type(Type)),fail). |
137 | | valid_type(couple(TA,TB)) :- valid_type(TA),valid_type(TB). |
138 | | valid_type(couple_left(TA)) :- valid_type(TA). |
139 | | valid_type(couple_right(TA)) :- valid_type(TA). |
140 | | valid_type(global(GS)) :- atomic(GS). |
141 | | valid_type(rec_fields(Fs)) :- maplist(valid_rec_type,Fs). |
142 | | valid_type(freeval_case(_,_,TA)) :- valid_type(TA). |
143 | | valid_type(integer). |
144 | | |
145 | | valid_rec_type(field(_,T)) :- valid_type(T). |
146 | | valid_rec_type(field_no_fd(_)). |
147 | | |
148 | | % ----------------------------------------------------- |
149 | | |
150 | | % extract from a Set (List) representation a list of FDValues which can be used by the clpfd library |
151 | | try_get_fd_value_list(Set,Type,FDList,GroundList) :- |
152 | | try_get_fd_value_list5(Set,Type,FDList,true,GroundList). |
153 | | try_get_fd_value_list5(V,_,_,_,_) :- var(V),!,fail. |
154 | | try_get_fd_value_list5([],_,[],G,G). % Note if this is the base case then the type could be that of an empty list of pairs ! |
155 | | try_get_fd_value_list5([H|T],Type,FDList,GroundIn,GroundOut) :- |
156 | | try_get_fd_value(Type,H,Value),!, FDH=Value, |
157 | | (GroundIn=true,integer(FDH) -> Ground1=true ; Ground1=false), |
158 | | %%(ground(T) -> true ; print(get_fd_val_list(H,T)),nl), %% |
159 | | check_non_var_list(T), % do not instantiate any free variable ! otherwise we get full domain probably anyway ? |
160 | | if(get_fd_value_list5(T,Type,FDT,Ground1,GroundOut,_NoFilterEl,1), |
161 | | FDList = [FDH|FDT], |
162 | | FDList = []). % obtaining FD value triggered inconsistency |
163 | | try_get_fd_value_list5(avl_set(A),_,_,_,_) :- |
164 | | add_internal_error('Not a list: ',try_get_fd_value_list5(avl_set(A),_,_,_,_)),fail. |
165 | | try_get_fd_value_list5(node(A,B,C,D,E),_,_,_,_) :- |
166 | | add_internal_error('Not a list: ',try_get_fd_value_list5(node(A,B,C,D,E),_,_,_,_)),fail. |
167 | | try_get_fd_value_list5(closure(A,B,C),_,_,_,_) :- |
168 | | add_internal_error('Not a list: ',try_get_fd_value_list5(closure(A,B,C),_,_,_,_)),fail. |
169 | | |
170 | | check_non_var_list(V) :- var(V),!,fail. %print(check_non_var_failed),nl,fail. |
171 | | check_non_var_list([]). |
172 | | check_non_var_list([H|T]) :- !, nonvar(H), check_non_var_list(T). |
173 | | |
174 | | % ----------------------------------------------------- |
175 | | |
176 | | % remove from a list of FDValues those that belong to objects that definitely cannot match Element |
177 | | % this improves the precision of a later in_fd_value_list_wf call |
178 | | % cannot_match: quick check to see if the (AVL or List) element could match |
179 | | |
180 | | :- use_module(kernel_tools,[cannot_match/2, cannot_match_aggressive/2]). |
181 | | |
182 | | % gets a (filtered) FD Value list (El used for filtering) |
183 | | get_fd_value_list(Set,Type,FDList,GroundList,El) :- |
184 | | get_fd_value_list5(Set,Type,FDList,true,GroundList,El,0). |
185 | | get_fd_value_list5(V,_,_,_,_,_,_) :- var(V),!,fail. |
186 | | get_fd_value_list5([],_,[],G,G,_,_). |
187 | | get_fd_value_list5([H|T],Type,FDValList,GroundIn,GroundOut,El,NrMatch) :- |
188 | | (NrMatch<2 -> cannot_match_aggressive(H,El) % there is still hope of obtaining something deterministic; try more aggressive version; important for test 34; see also test 985 where too much propagation hurts |
189 | | ; cannot_match(H,El)), |
190 | | !, % we can filter this FD Value out |
191 | | get_fd_value_list5(T,Type,FDValList,GroundIn,GroundOut,El,NrMatch). |
192 | | get_fd_value_list5([H|T],Type,FDValList,GroundIn,GroundOut,El,NrMatch) :- |
193 | | if(get_fd_value(Type,H,FDH), |
194 | | (FDValList = [FDH|FDT], N1 is NrMatch+1, |
195 | | (GroundIn=true,number(FDH) -> Ground1=true ; Ground1=false)), |
196 | | % Failure can happen when a variable gets instantiated (eg. X -> fd(_,t)) |
197 | | % and triggers co-routines which fail (happens for SelfGrandpas.als for scope 3) |
198 | | % TO DO: review that this is the only possibility of failure |
199 | | (debug:debug_println(9,get_fd_value_failed(Type,H,_)), |
200 | | check_valid_fd_type(Type),fail) |
201 | | ), |
202 | | get_fd_value_list5(T,Type,FDT,Ground1,GroundOut,El,N1). |
203 | | |
204 | | % ----------------------------------------------------- |
205 | | |
206 | | :- use_module(library(clpfd)). |
207 | | :- use_module(clpfd_interface). |
208 | | :- use_module(kernel_waitflags,[get_enumeration_starting_wait_flag/3]). |
209 | | |
210 | | in_fd_value_list_wf(Element,List,WF) :- |
211 | | (ground_integer_list(List) -> Gr=true ; Gr=false), |
212 | | in_fd_value_list_wf(Gr,Element,List,WF). |
213 | | |
214 | | ground_integer_list(Var) :- var(Var),!,fail. |
215 | | ground_integer_list([]). |
216 | | ground_integer_list([H|T]) :- integer(H), ground_integer_list(T). |
217 | | |
218 | | % assert that an FD Value is in a list of FD Values |
219 | | % in_fd_value_list(ListIsGroundOfSimpleIntegers, FDElement, ListOfFDValues) |
220 | | in_fd_value_list_wf(true,Element,List,_WF) :- |
221 | | List \= [], % avoid calling in case Element is compound (as try_get_fd_value_list will return ground for empty list) |
222 | | clpfd_inlist(Element,List). % element should not be a compound like fd_pair! |
223 | | in_fd_value_list_wf(false,Element,List,WF) :- |
224 | | %get_enumeration_finished_wait_flag(WF,EWF), |
225 | | get_enumeration_starting_wait_flag(in_fd_value_list_wf,WF,EWF), % relevant for test 2070 to avoid enum warning |
226 | | in_non_ground_fd_value_lists(Element,List,EWF,top). |
227 | | |
228 | | in_non_ground_fd_value_lists(FDP,List,EWF,_) :- nonvar(FDP), FDP = fd_pair(A,B), !, |
229 | | split_fd_pair_list(List,ListA,ListB), |
230 | | in_non_ground_fd_value_lists(A,ListA,EWF,left), |
231 | | in_non_ground_fd_value_lists(B,ListB,EWF,right). |
232 | | in_non_ground_fd_value_lists(FDR,List,EWF,_) :- nonvar(FDR), FDR = fd_rec(Fields), !, |
233 | | %print(treat_fd_rec_fields(Fields,List)),nl, |
234 | | treat_fd_rec_fields(Fields,List,EWF). |
235 | | in_non_ground_fd_value_lists(Element,List,_EWF,Path) :- |
236 | | Path \= top, % otherwise we know List not to be ground |
237 | | ground(List), %ground_number_list(List,Min,Max,Len), List can be a large term |
238 | | !, |
239 | | clpfd_interface:clpfd_inlist(Element,List). % this is considerably faster; especially in compiled version (see SLOT-PERFORMANCE2) |
240 | | % TODO: use force_clpfd_inlist ? clpfd_inlist uses try_post_constraint |
241 | | in_non_ground_fd_value_lists(Element,List,_EWF,_Path) :- |
242 | | tools:exact_member(Element,List), % avoid generating choice point for element position below |
243 | | !. |
244 | | in_non_ground_fd_value_lists(Element,List,EWF,_Path) :- |
245 | | % asserts that Element is the _Nr-th element of List; in contrast to clpfd_inlist List do not have to be numbers |
246 | | post_clpfd_element(List,Element,EWF). |
247 | | |
248 | | |
249 | | % we cannot use new element/2 constraint in SICStus 4.7.0, because this will not enumerate the Idx before infinite enumeration starts (cf test 2070) |
250 | | post_clpfd_element(List,Element,EWF) :- |
251 | | element(Nr,List,Element), |
252 | | label_el_nr(Nr,Element,List,EWF). |
253 | | |
254 | | |
255 | | |
256 | | /* using this + Element in Min..Max |
257 | | does not seem to buy anything/ a lot to comparing calling clpfd_inlist for large lists |
258 | | ground_number_list([],0,0,0). |
259 | | ground_number_list([H|T],Min,Max,Len) :- number(H), |
260 | | ground_number_list_acc(T,H,H,1,Min,Max,Len). |
261 | | ground_number_list_acc([],Min,Max,Len,Min,Max,Len). |
262 | | ground_number_list_acc([H|T],Min0,Max0,Len0,Min,Max,Len) :- number(H), |
263 | | (H<Min0 -> Min1 = H ; Min1 = Min0), |
264 | | (H>Max0 -> Max1 = H ; Max1 = Max0), |
265 | | L1 is Len0+1, |
266 | | ground_number_list_acc(T,Min1,Max1,L1,Min,Max,Len). |
267 | | */ |
268 | | |
269 | | treat_fd_rec_fields([],_,_). |
270 | | treat_fd_rec_fields([V|TF],List,EWF) :- |
271 | | get_next_fd_rec_field(List,FieldFDList,RemainingList), |
272 | | %print(check(V,FieldFDList)),nl, |
273 | | in_non_ground_fd_value_lists(V,FieldFDList,EWF,rec), |
274 | | treat_fd_rec_fields(TF,RemainingList,EWF). |
275 | | |
276 | | get_next_fd_rec_field([],FieldList,RemList) :- !, FieldList=[], RemList=[]. |
277 | | get_next_fd_rec_field([fd_rec([FDV|Rem]) | TList], [FDV|TFieldList], [ fd_rec(Rem) | TRemList]) :- !, |
278 | | get_next_fd_rec_field(TList, TFieldList, TRemList). |
279 | | get_next_fd_rec_field(List,FieldList,RemainingList) :- |
280 | | add_internal_error('Illegal call: ',get_next_fd_rec_field(List,FieldList,RemainingList)), |
281 | | FieldList=[], RemainingList=[]. |
282 | | |
283 | | % label ElementNr of element/3 clpfd constraint if necessary |
284 | | % Note: ElementNr is a local variable not used outside of in_non_ground_fd_value_lists |
285 | | :- block label_el_nr(?,-,?,?), label_el_nr(-,?,?,-). |
286 | | label_el_nr(ElementNr,Element,List,_) :- |
287 | | (number(ElementNr) -> true % clpfd:element already has a solution |
288 | | ; exact_member_nr(Element,List,1,Nr) -> ElementNr=Nr |
289 | | ; \+ fd_var(ElementNr) -> print(already_enumerating(Element,ElementNr)),nl |
290 | | % probably co-routine got activated while enumerating Element and clpfd has not yet set ElementNr, |
291 | | % but clpfd has removed the fd domain |
292 | | ; ground(List) -> (labeling([],[ElementNr]) -> true) % avoid pending co-routines in case the Element appears multiple times in the list by picking an arbitrary solution !) |
293 | | ; %translate:print_clpfd_variable(ElementNr),nl, |
294 | | labeling([],[ElementNr]) % enumerate ElementNr -> before infinite enumeration we chose possible values |
295 | | % we cannot use cut after labeling, labeling ElementNr can instantiate List |
296 | | % example where this is needed, {r|3 : {r,r+1} } in CLPFD=TRUE mode |
297 | | ). |
298 | | |
299 | | exact_member_nr(X,[Y|_],Acc,R) :- X==Y, !, Acc=R. |
300 | | exact_member_nr(X,[_|T],Acc,R) :- A1 is Acc+1, exact_member_nr(X,T,A1,R). |
301 | | |
302 | | split_fd_pair_list([],[],[]). |
303 | | split_fd_pair_list([fd_pair(A,B)|T],[A|TA],[B|TB]) :- split_fd_pair_list(T,TA,TB). |
304 | | |
305 | | |
306 | | % ----------------------------------------------------- |
307 | | |
308 | | :- use_module(kernel_objects,[equal_object/2]). |
309 | | |
310 | | % a lazy, blocking version which waits for Set to become sufficiently instantiated and then |
311 | | % calls in_fd_value_list_wf |
312 | | % Trys to transform E:Set into calls to clpfd library: ; |
313 | | % When FullyChecked becomes true, then there is no need to perform other processing (apart from labeling/enumeration of the involved values) |
314 | | % When FullyChecked becomes false |
315 | | lazy_fd_value_check(Set,E,_,FC) :- nonvar(Set), Set=[H|T], T==[], |
316 | | !, % we have a one-element singleton set |
317 | | %tools_printing:print_term_summary(equal_object(H,E)),nl, |
318 | | equal_object(H,E), |
319 | | FC=true. |
320 | | lazy_fd_value_check(Set,E,WF,FullyChecked) :- preferences:preference(use_clpfd_solver,true),!, |
321 | | lazy_in_list_propagation_block(Set,E,WF,FullyChecked). |
322 | | lazy_fd_value_check(_Set,_E,_WF,false). |
323 | | |
324 | | :- block lazy_in_list_propagation_block(-,?,?,?). |
325 | | lazy_in_list_propagation_block([],_,_,_) :- fail. % nothing can be element of empty set |
326 | | lazy_in_list_propagation_block([H|T],E,WF,FullyChecked) :- contains_fd_element(H,Res,WF), |
327 | | lazy_in_list_propagation_block_2(Res,H,T,E,WF,FullyChecked). |
328 | | |
329 | | :- block lazy_in_list_propagation_block_2(-,?,?,?,?,?). |
330 | | lazy_in_list_propagation_block_2(pred_false,_H,_T,_E,_WF,false). % nothing to propagate |
331 | | lazy_in_list_propagation_block_2(pred_true,H,T,E,WF,FullyChecked) :- % print(bound_h(H)),nl, |
332 | | bound_list(T,Bound), |
333 | | lazy_in_list_propagation_block_3(Bound,H,T,E,WF,FullyChecked). |
334 | | |
335 | | :- block lazy_in_list_propagation_block_3(-,?,?,?,?,?). |
336 | | lazy_in_list_propagation_block_3(pred_false,_H,_T,_E,_WF,FC) :- !, FC=false. % nothing to propagate |
337 | | lazy_in_list_propagation_block_3(pred_true,H,T,E,WF,FullyChecked) :- |
338 | ? | try_get_fd_value_type(E,H,Type), % print(fd_val_type(E,H,Type)),nl, |
339 | | get_fd_value_list([H|T],Type,FDVals,GroundList,E), % try and extract values which can be used for CLPFD |
340 | | get_fd_value(Type,E,EFD),!, |
341 | | FDVals \= [], % if we have the empty list then membership fails |
342 | | (complete_type(Type) -> FullyChecked = true ; FullyChecked = false), |
343 | | % print(lazy_in_element(FullyChecked,GroundList,E,[H|T],WF)),nl, |
344 | | % print(in_fd_value_list_wf(GroundList,EFD,FDVals,WF,FullyChecked)),nl, |
345 | | in_fd_value_list_wf(GroundList,EFD,FDVals,WF). |
346 | | lazy_in_list_propagation_block_3(pred_true,_H,_T,_E,_WF,FullyChecked) :- !, |
347 | | % should only happen for freeval with no fd type inside or for freevalues if element is not instantiated (we don't know which freval case we have) |
348 | | FullyChecked=false. |
349 | | lazy_in_list_propagation_block_3(P,H,T,E,WF,false) :- |
350 | | add_internal_error('Illegal call: ',lazy_in_list_propagation_block_3(P,H,T,E,WF,false)). |
351 | | |
352 | | :- block contains_fd_element(-,?,?). |
353 | | contains_fd_element(int(_),R,_WF) :- !, R=pred_true. |
354 | | contains_fd_element(fd(_,_),R,_WF) :- !, R=pred_true. |
355 | | contains_fd_element((A,B),R,WF) :- !,contains_fd_element(A,RA,WF), contains_fd_element(B,RB,WF), |
356 | | b_interpreter_check:disjoin(RA,RB,R,priority(16384),priority(16384),WF). % TO DO: examine priority to be used |
357 | | contains_fd_element(rec(Fields),R,WF) :- !, contains_field_fd_el(Fields,R,WF). |
358 | | contains_fd_element(freeval(_ID,_Case,_Val),R,_WF) :- !, |
359 | | % We assume that a freetype can contain FD elements; TO DO: really check ! |
360 | | % ID is something of the form 'List'(integer) ; we use get_freeval_type(ID,_Case) from kernel_freetypes to get subtypes |
361 | | % we could look at the value; but we could be unlucky in that this particular Case has no fd subtype but others do |
362 | | % anyway: try_get_fd_value_type will fail if there is no fd type |
363 | | R=pred_true. |
364 | | contains_fd_element(_,pred_false,_). |
365 | | |
366 | | :- block contains_field_fd_el(-,?,?). |
367 | | contains_field_fd_el([],R,_WF) :- !, R=pred_false. |
368 | | contains_field_fd_el([field(_,V)|_],R,WF) :- contains_fd_element(V,R,WF). % TO DO: look at other fields |
369 | | % deal with freetypes: freeval(ID,Case,Value); but here we need a different scheme: we need to find the case of the element and only look at elements in the list with the same constructor |
370 | | % we could also deal with set types {x,y} : { {1,2}, {2,3} } --> x/y : 1..3 |
371 | | % TO DO: maybe filter out non-matching elements also here (see filter_non_matching_elements for quick_propagate) |
372 | | |
373 | | % set output variable as soon as we can determine if we have a bound list |
374 | | :- block bound_list(-,?). |
375 | | bound_list(List,BoundList) :- |
376 | | (List = [] -> BoundList=pred_true |
377 | | ; List = [_|T] -> bound_list(T,BoundList) |
378 | | ; BoundList=pred_false). % we have avl_set or global_set or closure; TO DO: also allow avl_set |
379 | | |
380 | | |
381 | | % ----------------------------------------------------- |
382 | | |
383 | | % generate an in_fd_value_list_wf call for checking that E is a member of an AVL set encoding |
384 | | :- use_module(library(avl),[avl_domain/2]). |
385 | | avl_fd_value_check(AVL,E,WF,FullyChecked) :- |
386 | | AVL = node(TopEl,_True,_,_,_),!, |
387 | | contains_fd_element(TopEl,Res,WF), |
388 | | (Res==pred_true |
389 | | -> avl_domain(AVL,DomainList), |
390 | | DomainList = [H|T], |
391 | | lazy_in_list_propagation_block_3(pred_true,H,T,E,WF,FullyChecked) |
392 | | ; FullyChecked=false). |
393 | | avl_fd_value_check(AVL,E,WF,FullyChecked) :- |
394 | | add_internal_error('Illegal call: ',avl_fd_value_check(AVL,E,WF,FullyChecked)), |
395 | | FullyChecked=false. |
396 | | |
397 | | |
398 | | |
399 | | |
400 | | % ------------------------------------------------------------------------ |
401 | | |
402 | | % alternative utilities for collecting fd_set information, combine it and then use it |
403 | | |
404 | | % FD-SET |
405 | | |
406 | | % succeeds if we can obtain FD information for a B data value |
407 | | get_fdset_information(V,Info) :- var(V),!,Info=no_fdset_info. |
408 | | get_fdset_information(int(V),int_fdset(FDSET)) :- fd_set(V,FDSET). |
409 | | get_fdset_information(fd(V,GS),fd_fdset(FDSET,GS)) :- fd_set(V,FDSET). |
410 | | get_fdset_information(pred_true,single_value(pred_true)). |
411 | | get_fdset_information(pred_false,single_value(pred_false)). |
412 | | get_fdset_information(string(S),single_value(string(S))) :- ground(S). |
413 | | % TO DO: add more: couples, records, ... |
414 | | |
415 | | get_finite_fdset_information(V,_Info) :- var(V),!,fail. |
416 | | get_finite_fdset_information(int(V),int_fdset(FDSET)) :- finite_fd_set(V,FDSET). |
417 | | get_finite_fdset_information(fd(V,GS),fd_fdset(FDSET,GS)) :- finite_fd_set(V,FDSET). |
418 | | get_finite_fdset_information(pred_true,single_value(pred_true)). |
419 | | get_finite_fdset_information(pred_false,single_value(pred_false)). |
420 | | get_finite_fdset_information(string(S),single_value(string(S))) :- ground(S). |
421 | | |
422 | | finite_fd_set(V,FDSET) :- fd_set(V,FDSET), fdset_size(FDSET,N), number(N). %FDSET \= [[inf|sup]]. |
423 | | |
424 | | % will combine (union) two FD infos; have to be of compatible type |
425 | | combine_fdset_information(no_fdset_info,I,R) :- !, R=I. |
426 | | combine_fdset_information(I,no_fdset_info,R) :- !, R=I. |
427 | | combine_fdset_information(int_fdset(A),int_fdset(B),int_fdset(C)) :- !, |
428 | | %print(un(A,B,C)),nl, |
429 | | fdset_union(A,B,C). |
430 | | combine_fdset_information(fd_fdset(A,GS),fd_fdset(B,GS),fd_fdset(C,GS)) :- !, |
431 | | fdset_union(A,B,C). |
432 | | combine_fdset_information(single_value(V),single_value(W),R) :- !, |
433 | | (V==W -> R=single_value(V) ; R=no_fdset_info). |
434 | | combine_fdset_information(A,B,C) :- |
435 | | add_internal_error('Illegal FD info: ',combine_fdset_information(A,B,C)),fail. |
436 | | |
437 | | % assert that a variable/value matches collected FD information |
438 | | assert_fdset_information(int_fdset(FDSet),X) :- !, |
439 | | (ground(X) -> true ; X=int(XX),in_set(XX,FDSet)). |
440 | | assert_fdset_information(fd_fdset(FDSet,GS),X) :- !, |
441 | | (ground(X) -> true ; X=fd(XX,GS),in_set(XX,FDSet)). |
442 | | assert_fdset_information(single_value(V),X) :- !, equal_object(V,X). |
443 | | assert_fdset_information(_,_). |
444 | | |
445 | | |
446 | | |