this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Guido Tack <tack@gecode.org>
5 * Christian Schulte <schulte@gecode.org>
6 * Gabor Szokoli <szokoli@gecode.org>
7 * Denys Duchier <denys.duchier@univ-orleans.fr>
8 *
9 * Copyright:
10 * Guido Tack, 2004
11 * Christian Schulte, 2004
12 * Gabor Szokoli, 2004
13 *
14 * This file is part of Gecode, the generic constraint
15 * development environment:
16 * http://www.gecode.org
17 *
18 * Permission is hereby granted, free of charge, to any person obtaining
19 * a copy of this software and associated documentation files (the
20 * "Software"), to deal in the Software without restriction, including
21 * without limitation the rights to use, copy, modify, merge, publish,
22 * distribute, sublicense, and/or sell copies of the Software, and to
23 * permit persons to whom the Software is furnished to do so, subject to
24 * the following conditions:
25 *
26 * The above copyright notice and this permission notice shall be
27 * included in all copies or substantial portions of the Software.
28 *
29 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
30 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
31 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
32 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
33 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
34 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
35 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
36 *
37 */
38
39
40
41#include <gecode/set.hh>
42#include <gecode/int.hh>
43
44namespace Gecode { namespace Set { namespace Int {
45
46 template<class View>
47 forceinline
48 MinElement<View>::MinElement(Home home, View y0, Gecode::Int::IntView y1)
49 : MixBinaryPropagator<View,PC_SET_ANY,Gecode::Int::IntView,Gecode::Int::PC_INT_BND> (home, y0, y1) {}
50
51 template<class View>
52 forceinline ExecStatus
53 MinElement<View>::post(Home home, View x0, Gecode::Int::IntView x1) {
54 GECODE_ME_CHECK(x0.cardMin(home,1));
55 (void) new (home) MinElement(home,x0,x1);
56 return ES_OK;
57 }
58
59 template<class View>
60 forceinline
61 MinElement<View>::MinElement(Space& home, MinElement& p)
62 : MixBinaryPropagator<View,PC_SET_ANY,Gecode::Int::IntView,Gecode::Int::PC_INT_BND> (home, p) {}
63
64 template<class View>
65 Actor*
66 MinElement<View>::copy(Space& home) {
67 return new (home) MinElement(home,*this);
68 }
69
70 template<class View>
71 ExecStatus
72 MinElement<View>::propagate(Space& home, const ModEventDelta&) {
73 //x1 is an element of x0.ub
74 //x1 =< smallest element of x0.lb
75 //x1 =< x0.cardinialityMin-est largest element of x0.ub
76 //(these 2 take care of determined x0)
77 //No element in x0 is smaller than x1
78 //if x1 is determined, it is part of the ub.
79
80 //Consequently:
81 //The domain of x1 is a subset of x0.ub up to the first element in x0.lb.
82 //x0 lacks everything smaller than smallest possible x1.
83
84 {
85 LubRanges<View> ub(x0);
86 GECODE_ME_CHECK(x1.inter_r(home,ub,false));
87 }
88 GECODE_ME_CHECK(x1.lq(home,x0.glbMin()));
89 //if cardMin>lbSize?
90 assert(x0.cardMin()>=1);
91
92 {
93 /// Compute n-th largest element in x0.lub for n = x0.cardMin()-1
94 unsigned int size = 0;
95 int maxN = BndSet::MAX_OF_EMPTY;
96 for (LubRanges<View> ubr(x0); ubr(); ++ubr, ++size) {}
97 Region r;
98 int* ub = r.alloc<int>(size*2);
99 {
100 int i=0;
101 for (LubRanges<View> ubr(x0); ubr(); ++ubr, ++i) {
102 ub[2*i] = ubr.min();
103 ub[2*i+1] = ubr.max();
104 }
105 }
106 unsigned int x0cm = x0.cardMin()-1;
107 for (unsigned int i=size; i--;) {
108 unsigned int width = static_cast<unsigned int>(ub[2*i+1]-ub[2*i]+1);
109 if (width > x0cm) {
110 maxN = static_cast<int>(ub[2*i+1]-x0cm);
111 break;
112 }
113 x0cm -= width;
114 }
115 GECODE_ME_CHECK(x1.lq(home,maxN));
116 }
117
118 GECODE_ME_CHECK( x0.exclude(home,
119 Limits::min, x1.min()-1) );
120
121 if (x1.assigned()) {
122 GECODE_ME_CHECK(x0.include(home,x1.val()));
123 GECODE_ME_CHECK(x0.exclude(home,
124 Limits::min, x1.val()-1));
125 return home.ES_SUBSUMED(*this);
126 }
127
128 return ES_FIX;
129 }
130
131
132 template<class View>
133 forceinline
134 NotMinElement<View>::NotMinElement(Home home, View y0,
135 Gecode::Int::IntView y1)
136 : MixBinaryPropagator<View,PC_SET_ANY,
137 Gecode::Int::IntView,Gecode::Int::PC_INT_DOM> (home, y0, y1) {}
138
139 template<class View>
140 forceinline ExecStatus
141 NotMinElement<View>::post(Home home, View x0, Gecode::Int::IntView x1) {
142 (void) new (home) NotMinElement(home,x0,x1);
143 return ES_OK;
144 }
145
146 template<class View>
147 forceinline
148 NotMinElement<View>::NotMinElement(Space& home, NotMinElement& p)
149 : MixBinaryPropagator<View,PC_SET_ANY,
150 Gecode::Int::IntView,Gecode::Int::PC_INT_DOM> (home, p) {}
151
152 template<class View>
153 Actor*
154 NotMinElement<View>::copy(Space& home) {
155 return new (home) NotMinElement(home,*this);
156 }
157
158 template<class View>
159 ExecStatus
160 NotMinElement<View>::propagate(Space& home, const ModEventDelta&) {
161 // cheap tests for entailment:
162 // if x0 is empty, then entailed
163 // if max(x1) < min(x0.lub) or min(x1) > max(x0.lub), then entailed
164 // if min(x0.glb) < min(x1), then entailed
165 if ((x0.cardMax() == 0) ||
166 ((x1.max() < x0.lubMin()) || (x1.min() > x0.lubMax())) ||
167 ((x0.glbSize() > 0) && (x0.glbMin() < x1.min())))
168 return home.ES_SUBSUMED(*this);
169 // if x1 is determined and = x0.lub.min: remove it from x0,
170 // then entailed
171 if (x1.assigned() && x1.val()==x0.lubMin()) {
172 GECODE_ME_CHECK(x0.exclude(home,x1.val()));
173 return home.ES_SUBSUMED(*this);
174 }
175 // if min(x0) is decided: remove min(x0) from the domain of x1
176 // then entailed
177 if (x0.glbMin() == x0.lubMin()) {
178 GECODE_ME_CHECK(x1.nq(home,x0.glbMin()));
179 return home.ES_SUBSUMED(*this);
180 }
181 // if x1 is determined and = x0.glb.min, then we need at least
182 // one more element; if there is only one below, then we must
183 // take it.
184 if (x1.assigned() && x0.glbSize() > 0 && x1.val()==x0.glbMin()) {
185 unsigned int oldGlbSize = x0.glbSize();
186 // if there is only 1 unknown below x1, then we must take it
187 UnknownRanges<View> ur(x0);
188 assert(ur());
189 // the iterator is not empty: otherwise x0 would be determined
190 // and min(x0) would have been decided and the preceding if
191 // would have caught it. Also, the first range is not above
192 // x1 otherwise the very first if would have caught it.
193 // so let's check if the very first range of unknowns is of
194 // size 1 and there is no second one or it starts above x1.
195 if (ur.width()==1) {
196 int i=ur.min();
197 ++ur;
198 if (!ur() || ur.min()>x1.val()) {
199 GECODE_ME_CHECK(x0.include(home,i));
200 return home.ES_SUBSUMED(*this);
201 }
202 }
203 GECODE_ME_CHECK(x0.cardMin(home, oldGlbSize+1));
204 }
205 // if dom(x1) and lub(x0) are disjoint, then entailed;
206 {
207 LubRanges<View> ub(x0);
208 Gecode::Int::ViewRanges<Gecode::Int::IntView> d(x1);
209 Gecode::Iter::Ranges::Inter<LubRanges<View>,
210 Gecode::Int::ViewRanges<Gecode::Int::IntView> > ir(ub,d);
211 if (!ir()) return home.ES_SUBSUMED(*this);
212 }
213 // x0 is fated to eventually contain at least x0.cardMin elements.
214 // therefore min(x0) <= x0.cardMin-th largest element of x0.lub
215 // if x1 > than that, then entailed.
216 {
217 // to find the x0.cardMin-th largest element of x0.lub, we need
218 // some sort of reverse range iterator. we will need to fake one
219 // by storing the ranges of the forward iterator in an array.
220 // first we need to know how large the array needs to be. so, let's
221 // count the ranges:
222 int num_ranges = 0;
223 for (LubRanges<View> ur(x0); ur(); ++ur, ++num_ranges) {}
224 // create an array for storing min and max of each range
225 Region r;
226 int* _ur = r.alloc<int>(num_ranges*2);
227 // now, we fill the array:
228 {
229 int i = 0;
230 for (LubRanges<View> ur(x0); ur(); ++ur, ++i) {
231 _ur[2*i ] = ur.min();
232 _ur[2*i+1] = ur.max();
233 }
234 }
235 // now we search from the top the range that contains the
236 // nth largest value.
237 unsigned int n = x0.cardMin();
238 int nth_largest = BndSet::MAX_OF_EMPTY;
239 for (int i=num_ranges; i--; ) {
240 // number of values in range
241 unsigned int num_values = static_cast<unsigned int>(_ur[2*i+1]-_ur[2*i]+1);
242 // does the range contain the value?
243 if (num_values >= n) {
244 // record it and exit the loop
245 nth_largest = static_cast<int>(_ur[2*i+1]-n+1);
246 break;
247 }
248 // otherwise, we skipped num_values
249 n -= num_values;
250 }
251 // if x1.min > nth_largest, then entailed
252 if (x1.min() > nth_largest)
253 return home.ES_SUBSUMED(*this);
254 }
255 return ES_FIX;
256 }
257
258 template<class View, ReifyMode rm>
259 forceinline
260 ReMinElement<View,rm>::ReMinElement(Home home, View y0,
261 Gecode::Int::IntView y1,
262 Gecode::Int::BoolView b2)
263 : Gecode::Int::ReMixBinaryPropagator<View,PC_SET_ANY,
264 Gecode::Int::IntView,Gecode::Int::PC_INT_DOM,
265 Gecode::Int::BoolView> (home, y0, y1, b2) {}
266
267 template<class View, ReifyMode rm>
268 forceinline ExecStatus
269 ReMinElement<View,rm>::post(Home home, View x0, Gecode::Int::IntView x1,
270 Gecode::Int::BoolView b2) {
271 (void) new (home) ReMinElement(home,x0,x1,b2);
272 return ES_OK;
273 }
274
275 template<class View, ReifyMode rm>
276 forceinline
277 ReMinElement<View,rm>::ReMinElement(Space& home, ReMinElement& p)
278 : Gecode::Int::ReMixBinaryPropagator<View,PC_SET_ANY,
279 Gecode::Int::IntView,Gecode::Int::PC_INT_DOM,
280 Gecode::Int::BoolView> (home, p) {}
281
282 template<class View, ReifyMode rm>
283 Actor*
284 ReMinElement<View,rm>::copy(Space& home) {
285 return new (home) ReMinElement(home,*this);
286 }
287
288 template<class View, ReifyMode rm>
289 ExecStatus
290 ReMinElement<View,rm>::propagate(Space& home, const ModEventDelta&) {
291 // check if b is determined
292 if (b.one()) {
293 if (rm == RM_PMI)
294 return home.ES_SUBSUMED(*this);
295 GECODE_REWRITE(*this, (MinElement<View>::post(home(*this),x0,x1)));
296 }
297 if (b.zero()) {
298 if (rm == RM_IMP)
299 return home.ES_SUBSUMED(*this);
300 GECODE_REWRITE(*this, (NotMinElement<View>::post(home(*this),x0,x1)));
301 }
302 // cheap tests for => b=0
303 // if x0 is empty, then b=0 and entailed
304 // if max(x1) < min(x0.lub) or min(x1) > max(x0.lub), then b=0 and entailed
305 // if min(x0.glb) < min(x1), then b=0 and entailed
306 if ((x0.cardMax() == 0) ||
307 ((x1.max() < x0.lubMin()) || (x1.min() > x0.lubMax())) ||
308 ((x0.glbSize() > 0) && (x0.glbMin() < x1.min())))
309 {
310 if (rm != RM_PMI)
311 GECODE_ME_CHECK(b.zero(home));
312 return home.ES_SUBSUMED(*this);
313 }
314 // if min(x0) is decided
315 if (x0.glbMin() == x0.lubMin()) {
316 // if x1 is det: check if = min(x0), assign b, entailed
317 if (x1.assigned()) {
318 if (x1.val() == x0.glbMin()) {
319 if (rm != RM_IMP)
320 GECODE_ME_CHECK(b.one(home));
321 } else {
322 if (rm != RM_PMI)
323 GECODE_ME_CHECK(b.zero(home));
324 }
325 return home.ES_SUBSUMED(*this);
326 }
327 // if min(x0) not in dom(x1): b=0, entailed
328 else if ((x0.glbMin() < x1.min()) ||
329 (x0.glbMin() > x1.max()) ||
330 !x1.in(x0.glbMin()))
331 {
332 if (rm != RM_PMI)
333 GECODE_ME_CHECK(b.zero(home));
334 return home.ES_SUBSUMED(*this);
335 }
336 }
337 // // if dom(x1) and lub(x0) are disjoint, then b=0, entailed;
338 // {
339 // LubRanges<View> ub(x0);
340 // Gecode::Int::ViewRanges<Gecode::Int::IntView> d(x1);
341 // Gecode::Iter::Ranges::Inter<LubRanges<View>,
342 // Gecode::Int::ViewRanges<Gecode::Int::IntView> > ir(ub,d);
343 // if (!ir()) {
344 // GECODE_ME_CHECK(b.zero(home));
345 // return home.ES_SUBSUMED(*this);
346 // }
347 // }
348 // // x0 is fated to eventually contain at least x0.cardMin elements.
349 // // therefore min(x0) <= x0.cardMin-th largest element of x0.lub
350 // // if x1 > than that, then b=0 and entailed.
351 // {
352 // // to find the x0.cardMin-th largest element of x0.lub, we need
353 // // some sort of reverse range iterator. we will need to fake one
354 // // by storing the ranges of the forward iterator in an array.
355 // // first we need to know how large the array needs to be. so, let's
356 // // count the ranges:
357 // int num_ranges = 0;
358 // for (LubRanges<View> ur(x0); ur(); ++ur, ++num_ranges) {}
359 // // create an array for storing min and max of each range
360 // Region re(home);
361 // int* _ur = re.alloc<int>(num_ranges*2);
362 // // now, we fill the array:
363 // int i = 0;
364 // for (LubRanges<View> ur(x0); ur(); ++ur, ++i) {
365 // _ur[2*i ] = ur.min();
366 // _ur[2*i+1] = ur.max();
367 // }
368 // // now we search from the top the range that contains the
369 // // nth largest value.
370 // int n = x0.cardMin();
371 // int nth_largest = BndSet::MAX_OF_EMPTY;
372 // for (int i=num_ranges; i--; ) {
373 // // number of values in range
374 // int num_values = _ur[2*i+1]-_ur[2*i]+1;
375 // // does the range contain the value?
376 // if (num_values >= n)
377 // {
378 // // record it and exit the loop
379 // nth_largest = _ur[2*i+1]-n+1;
380 // break;
381 // }
382 // // otherwise, we skipped num_values
383 // n -= num_values;
384 // }
385 // // if x1.min > nth_largest, then entailed
386 // if (x1.min() > nth_largest) {
387 // GECODE_ME_CHECK(b.zero(home));
388 // return home.ES_SUBSUMED(*this);
389 // }
390 // }
391 return ES_FIX;
392 }
393
394 template<class View>
395 forceinline
396 MaxElement<View>::MaxElement(Home home, View y0, Gecode::Int::IntView y1)
397 : MixBinaryPropagator<View,PC_SET_ANY,
398 Gecode::Int::IntView,Gecode::Int::PC_INT_BND> (home, y0, y1) {}
399
400 template<class View>
401 forceinline
402 MaxElement<View>::MaxElement(Space& home, MaxElement& p)
403 : MixBinaryPropagator<View,PC_SET_ANY,
404 Gecode::Int::IntView,Gecode::Int::PC_INT_BND> (home, p) {}
405
406 template<class View>
407 ExecStatus
408 MaxElement<View>::post(Home home, View x0,
409 Gecode::Int::IntView x1) {
410 GECODE_ME_CHECK(x0.cardMin(home,1));
411 (void) new (home) MaxElement(home,x0,x1);
412 return ES_OK;
413 }
414
415 template<class View>
416 Actor*
417 MaxElement<View>::copy(Space& home) {
418 return new (home) MaxElement(home,*this);
419 }
420
421 template<class View>
422 ExecStatus
423 MaxElement<View>::propagate(Space& home, const ModEventDelta&) {
424 LubRanges<View> ub(x0);
425 GECODE_ME_CHECK(x1.inter_r(home,ub,false));
426 GECODE_ME_CHECK(x1.gq(home,x0.glbMax()));
427 assert(x0.cardMin()>=1);
428 GECODE_ME_CHECK(x1.gq(home,x0.lubMinN(x0.cardMin()-1)));
429 GECODE_ME_CHECK(x0.exclude(home,
430 x1.max()+1,Limits::max) );
431
432 if (x1.assigned()) {
433 GECODE_ME_CHECK(x0.include(home,x1.val()));
434 GECODE_ME_CHECK( x0.exclude(home,
435 x1.val()+1,Limits::max) );
436 return home.ES_SUBSUMED(*this);
437 }
438
439 return ES_FIX;
440 }
441
442 template<class View>
443 forceinline
444 NotMaxElement<View>::NotMaxElement(Home home, View y0,
445 Gecode::Int::IntView y1)
446 : MixBinaryPropagator<View,PC_SET_ANY,
447 Gecode::Int::IntView,Gecode::Int::PC_INT_DOM> (home, y0, y1) {}
448
449 template<class View>
450 forceinline
451 NotMaxElement<View>::NotMaxElement(Space& home, NotMaxElement& p)
452 : MixBinaryPropagator<View,PC_SET_ANY,
453 Gecode::Int::IntView,Gecode::Int::PC_INT_DOM> (home, p) {}
454
455 template<class View>
456 ExecStatus
457 NotMaxElement<View>::post(Home home, View x0, Gecode::Int::IntView x1) {
458 (void) new (home) NotMaxElement(home,x0,x1);
459 return ES_OK;
460 }
461
462 template<class View>
463 Actor*
464 NotMaxElement<View>::copy(Space& home) {
465 return new (home) NotMaxElement(home,*this);
466 }
467
468 template<class View>
469 ExecStatus
470 NotMaxElement<View>::propagate(Space& home, const ModEventDelta&) {
471 // cheap tests for entailment:
472 // if x0 is empty, then entailed
473 // if max(x1) < min(x0.lub) or min(x1) > max(x0.lub), then entailed
474 // if max(x0.glb) > max(x1), then entailed
475 if ((x0.cardMax() == 0) ||
476 ((x1.max() < x0.lubMin()) || (x1.min() > x0.lubMax())) ||
477 ((x0.glbSize() > 0) && (x0.glbMax() > x1.max())))
478 return home.ES_SUBSUMED(*this);
479 // if x1 is determined and = max(x0.lub): remove it from x0,
480 // then entailed
481 if (x1.assigned() && x1.val()==x0.lubMax()) {
482 GECODE_ME_CHECK(x0.exclude(home,x1.val()));
483 return home.ES_SUBSUMED(*this);
484 }
485 // if max(x0) is decided: remove max(x0) from the domain of x1
486 // then entailed
487 if (x0.glbMax() == x0.lubMax()) {
488 GECODE_ME_CHECK(x1.nq(home,x0.glbMax()));
489 return home.ES_SUBSUMED(*this);
490 }
491 // if x1 is determined and = max(x0.glb), then we need at least
492 // one more element; if there is only one above, then we must
493 // take it.
494 if (x1.assigned() && x0.glbSize() > 0 && x1.val()==x0.glbMax()) {
495 unsigned int oldGlbSize = x0.glbSize();
496 // if there is only 1 unknown above x1, then we must take it
497 UnknownRanges<View> ur(x0);
498 // there is at least one unknown above x1 otherwise it would
499 // have been caught by the if for x1=max(x0.lub)
500 while (ur.max() < x1.val()) {
501 assert(ur());
502 ++ur;
503 };
504 // if the first range above x1 contains just 1 element,
505 // and is the last range, then take that element
506 if (ur.width() == 1) {
507 int i = ur.min();
508 ++ur;
509 if (!ur()) {
510 // last range
511 GECODE_ME_CHECK(x0.include(home,i));
512 return home.ES_SUBSUMED(*this);
513 }
514 }
515 GECODE_ME_CHECK(x0.cardMin(home, oldGlbSize+1));
516 }
517 // if dom(x1) and lub(x0) are disjoint, then entailed
518 {
519 LubRanges<View> ub(x0);
520 Gecode::Int::ViewRanges<Gecode::Int::IntView> d(x1);
521 Gecode::Iter::Ranges::Inter<LubRanges<View>,
522 Gecode::Int::ViewRanges<Gecode::Int::IntView> > ir(ub,d);
523 if (!ir()) return home.ES_SUBSUMED(*this);
524 }
525 // x0 is fated to eventually contain at least x0.cardMin elements.
526 // therefore max(x0) >= x0.cardMin-th smallest element of x0.lub.
527 // if x1 < than that, then entailed.
528 {
529 unsigned int n = x0.cardMin();
530 int nth_smallest = BndSet::MIN_OF_EMPTY;
531 for (LubRanges<View> ur(x0); ur(); ++ur) {
532 if (ur.width() >= n) {
533 // record it and exit the loop
534 nth_smallest = static_cast<int>(ur.min() + n - 1);
535 break;
536 }
537 // otherwise, we skipped ur.width() values
538 n -= ur.width();
539 }
540 // if x1.max < nth_smallest, then entailed
541 if (x1.max() < nth_smallest)
542 return home.ES_SUBSUMED(*this);
543 }
544 return ES_FIX;
545 }
546
547 template<class View, ReifyMode rm>
548 forceinline
549 ReMaxElement<View,rm>::ReMaxElement(Home home, View y0,
550 Gecode::Int::IntView y1,
551 Gecode::Int::BoolView b2)
552 : Gecode::Int::ReMixBinaryPropagator<View,PC_SET_ANY,
553 Gecode::Int::IntView,Gecode::Int::PC_INT_DOM,
554 Gecode::Int::BoolView> (home, y0, y1, b2) {}
555
556 template<class View, ReifyMode rm>
557 forceinline
558 ReMaxElement<View,rm>::ReMaxElement(Space& home, ReMaxElement& p)
559 : Gecode::Int::ReMixBinaryPropagator<View,PC_SET_ANY,
560 Gecode::Int::IntView,Gecode::Int::PC_INT_DOM,
561 Gecode::Int::BoolView> (home, p) {}
562
563 template<class View, ReifyMode rm>
564 ExecStatus
565 ReMaxElement<View,rm>::post(Home home, View x0,
566 Gecode::Int::IntView x1,
567 Gecode::Int::BoolView b2) {
568 (void) new (home) ReMaxElement(home,x0,x1,b2);
569 return ES_OK;
570 }
571
572 template<class View, ReifyMode rm>
573 Actor*
574 ReMaxElement<View,rm>::copy(Space& home) {
575 return new (home) ReMaxElement(home,*this);
576 }
577
578 template<class View, ReifyMode rm>
579 ExecStatus
580 ReMaxElement<View,rm>::propagate(Space& home, const ModEventDelta&) {
581 // check if b is determined
582 if (b.one()) {
583 if (rm == RM_PMI)
584 return home.ES_SUBSUMED(*this);
585 GECODE_REWRITE(*this, (MaxElement<View>::post(home(*this),x0,x1)));
586 }
587 if (b.zero()) {
588 if (rm == RM_IMP)
589 return home.ES_SUBSUMED(*this);
590 GECODE_REWRITE(*this, (NotMaxElement<View>::post(home(*this),x0,x1)));
591 }
592 // cheap tests for => b=0
593 // if x0 is empty, then b=0 and entailed
594 // if max(x1) < min(x0.lub) or min(x1) > max(x0.lub), then b=0 and entailed
595 // if max(x0.glb) > max(x1), then b=0 and entailed
596 if ((x0.cardMax() == 0) ||
597 ((x1.max() < x0.lubMin()) || (x1.min() > x0.lubMax())) ||
598 ((x0.glbSize() > 0) && (x0.glbMax() > x1.max())))
599 {
600 if (rm != RM_PMI)
601 GECODE_ME_CHECK(b.zero(home));
602 return home.ES_SUBSUMED(*this);
603 }
604 // if max(x0) is decided
605 if (x0.glbMax() == x0.lubMax()) {
606 // if x1 is det: check if = max(x0), assign b, entailed
607 if (x1.assigned()) {
608 if (x1.val() == x0.glbMax()) {
609 if (rm != RM_IMP)
610 GECODE_ME_CHECK(b.one(home));
611 } else {
612 if (rm != RM_PMI)
613 GECODE_ME_CHECK(b.zero(home));
614 }
615 return home.ES_SUBSUMED(*this);
616 }
617 // if max(x0) not in dom(x1): b=0, entailed
618 else if ((x0.glbMax() < x1.min()) ||
619 (x0.glbMax() > x1.max()) ||
620 !x1.in(x0.glbMax()))
621 {
622 if (rm != RM_PMI)
623 GECODE_ME_CHECK(b.zero(home));
624 return home.ES_SUBSUMED(*this);
625 }
626 }
627 // if dom(x1) and lub(x0) are disjoint, then b=0, entailed
628 {
629 LubRanges<View> ub(x0);
630 Gecode::Int::ViewRanges<Gecode::Int::IntView> d(x1);
631 Gecode::Iter::Ranges::Inter<LubRanges<View>,
632 Gecode::Int::ViewRanges<Gecode::Int::IntView> > ir(ub,d);
633 if (!ir()) {
634 if (rm != RM_PMI)
635 GECODE_ME_CHECK(b.zero(home));
636 return home.ES_SUBSUMED(*this);
637 }
638 }
639 // x0 is fated to eventually contain at least x0.cardMin elements.
640 // therefore max(x0) >= x0.cardMin-th smallest element of x0.lub.
641 // if x1 < than that, then b=0, entailed.
642 {
643 unsigned int n = x0.cardMin();
644 int nth_smallest = BndSet::MIN_OF_EMPTY;
645 for (LubRanges<View> ur(x0); ur(); ++ur) {
646 if (ur.width() >= n)
647 {
648 // record it and exit the loop
649 nth_smallest = static_cast<int>(ur.min() + n - 1);
650 break;
651 }
652 // otherwise, we skipped ur.width() values
653 n -= ur.width();
654 }
655 // if x1.max < nth_smallest, then entailed
656 if (x1.max() < nth_smallest) {
657 if (rm != RM_PMI)
658 GECODE_ME_CHECK(b.zero(home));
659 return home.ES_SUBSUMED(*this);
660 }
661 }
662 return ES_FIX;
663 }
664
665}}}
666
667// STATISTICS: set-prop