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 44 namespace Gecode { namespace Set { namespace Int { 45 46 template<class View> 47 forceinline MinElement(Home home,View y0,Gecode::Int::IntView y1)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 post(Home home,View x0,Gecode::Int::IntView x1)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 MinElement(Space & home,MinElement & p)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* copy(Space & home)66 MinElement<View>::copy(Space& home) { 67 return new (home) MinElement(home,*this); 68 } 69 70 template<class View> 71 ExecStatus propagate(Space & home,const ModEventDelta &)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 NotMinElement(Home home,View y0,Gecode::Int::IntView y1)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 post(Home home,View x0,Gecode::Int::IntView x1)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 NotMinElement(Space & home,NotMinElement & p)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* copy(Space & home)154 NotMinElement<View>::copy(Space& home) { 155 return new (home) NotMinElement(home,*this); 156 } 157 158 template<class View> 159 ExecStatus propagate(Space & home,const ModEventDelta &)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 ReMinElement(Home home,View y0,Gecode::Int::IntView y1,Gecode::Int::BoolView b2)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 post(Home home,View x0,Gecode::Int::IntView x1,Gecode::Int::BoolView b2)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 ReMinElement(Space & home,ReMinElement & p)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* copy(Space & home)284 ReMinElement<View,rm>::copy(Space& home) { 285 return new (home) ReMinElement(home,*this); 286 } 287 288 template<class View, ReifyMode rm> 289 ExecStatus propagate(Space & home,const ModEventDelta &)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 MaxElement(Home home,View y0,Gecode::Int::IntView y1)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 MaxElement(Space & home,MaxElement & p)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 post(Home home,View x0,Gecode::Int::IntView x1)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* copy(Space & home)417 MaxElement<View>::copy(Space& home) { 418 return new (home) MaxElement(home,*this); 419 } 420 421 template<class View> 422 ExecStatus propagate(Space & home,const ModEventDelta &)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 NotMaxElement(Home home,View y0,Gecode::Int::IntView y1)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 NotMaxElement(Space & home,NotMaxElement & p)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 post(Home home,View x0,Gecode::Int::IntView x1)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* copy(Space & home)464 NotMaxElement<View>::copy(Space& home) { 465 return new (home) NotMaxElement(home,*this); 466 } 467 468 template<class View> 469 ExecStatus propagate(Space & home,const ModEventDelta &)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 ReMaxElement(Home home,View y0,Gecode::Int::IntView y1,Gecode::Int::BoolView b2)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 ReMaxElement(Space & home,ReMaxElement & p)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 post(Home home,View x0,Gecode::Int::IntView x1,Gecode::Int::BoolView b2)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* copy(Space & home)574 ReMaxElement<View,rm>::copy(Space& home) { 575 return new (home) ReMaxElement(home,*this); 576 } 577 578 template<class View, ReifyMode rm> 579 ExecStatus propagate(Space & home,const ModEventDelta &)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 668