1 | % (c) 2016-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_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 | maplist(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 (but with multiple FD values in an element; even that will not guarantee that there are no overflows) | |
34 | %(ElVList = [_,_|_] -> true ; print(Element),nl,fail,trace,true), | |
35 | SkeletonType \= boolean. % should we also disallow rec([field(_,boolean)]) % boolean treatment causes problems for 1624, 1627, 140, 1426 | |
36 | ||
37 | :- use_module(tools,[is_tagged_integer/1]). | |
38 | no_overflow(H) :- (var(H) -> true ; is_tagged_integer(H)). | |
39 | ||
40 | translate_avl_to_table(AVL,TableList) :- | |
41 | avl_domain(AVL,List), | |
42 | maplist(translate_avl_element_to_fd_list,List,TableList). | |
43 | ||
44 | check_element_of_avl_with_table(X,SkeletonType,AVL,WF) :- | |
45 | translate_avl_to_table(AVL,TableList), | |
46 | check_element_of_table(X,SkeletonType,TableList,WF). | |
47 | ||
48 | check_element_of_table(X,SkeletonType,TableList,WF) :- | |
49 | translate_to_fd_values(X,SkeletonType,XList,[]), | |
50 | clpfd_in_table(XList,TableList), | |
51 | add_fd_variables_for_labeling(XList,WF). | |
52 | ||
53 | :- use_module(clpfd_interface,[clpfd_inlist/2]). | |
54 | get_unique_el([X],X). | |
55 | clpfd_in_table([X],TableList) :- !, maplist(get_unique_el,TableList,FDList), | |
56 | %print(posting_clpfd_inlist(X,FDList)),nl, | |
57 | clpfd_inlist(X,FDList). | |
58 | clpfd_in_table(XList,TableList) :- | |
59 | %print(posting_clpfd_table([XList],TableList)),nl, | |
60 | clpfd:table([XList],TableList). % we could provide optional third argument, e.g., [order(id3)] | |
61 | % from the SICStus Manual: | |
62 | % table(+Tuples,+Extension,+Options) | |
63 | % Defines an n-ary constraint by extension. Extension should be a list of lists of | |
64 | % integers, each of length n. Tuples should be a list of lists of domain variables, | |
65 | % each also of length n. The constraint holds if every Tuple in Tuples occurs in | |
66 | % the Extension. The constraint will maintain domain consistency. | |
67 | % For convenience, Extension may contain ConstantRange (see Section 10.10.13.1 | |
68 | % [Syntax of Indexicals], page 485) expressions in addition to integers. | |
69 | ||
70 | % TO DO: also allow partial FD infos, in which case we would use table/2 just for quick propagation | |
71 | % we could also translate variables into ConstantRange expressions (see above) | |
72 | translate_avl_element_to_fd_list(Val,FDList) :- translate_to_fd_values(Val,_,FDList,[]). | |
73 | ||
74 | translate_to_fd_values(FD,fd(T)) --> {var(FD),nonvar(T)},!, % setup FD bounds | |
75 | {get_global_type_value(FD,T,X)},[X]. | |
76 | translate_to_fd_values(fd(X,T),fd(T)) --> !, [X]. | |
77 | translate_to_fd_values(int(A),integer) --> !, [A]. % warning: could overflow, we check above ! | |
78 | translate_to_fd_values((A,B),(SkelA,SkelB)) --> !, translate_to_fd_values(A,SkelA), translate_to_fd_values(B,SkelB). | |
79 | translate_to_fd_values(rec(F),rec(SkelF)) --> !, l_translate_to_fd_values(F,SkelF). | |
80 | translate_to_fd_values(Var,Type) --> {var(Var),Type==boolean},!, {prop_01(Var,FD)},[FD]. | |
81 | translate_to_fd_values(pred_true,boolean) --> [1]. | |
82 | translate_to_fd_values(pred_false,boolean) --> [0]. | |
83 | % TO DO: also free-types | |
84 | ||
85 | l_translate_to_fd_values([],[]) --> []. | |
86 | l_translate_to_fd_values([field(N,F)|T],[field(N,SF)|ST]) --> | |
87 | translate_to_fd_values(F,SF),l_translate_to_fd_values(T,ST). | |
88 | ||
89 | :- block prop_01(-,-). | |
90 | prop_01(pred_true,1). | |
91 | prop_01(pred_false,0). | |
92 | ||
93 | % ---------------------- | |
94 | ||
95 | :- use_module(bsyntaxtree,[is_set_type/2]). | |
96 | :- use_module(preferences,[preference/2]). | |
97 | ||
98 | % can a list be translated into CLPFD element constraints for function application | |
99 | can_translate_function_to_element_constraint(List,FunctionType) :- | |
100 | FunctionType \= unknown, | |
101 | is_list_skeleton(List), % TO DO: allow tail AVL list + enable delaying treatment | |
102 | preference(find_abort_values,false), | |
103 | preference(use_chr_solver,false), % avoid falling into the SICStus element/3 bug prior to 4.3.6; TO DO: remove later | |
104 | is_set_type(FunctionType,couple(Domain,Range)), | |
105 | is_simple_fd_type(Domain), % Domain must be translatable to simple FD value list | |
106 | is_fd_type(Range). | |
107 | ||
108 | is_list_skeleton(X) :- nonvar(X),is_list_skeleton_aux(X). | |
109 | is_list_skeleton_aux([]). | |
110 | is_list_skeleton_aux([_H|T]) :- is_list_skeleton(T). | |
111 | ||
112 | is_simple_fd_type(global(_)). | |
113 | is_simple_fd_type(integer). | |
114 | is_simple_fd_type(boolean). | |
115 | ||
116 | is_fd_type(couple(A,B)) :- !, is_fd_type(A), is_fd_type(B). | |
117 | is_fd_type(record(F)) :- !, is_fd_field_types(F). | |
118 | is_fd_type(X) :- is_simple_fd_type(X). | |
119 | ||
120 | is_fd_field_types([]). | |
121 | is_fd_field_types([field(_,FT)|T]) :- is_fd_type(FT), is_fd_field_types(T). | |
122 | ||
123 | :- use_module(b_global_sets,[get_global_type_value/3]). | |
124 | get_fd_type(couple(A,B),(VA,VB)) --> get_fd_type(A,VA), get_fd_type(B,VB). | |
125 | get_fd_type(global(T),FD) --> {get_global_type_value(FD,T,X)}, [X]. | |
126 | get_fd_type(integer,int(X)) --> [X]. | |
127 | get_fd_type(boolean,B) --> [FD], {prop_01(B,FD)}. | |
128 | get_fd_type(record(Fields),rec(VF)) --> get_field_fd_types(Fields,VF). | |
129 | ||
130 | get_field_fd_types([],[]) --> []. | |
131 | get_field_fd_types([field(Name,Type)|FT],[field(Name,VF)|VT]) --> | |
132 | get_fd_type(Type,VF), | |
133 | get_field_fd_types(FT,VT). | |
134 | ||
135 | get_fd_types(Domain,Range,(VD,VR),FDDom,FDRList) :- get_fd_type(Domain,VD,[FDDom],[]), get_fd_type(Range,VR,FDRList,[]). | |
136 | ||
137 | % Examples: | |
138 | % f = {x|->2, y|->3} & x:1..2 & y:4..5 & r = f(4) | |
139 | % 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 | |
140 | % from the SICStus manual: | |
141 | % element(?X,+List,?Y) | |
142 | % where X and Y are domain variables and List is a list of domain variables. True | |
143 | % if the X:th element of List is Y. Operationally, the domains of X and Y are | |
144 | % constrained so that for every element in the domain of X, there is a compatible | |
145 | % element in the domain of Y, and vice versa. | |
146 | % Maintains domain consistency in X and bounds consistency in List and Y. | |
147 | ||
148 | :- use_module(library(clpfd),[all_distinct/1]). | |
149 | :- use_module(library(lists),[nth1/3]). | |
150 | check_apply_with_element_constraint(List,X,Y,FunctionType,WF) :- | |
151 | is_set_type(FunctionType,couple(Domain,Range)), | |
152 | get_fd_type(Domain,X,[FDX],[]), | |
153 | if(l_get_fd_types(List,DomainList,RangeLists,Domain,Range,FDX,FoundY),true, | |
154 | (add_internal_error('Get FD Types failed: ',get_fd_types(Domain,Range)),fail)), | |
155 | debug_println(4,element_domain_list(FDX,DomainList)), | |
156 | %print(element_domain_list(FDX,DomainList,FoundY)),nl, | |
157 | (FoundY \== y_not_found | |
158 | -> FoundY=Y % no need for equal_object: we only have FD types + Bool + couples | |
159 | ; element(Idx,DomainList,FDX), % no need to call equal_object for X as we have simple fd types | |
160 | (nonvar(Idx) | |
161 | -> nth1(Idx,List,(X,Y)) %relevant for tests 387, 1579 | |
162 | ; 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) | |
163 | maplist(get_fd_types(Domain,Range),List,DomainList,RangeLists), | |
164 | get_fd_type(Range,Y,FDYList,[]), | |
165 | setup_element_domain_constraints(FDYList,Idx,RangeLists), | |
166 | add_fd_variables_for_labeling([FDX|FDYList],WF) | |
167 | ) | |
168 | ). | |
169 | ||
170 | % an unfolded version of maplist(get_fd_types(Domain,Range),List,DomainList,RangeLists) | |
171 | % we also check if the lookup FD variable occurs in the list; if so we return the Y value in Found | |
172 | % relevant for performance, e.g., for NQueens60; we avoid traversing the list a second time | |
173 | l_get_fd_types([],[],[],_,_,_,y_not_found). | |
174 | l_get_fd_types([Pair|PT],[FDDom|DT],[FDRList|RT],Domain,Range,FDX,FoundY) :- | |
175 | get_fd_types(Domain,Range,Pair,FDDom,FDRList), | |
176 | (FDX==FDDom -> Pair=(_,FoundY), DT=[],RT=[] | |
177 | ; l_get_fd_types(PT,DT,RT,Domain,Range,FDX,FoundY)). | |
178 | ||
179 | ||
180 | setup_element_domain_constraints([],_,_). | |
181 | setup_element_domain_constraints([FDY|YT],Idx,RangeLists) :- | |
182 | maplist(get_next_fd,RangeLists,FDYList,RestLists), | |
183 | %print(setting_up_range_element_constraint(Idx,FDYList,FDY)),nl, | |
184 | element(Idx,FDYList,FDY), | |
185 | setup_element_domain_constraints(YT,Idx,RestLists). | |
186 | ||
187 | get_next_fd([H|T],H,T). |