gecode » int » bool
clause.hpp

00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
00002 /*
00003  *  Main authors:
00004  *     Christian Schulte <schulte@gecode.org>
00005  *
00006  *  Copyright:
00007  *     Christian Schulte, 2008
00008  *
00009  *  Last modified:
00010  *     $Date: 2009-10-14 12:19:49 +0200 (Wed, 14 Oct 2009) $ by $Author: schulte $
00011  *     $Revision: 9909 $
00012  *
00013  *  This file is part of Gecode, the generic constraint
00014  *  development environment:
00015  *     http://www.gecode.org
00016  *
00017  *  Permission is hereby granted, free of charge, to any person obtaining
00018  *  a copy of this software and associated documentation files (the
00019  *  "Software"), to deal in the Software without restriction, including
00020  *  without limitation the rights to use, copy, modify, merge, publish,
00021  *  distribute, sublicense, and/or sell copies of the Software, and to
00022  *  permit persons to whom the Software is furnished to do so, subject to
00023  *  the following conditions:
00024  *
00025  *  The above copyright notice and this permission notice shall be
00026  *  included in all copies or substantial portions of the Software.
00027  *
00028  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00029  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00030  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00031  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00032  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00033  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00034  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00035  *
00036  */
00037 
00038 namespace Gecode { namespace Int { namespace Bool {
00039 
00040   /*
00041    * Boolean clause propagator (disjunctive, true)
00042    *
00043    */
00044 
00045   template<class VX, class VY>
00046   forceinline
00047   ClauseTrue<VX,VY>::ClauseTrue(Home home,
00048                                 ViewArray<VX>& x0, ViewArray<VY>& y0)
00049     : MixBinaryPropagator<VX,PC_BOOL_VAL,VY,PC_BOOL_VAL>
00050   (home,x0[x0.size()-1],y0[y0.size()-1]), x(x0), y(y0) {
00051     assert((x.size() > 0) && (y.size() > 0));
00052     x.size(x.size()-1); y.size(y.size()-1);
00053   }
00054 
00055   template<class VX, class VY>
00056   PropCost
00057   ClauseTrue<VX,VY>::cost(const Space&, const ModEventDelta&) const {
00058     return PropCost::binary(PropCost::LO);
00059   }
00060 
00061   template<class VX, class VY>
00062   forceinline
00063   ClauseTrue<VX,VY>::ClauseTrue(Space& home, bool share, ClauseTrue<VX,VY>& p)
00064     : MixBinaryPropagator<VX,PC_BOOL_VAL,VY,PC_BOOL_VAL>(home,share,p) {
00065     x.update(home,share,p.x);
00066     y.update(home,share,p.y);
00067   }
00068 
00069   template<class VX, class VY>
00070   Actor*
00071   ClauseTrue<VX,VY>::copy(Space& home, bool share) {
00072     {
00073       int n = x.size();
00074       if (n > 0) {
00075         // Eliminate all zeros and find a one
00076         for (int i=n; i--; )
00077           if (x[i].one()) {
00078             // Only keep the one
00079             x[0]=x[i]; n=1; break;
00080           } else if (x[i].zero()) {
00081             // Eliminate the zero
00082             x[i]=x[--n];
00083           }
00084         x.size(n);
00085       }
00086     }
00087     {
00088       int n = y.size();
00089       if (n > 0) {
00090         // Eliminate all zeros and find a one
00091         for (int i=n; i--; )
00092           if (y[i].one()) {
00093             // Only keep the one
00094             y[0]=y[i]; n=1; break;
00095           } else if (y[i].zero()) {
00096             // Eliminate the zero
00097             y[i]=y[--n];
00098           }
00099         y.size(n);
00100       }
00101     }
00102     if ((x.size() == 0) && (y.size() == 0))
00103       return new (home) BinOrTrue<VX,VY>(home,share,*this,x0,x1);
00104     else
00105       return new (home) ClauseTrue<VX,VY>(home,share,*this);
00106   }
00107 
00108   template<class VX, class VY>
00109   inline ExecStatus
00110   ClauseTrue<VX,VY>::post(Home home, ViewArray<VX>& x, ViewArray<VY>& y) {
00111     for (int i=x.size(); i--; )
00112       if (x[i].one())
00113         return ES_OK;
00114       else if (x[i].zero())
00115         x.move_lst(i);
00116     if (x.size() == 0)
00117       return NaryOrTrue<VY>::post(home,y);
00118     for (int i=y.size(); i--; )
00119       if (y[i].one())
00120         return ES_OK;
00121       else if (y[i].zero())
00122         y.move_lst(i);
00123     if (y.size() == 0)
00124       return NaryOrTrue<VX>::post(home,x);
00125     if ((x.size() == 1) && (y.size() == 1)) {
00126       return BinOrTrue<VX,VY>::post(home,x[0],y[0]);
00127     } else if (!x.shared(home,y)) {
00128       (void) new (home) ClauseTrue(home,x,y);
00129     }
00130     return ES_OK;
00131   }
00132 
00133   template<class VX, class VY>
00134   forceinline ExecStatus
00135   resubscribe(Space& home, Propagator& p,
00136               VX& x0, ViewArray<VX>& x,
00137               VY& x1, ViewArray<VY>& y) {
00138     if (x0.zero()) {
00139       int n = x.size();
00140       for (int i=n; i--; )
00141         if (x[i].one()) {
00142           x.size(n);
00143           return ES_SUBSUMED(p,home);
00144         } else if (x[i].zero()) {
00145           x[i] = x[--n];
00146         } else {
00147           // Rewrite if there is just one view left
00148           if ((i == 0) && (y.size() == 0)) {
00149             VX z = x[0]; x.size(0);
00150             GECODE_REWRITE(p,(BinOrTrue<VX,VY>::post(home(p),z,x1)));
00151           }
00152           // Move to x0 and subscribe
00153           x0=x[i]; x[i]=x[--n];
00154           x.size(n);
00155           x0.subscribe(home,p,PC_BOOL_VAL,false);
00156           return ES_FIX;
00157         }
00158       // All x-views have been assigned!
00159       ViewArray<VY> z(home,y.size()+1);
00160       for (int i=y.size(); i--; )
00161         z[i]=y[i];
00162       z[y.size()] = x1;
00163       GECODE_REWRITE(p,(NaryOrTrue<VY>::post(home(p),z)));
00164     }
00165     return ES_FIX;
00166   }
00167 
00168   template<class VX, class VY>
00169   ExecStatus
00170   ClauseTrue<VX,VY>::propagate(Space& home, const ModEventDelta&) {
00171     if (x0.one() || x1.one())
00172       return ES_SUBSUMED(*this,home);
00173     GECODE_ES_CHECK(resubscribe(home,*this,x0,x,x1,y));
00174     GECODE_ES_CHECK(resubscribe(home,*this,x1,y,x0,x));
00175     return ES_FIX;
00176   }
00177 
00178   template<class VX, class VY>
00179   size_t
00180   ClauseTrue<VX,VY>::dispose(Space& home) {
00181     (void) MixBinaryPropagator<VX,PC_BOOL_VAL,VY,PC_BOOL_VAL>::dispose(home);
00182     return sizeof(*this);
00183   }
00184 
00185 
00186   /*
00187    * Boolean clause propagator (disjunctive)
00188    *
00189    */
00190 
00191   /*
00192    * Index advisors
00193    *
00194    */
00195   template<class VX, class VY>
00196   forceinline
00197   Clause<VX,VY>::Tagged::Tagged(Space& home, Propagator& p,
00198                                 Council<Tagged>& c, bool x0)
00199     : Advisor(home,p,c), x(x0) {}
00200 
00201   template<class VX, class VY>
00202   forceinline
00203   Clause<VX,VY>::Tagged::Tagged(Space& home, bool share, Tagged& a)
00204     : Advisor(home,share,a), x(a.x) {}
00205 
00206   template<class VX, class VY>
00207   forceinline
00208   Clause<VX,VY>::Clause(Home home, ViewArray<VX>& x0, ViewArray<VY>& y0,
00209                         VX z0)
00210     : Propagator(home), x(x0), y(y0), z(z0), n_zero(0), c(home) {
00211     x.subscribe(home,*new (home) Tagged(home,*this,c,true));
00212     y.subscribe(home,*new (home) Tagged(home,*this,c,false));
00213     z.subscribe(home,*this,PC_BOOL_VAL);
00214   }
00215 
00216   template<class VX, class VY>
00217   forceinline
00218   Clause<VX,VY>::Clause(Space& home, bool share, Clause<VX,VY>& p)
00219     : Propagator(home,share,p), n_zero(p.n_zero) {
00220     x.update(home,share,p.x);
00221     y.update(home,share,p.y);
00222     z.update(home,share,p.z);
00223     c.update(home,share,p.c);
00224   }
00225 
00226   template<class VX>
00227   forceinline void
00228   eliminate_zero(ViewArray<VX>& x, int& n_zero) {
00229     if (n_zero > 0) {
00230       int n=x.size();
00231       // Eliminate all zeros
00232       for (int i=n; i--; )
00233         if (x[i].zero()) {
00234           x[i]=x[--n]; n_zero--;
00235         }
00236       x.size(n);
00237     }
00238   }
00239 
00240   template<class VX, class VY>
00241   Actor*
00242   Clause<VX,VY>::copy(Space& home, bool share) {
00243     eliminate_zero(x,n_zero);
00244     eliminate_zero(y,n_zero);
00245     return new (home) Clause<VX,VY>(home,share,*this);
00246   }
00247 
00248   template<class VX, class VY>
00249   inline ExecStatus
00250   Clause<VX,VY>::post(Home home, ViewArray<VX>& x, ViewArray<VY>& y, VX z) {
00251     assert(!x.shared(home) && !y.shared(home));
00252     if (z.one())
00253       return ClauseTrue<VX,VY>::post(home,x,y);
00254     if (z.zero()) {
00255       for (int i=x.size(); i--; )
00256         GECODE_ME_CHECK(x[i].zero(home));
00257       for (int i=y.size(); i--; )
00258         GECODE_ME_CHECK(y[i].zero(home));
00259       return ES_OK;
00260     }
00261     for (int i=x.size(); i--; )
00262       if (x[i].one()) {
00263         GECODE_ME_CHECK(z.one_none(home));
00264         return ES_OK;
00265       } else if (x[i].zero()) {
00266         x.move_lst(i);
00267       }
00268     if (x.size() == 0)
00269       return NaryOr<VY,VX>::post(home,y,z);
00270     for (int i=y.size(); i--; )
00271       if (y[i].one()) {
00272         GECODE_ME_CHECK(z.one_none(home));
00273         return ES_OK;
00274       } else if (y[i].zero()) {
00275         y.move_lst(i);
00276       }
00277     if (y.size() == 0)
00278       return NaryOr<VX,VX>::post(home,x,z);
00279     if ((x.size() == 1) && (y.size() == 1)) {
00280       return Or<VX,VY,VX>::post(home,x[0],y[0],z);
00281     } else if (x.shared(home,y)) {
00282       GECODE_ME_CHECK(z.one_none(home));
00283     } else {
00284       (void) new (home) Clause<VX,VY>(home,x,y,z);
00285     }
00286     return ES_OK;
00287   }
00288 
00289   template<class VX, class VY>
00290   PropCost
00291   Clause<VX,VY>::cost(const Space&, const ModEventDelta&) const {
00292     return PropCost::unary(PropCost::LO);
00293   }
00294 
00295   template<class VX, class VY>
00296   forceinline void
00297   Clause<VX,VY>::cancel(Space& home) {
00298     for (Advisors<Tagged> as(c); as(); ++as) {
00299       if (as.advisor().x)
00300         x.cancel(home,as.advisor());
00301       else
00302         y.cancel(home,as.advisor());
00303       as.advisor().dispose(home,c);
00304     }
00305     c.dispose(home);
00306     z.cancel(home,*this,PC_BOOL_VAL);
00307   }
00308 
00309 
00310   template<class VX, class VY>
00311   ExecStatus
00312   Clause<VX,VY>::advise(Space&, Advisor& _a, const Delta& d) {
00313     Tagged& a = static_cast<Tagged&>(_a);
00314     // Decides whether the propagator must be run
00315     if ((a.x && VX::zero(d)) || (!a.x && VY::zero(d)))
00316       if (++n_zero < x.size() + y.size())
00317         return ES_FIX;
00318     return ES_NOFIX;
00319   }
00320 
00321   template<class VX, class VY>
00322   ExecStatus
00323   Clause<VX,VY>::propagate(Space& home, const ModEventDelta&) {
00324     if (z.one())
00325       GECODE_REWRITE(*this,(ClauseTrue<VX,VY>::post(home(*this),x,y)));
00326     if (z.zero()) {
00327       for (int i = x.size(); i--; )
00328         GECODE_ME_CHECK(x[i].zero(home));
00329       for (int i = y.size(); i--; )
00330         GECODE_ME_CHECK(y[i].zero(home));
00331       c.dispose(home);
00332     } else if (n_zero == x.size() + y.size()) {
00333       GECODE_ME_CHECK(z.zero_none(home));
00334       c.dispose(home);
00335     } else {
00336       // There is exactly one view which is one
00337       cancel(home);
00338       GECODE_ME_CHECK(z.one_none(home));
00339     }
00340     return ES_SUBSUMED(*this,sizeof(*this));
00341   }
00342 
00343   template<class VX, class VY>
00344   size_t
00345   Clause<VX,VY>::dispose(Space& home) {
00346     cancel(home);
00347     (void) Propagator::dispose(home);
00348     return sizeof(*this);
00349   }
00350 
00351 }}}
00352 
00353 // STATISTICS: int-prop
00354