Generated on Wed Feb 7 10:27:53 2018 for Gecode by doxygen 1.6.3

clause.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  *
00006  *  Copyright:
00007  *     Christian Schulte, 2008
00008  *
00009  *  Last modified:
00010  *     $Date: 2017-05-10 14:58:42 +0200 (Wed, 10 May 2017) $ by $Author: schulte $
00011  *     $Revision: 15697 $
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, ClauseTrue<VX,VY>& p)
00064     : MixBinaryPropagator<VX,PC_BOOL_VAL,VY,PC_BOOL_VAL>(home,p) {
00065     x.update(home,p.x);
00066     y.update(home,p.y);
00067   }
00068 
00069   template<class VX, class VY>
00070   Actor*
00071   ClauseTrue<VX,VY>::copy(Space& home) {
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,*this,x0,x1);
00104     else
00105       return new (home) ClauseTrue<VX,VY>(home,*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(y)) {
00128       (void) new (home) ClauseTrue(home,x,y);
00129     }
00130     return ES_OK;
00131   }
00132 
00133   template<class VX, class VY>
00134   forceinline size_t
00135   ClauseTrue<VX,VY>::dispose(Space& home) {
00136     (void) MixBinaryPropagator<VX,PC_BOOL_VAL,VY,PC_BOOL_VAL>::dispose(home);
00137     return sizeof(*this);
00138   }
00139 
00140   template<class VX, class VY>
00141   forceinline ExecStatus
00142   resubscribe(Space& home, Propagator& p,
00143               VX& x0, ViewArray<VX>& x,
00144               VY& x1, ViewArray<VY>& y) {
00145     if (x0.zero()) {
00146       int n = x.size();
00147       for (int i=n; i--; )
00148         if (x[i].one()) {
00149           x.size(n);
00150           return home.ES_SUBSUMED(p);
00151         } else if (x[i].zero()) {
00152           x[i] = x[--n];
00153         } else {
00154           // Rewrite if there is just one view left
00155           if ((i == 0) && (y.size() == 0)) {
00156             VX z = x[0]; x.size(0);
00157             GECODE_REWRITE(p,(BinOrTrue<VX,VY>::post(home(p),z,x1)));
00158           }
00159           // Move to x0 and subscribe
00160           x0=x[i]; x[i]=x[--n];
00161           x.size(n);
00162           x0.subscribe(home,p,PC_BOOL_VAL,false);
00163           return ES_FIX;
00164         }
00165       // All x-views have been assigned!
00166       ViewArray<VY> z(home,y.size()+1);
00167       for (int i=y.size(); i--; )
00168         z[i]=y[i];
00169       z[y.size()] = x1;
00170       GECODE_REWRITE(p,(NaryOrTrue<VY>::post(home(p),z)));
00171     }
00172     return ES_FIX;
00173   }
00174 
00175   template<class VX, class VY>
00176   ExecStatus
00177   ClauseTrue<VX,VY>::propagate(Space& home, const ModEventDelta&) {
00178     if (x0.one() || x1.one())
00179       return home.ES_SUBSUMED(*this);
00180     GECODE_ES_CHECK(resubscribe(home,*this,x0,x,x1,y));
00181     GECODE_ES_CHECK(resubscribe(home,*this,x1,y,x0,x));
00182     return ES_FIX;
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, Tagged& a)
00204     : Advisor(home,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, Clause<VX,VY>& p)
00219     : Propagator(home,p), n_zero(p.n_zero) {
00220     x.update(home,p.x);
00221     y.update(home,p.y);
00222     z.update(home,p.z);
00223     c.update(home,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) {
00243     eliminate_zero(x,n_zero);
00244     eliminate_zero(y,n_zero);
00245     return new (home) Clause<VX,VY>(home,*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() && !y.shared());
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(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   template<class VX, class VY>
00310   forceinline size_t
00311   Clause<VX,VY>::dispose(Space& home) {
00312     cancel(home);
00313     (void) Propagator::dispose(home);
00314     return sizeof(*this);
00315   }
00316 
00317 
00318   template<class VX, class VY>
00319   ExecStatus
00320   Clause<VX,VY>::advise(Space&, Advisor& _a, const Delta& d) {
00321     Tagged& a = static_cast<Tagged&>(_a);
00322     // Decides whether the propagator must be run
00323     if ((a.x && VX::zero(d)) || (!a.x && VY::zero(d)))
00324       if (++n_zero < x.size() + y.size())
00325         return ES_FIX;
00326     return ES_NOFIX;
00327   }
00328 
00329   template<class VX, class VY>
00330   void
00331   Clause<VX,VY>::reschedule(Space& home) {
00332     z.reschedule(home,*this,PC_BOOL_VAL);
00333     if (n_zero == x.size() + y.size())
00334       VX::schedule(home,*this,ME_BOOL_VAL);
00335     for (int i=x.size(); i--; )
00336       if (x[i].one()) {
00337         VX::schedule(home,*this,ME_BOOL_VAL);
00338         return;
00339       }
00340     for (int i=y.size(); i--; )
00341       if (y[i].one()) {
00342         VX::schedule(home,*this,ME_BOOL_VAL);
00343         return;
00344       }
00345   }
00346 
00347   template<class VX, class VY>
00348   ExecStatus
00349   Clause<VX,VY>::propagate(Space& home, const ModEventDelta&) {
00350     if (z.one())
00351       GECODE_REWRITE(*this,(ClauseTrue<VX,VY>::post(home(*this),x,y)));
00352     if (z.zero()) {
00353       for (int i = x.size(); i--; )
00354         GECODE_ME_CHECK(x[i].zero(home));
00355       for (int i = y.size(); i--; )
00356         GECODE_ME_CHECK(y[i].zero(home));
00357       c.dispose(home);
00358     } else if (n_zero == x.size() + y.size()) {
00359       GECODE_ME_CHECK(z.zero_none(home));
00360       c.dispose(home);
00361     } else {
00362       // There is at least one view which is one
00363       GECODE_ME_CHECK(z.one_none(home));
00364     }
00365     return home.ES_SUBSUMED(*this);
00366   }
00367 
00368 }}}
00369 
00370 // STATISTICS: int-prop
00371