bool-int.hpp
Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 00002 /* 00003 * Main authors: 00004 * Christian Schulte <schulte@gecode.org> 00005 * Tias Guns <tias.guns@cs.kuleuven.be> 00006 * 00007 * Copyright: 00008 * Christian Schulte, 2006 00009 * Tias Guns, 2009 00010 * 00011 * Last modified: 00012 * $Date: 2010-04-08 12:35:31 +0200 (Thu, 08 Apr 2010) $ by $Author: schulte $ 00013 * $Revision: 10684 $ 00014 * 00015 * This file is part of Gecode, the generic constraint 00016 * development environment: 00017 * http://www.gecode.org 00018 * 00019 * Permission is hereby granted, free of charge, to any person obtaining 00020 * a copy of this software and associated documentation files (the 00021 * "Software"), to deal in the Software without restriction, including 00022 * without limitation the rights to use, copy, modify, merge, publish, 00023 * distribute, sublicense, and/or sell copies of the Software, and to 00024 * permit persons to whom the Software is furnished to do so, subject to 00025 * the following conditions: 00026 * 00027 * The above copyright notice and this permission notice shall be 00028 * included in all copies or substantial portions of the Software. 00029 * 00030 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 00031 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 00032 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 00033 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE 00034 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION 00035 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION 00036 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 00037 * 00038 */ 00039 00040 #include <algorithm> 00041 00042 #include <gecode/int/bool.hh> 00043 00044 namespace Gecode { namespace Int { namespace Linear { 00045 00046 /* 00047 * Baseclass for integer Boolean sum using dependencies 00048 * 00049 */ 00050 template<class VX> 00051 forceinline 00052 LinBoolInt<VX>::LinBoolInt(Home home, ViewArray<VX>& x0, 00053 int n_s, int c0) 00054 : Propagator(home), co(home), x(x0), n_as(n_s), n_hs(n_s), c(c0) { 00055 Advisor* a = new (home) Advisor(home,*this,co); 00056 for (int i=n_as; i--; ) 00057 x[i].subscribe(home,*a); 00058 } 00059 00060 template<class VX> 00061 forceinline void 00062 LinBoolInt<VX>::normalize(void) { 00063 if (n_as != n_hs) { 00064 // Remove views for which no more subscriptions exist 00065 int n_x = x.size(); 00066 for (int i=n_hs; i--; ) 00067 if (!x[i].none()) { 00068 x[i]=x[--n_hs]; x[n_hs]=x[--n_x]; 00069 } 00070 x.size(n_x); 00071 } 00072 assert(n_as == n_hs); 00073 // Remove assigned yet unsubscribed views 00074 { 00075 int n_x = x.size(); 00076 for (int i=n_x-1; i>=n_hs; i--) 00077 if (x[i].one()) { 00078 c--; x[i]=x[--n_x]; 00079 } else if (x[i].zero()) { 00080 x[i]=x[--n_x]; 00081 } 00082 x.size(n_x); 00083 } 00084 } 00085 00086 template<class VX> 00087 forceinline 00088 LinBoolInt<VX>::LinBoolInt(Space& home, bool share, LinBoolInt<VX>& p) 00089 : Propagator(home,share,p), n_as(p.n_as), n_hs(n_as) { 00090 p.normalize(); 00091 c=p.c; 00092 co.update(home,share,p.co); 00093 x.update(home,share,p.x); 00094 } 00095 00096 template<class VX> 00097 PropCost 00098 LinBoolInt<VX>::cost(const Space&, const ModEventDelta&) const { 00099 return PropCost::unary(PropCost::HI); 00100 } 00101 00102 template<class VX> 00103 forceinline size_t 00104 LinBoolInt<VX>::dispose(Space& home) { 00105 Advisors<Advisor> as(co); 00106 for (int i=n_hs; i--; ) 00107 x[i].cancel(home,as.advisor()); 00108 co.dispose(home); 00109 (void) Propagator::dispose(home); 00110 return sizeof(*this); 00111 } 00112 00113 /* 00114 * Greater or equal propagator (integer rhs) 00115 * 00116 */ 00117 template<class VX> 00118 forceinline 00119 GqBoolInt<VX>::GqBoolInt(Home home, ViewArray<VX>& x, int c) 00120 : LinBoolInt<VX>(home,x,c+1,c) {} 00121 00122 template<class VX> 00123 forceinline 00124 GqBoolInt<VX>::GqBoolInt(Space& home, bool share, GqBoolInt<VX>& p) 00125 : LinBoolInt<VX>(home,share,p) {} 00126 00127 template<class VX> 00128 Actor* 00129 GqBoolInt<VX>::copy(Space& home, bool share) { 00130 return new (home) GqBoolInt<VX>(home,share,*this); 00131 } 00132 00133 template<class VX> 00134 ExecStatus 00135 GqBoolInt<VX>::advise(Space& home, Advisor& a, const Delta& d) { 00136 // Check whether propagator is running 00137 if (n_as == 0) 00138 return ES_FIX; 00139 00140 if (VX::one(d)) { 00141 c--; goto check; 00142 } 00143 if (c+1 < n_as) 00144 goto check; 00145 // Find a new subscription 00146 for (int i = x.size()-1; i>=n_hs; i--) 00147 if (x[i].none()) { 00148 std::swap(x[i],x[n_hs]); 00149 x[n_hs++].subscribe(home,a); 00150 x.size(i+1); 00151 return ES_FIX; 00152 } else if (x[i].one()) { 00153 c--; 00154 if (c+1 < n_as) { 00155 x.size(i); 00156 assert(n_hs <= x.size()); 00157 goto check; 00158 } 00159 } 00160 // No view left for subscription 00161 x.size(n_hs); 00162 check: 00163 // Do not update subscription 00164 n_as--; 00165 int n = x.size()-n_hs+n_as; 00166 if (n < c) 00167 return ES_FAILED; 00168 if ((c <= 0) || (c == n)) 00169 return ES_NOFIX; 00170 else 00171 return ES_FIX; 00172 } 00173 00174 template<class VX> 00175 ExecStatus 00176 GqBoolInt<VX>::propagate(Space& home, const ModEventDelta&) { 00177 if (c > 0) { 00178 assert((n_as == c) && (x.size() == n_hs)); 00179 // Signal that propagator is running 00180 n_as = 0; 00181 // All views must be one to satisfy inequality 00182 for (int i=n_hs; i--; ) 00183 if (x[i].none()) 00184 GECODE_ME_CHECK(x[i].one_none(home)); 00185 } 00186 return home.ES_SUBSUMED(*this); 00187 } 00188 00189 template<class VX> 00190 ExecStatus 00191 GqBoolInt<VX>::post(Home home, ViewArray<VX>& x, int c) { 00192 // Eliminate assigned views 00193 int n_x = x.size(); 00194 for (int i=n_x; i--; ) 00195 if (x[i].zero()) { 00196 x[i] = x[--n_x]; 00197 } else if (x[i].one()) { 00198 x[i] = x[--n_x]; c--; 00199 } 00200 x.size(n_x); 00201 // RHS too large 00202 if (n_x < c) 00203 return ES_FAILED; 00204 // Whatever the x[i] take for values, the inequality is subsumed 00205 if (c <= 0) 00206 return ES_OK; 00207 // Use Boolean disjunction for this special case 00208 if (c == 1) 00209 return Bool::NaryOrTrue<VX>::post(home,x); 00210 // All views must be one to satisfy inequality 00211 if (c == n_x) { 00212 for (int i=n_x; i--; ) 00213 GECODE_ME_CHECK(x[i].one_none(home)); 00214 return ES_OK; 00215 } 00216 // This is the needed invariant as c+1 subscriptions must be created 00217 assert(n_x > c); 00218 (void) new (home) GqBoolInt<VX>(home,x,c); 00219 return ES_OK; 00220 } 00221 00222 00223 00224 00225 /* 00226 * Equal propagator (integer rhs) 00227 * 00228 */ 00229 template<class VX> 00230 forceinline 00231 EqBoolInt<VX>::EqBoolInt(Home home, ViewArray<VX>& x, int c) 00232 : LinBoolInt<VX>(home,x,std::max(c,x.size()-c)+1,c) {} 00233 00234 template<class VX> 00235 forceinline 00236 EqBoolInt<VX>::EqBoolInt(Space& home, bool share, EqBoolInt<VX>& p) 00237 : LinBoolInt<VX>(home,share,p) {} 00238 00239 template<class VX> 00240 Actor* 00241 EqBoolInt<VX>::copy(Space& home, bool share) { 00242 return new (home) EqBoolInt<VX>(home,share,*this); 00243 } 00244 00245 template<class VX> 00246 ExecStatus 00247 EqBoolInt<VX>::advise(Space& home, Advisor& a, const Delta& d) { 00248 // Check whether propagator is running 00249 if (n_as == 0) 00250 return ES_FIX; 00251 00252 if (VX::one(d)) 00253 c--; 00254 if ((c+1 < n_as) && (x.size()-n_hs < c)) 00255 goto check; 00256 // Find a new subscription 00257 for (int i = x.size()-1; i>=n_hs; i--) 00258 if (x[i].none()) { 00259 std::swap(x[i],x[n_hs]); 00260 x[n_hs++].subscribe(home,a); 00261 x.size(i+1); 00262 return ES_FIX; 00263 } else if (x[i].one()) { 00264 c--; 00265 } 00266 // No view left for subscription 00267 x.size(n_hs); 00268 check: 00269 // Do not update subscription 00270 n_as--; 00271 int n = x.size()-n_hs+n_as; 00272 if ((c < 0) || (c > n)) 00273 return ES_FAILED; 00274 if ((c == 0) || (c == n)) 00275 return ES_NOFIX; 00276 else 00277 return ES_FIX; 00278 } 00279 00280 template<class VX> 00281 ExecStatus 00282 EqBoolInt<VX>::propagate(Space& home, const ModEventDelta&) { 00283 assert(x.size() == n_hs); 00284 // Signal that propagator is running 00285 n_as = 0; 00286 if (c == 0) { 00287 // All views must be zero to satisfy equality 00288 for (int i=n_hs; i--; ) 00289 if (x[i].none()) 00290 GECODE_ME_CHECK(x[i].zero_none(home)); 00291 } else { 00292 // All views must be one to satisfy equality 00293 for (int i=n_hs; i--; ) 00294 if (x[i].none()) 00295 GECODE_ME_CHECK(x[i].one_none(home)); 00296 } 00297 return home.ES_SUBSUMED(*this); 00298 } 00299 00300 template<class VX> 00301 ExecStatus 00302 EqBoolInt<VX>::post(Home home, ViewArray<VX>& x, int c) { 00303 // Eliminate assigned views 00304 int n_x = x.size(); 00305 for (int i=n_x; i--; ) 00306 if (x[i].zero()) { 00307 x[i] = x[--n_x]; 00308 } else if (x[i].one()) { 00309 x[i] = x[--n_x]; c--; 00310 } 00311 x.size(n_x); 00312 // RHS too small or too large 00313 if ((c < 0) || (c > n_x)) 00314 return ES_FAILED; 00315 // All views must be zero to satisfy equality 00316 if (c == 0) { 00317 for (int i=n_x; i--; ) 00318 GECODE_ME_CHECK(x[i].zero_none(home)); 00319 return ES_OK; 00320 } 00321 // All views must be one to satisfy equality 00322 if (c == n_x) { 00323 for (int i=n_x; i--; ) 00324 GECODE_ME_CHECK(x[i].one_none(home)); 00325 return ES_OK; 00326 } 00327 (void) new (home) EqBoolInt<VX>(home,x,c); 00328 return ES_OK; 00329 } 00330 00331 00332 /* 00333 * Integer disequal to Boolean sum 00334 * 00335 */ 00336 00337 template<class VX> 00338 forceinline 00339 NqBoolInt<VX>::NqBoolInt(Home home, ViewArray<VX>& b, int c0) 00340 : BinaryPropagator<VX,PC_INT_VAL>(home, 00341 b[b.size()-2], 00342 b[b.size()-1]), x(b), c(c0) { 00343 assert(x.size() >= 2); 00344 x.size(x.size()-2); 00345 } 00346 00347 template<class VX> 00348 forceinline size_t 00349 NqBoolInt<VX>::dispose(Space& home) { 00350 (void) BinaryPropagator<VX,PC_INT_VAL>::dispose(home); 00351 return sizeof(*this); 00352 } 00353 00354 template<class VX> 00355 forceinline 00356 NqBoolInt<VX>::NqBoolInt(Space& home, bool share, NqBoolInt<VX>& p) 00357 : BinaryPropagator<VX,PC_INT_VAL>(home,share,p), x(home,p.x.size()) { 00358 // Eliminate all zeros and ones in original and update 00359 int n = p.x.size(); 00360 int p_c = p.c; 00361 for (int i=n; i--; ) 00362 if (p.x[i].zero()) { 00363 n--; p.x[i]=p.x[n]; x[i]=x[n]; 00364 } else if (p.x[i].one()) { 00365 n--; p_c--; p.x[i]=p.x[n]; x[i]=x[n]; 00366 } else { 00367 x[i].update(home,share,p.x[i]); 00368 } 00369 c = p_c; p.c = p_c; 00370 x.size(n); p.x.size(n); 00371 } 00372 00373 template<class VX> 00374 forceinline ExecStatus 00375 NqBoolInt<VX>::post(Home home, ViewArray<VX>& x, int c) { 00376 int n = x.size(); 00377 for (int i=n; i--; ) 00378 if (x[i].one()) { 00379 x[i]=x[--n]; c--; 00380 } else if (x[i].zero()) { 00381 x[i]=x[--n]; 00382 } 00383 x.size(n); 00384 if ((n < c) || (c < 0)) 00385 return ES_OK; 00386 if (n == 0) 00387 return (c == 0) ? ES_FAILED : ES_OK; 00388 if (n == 1) { 00389 if (c == 1) { 00390 GECODE_ME_CHECK(x[0].zero_none(home)); 00391 } else { 00392 GECODE_ME_CHECK(x[0].one_none(home)); 00393 } 00394 return ES_OK; 00395 } 00396 (void) new (home) NqBoolInt(home,x,c); 00397 return ES_OK; 00398 } 00399 00400 template<class VX> 00401 Actor* 00402 NqBoolInt<VX>::copy(Space& home, bool share) { 00403 return new (home) NqBoolInt<VX>(home,share,*this); 00404 } 00405 00406 template<class VX> 00407 PropCost 00408 NqBoolInt<VX>::cost(const Space&, const ModEventDelta&) const { 00409 return PropCost::linear(PropCost::LO, x.size()); 00410 } 00411 00412 template<class VX> 00413 forceinline bool 00414 NqBoolInt<VX>::resubscribe(Space& home, VX& y) { 00415 if (y.one()) 00416 c--; 00417 int n = x.size(); 00418 for (int i=n; i--; ) 00419 if (x[i].one()) { 00420 c--; x[i]=x[--n]; 00421 } else if (x[i].zero()) { 00422 x[i] = x[--n]; 00423 } else { 00424 // New unassigned view found 00425 assert(!x[i].zero() && !x[i].one()); 00426 // Move to y and subscribe 00427 y=x[i]; x[i]=x[--n]; 00428 x.size(n); 00429 y.subscribe(home,*this,PC_INT_VAL,false); 00430 return true; 00431 } 00432 // All views have been assigned! 00433 x.size(0); 00434 return false; 00435 } 00436 00437 template<class VX> 00438 ExecStatus 00439 NqBoolInt<VX>::propagate(Space& home, const ModEventDelta&) { 00440 bool s0 = true; 00441 if (x0.zero() || x0.one()) 00442 s0 = resubscribe(home,x0); 00443 bool s1 = true; 00444 if (x1.zero() || x1.one()) 00445 s1 = resubscribe(home,x1); 00446 int n = x.size() + s0 + s1; 00447 if ((n < c) || (c < 0)) 00448 return home.ES_SUBSUMED(*this); 00449 if (n == 0) 00450 return (c == 0) ? ES_FAILED : home.ES_SUBSUMED(*this); 00451 if (n == 1) { 00452 if (s0) { 00453 if (c == 1) { 00454 GECODE_ME_CHECK(x0.zero_none(home)); 00455 } else { 00456 GECODE_ME_CHECK(x0.one_none(home)); 00457 } 00458 } else { 00459 assert(s1); 00460 if (c == 1) { 00461 GECODE_ME_CHECK(x1.zero_none(home)); 00462 } else { 00463 GECODE_ME_CHECK(x1.one_none(home)); 00464 } 00465 } 00466 return home.ES_SUBSUMED(*this); 00467 } 00468 return ES_FIX; 00469 } 00470 00471 /* 00472 * Baseclass for reified integer Boolean sum 00473 * 00474 */ 00475 template<class VX, class VB> 00476 forceinline 00477 ReLinBoolInt<VX,VB>::ReLinBoolInt(Home home, ViewArray<VX>& x0, 00478 int c0, VB b0) 00479 : Propagator(home), co(home), x(x0), n_s(x.size()), c(c0), b(b0) { 00480 x.subscribe(home,*new (home) Advisor(home,*this,co)); 00481 b.subscribe(home,*this,PC_BOOL_VAL); 00482 } 00483 00484 template<class VX, class VB> 00485 forceinline void 00486 ReLinBoolInt<VX,VB>::normalize(void) { 00487 if (n_s != x.size()) { 00488 int n_x = x.size(); 00489 for (int i=n_x; i--; ) 00490 if (!x[i].none()) 00491 x[i] = x[--n_x]; 00492 x.size(n_x); 00493 assert(x.size() == n_s); 00494 } 00495 } 00496 00497 template<class VX, class VB> 00498 forceinline 00499 ReLinBoolInt<VX,VB>::ReLinBoolInt(Space& home, bool share, 00500 ReLinBoolInt<VX,VB>& p) 00501 : Propagator(home,share,p), n_s(p.n_s), c(p.c) { 00502 p.normalize(); 00503 co.update(home,share,p.co); 00504 x.update(home,share,p.x); 00505 b.update(home,share,p.b); 00506 } 00507 00508 template<class VX, class VB> 00509 forceinline size_t 00510 ReLinBoolInt<VX,VB>::dispose(Space& home) { 00511 Advisors<Advisor> as(co); 00512 x.cancel(home,as.advisor()); 00513 co.dispose(home); 00514 b.cancel(home,*this,PC_BOOL_VAL); 00515 (void) Propagator::dispose(home); 00516 return sizeof(*this); 00517 } 00518 00519 template<class VX, class VB> 00520 PropCost 00521 ReLinBoolInt<VX,VB>::cost(const Space&, const ModEventDelta&) const { 00522 return PropCost::unary(PropCost::HI); 00523 } 00524 00525 00526 template<> 00528 class BoolNegTraits<BoolView> { 00529 public: 00531 typedef NegBoolView NegView; 00533 static NegBoolView neg(BoolView x) { 00534 NegBoolView y(x); return y; 00535 } 00536 }; 00537 00538 template<> 00540 class BoolNegTraits<NegBoolView> { 00541 public: 00543 typedef BoolView NegView; 00545 static BoolView neg(NegBoolView x) { 00546 return x.base(); 00547 } 00548 }; 00549 00550 00551 /* 00552 * Reified greater or equal propagator (integer rhs) 00553 * 00554 */ 00555 template<class VX, class VB> 00556 forceinline 00557 ReGqBoolInt<VX,VB>::ReGqBoolInt(Home home, ViewArray<VX>& x, int c, VB b) 00558 : ReLinBoolInt<VX,VB>(home,x,c,b) {} 00559 00560 template<class VX, class VB> 00561 forceinline 00562 ReGqBoolInt<VX,VB>::ReGqBoolInt(Space& home, bool share, 00563 ReGqBoolInt<VX,VB>& p) 00564 : ReLinBoolInt<VX,VB>(home,share,p) {} 00565 00566 template<class VX, class VB> 00567 Actor* 00568 ReGqBoolInt<VX,VB>::copy(Space& home, bool share) { 00569 return new (home) ReGqBoolInt<VX,VB>(home,share,*this); 00570 } 00571 00572 template<class VX, class VB> 00573 ExecStatus 00574 ReGqBoolInt<VX,VB>::advise(Space&, Advisor&, const Delta& d) { 00575 if (VX::one(d)) 00576 c--; 00577 n_s--; 00578 if ((n_s < c) || (c <= 0)) 00579 return ES_NOFIX; 00580 else 00581 return ES_FIX; 00582 } 00583 00584 template<class VX, class VB> 00585 ExecStatus 00586 ReGqBoolInt<VX,VB>::propagate(Space& home, const ModEventDelta&) { 00587 if (b.none()) { 00588 if (c <= 0) { 00589 GECODE_ME_CHECK(b.one_none(home)); 00590 } else { 00591 GECODE_ME_CHECK(b.zero_none(home)); 00592 } 00593 } else { 00594 normalize(); 00595 if (b.one()) { 00596 GECODE_REWRITE(*this,(GqBoolInt<VX>::post(home(*this),x,c))); 00597 } else { 00598 ViewArray<typename BoolNegTraits<VX>::NegView> nx(home,x.size()); 00599 for (int i=x.size(); i--; ) 00600 nx[i]=BoolNegTraits<VX>::neg(x[i]); 00601 GECODE_REWRITE(*this,GqBoolInt<typename BoolNegTraits<VX>::NegView> 00602 ::post(home(*this),nx,x.size()-c+1)); 00603 } 00604 } 00605 return home.ES_SUBSUMED(*this); 00606 } 00607 00608 template<class VX, class VB> 00609 ExecStatus 00610 ReGqBoolInt<VX,VB>::post(Home home, ViewArray<VX>& x, int c, VB b) { 00611 assert(!b.assigned()); // checked before posting 00612 00613 // Eliminate assigned views 00614 int n_x = x.size(); 00615 for (int i=n_x; i--; ) 00616 if (x[i].zero()) { 00617 x[i] = x[--n_x]; 00618 } else if (x[i].one()) { 00619 x[i] = x[--n_x]; c--; 00620 } 00621 x.size(n_x); 00622 if (n_x < c) { 00623 // RHS too large 00624 GECODE_ME_CHECK(b.zero_none(home)); 00625 } else if (c <= 0) { 00626 // Whatever the x[i] take for values, the inequality is subsumed 00627 GECODE_ME_CHECK(b.one_none(home)); 00628 } else if (c == 1) { 00629 // Equivalent to Boolean disjunction 00630 return Bool::NaryOr<VX,VB>::post(home,x,b); 00631 } else if (c == n_x) { 00632 // Equivalent to Boolean conjunction, transform to Boolean disjunction 00633 ViewArray<typename BoolNegTraits<VX>::NegView> nx(home,n_x); 00634 for (int i=n_x; i--; ) 00635 nx[i]=BoolNegTraits<VX>::neg(x[i]); 00636 return Bool::NaryOr 00637 <typename BoolNegTraits<VX>::NegView, 00638 typename BoolNegTraits<VB>::NegView> 00639 ::post(home,nx,BoolNegTraits<VB>::neg(b)); 00640 } else { 00641 (void) new (home) ReGqBoolInt<VX,VB>(home,x,c,b); 00642 } 00643 return ES_OK; 00644 } 00645 00646 /* 00647 * Reified equal propagator (integer rhs) 00648 * 00649 */ 00650 template<class VX, class VB> 00651 forceinline 00652 ReEqBoolInt<VX,VB>::ReEqBoolInt(Home home, ViewArray<VX>& x, int c, VB b) 00653 : ReLinBoolInt<VX,VB>(home,x,c,b) {} 00654 00655 template<class VX, class VB> 00656 forceinline 00657 ReEqBoolInt<VX,VB>::ReEqBoolInt(Space& home, bool share, 00658 ReEqBoolInt<VX,VB>& p) 00659 : ReLinBoolInt<VX,VB>(home,share,p) {} 00660 00661 template<class VX, class VB> 00662 Actor* 00663 ReEqBoolInt<VX,VB>::copy(Space& home, bool share) { 00664 return new (home) ReEqBoolInt<VX,VB>(home,share,*this); 00665 } 00666 00667 template<class VX, class VB> 00668 ExecStatus 00669 ReEqBoolInt<VX,VB>::advise(Space&, Advisor&, const Delta& d) { 00670 if (VX::one(d)) 00671 c--; 00672 n_s--; 00673 00674 if ((c < 0) || (c > n_s) || (n_s == 0)) 00675 return ES_NOFIX; 00676 else 00677 return ES_FIX; 00678 } 00679 00680 template<class VX, class VB> 00681 ExecStatus 00682 ReEqBoolInt<VX,VB>::propagate(Space& home, const ModEventDelta&) { 00683 if (b.none()) { 00684 if ((c == 0) && (n_s == 0)) { 00685 GECODE_ME_CHECK(b.one_none(home)); 00686 } else { 00687 GECODE_ME_CHECK(b.zero_none(home)); 00688 } 00689 } else { 00690 normalize(); 00691 if (b.one()) { 00692 GECODE_REWRITE(*this,(EqBoolInt<VX>::post(home(*this),x,c))); 00693 } else { 00694 GECODE_REWRITE(*this,(NqBoolInt<VX>::post(home(*this),x,c))); 00695 } 00696 } 00697 return home.ES_SUBSUMED(*this); 00698 } 00699 00700 template<class VX, class VB> 00701 ExecStatus 00702 ReEqBoolInt<VX,VB>::post(Home home, ViewArray<VX>& x, int c, VB b) { 00703 assert(!b.assigned()); // checked before posting 00704 00705 // Eliminate assigned views 00706 int n_x = x.size(); 00707 for (int i=n_x; i--; ) 00708 if (x[i].zero()) { 00709 x[i] = x[--n_x]; 00710 } else if (x[i].one()) { 00711 x[i] = x[--n_x]; c--; 00712 } 00713 x.size(n_x); 00714 if ((n_x < c) || (c < 0)) { 00715 // RHS too large 00716 GECODE_ME_CHECK(b.zero_none(home)); 00717 } else if ((c == 0) && (n_x == 0)) { 00718 // all variables set, and c == 0: equality 00719 GECODE_ME_CHECK(b.one_none(home)); 00720 } else if (c == 0) { 00721 // Equivalent to Boolean disjunction 00722 return Bool::NaryOr<VX,typename BoolNegTraits<VB>::NegView> 00723 ::post(home,x,BoolNegTraits<VB>::neg(b)); 00724 } else if (c == n_x) { 00725 // Equivalent to Boolean conjunction, transform to Boolean disjunction 00726 ViewArray<typename BoolNegTraits<VX>::NegView> nx(home,n_x); 00727 for (int i=n_x; i--; ) 00728 nx[i]=BoolNegTraits<VX>::neg(x[i]); 00729 return Bool::NaryOr 00730 <typename BoolNegTraits<VX>::NegView, 00731 typename BoolNegTraits<VB>::NegView> 00732 ::post(home,nx,BoolNegTraits<VB>::neg(b)); 00733 } else { 00734 (void) new (home) ReEqBoolInt<VX,VB>(home,x,c,b); 00735 } 00736 return ES_OK; 00737 } 00738 00739 00740 }}} 00741 00742 // STATISTICS: int-prop 00743