| 1 | % (c) 2016-2024 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_tables,[can_translate_avl_to_table/2, translate_avl_to_table/2, check_element_of_table/4, | |
| 6 | check_element_of_avl_with_table/4, | |
| 7 | clpfd_in_table/2, | |
| 8 | ||
| 9 | can_translate_function_to_element_constraint/2, | |
| 10 | check_apply_with_element_constraint/5]). | |
| 11 | ||
| 12 | :- use_module(module_information,[module_info/2]). | |
| 13 | :- module_info(group,kernel). | |
| 14 | :- module_info(description,'Provide interface to CLP(FD) table constraint.'). | |
| 15 | ||
| 16 | % Example usage of CLPFD table/2 : | |
| 17 | %| ?- table([[X,Y]],[[1,2],[2,3],[3,4],[4,5]]), X in 1..2. | |
| 18 | %X in 1..2, | |
| 19 | %Y in 2..3 ? | |
| 20 | ||
| 21 | :- use_module(library(clpfd)). | |
| 22 | :- use_module(library(avl),[avl_domain/2]). | |
| 23 | :- use_module(library(lists),[maplist/3, maplist/4, maplist/2]). | |
| 24 | :- use_module(kernel_waitflags,[add_fd_variables_for_labeling/2]). | |
| 25 | :- use_module(debug,[debug_println/2]). | |
| 26 | :- use_module(error_manager,[add_internal_error/2]). | |
| 27 | ||
| 28 | % can an AVL set be translated into a CLPFD table membership constraint | |
| 29 | can_translate_avl_to_table(AVL,SkeletonType) :- | |
| 30 | AVL = node(Element,_True,_,_,_), | |
| 31 | translate_to_fd_values(Element,SkeletonType,ElVList,[]), | |
| 32 | l_no_overflow(ElVList), % check that the element constraint will not generate an overflow, e.g., for test 1353 | |
| 33 | % TO DO: ideally we should check avl_min / avl_max | |
| 34 | % (but with multiple FD values in an element; even that will not guarantee that there are no overflows) | |
| 35 | SkeletonType \= boolean. % should we also disallow rec([field(_,boolean)]) % boolean treatment causes problems for 1624, 1627, 140, 1426 | |
| 36 | ||
| 37 | l_no_overflow([]). | |
| 38 | l_no_overflow([H|T]) :- no_overflow(H), l_no_overflow(T). | |
| 39 | ||
| 40 | :- use_module(tools_platform, [is_tagged_integer/1]). | |
| 41 | no_overflow(H) :- (var(H) -> true ; is_tagged_integer(H)). | |
| 42 | ||
| 43 | translate_avl_to_table(AVL,TableList) :- | |
| 44 | avl_domain(AVL,List), | |
| 45 | maplist(translate_avl_element_to_fd_list,List,TableList). | |
| 46 | ||
| 47 | check_element_of_avl_with_table(X,SkeletonType,AVL,WF) :- | |
| 48 | translate_avl_to_table(AVL,TableList), | |
| 49 | ? | check_element_of_table(X,SkeletonType,TableList,WF). |
| 50 | ||
| 51 | check_element_of_table(X,SkeletonType,TableList,WF) :- | |
| 52 | translate_to_fd_values(X,SkeletonType,XList,[]), | |
| 53 | ? | clpfd_in_table(XList,TableList), |
| 54 | add_fd_variables_for_labeling(XList,WF). % important for test 1716 | |
| 55 | ||
| 56 | ||
| 57 | :- use_module(clpfd_interface,[force_clpfd_inlist/2]). | |
| 58 | get_unique_el([X],X). | |
| 59 | clpfd_in_table([X],TableList) :- !, maplist(get_unique_el,TableList,FDList), | |
| 60 | %print(posting_clpfd_inlist(X,FDList)),nl, | |
| 61 | force_clpfd_inlist(X,FDList). | |
| 62 | :- if(current_prolog_flag(dialect, sicstus)). | |
| 63 | clpfd_in_table(XList,TableList) :- | |
| 64 | %print(posting_clpfd_table([XList],TableList)),nl, | |
| 65 | ? | table([XList],TableList,[method(aux)]). % we use aux to circumvent a bug in SICStus 4.4-4.7 |
| 66 | % we could provide in third argument, e.g., [order(id3)] | |
| 67 | :-else. | |
| 68 | clpfd_in_table(XList,TableList) :- | |
| 69 | %print(posting_clpfd_table([XList],TableList)),nl, | |
| 70 | table([XList],TableList). % translated to tuples_in in SWI | |
| 71 | :- endif. | |
| 72 | % from the SICStus Manual: | |
| 73 | % table(+Tuples,+Extension,+Options) | |
| 74 | % Defines an n-ary constraint by extension. Extension should be a list of lists of | |
| 75 | % integers, each of length n. Tuples should be a list of lists of domain variables, | |
| 76 | % each also of length n. The constraint holds if every Tuple in Tuples occurs in | |
| 77 | % the Extension. The constraint will maintain domain consistency. | |
| 78 | % For convenience, Extension may contain ConstantRange (see Section 10.10.13.1 | |
| 79 | % [Syntax of Indexicals], page 485) expressions in addition to integers. | |
| 80 | % | |
| 81 | % WARNING, SICSTUS 4.7 and earlier has a bug with negative numbers | |
| 82 | % | ?- clpfd:table([[X,Y]],[[1,0],[2,-1]]). | |
| 83 | % Y = 0, <-- this should not be !! | |
| 84 | % X in 1..2 | |
| 85 | % with aux as method we solve the issue | |
| 86 | % | ?- clpfd:table([[X,Y]],[[1,0],[2,-1]],[method(aux)]). | |
| 87 | % X in 1..2, | |
| 88 | % Y in-1..0 | |
| 89 | ||
| 90 | % TO DO: also allow partial FD infos, in which case we would use table/2 just for quick propagation | |
| 91 | % we could also translate variables into ConstantRange expressions (see above) | |
| 92 | translate_avl_element_to_fd_list(Val,FDList) :- translate_to_fd_values(Val,_,FDList,[]). | |
| 93 | ||
| 94 | translate_to_fd_values(FD,fd(T)) --> {var(FD),nonvar(T)},!, % setup FD bounds | |
| 95 | {get_global_type_value(FD,T,X)},[X]. | |
| 96 | translate_to_fd_values(fd(X,T),fd(T)) --> !, [X]. | |
| 97 | translate_to_fd_values(int(A),integer) --> !, [A]. % warning: could overflow, we check above ! | |
| 98 | translate_to_fd_values((A,B),(SkelA,SkelB)) --> !, translate_to_fd_values(A,SkelA), translate_to_fd_values(B,SkelB). | |
| 99 | translate_to_fd_values(rec(F),rec(SkelF)) --> !, l_translate_to_fd_values(F,SkelF). | |
| 100 | translate_to_fd_values(Var,Type) --> {var(Var),Type==boolean},!, {prop_01(Var,FD)},[FD]. | |
| 101 | translate_to_fd_values(pred_true,boolean) --> [1]. | |
| 102 | translate_to_fd_values(pred_false,boolean) --> [0]. | |
| 103 | % TO DO: also free-types | |
| 104 | ||
| 105 | l_translate_to_fd_values([],[]) --> []. | |
| 106 | l_translate_to_fd_values([field(N,F)|T],[field(N,SF)|ST]) --> | |
| 107 | translate_to_fd_values(F,SF),l_translate_to_fd_values(T,ST). | |
| 108 | ||
| 109 | :- block prop_01(-,-). | |
| 110 | prop_01(pred_true,1). | |
| 111 | prop_01(pred_false,0). | |
| 112 | ||
| 113 | % ---------------------- | |
| 114 | ||
| 115 | :- use_module(bsyntaxtree,[is_set_type/2]). | |
| 116 | :- use_module(preferences,[preference/2]). | |
| 117 | ||
| 118 | % can a list be translated into CLPFD element constraints for function application | |
| 119 | can_translate_function_to_element_constraint(List,FunctionType) :- | |
| 120 | FunctionType \= unknown, | |
| 121 | is_list_skeleton(List), % TO DO: allow tail AVL list + enable delaying treatment | |
| 122 | preference(find_abort_values,false), | |
| 123 | preference(use_clpfd_solver,true), | |
| 124 | % initially we checked if chr is false to avoid falling into the SICStus element/3 bug prior to 4.3.6 | |
| 125 | is_set_type(FunctionType,couple(Domain,Range)), | |
| 126 | is_simple_fd_type(Domain), % Domain must be translatable to simple FD value list | |
| 127 | is_fd_type(Range). | |
| 128 | ||
| 129 | is_list_skeleton(X) :- nonvar(X),is_list_skeleton_aux(X). | |
| 130 | is_list_skeleton_aux([]). | |
| 131 | is_list_skeleton_aux([_H|T]) :- is_list_skeleton(T). | |
| 132 | ||
| 133 | is_simple_fd_type(global(_)). | |
| 134 | is_simple_fd_type(integer). | |
| 135 | is_simple_fd_type(boolean). | |
| 136 | ||
| 137 | is_fd_type(couple(A,B)) :- !, is_fd_type(A), is_fd_type(B). | |
| 138 | is_fd_type(record(F)) :- !, is_fd_field_types(F). | |
| 139 | is_fd_type(X) :- is_simple_fd_type(X). | |
| 140 | ||
| 141 | is_fd_field_types([]). | |
| 142 | is_fd_field_types([field(_,FT)|T]) :- is_fd_type(FT), is_fd_field_types(T). | |
| 143 | ||
| 144 | :- use_module(b_global_sets,[get_global_type_value/3]). | |
| 145 | get_fd_type(couple(A,B),(VA,VB)) --> get_fd_type(A,VA), get_fd_type(B,VB). | |
| 146 | get_fd_type(global(T),FD) --> {get_global_type_value(FD,T,X)}, [X]. | |
| 147 | get_fd_type(integer,int(X)) --> [X]. | |
| 148 | get_fd_type(boolean,B) --> [FD], {prop_01(B,FD)}. | |
| 149 | get_fd_type(record(Fields),rec(VF)) --> get_field_fd_types(Fields,VF). | |
| 150 | ||
| 151 | get_field_fd_types([],[]) --> []. | |
| 152 | get_field_fd_types([field(Name,Type)|FT],[field(Name,VF)|VT]) --> | |
| 153 | get_fd_type(Type,VF), | |
| 154 | get_field_fd_types(FT,VT). | |
| 155 | ||
| 156 | get_fd_types(Domain,Range,(VD,VR),FDDom,FDRList) :- get_fd_type(Domain,VD,[FDDom],[]), get_fd_type(Range,VR,FDRList,[]). | |
| 157 | ||
| 158 | % Examples: | |
| 159 | % f = {x|->2, y|->3} & x:1..2 & y:4..5 & r = f(4) | |
| 160 | % f = {x|->(2,x+1), y|->(3,y+1)} & x:1..2 & y:4..5 & r = f(v) & v:3..4 --> deterministically sets v=4, r=(3,5),y=4 | |
| 161 | % from the SICStus manual: | |
| 162 | % element(?X,+List,?Y) | |
| 163 | % where X and Y are domain variables and List is a list of domain variables. True | |
| 164 | % if the X:th element of List is Y. Operationally, the domains of X and Y are | |
| 165 | % constrained so that for every element in the domain of X, there is a compatible | |
| 166 | % element in the domain of Y, and vice versa. | |
| 167 | % Maintains domain consistency in X and bounds consistency in List and Y. | |
| 168 | % Corresponds to nth1/3 in library(lists) and to element in MiniZinc | |
| 169 | ||
| 170 | :- use_module(library(clpfd),[all_distinct/1]). | |
| 171 | :- use_module(library(lists),[nth1/3]). | |
| 172 | check_apply_with_element_constraint(List,X,Y,FunctionType,WF) :- | |
| 173 | is_set_type(FunctionType,couple(Domain,Range)), | |
| 174 | get_fd_type(Domain,X,[FDX],[]), | |
| 175 | if(l_get_fd_types(List,DomainList,RangeLists,Domain,Range,FDX,FoundY),true, | |
| 176 | (add_internal_error('Get FD Types failed: ',get_fd_types(Domain,Range)),fail)), | |
| 177 | debug_println(4,element_domain_list(FDX,DomainList)), | |
| 178 | (FoundY \== y_not_found | |
| 179 | -> FoundY=Y % no need for equal_object: we only have FD types + Bool + couples (+ record of them) | |
| 180 | % TODO: check that for records we can also use unification | |
| 181 | ; element(Idx,DomainList,FDX), % no need to call equal_object for X as we have simple fd types | |
| 182 | % DomainList are the elements of the domain of the function | |
| 183 | (nonvar(Idx) | |
| 184 | -> nth1(Idx,List,(X,Y)) %relevant for tests 387, 1579 | |
| 185 | ; all_distinct(DomainList), % ensures that Idx will get bound eventually if we enumerate DomainList and X (if multiple entries in DomainList then Idx would not get bound) | |
| 186 | maplist(get_fd_types(Domain,Range),List,DomainList,RangeLists), | |
| 187 | get_fd_type(Range,Y,FDYList,[]), | |
| 188 | ? | setup_element_range_constraints(FDYList,Idx,RangeLists), |
| 189 | % tools_printing:print_term_summary(element_constraint(FDX,FDYList,Idx,DomainList)),nl, | |
| 190 | % used to call this: add_fd_variables_for_labeling([FDX|FDYList],WF) but not sure if we need to enumerate FDYList | |
| 191 | add_fd_variables_for_labeling([FDX],WF) % FDX can have an infinite domain; e.g., test 1717 | |
| 192 | ) | |
| 193 | ). | |
| 194 | ||
| 195 | % an unfolded version of maplist(get_fd_types(Domain,Range),List,DomainList,RangeLists) | |
| 196 | % we also check if the lookup FD variable occurs in the list; if so we return the Y value in Found | |
| 197 | % relevant for performance, e.g., for NQueens60; we avoid traversing the list a second time | |
| 198 | l_get_fd_types([],[],[],_,_,_,y_not_found). | |
| 199 | l_get_fd_types([Pair|PT],[FDDom|DT],[FDRList|RT],Domain,Range,FDX,FoundY) :- | |
| 200 | get_fd_types(Domain,Range,Pair,FDDom,FDRList), | |
| 201 | (FDX==FDDom -> Pair=(_,FoundY), DT=[],RT=[] | |
| 202 | ; l_get_fd_types(PT,DT,RT,Domain,Range,FDX,FoundY)). | |
| 203 | ||
| 204 | ||
| 205 | setup_element_range_constraints([],_,_). | |
| 206 | setup_element_range_constraints([FDY|YT],Idx,RangeLists) :- | |
| 207 | maplist(get_next_fd,RangeLists,FDYList,RestLists), | |
| 208 | % print(setting_up_range_element_constraint(Idx,FDYList,FDY)),nl, | |
| 209 | ? | element(Idx,FDYList,FDY), |
| 210 | setup_element_range_constraints(YT,Idx,RestLists). | |
| 211 | ||
| 212 | get_next_fd([H|T],H,T). |