this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Christian Schulte <schulte@gecode.org>
5 *
6 * Copyright:
7 * Christian Schulte, 2003
8 *
9 * This file is part of Gecode, the generic constraint
10 * development environment:
11 * http://www.gecode.org
12 *
13 * Permission is hereby granted, free of charge, to any person obtaining
14 * a copy of this software and associated documentation files (the
15 * "Software"), to deal in the Software without restriction, including
16 * without limitation the rights to use, copy, modify, merge, publish,
17 * distribute, sublicense, and/or sell copies of the Software, and to
18 * permit persons to whom the Software is furnished to do so, subject to
19 * the following conditions:
20 *
21 * The above copyright notice and this permission notice shall be
22 * included in all copies or substantial portions of the Software.
23 *
24 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
25 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
26 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
27 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
28 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
29 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
30 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
31 *
32 */
33
34namespace Gecode { namespace Int { namespace Rel {
35
36 /*
37 * Lexical order propagator
38 */
39 template<class VX, class VY>
40 inline
41 LexLqLe<VX,VY>::LexLqLe(Home home,
42 ViewArray<VX>& x0, ViewArray<VY>& y0, bool s)
43 : Propagator(home), x(x0), y(y0), strict(s) {
44 x.subscribe(home, *this, PC_INT_BND);
45 y.subscribe(home, *this, PC_INT_BND);
46 }
47
48 template<class VX, class VY>
49 forceinline
50 LexLqLe<VX,VY>::LexLqLe(Space& home, LexLqLe<VX,VY>& p)
51 : Propagator(home,p), strict(p.strict) {
52 x.update(home,p.x);
53 y.update(home,p.y);
54 }
55
56 template<class VX, class VY>
57 Actor*
58 LexLqLe<VX,VY>::copy(Space& home) {
59 return new (home) LexLqLe<VX,VY>(home,*this);
60 }
61
62 template<class VX, class VY>
63 PropCost
64 LexLqLe<VX,VY>::cost(const Space&, const ModEventDelta&) const {
65 return PropCost::linear(PropCost::LO, x.size());
66 }
67
68 template<class VX, class VY>
69 void
70 LexLqLe<VX,VY>::reschedule(Space& home) {
71 x.reschedule(home,*this,PC_INT_BND);
72 y.reschedule(home,*this,PC_INT_BND);
73 }
74
75 template<class VX, class VY>
76 forceinline size_t
77 LexLqLe<VX,VY>::dispose(Space& home) {
78 assert(!home.failed());
79 x.cancel(home,*this,PC_INT_BND);
80 y.cancel(home,*this,PC_INT_BND);
81 (void) Propagator::dispose(home);
82 return sizeof(*this);
83 }
84
85 template<class VX, class VY>
86 ExecStatus
87 LexLqLe<VX,VY>::propagate(Space& home, const ModEventDelta&) {
88 /*
89 * State 1
90 *
91 */
92 {
93 int i = 0;
94 int n = x.size();
95
96 while ((i < n) && (x[i].min() == y[i].max())) {
97 // case: =, >=
98 GECODE_ME_CHECK(x[i].lq(home,y[i].max()));
99 GECODE_ME_CHECK(y[i].gq(home,x[i].min()));
100 i++;
101 }
102
103 if (i == n) // case: $
104 return strict ? ES_FAILED : home.ES_SUBSUMED(*this);
105
106 // Possible cases left: <, <=, > (yields failure), ?
107 GECODE_ME_CHECK(x[i].lq(home,y[i].max()));
108 GECODE_ME_CHECK(y[i].gq(home,x[i].min()));
109
110 if (x[i].max() < y[i].min()) // case: < (after tell)
111 return home.ES_SUBSUMED(*this);
112
113 // x[i] can never be equal to y[i] (otherwise: >=)
114 assert(!(x[i].assigned() && y[i].assigned() &&
115 x[i].val() == y[i].val()));
116 // Remove all elements between 0...i-1 as they are assigned and equal
117 x.drop_fst(i); y.drop_fst(i);
118 // After this, execution continues at [1]
119 }
120
121 /*
122 * State 2
123 * prefix: (?|<=)
124 *
125 */
126 {
127 int i = 1;
128 int n = x.size();
129
130 while ((i < n) &&
131 (x[i].min() == y[i].max()) &&
132 (x[i].max() == y[i].min())) { // case: =
133 assert(x[i].assigned() && y[i].assigned() &&
134 (x[i].val() == y[i].val()));
135 i++;
136 }
137
138 if (i == n) { // case: $
139 if (strict)
140 goto rewrite_le;
141 else
142 goto rewrite_lq;
143 }
144
145 if (x[i].max() < y[i].min()) // case: <
146 goto rewrite_lq;
147
148 if (x[i].min() > y[i].max()) // case: >
149 goto rewrite_le;
150
151 if (i > 1) {
152 // Remove equal elements [1...i-1], keep element [0]
153 x[i-1]=x[0]; x.drop_fst(i-1);
154 y[i-1]=y[0]; y.drop_fst(i-1);
155 }
156 }
157
158 if (x[1].max() <= y[1].min()) {
159 // case: <= (invariant: not =, <)
160 /*
161 * State 3
162 * prefix: (?|<=),<=
163 *
164 */
165 int i = 2;
166 int n = x.size();
167
168 while ((i < n) && (x[i].max() == y[i].min())) // case: <=, =
169 i++;
170
171 if (i == n) { // case: $
172 if (strict)
173 return ES_FIX;
174 else
175 goto rewrite_lq;
176 }
177
178 if (x[i].max() < y[i].min()) // case: <
179 goto rewrite_lq;
180
181 if (x[i].min() > y[i].max()) { // case: >
182 // Eliminate [i]...[n-1]
183 for (int j=i; j<n; j++) {
184 x[j].cancel(home,*this,PC_INT_BND);
185 y[j].cancel(home,*this,PC_INT_BND);
186 }
187 x.size(i); y.size(i);
188 strict = true;
189 }
190
191 return ES_FIX;
192 }
193
194 if (x[1].min() >= y[1].max()) {
195 // case: >= (invariant: not =, >)
196 /*
197 * State 4
198 * prefix: (?|<=) >=
199 *
200 */
201 int i = 2;
202 int n = x.size();
203
204 while ((i < n) && (x[i].min() == y[i].max()))
205 // case: >=, =
206 i++;
207
208 if (i == n) { // case: $
209 if (strict)
210 goto rewrite_le;
211 else
212 return ES_FIX;
213 }
214
215 if (x[i].min() > y[i].max()) // case: >
216 goto rewrite_le;
217
218 if (x[i].max() < y[i].min()) { // case: <
219 // Eliminate [i]...[n-1]
220 for (int j=i; j<n; j++) {
221 x[j].cancel(home,*this,PC_INT_BND);
222 y[j].cancel(home,*this,PC_INT_BND);
223 }
224 x.size(i); y.size(i);
225 strict = false;
226 }
227
228 return ES_FIX;
229 }
230
231 return ES_FIX;
232
233 rewrite_le:
234 GECODE_REWRITE(*this,(Le<VX,VY>::post(home(*this),x[0],y[0])));
235 rewrite_lq:
236 GECODE_REWRITE(*this,(Lq<VX,VY>::post(home(*this),x[0],y[0])));
237 }
238
239 template<class VX, class VY>
240 ExecStatus
241 LexLqLe<VX,VY>::post(Home home,
242 ViewArray<VX>& x, ViewArray<VY>& y, bool strict) {
243 if (x.size() < y.size()) {
244 y.size(x.size()); strict=false;
245 } else if (x.size() > y.size()) {
246 x.size(y.size()); strict=true;
247 }
248 if (x.size() == 0)
249 return strict ? ES_FAILED : ES_OK;
250 if (x.size() == 1) {
251 if (strict)
252 return Le<VX,VY>::post(home,x[0],y[0]);
253 else
254 return Lq<VX,VY>::post(home,x[0],y[0]);
255 }
256 (void) new (home) LexLqLe<VX,VY>(home,x,y,strict);
257 return ES_OK;
258 }
259
260
261 /*
262 * Lexical disequality propagator
263 */
264 template<class VX, class VY>
265 forceinline
266 LexNq<VX,VY>::LexNq(Home home, ViewArray<VX>& xv, ViewArray<VY>& yv)
267 : Propagator(home),
268 x0(xv[xv.size()-2]), y0(yv[xv.size()-2]),
269 x1(xv[xv.size()-1]), y1(yv[xv.size()-1]),
270 x(xv), y(yv) {
271 int n = x.size();
272 assert(n > 1);
273 assert(n == y.size());
274 x.size(n-2); y.size(n-2);
275 x0.subscribe(home,*this,PC_INT_VAL); y0.subscribe(home,*this,PC_INT_VAL);
276 x1.subscribe(home,*this,PC_INT_VAL); y1.subscribe(home,*this,PC_INT_VAL);
277 }
278
279 template<class VX, class VY>
280 PropCost
281 LexNq<VX,VY>::cost(const Space&, const ModEventDelta&) const {
282 return PropCost::binary(PropCost::HI);
283 }
284
285 template<class VX, class VY>
286 void
287 LexNq<VX,VY>::reschedule(Space& home) {
288 x0.reschedule(home,*this,PC_INT_VAL);
289 y0.reschedule(home,*this,PC_INT_VAL);
290 x1.reschedule(home,*this,PC_INT_VAL);
291 y1.reschedule(home,*this,PC_INT_VAL);
292 }
293
294 template<class VX, class VY>
295 forceinline
296 LexNq<VX,VY>::LexNq(Space& home, LexNq<VX,VY>& p)
297 : Propagator(home,p) {
298 x0.update(home,p.x0); y0.update(home,p.y0);
299 x1.update(home,p.x1); y1.update(home,p.y1);
300 x.update(home,p.x); y.update(home,p.y);
301 }
302
303 template<class VX, class VY>
304 Actor*
305 LexNq<VX,VY>::copy(Space& home) {
306 int n = x.size();
307 if (n > 0) {
308 // Eliminate all equal views and keep one disequal pair
309 for (int i=n; i--; )
310 switch (rtest_eq_bnd(x[i],y[i])) {
311 case RT_TRUE:
312 // Eliminate equal pair
313 n--; x[i]=x[n]; y[i]=y[n];
314 break;
315 case RT_FALSE:
316 // Just keep a single disequal pair
317 n=1; x[0]=x[i]; y[0]=y[i];
318 goto done;
319 case RT_MAYBE:
320 break;
321 default:
322 GECODE_NEVER;
323 }
324 done:
325 x.size(n); y.size(n);
326 }
327 return new (home) LexNq<VX,VY>(home,*this);
328 }
329
330 template<class VX, class VY>
331 inline ExecStatus
332 LexNq<VX,VY>::post(Home home, ViewArray<VX>& x, ViewArray<VY>& y) {
333 if (x.size() != y.size())
334 return ES_OK;
335 int n = x.size();
336 if (n > 0) {
337 // Eliminate all equal views
338 for (int i=n; i--; )
339 switch (rtest_eq_dom(x[i],y[i])) {
340 case RT_TRUE:
341 // Eliminate equal pair
342 n--; x[i]=x[n]; y[i]=y[n];
343 break;
344 case RT_FALSE:
345 return ES_OK;
346 case RT_MAYBE:
347 if (x[i] == y[i]) {
348 // Eliminate equal pair
349 n--; x[i]=x[n]; y[i]=y[n];
350 }
351 break;
352 default:
353 GECODE_NEVER;
354 }
355 x.size(n); y.size(n);
356 }
357 if (n == 0)
358 return ES_FAILED;
359 if (n == 1)
360 return Nq<VX,VY>::post(home,x[0],y[0]);
361 (void) new (home) LexNq<VX,VY>(home,x,y);
362 return ES_OK;
363 }
364
365 template<class VX, class VY>
366 forceinline size_t
367 LexNq<VX,VY>::dispose(Space& home) {
368 x0.cancel(home,*this,PC_INT_VAL); y0.cancel(home,*this,PC_INT_VAL);
369 x1.cancel(home,*this,PC_INT_VAL); y1.cancel(home,*this,PC_INT_VAL);
370 (void) Propagator::dispose(home);
371 return sizeof(*this);
372 }
373
374 template<class VX, class VY>
375 forceinline ExecStatus
376 LexNq<VX,VY>::resubscribe(Space& home,
377 RelTest rt, VX& x0, VY& y0, VX x1, VY y1) {
378 if (rt == RT_TRUE) {
379 assert(x0.assigned() && y0.assigned());
380 assert(x0.val() == y0.val());
381 int n = x.size();
382 for (int i=n; i--; )
383 switch (rtest_eq_dom(x[i],y[i])) {
384 case RT_TRUE:
385 // Eliminate equal pair
386 n--; x[i]=x[n]; y[i]=y[n];
387 break;
388 case RT_FALSE:
389 return home.ES_SUBSUMED(*this);
390 case RT_MAYBE:
391 // Move to x0, y0 and subscribe
392 x0=x[i]; y0=y[i];
393 n--; x[i]=x[n]; y[i]=y[n];
394 x.size(n); y.size(n);
395 x0.subscribe(home,*this,PC_INT_VAL,false);
396 y0.subscribe(home,*this,PC_INT_VAL,false);
397 return ES_FIX;
398 default:
399 GECODE_NEVER;
400 }
401 // No more views to subscribe to left
402 GECODE_REWRITE(*this,(Nq<VX,VY>::post(home(*this),x1,y1)));
403 }
404 return ES_FIX;
405 }
406
407 template<class VX, class VY>
408 ExecStatus
409 LexNq<VX,VY>::propagate(Space& home, const ModEventDelta&) {
410 RelTest rt0 = rtest_eq_dom(x0,y0);
411 if (rt0 == RT_FALSE)
412 return home.ES_SUBSUMED(*this);
413 RelTest rt1 = rtest_eq_dom(x1,y1);
414 if (rt1 == RT_FALSE)
415 return home.ES_SUBSUMED(*this);
416 GECODE_ES_CHECK(resubscribe(home,rt0,x0,y0,x1,y1));
417 GECODE_ES_CHECK(resubscribe(home,rt1,x1,y1,x0,y0));
418 return ES_FIX;
419 }
420
421
422}}}
423
424// STATISTICS: int-prop