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