Generated on Fri Oct 19 11:25:07 2018 for Gecode by doxygen 1.6.3

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