this repo has no description
dekker.one
1include "fzn_geost.mzn";
2include "fzn_geost_reif.mzn";
3include "fzn_geost_bb.mzn";
4include "fzn_geost_bb_reif.mzn";
5include "fzn_geost_smallest_bb.mzn";
6include "fzn_geost_smallest_bb_reif.mzn";
7include "fzn_geost_nonoverlap_k.mzn";
8include "fzn_geost_nonoverlap_k_reif.mzn";
9
10/** @group globals.packing
11 A global non-overlap constraint for \a k dimensional objects. It enforces that no two objects overlap.
12
13@param k: the number of dimensions
14@param rect_size: the size of each box in \a k dimensios
15@param rect_offset: the offset of each box from the base position in \a k dimensions
16
17@param shape: the set of rectangles defining the \p i-th shape.
18
19@param x: the base position of each object. \a x[\p i,\p j] is the position of object \p i in. dimension \p j.
20@param kind: the shape used by each object.
21*/
22
23predicate geost(
24 int : k ,
25 array[int,int] of int : rect_size ,
26 array[int,int] of int : rect_offset ,
27 array[int ] of set of int : shape ,
28 array[int,int] of var int : x ,
29 array[int ] of var int : kind
30) =
31 assert(
32 % Some sanity checks
33 index_set_1of2( rect_size ) = index_set_1of2(rect_offset) /\
34 index_set_2of2( rect_size ) = 1..k /\
35 index_set_2of2( rect_offset ) = 1..k /\
36 index_set( shape ) = 1..length(shape) /\
37 index_set_1of2( x ) = index_set(kind) /\
38 index_set_2of2( x ) = 1..k /\
39 forall(i in index_set(shape))(
40 shape[i] subset index_set_1of2(rect_size)
41 ),
42 % Error message
43 "geost: index sets of arguments are incorrect",
44 assert(
45 % More sanity checks
46 forall(i in index_set(shape))(card(shape[i]) > 0),
47 % Error message
48 "geost: sets in shape must be non-empty",
49
50 fzn_geost(k, rect_size, rect_offset, shape, x, kind)
51 )); % End assert statements
52
53
54/** @group globals.packing
55 A global non-overlap constraint for \a k dimensional objects. It enforces that no two objects overlap, and that all objects fit within a global \a k dimensional bounding box.
56
57@param k: the number of dimensions
58@param rect_size: the size of each box in \a k dimensios
59@param rect_offset: the offset of each box from the base position in \a k dimensions
60
61@param shape: the set of rectangles defining the \p i-th shape.
62
63@param x: the base position of each object. \a x[\p i,\p j] is the position of object \p i in dimension \p j.
64@param kind: the shape used by each object.
65
66@param l: is an array of lower bounds, \a l[\p i] is the minimum bounding box for all objects in dimension \p i.
67@param u: is an array of upper bounds, \a u[\p i] is the maximum bounding box for all objects in dimension \p i.
68*/
69
70predicate geost_bb(
71 int : k ,
72 array[int,int] of int : rect_size ,
73 array[int,int] of int : rect_offset ,
74 array[int ] of set of int : shape ,
75 array[int,int] of var int : x ,
76 array[int ] of var int : kind ,
77 array[int ] of var int : l ,
78 array[int ] of var int : u
79) =
80 assert(
81 % Some sanity checks
82 index_set_1of2( rect_size ) = index_set_1of2(rect_offset) /\
83 index_set_2of2( rect_size ) = 1..k /\
84 index_set_2of2( rect_offset ) = 1..k /\
85 index_set( shape ) = 1..length(shape) /\
86 index_set_1of2( x ) = index_set(kind) /\
87 index_set_2of2( x ) = 1..k /\
88 forall(i in index_set(shape))(
89 shape[i] subset index_set_1of2(rect_size)
90 ),
91 % Error message
92 "geost_bb: index sets of arguments are incorrect",
93 assert(
94 % More sanity checks
95 forall(i in index_set(shape))(card(shape[i]) > 0),
96 % Error message
97 "geost_bb: sets in shape must be non-empty",
98
99 assert(
100 % Sanity check
101 index_set(l) = 1..k /\ index_set(u) = 1..k,
102 % Error message
103 "geost_bb: index set of bounds arrays is not 1.." ++ show(k),
104 % Posting the geost constraint
105 fzn_geost_bb(k, rect_size, rect_offset, shape, x, kind, l, u)
106 )));
107
108/** @group globals.packing
109 A global non-overlap constraint for \a k dimensional objects. It enforces that no two objects overlap, and that all objects fit within a global \a k dimensional bounding box. In addition, it enforces that the bounding box is the smallest one containing all objects, i.e., each of the \a 2k boundaries is touched by at least by one object.
110
111@param k: the number of dimensions
112@param rect_size: the size of each box in \a k dimensios
113@param rect_offset: the offset of each box from the base position in \a k dimensions
114
115@param shape: the set of rectangles defining the \p i-th shape.
116
117@param x: the base position of each object. \a x[\p i,\p j] is the position of object \p i in dimension \p j.
118@param kind: the shape used by each object.
119
120@param l: is an array of lower bounds, \a l[\p i] is the minimum bounding box for all objects in dimension \p i.
121@param u: is an array of upper bounds, \a u[\p i] is the maximum bounding box for all objects in dimension \p i.
122*/
123
124predicate geost_smallest_bb(
125 int : k ,
126 array[int,int] of int : rect_size ,
127 array[int,int] of int : rect_offset ,
128 array[int ] of set of int : shape ,
129 array[int,int] of var int : x ,
130 array[int ] of var int : kind ,
131 array[int ] of var int : l ,
132 array[int ] of var int : u
133) =
134 assert(
135 % Some sanity checks
136 index_set_1of2( rect_size ) = index_set_1of2(rect_offset) /\
137 index_set_2of2( rect_size ) = 1..k /\
138 index_set_2of2( rect_offset ) = 1..k /\
139 index_set( shape ) = 1..length(shape) /\
140 index_set_1of2( x ) = index_set(kind) /\
141 index_set_2of2( x ) = 1..k /\
142 forall(i in index_set(shape))(
143 shape[i] subset index_set_1of2(rect_size)
144 ),
145 % Error message
146 "geost_bb: index sets of arguments are incorrect",
147 assert(
148 % More sanity checks
149 forall(i in index_set(shape))(card(shape[i]) > 0),
150 % Error message
151 "geost_bb: sets in shape must be non-empty",
152
153 % A few useful definitions
154 let {
155 set of int: DIMS = 1..k;
156 set of int: SHAPES = 1..length(shape);
157 set of int: OBJECTS = index_set(kind);
158 } in
159 % Two useful definitions
160 let {
161 set of int: DIMS = 1..k;
162 set of int: OBJECTS = index_set(kind);
163 } in (
164 assert(
165 % Sanity check
166 index_set(l) = 1..k /\ index_set(u) = 1..k,
167 % Error message
168 "geost_bb: index set of bounds arrays is not 1.." ++ show(k),
169 % Posting the geost constraint
170 fzn_geost_smallest_bb(k, rect_size, rect_offset, shape, x, kind, l, u)
171 ))));
172
173/** @group globals.packing
174 A global non-overlap constraint for \a 2 dimensional objects. It enforces that no two objects overlap
175 and zero-length objects do not appear in the middle of other objects.
176
177@param x1: first coordinate of each object
178@param w2: width in first dimension for each object
179@param x2: second coordinate of each object
180@param w2: width in second dimension for each object
181*/
182predicate geost_nonoverlap_k(
183 array[int] of var int : x1,
184 array[int] of int : w1,
185 array[int] of var int : x2,
186 array[int] of int : w2
187) =
188 assert(
189 % Some sanity checks
190 index_set( x1 ) = index_set( w1 ) /\
191 index_set( x1 ) = index_set( x2 ) /\
192 index_set( x1 ) = index_set( w2 ),
193 % Error message
194 "geost_nonoverlap_k: index sets of arguments do not match",
195 % Non-overlap constraint
196 fzn_geost_nonoverlap_k(x1,w1,x2,w2)
197 );
198
199test geost_nonoverlap_k(
200 array[int] of int: x1,
201 array[int] of int: w1,
202 array[int] of int: x2,
203 array[int] of int: w2
204) =
205 assert(
206 % Some sanity checks
207 index_set( x1 ) = index_set( w1 ) /\
208 index_set( x1 ) = index_set( x2 ) /\
209 index_set( x1 ) = index_set( w2 ),
210 % Error message
211 "geost_nonoverlap_k: index sets of arguments do not match",
212 % Non-overlap test
213 exists(j in index_set(x1))(
214 x1[j] + w1[j] <= x2[j] \/ x2[j] + w2[j] <= x1[j]
215 )
216 );
217