this repo has no description
dekker.one
1%%% Inclusion of this file eliminates set variables by converting them into arrays of var bool.
2% AUTHORS
3% Guido Tack <guido.tack@monash.edu>
4% Gleb Belov <gleb.belov@monash.edu>
5%
6
7predicate mzn_reverse_map_var(var set of int: x) = let {
8 array[int] of var bool: b = set2bools(x)
9} in true;
10
11function var set of int: reverse_map(array[int] of var bool: b);
12function set of int: reverse_map(array[int] of bool: b) ::promise_total =
13 { i | i in index_set(b) where b[i] };
14
15array[int] of var bool: set2bools(var set of int: x) ::promise_total =
16 if is_fixed(x) then set2bools(fix(x)) else
17 let {
18 array[int] of var bool: b = array1d( min(ub(x))..max(ub(x)),
19 [ set2bools_bit( x, i ) | i in min(ub(x))..max(ub(x)) ] );
20 constraint (x = reverse_map(b)) :: is_reverse_map;
21 } in b
22 endif;
23array[int] of var bool: set2bools(var set of int: x, set of int: ubx) ::promise_total =
24 if is_fixed(x) then set2bools(fix(x), ubx) else
25 let {
26 array[int] of var bool: b0 = set2bools( x ); %% Call in any case ?? TODO
27 array[int] of var bool: b = array1d( min(ubx)..max(ubx),
28 [ if i in ubx then set2bools_bit( x, i ) else false endif
29 | i in min(ubx)..max(ubx) ] );
30%% Not again: constraint (x = reverse_map(b)) :: is_reverse_map;
31 } in b
32 endif;
33array[int] of bool: set2bools(set of int: x) ::promise_total =
34 array1d(min(x)..max(x),[i in x | i in min(x)..max(x)]);
35array[int] of bool: set2bools(set of int: x, set of int: ubx) ::promise_total =
36 array1d(min(ubx)..max(ubx),[i in x | i in min(ubx)..max(ubx)]);
37function var bool: set2bools_bit( var set of int: x, int: i ) ::promise_total =
38 if i in ub(x) then
39 let {
40 var bool: bi;
41 } in bi
42 else false endif;
43
44
45predicate set_eq(var set of int: x, var set of int: y) ::promise_total =
46 if not has_ub_set(x) /\ not has_ub_set(y) then
47 assert(false, "set_eq: cannot determine bounds of set variables")
48 elseif not has_ub_set(x) then set_eq(y,x)
49 else
50 let {
51 constraint y subset x, %% Constrain domains first
52 constraint x subset y,
53 } in let {
54 array[int] of var bool: bx = set2bools(x);
55 array[int] of var bool: by = set2bools(y);
56 } in forall (i in index_set(bx) union index_set(by)) (
57 if not (i in index_set(bx)) then not by[i] %% Should be impossible
58 elseif not (i in index_set(by)) then not bx[i]
59 else bx[i]=by[i] endif
60 )
61 endif;
62
63predicate set_eq_reif(var set of int: x, var set of int: y, var bool: b) ::promise_total =
64 if is_fixed(b) then
65 if true==fix(b) then x==y else x!=y endif
66 else
67 let {
68 array[int] of var bool: bx = set2bools(x);
69 array[int] of var bool: by = set2bools(y);
70 } in b <-> forall (i in index_set(bx) union index_set(by)) (
71 if not (i in index_set(bx)) then not by[i]
72 elseif not (i in index_set(by)) then not bx[i]
73 else bx[i]=by[i] endif
74 )
75 endif;
76
77predicate set_eq_imp(var set of int: x, var set of int: y, var bool: b) =
78 if is_fixed(b) then
79 if fix(b) then (x = y) else true endif
80 else
81 let {
82 array[int] of var bool: bx = set2bools(x);
83 array[int] of var bool: by = set2bools(y);
84 } in b -> forall (i in index_set(bx) union index_set(by)) (
85 if not (i in index_set(bx)) then not by[i]
86 elseif not (i in index_set(by)) then not bx[i]
87 else bx[i]=by[i] endif
88 )
89 endif;
90
91 predicate set_ne(var set of int: x, var set of int: y) ::promise_total =
92 let {
93 array[int] of var bool: bx = set2bools(x);
94 array[int] of var bool: by = set2bools(y);
95 } in exists (i in index_set(bx) union index_set(by)) (
96 if not (i in index_set(bx)) then by[i]
97 elseif not (i in index_set(by)) then bx[i]
98 else bx[i]!=by[i] endif
99 );
100
101predicate set_ne_reif(var set of int: x, var set of int: y, var bool: b) ::promise_total =
102 set_eq_reif( x, y, not b );
103
104predicate set_ne_imp(var set of int: x, var set of int: y, var bool: b) =
105 if is_fixed(b) then
106 if fix(b) then (x != y) else true endif
107 else
108 let {
109 array[int] of var bool: bx = set2bools(x);
110 array[int] of var bool: by = set2bools(y);
111 } in b -> exists (i in index_set(bx) union index_set(by)) (
112 if not (i in index_set(bx)) then by[i]
113 elseif not (i in index_set(by)) then bx[i]
114 else (bx[i] != by[i]) endif
115 )
116 endif;
117
118% Set comparisons are often used just to avoid symmetries.
119% Reifs/imps are done automatically from these templates
120predicate set_le(var set of int: x, var set of int: y) ::promise_total =
121 let {
122 set of int: U = ub(x) union ub(y);
123 int: l = min(U);
124 int: u = max(U);
125 array[U] of var bool: xb = [i in x | i in U];
126 var l-1..u: xmax = max(x union {l-1});
127 array[U] of var bool: yb = [i in y | i in U];
128 var l-1..u: ymax = max(y union {l-1});
129 array[U] of var bool: b;
130 constraint forall(i in l..u-1) (
131 b[i] = let {var 1..4: cmp = 2*xb[i] + yb[i] + 1} in
132 [b[i+1], xmax < i, ymax > i, b[i+1]][cmp]
133 );
134 constraint b[u] = (xb[u] -> yb[u]);
135 } in b[l];
136
137predicate set_lt(var set of int: x, var set of int: y) ::promise_total =
138 let {
139 set of int: U = ub(x) union ub(y);
140 int: l = min(U);
141 int: u = max(U);
142 array[U] of var bool: xb = [i in x | i in U];
143 var l-1..u: xmax = max(x union {l-1});
144 array[U] of var bool: yb = [i in y | i in U];
145 var l-1..u: ymax = max(y union {l-1});
146 array[U] of var bool: b;
147 constraint forall(i in l..u-1) (
148 b[i] = let {var 1..4: cmp = 2*xb[i] + yb[i] + 1} in
149 [b[i+1], xmax < i, ymax > i, b[i+1]][cmp]
150 );
151 constraint b[u] = (not xb[u] /\ yb[u]);
152 } in b[l];
153
154predicate set_subset(var set of int: x, var set of int: y) ::promise_total =
155 let {
156 array[int] of var bool: bx = set2bools(x);
157 array[int] of var bool: by = set2bools(y);
158 } in forall (i in index_set(bx)) (
159 if not (i in index_set(by)) then not bx[i]
160 else bx[i] -> by[i] endif
161 );
162
163predicate set_subset_reif(var set of int: x, var set of int: y, var bool: b) ::promise_total =
164 let {
165 array[int] of var bool: bx = set2bools(x);
166 array[int] of var bool: by = set2bools(y);
167 } in b <-> forall (i in index_set(bx)) (
168 if not (i in index_set(by)) then not bx[i]
169 else bx[i] -> by[i] endif
170 );
171
172predicate set_subset_imp(var set of int: x, var set of int: y, var bool: b) =
173 let {
174 array[int] of var bool: bx = set2bools(x);
175 array[int] of var bool: by = set2bools(y);
176 } in b -> forall (i in index_set(bx)) (
177 if not (i in index_set(by)) then not bx[i]
178 else bx[i] -> by[i] endif
179 );
180
181%%% Map the subset operation to superset
182predicate set_superset(var set of int: x, var set of int: y) ::promise_total = set_subset( y, x );
183predicate set_superset_reif(var set of int: x, var set of int: y, var bool: b) ::promise_total =
184 set_subset_reif( y, x, b );
185predicate set_superset_imp(var set of int: x, var set of int: y, var bool: b) =
186 set_subset_imp(y,x,b);
187
188function var set of int: set_intersect(var set of int: x, var set of int: y) ::promise_total =
189 let {
190 array[int] of var bool: bx = set2bools(x);
191 array[int] of var bool: by = set2bools(y);
192 var set of (index_set(bx) intersect index_set(by)): z;
193 array[int] of var bool: bz = set2bools(z);
194 constraint forall (i in index_set(bz)) (
195 bz[i] = (bx[i] /\ by[i])
196 );
197 } in z;
198
199function var set of int: set_union(var set of int: x, var set of int: y) ::promise_total =
200 let {
201 array[int] of var bool: bx = set2bools(x);
202 array[int] of var bool: by = set2bools(y);
203 var set of (index_set(bx) union index_set(by)): z;
204 array[int] of var bool: bz = set2bools(z);
205 constraint forall (i in index_set(bx) union index_set(by)) (
206 if (i in index_set(bx)) then
207 if (i in index_set(by)) then
208 bz[i] = (bx[i] \/ by[i])
209 else
210 bz[i] = bx[i]
211 endif
212 else
213 bz[i] = by[i]
214 endif
215 );
216 } in z;
217
218function var set of int: set_diff(var set of int: x, var set of int: y) ::promise_total =
219 let {
220 array[int] of var bool: bx = set2bools(x);
221 array[int] of var bool: by = set2bools(y);
222 var set of ub(x) diff lb(y): z;
223 array[int] of var bool: bz = set2bools(z);
224 constraint forall (i in ub(z)) (
225 bz[i] = (bx[i] /\ (not by[i]))
226 );
227 } in z;
228
229function var set of int: set_symdiff(var set of int: x, var set of int: y) ::promise_total =
230 let {
231 array[int] of var bool: bx = set2bools(x);
232 array[int] of var bool: by = set2bools(y);
233 var set of (ub(x) diff lb(y)) union (ub(y) diff lb(x)): z;
234 array[int] of var bool: bz = set2bools(z);
235 constraint forall (i in ub(z)) (
236 bz[i] = (bx[i] xor by[i])
237 );
238 } in z;
239
240function var int: card(var set of int: x) ::promise_total =
241 let {
242 array[int] of var bool: bx = set2bools(x);
243 var 0..length(bx) : c;
244 constraint bool_lin_eq([1 | i in index_set(bx)],[bx[i] | i in index_set(bx)],c);
245 } in c;
246
247predicate set_in(int: x, var set of int: y) ::promise_total =
248 let {
249 array[int] of var bool: by = set2bools(y);
250 } in by[x];
251predicate set_in(var int: x, var set of int: y) ::promise_total =
252 let {
253 array[int] of var bool: by = set2bools(y);
254 } in by[x];
255
256predicate set_in_reif(int: x, var set of int: y, var bool: b) ::promise_total =
257 if x in ub(y) then
258 b <-> set2bools(y)[x]
259 else
260 not b
261 endif;
262predicate set_in_reif(var int: x, var set of int: y, var bool: b) ::promise_total =
263 b <-> set2bools(y)[x];
264predicate set_in_imp(var int: x, var set of int: y, var bool: b) =
265 b -> set2bools(y)[x];
266
267function array[int] of var bool: setarray2bools(array[int] of var set of int: x) =
268 if length(x)=0 then [] else
269 set2bools(x[1])++setarray2bools([x[i]|i in 2..length(x)])
270 endif;
271%% Par version no sense
272
273
274predicate array_var_set_element(var int: x, array[int] of var set of int: y, var set of int: z) ::promise_total =
275 let {
276 constraint x in { i | i in index_set( y ) where
277 lb(y[i]) subset ub(z) /\ lb(z) subset ub(y[i])
278 };
279 set of int: sUB = array_union( [ ub(y[i]) | i in dom(x) ] );
280 set of int: sLB = array_intersect( [ lb(y[i]) | i in dom(x) ] );
281 constraint z subset sUB,
282 constraint sLB subset z,
283 } in
284 forall (k in ub(z)) (
285 set2bools(z)[k] ==
286 if k in sUB then
287 if k in sLB then
288 true
289 else
290 array1d( lb(x)..ub(x),
291 [ if k in ub(y[i]) then set2bools(y[i])[k] else false endif | i in dom(x) ] )[x]
292 endif
293 else
294 false
295 endif
296 ) /\
297 forall (k in sUB diff ub(z))(
298 if k in sLB then
299 false %% fail the constraint
300 else
301 not array1d( lb(x)..ub(x),
302 [ if k in ub(y[i]) then set2bools(y[i])[k] else false endif | i in dom(x) ] )[x]
303 endif
304 );
305
306predicate array_set_element(var int: x, array[int] of set of int: y, var set of int: z) ::promise_total =
307 let {
308 constraint x in { i | i in index_set( y ) where
309 y[i] subset ub(z) /\ lb(z) subset y[i]
310 };
311 set of int: sUB = array_union( [ y[i] | i in dom(x) ] );
312 set of int: sLB = array_intersect( [ y[i] | i in dom(x) ] );
313 constraint z subset sUB,
314 constraint sLB subset z,
315 } in
316 forall (k in ub(z)) (
317 set2bools(z)[k] ==
318 if k in sUB then
319 if k in sLB then
320 true
321 else
322 array1d( lb(x)..ub(x),
323 [ if k in ub(y[i]) then set2bools(y[i])[k] else false endif | i in dom(x) ] )[x]
324 endif
325 else
326 false
327 endif
328 ) /\
329 forall (k in sUB diff ub(z))(
330 if k in sLB then
331 false %% fail the constraint
332 else
333 not array1d( lb(x)..ub(x),
334 [ if k in ub(y[i]) then set2bools(y[i])[k] else false endif | i in dom(x) ] )[x]
335 endif
336 );
337
338annotation set_search(array[$X] of var set of int: x, ann: a1, ann: a2, ann: a3) =
339 let { array[int] of var set of int: xx = array1d(x) } in
340 seq_search( [ bool_search(set2bools(xx[i]),a1,a2,a3) | i in index_set(xx) ] );
341
342annotation warm_start( array[int] of var set of int: x, array[int] of set of int: v ) =
343 warm_start_array( [
344 let {
345 array[int] of var bool: xb = set2bools(x[i]),
346 set of int: is_var = ub(x[i]) diff lb(x[i]),
347 int: iV = i - min(index_set(x)) + if 0<length(v) then min(index_set(v)) else 0 endif,
348 } in
349 warm_start( [ xb[k] | k in is_var ],
350 if iV in index_set(v) then [ k in v[iV] | k in is_var ] else [] endif )
351 | i in index_set(x) ] ); %% ignoring v[i] diff ub(x[i]) and lb(x[i]) diff v[i]
352