1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 2 /* 3 * Main authors: 4 * Christian Schulte <schulte@gecode.org> 5 * Tias Guns <tias.guns@cs.kuleuven.be> 6 * 7 * Copyright: 8 * Christian Schulte, 2006 9 * Tias Guns, 2009 10 * 11 * This file is part of Gecode, the generic constraint 12 * development environment: 13 * http://www.gecode.org 14 * 15 * Permission is hereby granted, free of charge, to any person obtaining 16 * a copy of this software and associated documentation files (the 17 * "Software"), to deal in the Software without restriction, including 18 * without limitation the rights to use, copy, modify, merge, publish, 19 * distribute, sublicense, and/or sell copies of the Software, and to 20 * permit persons to whom the Software is furnished to do so, subject to 21 * the following conditions: 22 * 23 * The above copyright notice and this permission notice shall be 24 * included in all copies or substantial portions of the Software. 25 * 26 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 27 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 28 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 29 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE 30 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION 31 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION 32 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 33 * 34 */ 35 36 #include <algorithm> 37 38 #include <gecode/int/bool.hh> 39 40 namespace Gecode { namespace Int { namespace Linear { 41 42 /* 43 * Baseclass for integer Boolean sum using dependencies 44 * 45 */ 46 template<class VX> 47 forceinline LinBoolInt(Home home,ViewArray<VX> & x0,int n_s,int c0)48 LinBoolInt<VX>::LinBoolInt(Home home, ViewArray<VX>& x0, 49 int n_s, int c0) 50 : Propagator(home), co(home), x(x0), n_as(n_s), n_hs(n_s), c(c0) { 51 Advisor* a = new (home) Advisor(home,*this,co); 52 for (int i=0; i<n_as; i++) 53 x[i].subscribe(home,*a); 54 } 55 56 template<class VX> 57 forceinline void normalize(void)58 LinBoolInt<VX>::normalize(void) { 59 if (n_as != n_hs) { 60 // Remove views for which no more subscriptions exist 61 int n_x = x.size(); 62 for (int i=n_hs; i--; ) 63 if (!x[i].none()) { 64 x[i]=x[--n_hs]; x[n_hs]=x[--n_x]; 65 } 66 x.size(n_x); 67 } 68 assert(n_as == n_hs); 69 // Remove assigned yet unsubscribed views 70 { 71 int n_x = x.size(); 72 for (int i=n_x-1; i>=n_hs; i--) 73 if (x[i].one()) { 74 c--; x[i]=x[--n_x]; 75 } else if (x[i].zero()) { 76 x[i]=x[--n_x]; 77 } 78 x.size(n_x); 79 } 80 } 81 82 template<class VX> 83 forceinline LinBoolInt(Space & home,LinBoolInt<VX> & p)84 LinBoolInt<VX>::LinBoolInt(Space& home, LinBoolInt<VX>& p) 85 : Propagator(home,p), n_as(p.n_as), n_hs(n_as) { 86 p.normalize(); 87 c=p.c; 88 co.update(home,p.co); 89 x.update(home,p.x); 90 } 91 92 template<class VX> 93 PropCost cost(const Space &,const ModEventDelta &) const94 LinBoolInt<VX>::cost(const Space&, const ModEventDelta&) const { 95 return PropCost::unary(PropCost::HI); 96 } 97 98 template<class VX> 99 forceinline size_t dispose(Space & home)100 LinBoolInt<VX>::dispose(Space& home) { 101 Advisors<Advisor> as(co); 102 for (int i=0; i<n_hs; i++) 103 x[i].cancel(home,as.advisor()); 104 co.dispose(home); 105 (void) Propagator::dispose(home); 106 return sizeof(*this); 107 } 108 109 /* 110 * Greater or equal propagator (integer rhs) 111 * 112 */ 113 template<class VX> 114 forceinline GqBoolInt(Home home,ViewArray<VX> & x,int c)115 GqBoolInt<VX>::GqBoolInt(Home home, ViewArray<VX>& x, int c) 116 : LinBoolInt<VX>(home,x,c+1,c) {} 117 118 template<class VX> 119 forceinline GqBoolInt(Space & home,GqBoolInt<VX> & p)120 GqBoolInt<VX>::GqBoolInt(Space& home, GqBoolInt<VX>& p) 121 : LinBoolInt<VX>(home,p) {} 122 123 template<class VX> 124 Actor* copy(Space & home)125 GqBoolInt<VX>::copy(Space& home) { 126 return new (home) GqBoolInt<VX>(home,*this); 127 } 128 129 template<class VX> 130 ExecStatus advise(Space & home,Advisor & a,const Delta & d)131 GqBoolInt<VX>::advise(Space& home, Advisor& a, const Delta& d) { 132 // Check whether propagator is running 133 if (n_as == 0) 134 return ES_FIX; 135 136 if (VX::one(d)) { 137 c--; goto check; 138 } 139 if (c+1 < n_as) 140 goto check; 141 // Find a new subscription 142 for (int i = x.size()-1; i>=n_hs; i--) 143 if (x[i].none()) { 144 std::swap(x[i],x[n_hs]); 145 x[n_hs++].subscribe(home,a); 146 x.size(i+1); 147 return ES_FIX; 148 } else if (x[i].one()) { 149 c--; 150 if (c+1 < n_as) { 151 x.size(i); 152 assert(n_hs <= x.size()); 153 goto check; 154 } 155 } 156 // No view left for subscription 157 x.size(n_hs); 158 check: 159 // Do not update subscription 160 n_as--; 161 int n = x.size()-n_hs+n_as; 162 if ((n < c) && !disabled()) 163 return ES_FAILED; 164 if ((c <= 0) || (c == n)) 165 return ES_NOFIX; 166 else 167 return ES_FIX; 168 } 169 170 template<class VX> 171 void reschedule(Space & home)172 GqBoolInt<VX>::reschedule(Space& home) { 173 int n = x.size()-n_hs+n_as; 174 if ((c <= 0) || (c >= n)) 175 VX::schedule(home,*this,ME_INT_VAL); 176 } 177 178 template<class VX> 179 ExecStatus propagate(Space & home,const ModEventDelta &)180 GqBoolInt<VX>::propagate(Space& home, const ModEventDelta&) { 181 // Check for failure due to a disabled propagator 182 if (x.size() - n_hs + n_as < c) 183 return ES_FAILED; 184 if (c > 0) { 185 assert((n_as == c) && (x.size() == n_hs)); 186 // Signal that propagator is running 187 n_as = 0; 188 // All views must be one to satisfy inequality 189 for (int i=0; i<n_hs; i++) 190 if (x[i].none()) 191 GECODE_ME_CHECK(x[i].one_none(home)); 192 } 193 return home.ES_SUBSUMED(*this); 194 } 195 196 template<class VX> 197 ExecStatus post(Home home,ViewArray<VX> & x,int c)198 GqBoolInt<VX>::post(Home home, ViewArray<VX>& x, int c) { 199 // Eliminate assigned views 200 int n_x = x.size(); 201 for (int i=n_x; i--; ) 202 if (x[i].zero()) { 203 x[i] = x[--n_x]; 204 } else if (x[i].one()) { 205 x[i] = x[--n_x]; c--; 206 } 207 x.size(n_x); 208 // RHS too large 209 if (n_x < c) 210 return ES_FAILED; 211 // Whatever the x[i] take for values, the inequality is subsumed 212 if (c <= 0) 213 return ES_OK; 214 // Use Boolean disjunction for this special case 215 if (c == 1) 216 return Bool::NaryOrTrue<VX>::post(home,x); 217 // All views must be one to satisfy inequality 218 if (c == n_x) { 219 for (int i=0; i<n_x; i++) 220 GECODE_ME_CHECK(x[i].one_none(home)); 221 return ES_OK; 222 } 223 // This is the needed invariant as c+1 subscriptions must be created 224 assert(n_x > c); 225 (void) new (home) GqBoolInt<VX>(home,x,c); 226 return ES_OK; 227 } 228 229 230 231 232 /* 233 * Equal propagator (integer rhs) 234 * 235 */ 236 template<class VX> 237 forceinline EqBoolInt(Home home,ViewArray<VX> & x,int c)238 EqBoolInt<VX>::EqBoolInt(Home home, ViewArray<VX>& x, int c) 239 : LinBoolInt<VX>(home,x,std::max(c,x.size()-c)+1,c) {} 240 241 template<class VX> 242 forceinline EqBoolInt(Space & home,EqBoolInt<VX> & p)243 EqBoolInt<VX>::EqBoolInt(Space& home, EqBoolInt<VX>& p) 244 : LinBoolInt<VX>(home,p) {} 245 246 template<class VX> 247 Actor* copy(Space & home)248 EqBoolInt<VX>::copy(Space& home) { 249 return new (home) EqBoolInt<VX>(home,*this); 250 } 251 252 template<class VX> 253 ExecStatus advise(Space & home,Advisor & a,const Delta & d)254 EqBoolInt<VX>::advise(Space& home, Advisor& a, const Delta& d) { 255 // Check whether propagator is running 256 if (n_as == 0) 257 return ES_FIX; 258 259 if (VX::one(d)) 260 c--; 261 if ((c+1 < n_as) && (x.size()-n_hs < c)) 262 goto check; 263 // Find a new subscription 264 for (int i = x.size()-1; i>=n_hs; i--) 265 if (x[i].none()) { 266 std::swap(x[i],x[n_hs]); 267 x[n_hs++].subscribe(home,a); 268 x.size(i+1); 269 return ES_FIX; 270 } else if (x[i].one()) { 271 c--; 272 } 273 // No view left for subscription 274 x.size(n_hs); 275 check: 276 // Do not update subscription 277 n_as--; 278 int n = x.size()-n_hs+n_as; 279 if (((c < 0) || (c > n)) && !disabled()) 280 return ES_FAILED; 281 if ((c == 0) || (c == n)) 282 return ES_NOFIX; 283 else 284 return ES_FIX; 285 } 286 287 template<class VX> 288 void reschedule(Space & home)289 EqBoolInt<VX>::reschedule(Space& home) { 290 int n = x.size()-n_hs+n_as; 291 if ((c <= 0) || (c >= n)) 292 VX::schedule(home,*this,ME_INT_VAL); 293 } 294 295 template<class VX> 296 ExecStatus propagate(Space & home,const ModEventDelta &)297 EqBoolInt<VX>::propagate(Space& home, const ModEventDelta&) { 298 // Check for failure due to being disabled before 299 if ((c < 0) || (c > x.size()-n_hs+n_as)) 300 return ES_FAILED; 301 302 assert(x.size() == n_hs); 303 // Signal that propagator is running 304 n_as = 0; 305 if (c == 0) { 306 // All views must be zero to satisfy equality 307 for (int i=0; i<n_hs; i++) 308 if (x[i].none()) 309 GECODE_ME_CHECK(x[i].zero_none(home)); 310 } else { 311 // All views must be one to satisfy equality 312 for (int i=0; i<n_hs; i++) 313 if (x[i].none()) 314 GECODE_ME_CHECK(x[i].one_none(home)); 315 } 316 return home.ES_SUBSUMED(*this); 317 } 318 319 template<class VX> 320 ExecStatus post(Home home,ViewArray<VX> & x,int c)321 EqBoolInt<VX>::post(Home home, ViewArray<VX>& x, int c) { 322 // Eliminate assigned views 323 int n_x = x.size(); 324 for (int i=n_x; i--; ) 325 if (x[i].zero()) { 326 x[i] = x[--n_x]; 327 } else if (x[i].one()) { 328 x[i] = x[--n_x]; c--; 329 } 330 x.size(n_x); 331 // RHS too small or too large 332 if ((c < 0) || (c > n_x)) 333 return ES_FAILED; 334 // All views must be zero to satisfy equality 335 if (c == 0) { 336 for (int i=0; i<n_x; i++) 337 GECODE_ME_CHECK(x[i].zero_none(home)); 338 return ES_OK; 339 } 340 // All views must be one to satisfy equality 341 if (c == n_x) { 342 for (int i=0; i<n_x; i++) 343 GECODE_ME_CHECK(x[i].one_none(home)); 344 return ES_OK; 345 } 346 (void) new (home) EqBoolInt<VX>(home,x,c); 347 return ES_OK; 348 } 349 350 351 /* 352 * Integer disequal to Boolean sum 353 * 354 */ 355 356 template<class VX> 357 forceinline NqBoolInt(Home home,ViewArray<VX> & b,int c0)358 NqBoolInt<VX>::NqBoolInt(Home home, ViewArray<VX>& b, int c0) 359 : BinaryPropagator<VX,PC_INT_VAL>(home, 360 b[b.size()-2], 361 b[b.size()-1]), x(b), c(c0) { 362 assert(x.size() >= 2); 363 x.size(x.size()-2); 364 } 365 366 template<class VX> 367 forceinline size_t dispose(Space & home)368 NqBoolInt<VX>::dispose(Space& home) { 369 (void) BinaryPropagator<VX,PC_INT_VAL>::dispose(home); 370 return sizeof(*this); 371 } 372 373 template<class VX> 374 forceinline NqBoolInt(Space & home,NqBoolInt<VX> & p)375 NqBoolInt<VX>::NqBoolInt(Space& home, NqBoolInt<VX>& p) 376 : BinaryPropagator<VX,PC_INT_VAL>(home,p), x(home,p.x.size()) { 377 // Eliminate all zeros and ones in original and update 378 int n = p.x.size(); 379 int p_c = p.c; 380 for (int i=n; i--; ) 381 if (p.x[i].zero()) { 382 n--; p.x[i]=p.x[n]; x[i]=x[n]; 383 } else if (p.x[i].one()) { 384 n--; p_c--; p.x[i]=p.x[n]; x[i]=x[n]; 385 } else { 386 x[i].update(home,p.x[i]); 387 } 388 c = p_c; p.c = p_c; 389 x.size(n); p.x.size(n); 390 } 391 392 template<class VX> 393 forceinline ExecStatus post(Home home,ViewArray<VX> & x,int c)394 NqBoolInt<VX>::post(Home home, ViewArray<VX>& x, int c) { 395 int n = x.size(); 396 for (int i=n; i--; ) 397 if (x[i].one()) { 398 x[i]=x[--n]; c--; 399 } else if (x[i].zero()) { 400 x[i]=x[--n]; 401 } 402 x.size(n); 403 if ((n < c) || (c < 0)) 404 return ES_OK; 405 if (n == 0) 406 return (c == 0) ? ES_FAILED : ES_OK; 407 if (n == 1) { 408 if (c == 1) { 409 GECODE_ME_CHECK(x[0].zero_none(home)); 410 } else { 411 GECODE_ME_CHECK(x[0].one_none(home)); 412 } 413 return ES_OK; 414 } 415 (void) new (home) NqBoolInt(home,x,c); 416 return ES_OK; 417 } 418 419 template<class VX> 420 Actor* copy(Space & home)421 NqBoolInt<VX>::copy(Space& home) { 422 return new (home) NqBoolInt<VX>(home,*this); 423 } 424 425 template<class VX> 426 PropCost cost(const Space &,const ModEventDelta &) const427 NqBoolInt<VX>::cost(const Space&, const ModEventDelta&) const { 428 return PropCost::linear(PropCost::LO, x.size()); 429 } 430 431 template<class VX> 432 forceinline bool resubscribe(Space & home,VX & y)433 NqBoolInt<VX>::resubscribe(Space& home, VX& y) { 434 if (y.one()) 435 c--; 436 int n = x.size(); 437 for (int i=n; i--; ) 438 if (x[i].one()) { 439 c--; x[i]=x[--n]; 440 } else if (x[i].zero()) { 441 x[i] = x[--n]; 442 } else { 443 // New unassigned view found 444 assert(!x[i].zero() && !x[i].one()); 445 // Move to y and subscribe 446 y=x[i]; x[i]=x[--n]; 447 x.size(n); 448 y.subscribe(home,*this,PC_INT_VAL,false); 449 return true; 450 } 451 // All views have been assigned! 452 x.size(0); 453 return false; 454 } 455 456 template<class VX> 457 ExecStatus propagate(Space & home,const ModEventDelta &)458 NqBoolInt<VX>::propagate(Space& home, const ModEventDelta&) { 459 bool s0 = true; 460 if (x0.zero() || x0.one()) 461 s0 = resubscribe(home,x0); 462 bool s1 = true; 463 if (x1.zero() || x1.one()) 464 s1 = resubscribe(home,x1); 465 int n = x.size() + s0 + s1; 466 if ((n < c) || (c < 0)) 467 return home.ES_SUBSUMED(*this); 468 if (n == 0) 469 return (c == 0) ? ES_FAILED : home.ES_SUBSUMED(*this); 470 if (n == 1) { 471 if (s0) { 472 if (c == 1) { 473 GECODE_ME_CHECK(x0.zero_none(home)); 474 } else { 475 GECODE_ME_CHECK(x0.one_none(home)); 476 } 477 } else { 478 assert(s1); 479 if (c == 1) { 480 GECODE_ME_CHECK(x1.zero_none(home)); 481 } else { 482 GECODE_ME_CHECK(x1.one_none(home)); 483 } 484 } 485 return home.ES_SUBSUMED(*this); 486 } 487 return ES_FIX; 488 } 489 490 /* 491 * Baseclass for reified integer Boolean sum 492 * 493 */ 494 template<class VX, class VB> 495 forceinline ReLinBoolInt(Home home,ViewArray<VX> & x0,int c0,VB b0)496 ReLinBoolInt<VX,VB>::ReLinBoolInt(Home home, ViewArray<VX>& x0, 497 int c0, VB b0) 498 : Propagator(home), co(home), x(x0), n_s(x.size()), c(c0), b(b0) { 499 x.subscribe(home,*new (home) Advisor(home,*this,co)); 500 b.subscribe(home,*this,PC_BOOL_VAL); 501 } 502 503 template<class VX, class VB> 504 forceinline void normalize(void)505 ReLinBoolInt<VX,VB>::normalize(void) { 506 if (n_s != x.size()) { 507 int n_x = x.size(); 508 for (int i=n_x; i--; ) 509 if (!x[i].none()) 510 x[i] = x[--n_x]; 511 x.size(n_x); 512 assert(x.size() == n_s); 513 } 514 } 515 516 template<class VX, class VB> 517 forceinline ReLinBoolInt(Space & home,ReLinBoolInt<VX,VB> & p)518 ReLinBoolInt<VX,VB>::ReLinBoolInt(Space& home, ReLinBoolInt<VX,VB>& p) 519 : Propagator(home,p), n_s(p.n_s), c(p.c) { 520 p.normalize(); 521 co.update(home,p.co); 522 x.update(home,p.x); 523 b.update(home,p.b); 524 } 525 526 template<class VX, class VB> 527 forceinline size_t dispose(Space & home)528 ReLinBoolInt<VX,VB>::dispose(Space& home) { 529 Advisors<Advisor> as(co); 530 x.cancel(home,as.advisor()); 531 co.dispose(home); 532 b.cancel(home,*this,PC_BOOL_VAL); 533 (void) Propagator::dispose(home); 534 return sizeof(*this); 535 } 536 537 template<class VX, class VB> 538 PropCost cost(const Space &,const ModEventDelta &) const539 ReLinBoolInt<VX,VB>::cost(const Space&, const ModEventDelta&) const { 540 return PropCost::unary(PropCost::HI); 541 } 542 543 template<> 544 /// Traits for Boolean negation view 545 class BoolNegTraits<BoolView> { 546 public: 547 /// The negated view 548 typedef NegBoolView NegView; 549 /// Return negated View neg(BoolView x)550 static NegBoolView neg(BoolView x) { 551 NegBoolView y(x); return y; 552 } 553 }; 554 555 template<> 556 /// Traits for Boolean negation view 557 class BoolNegTraits<NegBoolView> { 558 public: 559 /// The negated view 560 typedef BoolView NegView; 561 /// Return negated View neg(NegBoolView x)562 static BoolView neg(NegBoolView x) { 563 return x.base(); 564 } 565 }; 566 567 568 /* 569 * Reified greater or equal propagator (integer rhs) 570 * 571 */ 572 template<class VX, class VB, ReifyMode rm> 573 forceinline ReGqBoolInt(Home home,ViewArray<VX> & x,int c,VB b)574 ReGqBoolInt<VX,VB,rm>::ReGqBoolInt(Home home, ViewArray<VX>& x, int c, VB b) 575 : ReLinBoolInt<VX,VB>(home,x,c,b) {} 576 577 template<class VX, class VB, ReifyMode rm> 578 forceinline ReGqBoolInt(Space & home,ReGqBoolInt<VX,VB,rm> & p)579 ReGqBoolInt<VX,VB,rm>::ReGqBoolInt(Space& home, ReGqBoolInt<VX,VB,rm>& p) 580 : ReLinBoolInt<VX,VB>(home,p) {} 581 582 template<class VX, class VB, ReifyMode rm> 583 Actor* copy(Space & home)584 ReGqBoolInt<VX,VB,rm>::copy(Space& home) { 585 return new (home) ReGqBoolInt<VX,VB,rm>(home,*this); 586 } 587 588 template<class VX, class VB, ReifyMode rm> 589 ExecStatus advise(Space &,Advisor &,const Delta & d)590 ReGqBoolInt<VX,VB,rm>::advise(Space&, Advisor&, const Delta& d) { 591 if (VX::one(d)) 592 c--; 593 n_s--; 594 if ((n_s < c) || (c <= 0)) 595 return ES_NOFIX; 596 else 597 return ES_FIX; 598 } 599 600 template<class VX, class VB, ReifyMode rm> 601 void reschedule(Space & home)602 ReGqBoolInt<VX,VB,rm>::reschedule(Space& home) { 603 b.reschedule(home,*this,PC_BOOL_VAL); 604 if ((n_s < c) || (c <= 0)) 605 VX::schedule(home,*this,ME_BOOL_VAL); 606 } 607 608 template<class VX, class VB, ReifyMode rm> 609 ExecStatus propagate(Space & home,const ModEventDelta &)610 ReGqBoolInt<VX,VB,rm>::propagate(Space& home, const ModEventDelta&) { 611 if (b.none()) { 612 if (c <= 0) { 613 if (rm != RM_IMP) 614 GECODE_ME_CHECK(b.one_none(home)); 615 } else { 616 if (rm != RM_PMI) 617 GECODE_ME_CHECK(b.zero_none(home)); 618 } 619 } else { 620 normalize(); 621 if (b.one()) { 622 if (rm != RM_PMI) 623 GECODE_REWRITE(*this,(GqBoolInt<VX>::post(home(*this),x,c))); 624 } else { 625 if (rm != RM_IMP) { 626 ViewArray<typename BoolNegTraits<VX>::NegView> nx(home,x.size()); 627 for (int i=0; i<x.size(); i++) 628 nx[i]=BoolNegTraits<VX>::neg(x[i]); 629 GECODE_REWRITE(*this,GqBoolInt<typename BoolNegTraits<VX>::NegView> 630 ::post(home(*this),nx,x.size()-c+1)); 631 } 632 } 633 } 634 return home.ES_SUBSUMED(*this); 635 } 636 637 template<class VX, class VB, ReifyMode rm> 638 ExecStatus post(Home home,ViewArray<VX> & x,int c,VB b)639 ReGqBoolInt<VX,VB,rm>::post(Home home, ViewArray<VX>& x, int c, VB b) { 640 assert(!b.assigned()); // checked before posting 641 642 // Eliminate assigned views 643 int n_x = x.size(); 644 for (int i=n_x; i--; ) 645 if (x[i].zero()) { 646 x[i] = x[--n_x]; 647 } else if (x[i].one()) { 648 x[i] = x[--n_x]; c--; 649 } 650 x.size(n_x); 651 if (n_x < c) { 652 // RHS too large 653 if (rm != RM_PMI) 654 GECODE_ME_CHECK(b.zero_none(home)); 655 } else if (c <= 0) { 656 // Whatever the x[i] take for values, the inequality is subsumed 657 if (rm != RM_IMP) 658 GECODE_ME_CHECK(b.one_none(home)); 659 } else if ((c == 1) && (rm == RM_EQV)) { 660 // Equivalent to Boolean disjunction 661 return Bool::NaryOr<VX,VB>::post(home,x,b); 662 } else if ((c == n_x) && (rm == RM_EQV)) { 663 // Equivalent to Boolean conjunction, transform to Boolean disjunction 664 ViewArray<typename BoolNegTraits<VX>::NegView> nx(home,n_x); 665 for (int i=0; i<n_x; i++) 666 nx[i]=BoolNegTraits<VX>::neg(x[i]); 667 return Bool::NaryOr 668 <typename BoolNegTraits<VX>::NegView, 669 typename BoolNegTraits<VB>::NegView> 670 ::post(home,nx,BoolNegTraits<VB>::neg(b)); 671 } else { 672 (void) new (home) ReGqBoolInt<VX,VB,rm>(home,x,c,b); 673 } 674 return ES_OK; 675 } 676 677 /* 678 * Reified equal propagator (integer rhs) 679 * 680 */ 681 template<class VX, class VB, ReifyMode rm> 682 forceinline ReEqBoolInt(Home home,ViewArray<VX> & x,int c,VB b)683 ReEqBoolInt<VX,VB,rm>::ReEqBoolInt(Home home, ViewArray<VX>& x, int c, VB b) 684 : ReLinBoolInt<VX,VB>(home,x,c,b) {} 685 686 template<class VX, class VB, ReifyMode rm> 687 forceinline ReEqBoolInt(Space & home,ReEqBoolInt<VX,VB,rm> & p)688 ReEqBoolInt<VX,VB,rm>::ReEqBoolInt(Space& home, ReEqBoolInt<VX,VB,rm>& p) 689 : ReLinBoolInt<VX,VB>(home,p) {} 690 691 template<class VX, class VB, ReifyMode rm> 692 Actor* copy(Space & home)693 ReEqBoolInt<VX,VB,rm>::copy(Space& home) { 694 return new (home) ReEqBoolInt<VX,VB,rm>(home,*this); 695 } 696 697 template<class VX, class VB, ReifyMode rm> 698 ExecStatus advise(Space &,Advisor &,const Delta & d)699 ReEqBoolInt<VX,VB,rm>::advise(Space&, Advisor&, const Delta& d) { 700 if (VX::one(d)) 701 c--; 702 n_s--; 703 704 if ((c < 0) || (c > n_s) || (n_s == 0)) 705 return ES_NOFIX; 706 else 707 return ES_FIX; 708 } 709 710 template<class VX, class VB, ReifyMode rm> 711 void reschedule(Space & home)712 ReEqBoolInt<VX,VB,rm>::reschedule(Space& home) { 713 b.reschedule(home,*this,PC_BOOL_VAL); 714 if ((c < 0) || (c > n_s) || (n_s == 0)) 715 VX::schedule(home,*this,ME_BOOL_VAL); 716 } 717 718 template<class VX, class VB, ReifyMode rm> 719 ExecStatus propagate(Space & home,const ModEventDelta &)720 ReEqBoolInt<VX,VB,rm>::propagate(Space& home, const ModEventDelta&) { 721 if (b.none()) { 722 if ((c == 0) && (n_s == 0)) { 723 if (rm != RM_IMP) 724 GECODE_ME_CHECK(b.one_none(home)); 725 } else { 726 if (rm != RM_PMI) 727 GECODE_ME_CHECK(b.zero_none(home)); 728 } 729 } else { 730 normalize(); 731 if (b.one()) { 732 if (rm != RM_PMI) 733 GECODE_REWRITE(*this,(EqBoolInt<VX>::post(home(*this),x,c))); 734 } else { 735 if (rm != RM_IMP) 736 GECODE_REWRITE(*this,(NqBoolInt<VX>::post(home(*this),x,c))); 737 } 738 } 739 return home.ES_SUBSUMED(*this); 740 } 741 742 template<class VX, class VB, ReifyMode rm> 743 ExecStatus post(Home home,ViewArray<VX> & x,int c,VB b)744 ReEqBoolInt<VX,VB,rm>::post(Home home, ViewArray<VX>& x, int c, VB b) { 745 assert(!b.assigned()); // checked before posting 746 747 // Eliminate assigned views 748 int n_x = x.size(); 749 for (int i=n_x; i--; ) 750 if (x[i].zero()) { 751 x[i] = x[--n_x]; 752 } else if (x[i].one()) { 753 x[i] = x[--n_x]; c--; 754 } 755 x.size(n_x); 756 if ((n_x < c) || (c < 0)) { 757 // RHS too large 758 if (rm != RM_PMI) 759 GECODE_ME_CHECK(b.zero_none(home)); 760 } else if ((c == 0) && (n_x == 0)) { 761 // all variables set, and c == 0: equality 762 if (rm != RM_IMP) 763 GECODE_ME_CHECK(b.one_none(home)); 764 } else if ((c == 0) && (rm == RM_EQV)) { 765 // Equivalent to Boolean disjunction 766 return Bool::NaryOr<VX,typename BoolNegTraits<VB>::NegView> 767 ::post(home,x,BoolNegTraits<VB>::neg(b)); 768 } else if ((c == n_x) && (rm == RM_EQV)) { 769 // Equivalent to Boolean conjunction, transform to Boolean disjunction 770 ViewArray<typename BoolNegTraits<VX>::NegView> nx(home,n_x); 771 for (int i=0; i<n_x; i++) 772 nx[i]=BoolNegTraits<VX>::neg(x[i]); 773 return Bool::NaryOr 774 <typename BoolNegTraits<VX>::NegView, 775 typename BoolNegTraits<VB>::NegView> 776 ::post(home,nx,BoolNegTraits<VB>::neg(b)); 777 } else { 778 (void) new (home) ReEqBoolInt<VX,VB,rm>(home,x,c,b); 779 } 780 return ES_OK; 781 } 782 783 784 }}} 785 786 // STATISTICS: int-prop 787 788