gecode » int » linear
bool-int.hpp

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: 2009-10-20 11:15:31 +0200 (Tue, 20 Oct 2009) $ by $Author: schulte $
00013  *     $Revision: 9973 $
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     assert(!home.failed());
00106     Advisors<Advisor> as(co);
00107     for (int i=n_hs; i--; )
00108       x[i].cancel(home,as.advisor());
00109     co.dispose(home);
00110     (void) Propagator::dispose(home);
00111     return sizeof(*this);
00112   }
00113 
00114   /*
00115    * Greater or equal propagator (integer rhs)
00116    *
00117    */
00118   template<class VX>
00119   forceinline
00120   GqBoolInt<VX>::GqBoolInt(Home home, ViewArray<VX>& x, int c)
00121     : LinBoolInt<VX>(home,x,c+1,c) {}
00122 
00123   template<class VX>
00124   forceinline
00125   GqBoolInt<VX>::GqBoolInt(Space& home, bool share, GqBoolInt<VX>& p)
00126     : LinBoolInt<VX>(home,share,p) {}
00127 
00128   template<class VX>
00129   Actor*
00130   GqBoolInt<VX>::copy(Space& home, bool share) {
00131     return new (home) GqBoolInt<VX>(home,share,*this);
00132   }
00133 
00134   template<class VX>
00135   ExecStatus
00136   GqBoolInt<VX>::advise(Space& home, Advisor& a, const Delta& d) {
00137     // Check whether propagator is running
00138     if (n_as == 0)
00139       return ES_FIX;
00140 
00141     if (VX::one(d)) {
00142       c--; goto check;
00143     }
00144     if (c+1 < n_as)
00145       goto check;
00146     // Find a new subscription
00147     for (int i = x.size()-1; i>=n_hs; i--)
00148       if (x[i].none()) {
00149         std::swap(x[i],x[n_hs]);
00150         x[n_hs++].subscribe(home,a);
00151         x.size(i+1);
00152         return ES_FIX;
00153       } else if (x[i].one()) {
00154         c--;
00155         if (c+1 < n_as) {
00156           x.size(i);
00157           assert(n_hs <= x.size());
00158           goto check;
00159         }
00160       }
00161     // No view left for subscription
00162     x.size(n_hs);
00163   check:
00164     // Do not update subscription
00165     n_as--;
00166     int n = x.size()-n_hs+n_as;
00167     if (n < c)
00168       return ES_FAILED;
00169     if ((c <= 0) || (c == n))
00170       return ES_NOFIX;
00171     else
00172       return ES_FIX;
00173   }
00174 
00175   template<class VX>
00176   ExecStatus
00177   GqBoolInt<VX>::propagate(Space& home, const ModEventDelta&) {
00178     if (c > 0) {
00179       assert((n_as == c) && (x.size() == n_hs));
00180       // Signal that propagator is running
00181       n_as = 0;
00182       // All views must be one to satisfy inequality
00183       for (int i=n_hs; i--; )
00184         if (x[i].none())
00185           GECODE_ME_CHECK(x[i].one_none(home));
00186     } else {
00187       Advisors<Advisor> as(co);
00188       for (int i=n_hs; i--; )
00189         x[i].cancel(home,as.advisor());
00190     }
00191     co.dispose(home);
00192     return ES_SUBSUMED(*this,sizeof(*this));
00193   }
00194 
00195   template<class VX>
00196   ExecStatus
00197   GqBoolInt<VX>::post(Home home, ViewArray<VX>& x, int c) {
00198     // Eliminate assigned views
00199     int n_x = x.size();
00200     for (int i=n_x; i--; )
00201       if (x[i].zero()) {
00202         x[i] = x[--n_x];
00203       } else if (x[i].one()) {
00204         x[i] = x[--n_x]; c--;
00205       }
00206     x.size(n_x);
00207     // RHS too large
00208     if (n_x < c)
00209       return ES_FAILED;
00210     // Whatever the x[i] take for values, the inequality is subsumed
00211     if (c <= 0)
00212       return ES_OK;
00213     // Use Boolean disjunction for this special case
00214     if (c == 1)
00215       return Bool::NaryOrTrue<VX>::post(home,x);
00216     // All views must be one to satisfy inequality
00217     if (c == n_x) {
00218       for (int i=n_x; i--; )
00219         GECODE_ME_CHECK(x[i].one_none(home));
00220       return ES_OK;
00221     }
00222     // This is the needed invariant as c+1 subscriptions must be created
00223     assert(n_x > c);
00224     (void) new (home) GqBoolInt<VX>(home,x,c);
00225     return ES_OK;
00226   }
00227 
00228 
00229 
00230 
00231   /*
00232    * Equal propagator (integer rhs)
00233    *
00234    */
00235   template<class VX>
00236   forceinline
00237   EqBoolInt<VX>::EqBoolInt(Home home, ViewArray<VX>& x, int c)
00238     : LinBoolInt<VX>(home,x,std::max(c,x.size()-c)+1,c) {}
00239 
00240   template<class VX>
00241   forceinline
00242   EqBoolInt<VX>::EqBoolInt(Space& home, bool share, EqBoolInt<VX>& p)
00243     : LinBoolInt<VX>(home,share,p) {}
00244 
00245   template<class VX>
00246   Actor*
00247   EqBoolInt<VX>::copy(Space& home, bool share) {
00248     return new (home) EqBoolInt<VX>(home,share,*this);
00249   }
00250 
00251   template<class VX>
00252   ExecStatus
00253   EqBoolInt<VX>::advise(Space& home, Advisor& a, const Delta& d) {
00254     // Check whether propagator is running
00255     if (n_as == 0)
00256       return ES_FIX;
00257 
00258     if (VX::one(d))
00259       c--;
00260     if ((c+1 < n_as) && (x.size()-n_hs < c))
00261       goto check;
00262     // Find a new subscription
00263     for (int i = x.size()-1; i>=n_hs; i--)
00264       if (x[i].none()) {
00265         std::swap(x[i],x[n_hs]);
00266         x[n_hs++].subscribe(home,a);
00267         x.size(i+1);
00268         return ES_FIX;
00269       } else if (x[i].one()) {
00270         c--;
00271       }
00272     // No view left for subscription
00273     x.size(n_hs);
00274   check:
00275     // Do not update subscription
00276     n_as--;
00277     int n = x.size()-n_hs+n_as;
00278     if ((c < 0) || (c > n))
00279       return ES_FAILED;
00280     if ((c == 0) || (c == n))
00281       return ES_NOFIX;
00282     else
00283       return ES_FIX;
00284   }
00285 
00286   template<class VX>
00287   ExecStatus
00288   EqBoolInt<VX>::propagate(Space& home, const ModEventDelta&) {
00289     assert(x.size() == n_hs);
00290     // Signal that propagator is running
00291     n_as = 0;
00292     if (c == 0) {
00293       // All views must be zero to satisfy equality
00294       for (int i=n_hs; i--; )
00295         if (x[i].none())
00296           GECODE_ME_CHECK(x[i].zero_none(home));
00297     } else {
00298       // All views must be one to satisfy equality
00299       for (int i=n_hs; i--; )
00300         if (x[i].none())
00301           GECODE_ME_CHECK(x[i].one_none(home));
00302     }
00303     co.dispose(home);
00304     return ES_SUBSUMED(*this,sizeof(*this));
00305   }
00306 
00307   template<class VX>
00308   ExecStatus
00309   EqBoolInt<VX>::post(Home home, ViewArray<VX>& x, int c) {
00310     // Eliminate assigned views
00311     int n_x = x.size();
00312     for (int i=n_x; i--; )
00313       if (x[i].zero()) {
00314         x[i] = x[--n_x];
00315       } else if (x[i].one()) {
00316         x[i] = x[--n_x]; c--;
00317       }
00318     x.size(n_x);
00319     // RHS too small or too large
00320     if ((c < 0) || (c > n_x))
00321       return ES_FAILED;
00322     // All views must be zero to satisfy equality
00323     if (c == 0) {
00324       for (int i=n_x; i--; )
00325         GECODE_ME_CHECK(x[i].zero_none(home));
00326       return ES_OK;
00327     }
00328     // All views must be one to satisfy equality
00329     if (c == n_x) {
00330       for (int i=n_x; i--; )
00331         GECODE_ME_CHECK(x[i].one_none(home));
00332       return ES_OK;
00333     }
00334     (void) new (home) EqBoolInt<VX>(home,x,c);
00335     return ES_OK;
00336   }
00337 
00338 
00339   /*
00340    * Integer disequal to Boolean sum
00341    *
00342    */
00343 
00344   template<class VX>
00345   forceinline
00346   NqBoolInt<VX>::NqBoolInt(Home home, ViewArray<VX>& b, int c0)
00347     : BinaryPropagator<VX,PC_INT_VAL>(home,
00348                                       b[b.size()-2],
00349                                       b[b.size()-1]), x(b), c(c0) {
00350     assert(x.size() >= 2);
00351     x.size(x.size()-2);
00352   }
00353 
00354   template<class VX>
00355   size_t
00356   NqBoolInt<VX>::dispose(Space& home) {
00357     (void) BinaryPropagator<VX,PC_INT_VAL>::dispose(home);
00358     return sizeof(*this);
00359   }
00360 
00361   template<class VX>
00362   forceinline
00363   NqBoolInt<VX>::NqBoolInt(Space& home, bool share, NqBoolInt<VX>& p)
00364     : BinaryPropagator<VX,PC_INT_VAL>(home,share,p), x(home,p.x.size()) {
00365     // Eliminate all zeros and ones in original and update
00366     int n = p.x.size();
00367     int p_c = p.c;
00368     for (int i=n; i--; )
00369       if (p.x[i].zero()) {
00370         n--; p.x[i]=p.x[n]; x[i]=x[n];
00371       } else if (p.x[i].one()) {
00372         n--; p_c--; p.x[i]=p.x[n]; x[i]=x[n];
00373       } else {
00374         x[i].update(home,share,p.x[i]);
00375       }
00376     c = p_c; p.c = p_c;
00377     x.size(n); p.x.size(n);
00378   }
00379 
00380   template<class VX>
00381   forceinline ExecStatus
00382   NqBoolInt<VX>::post(Home home, ViewArray<VX>& x, int c) {
00383     int n = x.size();
00384     for (int i=n; i--; )
00385       if (x[i].one()) {
00386         x[i]=x[--n]; c--;
00387       } else if (x[i].zero()) {
00388         x[i]=x[--n];
00389       }
00390     x.size(n);
00391     if ((n < c) || (c < 0))
00392       return ES_OK;
00393     if (n == 0)
00394       return (c == 0) ? ES_FAILED : ES_OK;
00395     if (n == 1) {
00396       if (c == 1) {
00397         GECODE_ME_CHECK(x[0].zero_none(home));
00398       } else {
00399         GECODE_ME_CHECK(x[0].one_none(home));
00400       }
00401       return ES_OK;
00402     }
00403     (void) new (home) NqBoolInt(home,x,c);
00404     return ES_OK;
00405   }
00406 
00407   template<class VX>
00408   Actor*
00409   NqBoolInt<VX>::copy(Space& home, bool share) {
00410     return new (home) NqBoolInt<VX>(home,share,*this);
00411   }
00412 
00413   template<class VX>
00414   PropCost
00415   NqBoolInt<VX>::cost(const Space&, const ModEventDelta&) const {
00416     return PropCost::linear(PropCost::LO, x.size());
00417   }
00418 
00419   template<class VX>
00420   forceinline bool
00421   NqBoolInt<VX>::resubscribe(Space& home, VX& y) {
00422     if (y.one())
00423       c--;
00424     int n = x.size();
00425     for (int i=n; i--; )
00426       if (x[i].one()) {
00427         c--; x[i]=x[--n];
00428       } else if (x[i].zero()) {
00429         x[i] = x[--n];
00430       } else {
00431         // New unassigned view found
00432         assert(!x[i].zero() && !x[i].one());
00433         // Move to y and subscribe
00434         y=x[i]; x[i]=x[--n];
00435         x.size(n);
00436         y.subscribe(home,*this,PC_INT_VAL,false);
00437         return true;
00438       }
00439     // All views have been assigned!
00440     x.size(0);
00441     return false;
00442   }
00443 
00444   template<class VX>
00445   ExecStatus
00446   NqBoolInt<VX>::propagate(Space& home, const ModEventDelta&) {
00447     bool s0 = true;
00448     if (x0.zero() || x0.one())
00449       s0 = resubscribe(home,x0);
00450     bool s1 = true;
00451     if (x1.zero() || x1.one())
00452       s1 = resubscribe(home,x1);
00453     int n = x.size() + s0 + s1;
00454     if ((n < c) || (c < 0))
00455       return ES_SUBSUMED(*this,home);
00456     if (n == 0)
00457       return (c == 0) ? ES_FAILED : ES_SUBSUMED(*this,sizeof(*this));
00458     if (n == 1) {
00459       if (s0) {
00460         if (c == 1) {
00461           GECODE_ME_CHECK(x0.zero_none(home));
00462         } else {
00463           GECODE_ME_CHECK(x0.one_none(home));
00464         }
00465       } else {
00466         assert(s1);
00467         if (c == 1) {
00468           GECODE_ME_CHECK(x1.zero_none(home));
00469         } else {
00470           GECODE_ME_CHECK(x1.one_none(home));
00471         }
00472       }
00473       return ES_SUBSUMED(*this,sizeof(*this));
00474     }
00475     return ES_FIX;
00476   }
00477 
00478   /*
00479    * Baseclass for reified integer Boolean sum
00480    *
00481    */
00482   template<class VX, class VB>
00483   forceinline
00484   ReLinBoolInt<VX,VB>::ReLinBoolInt(Home home, ViewArray<VX>& x0,
00485                                     int c0, VB b0)
00486     : Propagator(home), co(home), x(x0), n_s(x.size()), c(c0), b(b0) {
00487     x.subscribe(home,*new (home) Advisor(home,*this,co));
00488     b.subscribe(home,*this,PC_BOOL_VAL);
00489   }
00490 
00491   template<class VX, class VB>
00492   forceinline void
00493   ReLinBoolInt<VX,VB>::normalize(void) {
00494     if (n_s != x.size()) {
00495       int n_x = x.size();
00496       for (int i=n_x; i--; )
00497         if (!x[i].none())
00498           x[i] = x[--n_x];
00499       x.size(n_x);
00500       assert(x.size() == n_s);
00501     }
00502   }
00503 
00504   template<class VX, class VB>
00505   forceinline
00506   ReLinBoolInt<VX,VB>::ReLinBoolInt(Space& home, bool share, 
00507                                     ReLinBoolInt<VX,VB>& p)
00508     : Propagator(home,share,p), n_s(p.n_s), c(p.c) {
00509     p.normalize();
00510     co.update(home,share,p.co);
00511     x.update(home,share,p.x);
00512     b.update(home,share,p.b);
00513   }
00514 
00515   template<class VX, class VB>
00516   forceinline size_t
00517   ReLinBoolInt<VX,VB>::dispose(Space& home) {
00518     assert(!home.failed());
00519     Advisors<Advisor> as(co);
00520     x.cancel(home,as.advisor());
00521     co.dispose(home);
00522     b.cancel(home,*this,PC_BOOL_VAL);
00523     (void) Propagator::dispose(home);
00524     return sizeof(*this);
00525   }
00526 
00527   template<class VX, class VB>
00528   PropCost
00529   ReLinBoolInt<VX,VB>::cost(const Space&, const ModEventDelta&) const {
00530     return PropCost::unary(PropCost::HI);
00531   }
00532 
00533 
00534   /*
00535    * Traits for Boolean view negation
00536    */
00537   template<>
00538   class BoolNegTraits<BoolView> {
00539   public:
00541     typedef NegBoolView NegView;
00543     static NegBoolView neg(BoolView x) {
00544       NegBoolView y(x); return y;
00545     }
00546   };
00547 
00548   template<>
00549   class BoolNegTraits<NegBoolView> {
00550   public:
00552     typedef BoolView NegView;
00554     static BoolView neg(NegBoolView x) {
00555       return x.base();
00556     }
00557   };
00558 
00559 
00560   /*
00561    * Reified greater or equal propagator (integer rhs)
00562    * 
00563    */
00564   template<class VX, class VB>
00565   forceinline
00566   ReGqBoolInt<VX,VB>::ReGqBoolInt(Home home, ViewArray<VX>& x, int c, VB b)
00567     : ReLinBoolInt<VX,VB>(home,x,c,b) {}
00568 
00569   template<class VX, class VB>
00570   forceinline
00571   ReGqBoolInt<VX,VB>::ReGqBoolInt(Space& home, bool share, 
00572                                   ReGqBoolInt<VX,VB>& p)
00573     : ReLinBoolInt<VX,VB>(home,share,p) {}
00574 
00575   template<class VX, class VB>
00576   Actor*
00577   ReGqBoolInt<VX,VB>::copy(Space& home, bool share) {
00578     return new (home) ReGqBoolInt<VX,VB>(home,share,*this);
00579   }
00580 
00581   template<class VX, class VB>
00582   ExecStatus
00583   ReGqBoolInt<VX,VB>::advise(Space&, Advisor&, const Delta& d) {
00584     if (VX::one(d))
00585       c--;
00586     n_s--;
00587     if ((n_s < c) || (c <= 0))
00588       return ES_NOFIX;
00589     else
00590       return ES_FIX;
00591   }
00592 
00593   template<class VX, class VB>
00594   ExecStatus
00595   ReGqBoolInt<VX,VB>::propagate(Space& home, const ModEventDelta&) {
00596     if (b.none()) {
00597       if (c <= 0) {
00598         GECODE_ME_CHECK(b.one_none(home));
00599       } else {
00600         GECODE_ME_CHECK(b.zero_none(home));
00601       }
00602     } else {
00603       normalize();
00604       if (b.one()) {
00605         GECODE_REWRITE(*this,(GqBoolInt<VX>::post(home(*this),x,c)));
00606       } else {
00607         ViewArray<typename BoolNegTraits<VX>::NegView> nx(home,x.size());
00608         for (int i=x.size(); i--; )
00609           nx[i]=BoolNegTraits<VX>::neg(x[i]);
00610         GECODE_REWRITE(*this,GqBoolInt<typename BoolNegTraits<VX>::NegView>
00611                        ::post(home(*this),nx,x.size()-c+1));
00612       }
00613     }
00614     return ES_SUBSUMED(*this,home);
00615   }
00616 
00617   template<class VX, class VB>
00618   ExecStatus
00619   ReGqBoolInt<VX,VB>::post(Home home, ViewArray<VX>& x, int c, VB b) {
00620     assert(!b.assigned()); // checked before posting
00621 
00622     // Eliminate assigned views
00623     int n_x = x.size();
00624     for (int i=n_x; i--; )
00625       if (x[i].zero()) {
00626         x[i] = x[--n_x];
00627       } else if (x[i].one()) {
00628         x[i] = x[--n_x]; c--;
00629       }
00630     x.size(n_x);
00631     if (n_x < c) {
00632       // RHS too large
00633       GECODE_ME_CHECK(b.zero_none(home));
00634     } else if (c <= 0) {
00635       // Whatever the x[i] take for values, the inequality is subsumed
00636       GECODE_ME_CHECK(b.one_none(home));
00637     } else if (c == 1) {
00638       // Equivalent to Boolean disjunction
00639       return Bool::NaryOr<VX,VB>::post(home,x,b);
00640     } else if (c == n_x) {
00641       // Equivalent to Boolean conjunction, transform to Boolean disjunction
00642       ViewArray<typename BoolNegTraits<VX>::NegView> nx(home,n_x);
00643       for (int i=n_x; i--; )
00644         nx[i]=BoolNegTraits<VX>::neg(x[i]);
00645       return Bool::NaryOr
00646         <typename BoolNegTraits<VX>::NegView,
00647          typename BoolNegTraits<VB>::NegView>
00648         ::post(home,nx,BoolNegTraits<VB>::neg(b));
00649     } else {
00650       (void) new (home) ReGqBoolInt<VX,VB>(home,x,c,b);
00651     }
00652     return ES_OK;
00653   }
00654 
00655   /*
00656    * Reified equal propagator (integer rhs)
00657    * 
00658    */
00659   template<class VX, class VB>
00660   forceinline
00661   ReEqBoolInt<VX,VB>::ReEqBoolInt(Home home, ViewArray<VX>& x, int c, VB b)
00662     : ReLinBoolInt<VX,VB>(home,x,c,b) {}
00663 
00664   template<class VX, class VB>
00665   forceinline
00666   ReEqBoolInt<VX,VB>::ReEqBoolInt(Space& home, bool share, 
00667                                   ReEqBoolInt<VX,VB>& p)
00668     : ReLinBoolInt<VX,VB>(home,share,p) {}
00669 
00670   template<class VX, class VB>
00671   Actor*
00672   ReEqBoolInt<VX,VB>::copy(Space& home, bool share) {
00673     return new (home) ReEqBoolInt<VX,VB>(home,share,*this);
00674   }
00675 
00676   template<class VX, class VB>
00677   ExecStatus
00678   ReEqBoolInt<VX,VB>::advise(Space&, Advisor&, const Delta& d) {
00679     if (VX::one(d))
00680       c--;
00681     n_s--;
00682 
00683     if ((c < 0) || (c > n_s) || (n_s == 0))
00684       return ES_NOFIX;
00685     else
00686       return ES_FIX;
00687   }
00688 
00689   template<class VX, class VB>
00690   ExecStatus
00691   ReEqBoolInt<VX,VB>::propagate(Space& home, const ModEventDelta&) {
00692     if (b.none()) {
00693       if ((c == 0) && (n_s == 0)) {
00694         GECODE_ME_CHECK(b.one_none(home));
00695       } else {
00696         GECODE_ME_CHECK(b.zero_none(home));
00697       }
00698     } else {
00699       normalize();
00700       if (b.one()) {
00701         GECODE_REWRITE(*this,(EqBoolInt<VX>::post(home(*this),x,c)));
00702       } else {
00703         GECODE_REWRITE(*this,(NqBoolInt<VX>::post(home(*this),x,c)));
00704       }
00705     }
00706     return ES_SUBSUMED(*this,home);
00707   }
00708 
00709   template<class VX, class VB>
00710   ExecStatus
00711   ReEqBoolInt<VX,VB>::post(Home home, ViewArray<VX>& x, int c, VB b) {
00712     assert(!b.assigned()); // checked before posting
00713 
00714     // Eliminate assigned views
00715     int n_x = x.size();
00716     for (int i=n_x; i--; )
00717       if (x[i].zero()) {
00718         x[i] = x[--n_x];
00719       } else if (x[i].one()) {
00720         x[i] = x[--n_x]; c--;
00721       }
00722     x.size(n_x);
00723     if ((n_x < c) || (c < 0)) {
00724       // RHS too large
00725       GECODE_ME_CHECK(b.zero_none(home));
00726     } else if ((c == 0) && (n_x == 0)) {
00727       // all variables set, and c == 0: equality
00728       GECODE_ME_CHECK(b.one_none(home));
00729     } else if (c == 0) {
00730       // Equivalent to Boolean disjunction
00731       return Bool::NaryOr<VX,typename BoolNegTraits<VB>::NegView>
00732         ::post(home,x,BoolNegTraits<VB>::neg(b));
00733     } else if (c == n_x) {
00734       // Equivalent to Boolean conjunction, transform to Boolean disjunction
00735       ViewArray<typename BoolNegTraits<VX>::NegView> nx(home,n_x);
00736       for (int i=n_x; i--; )
00737         nx[i]=BoolNegTraits<VX>::neg(x[i]);
00738       return Bool::NaryOr
00739         <typename BoolNegTraits<VX>::NegView,
00740          typename BoolNegTraits<VB>::NegView>
00741         ::post(home,nx,BoolNegTraits<VB>::neg(b));
00742     } else {
00743       (void) new (home) ReEqBoolInt<VX,VB>(home,x,c,b);
00744     }
00745     return ES_OK;
00746   }
00747 
00748 
00749 }}}
00750 
00751 // STATISTICS: int-prop
00752