int.icc

00001 /*
00002  *  Main authors:
00003  *     Christian Schulte <schulte@gecode.org>
00004  *
00005  *  Copyright:
00006  *     Christian Schulte, 2006
00007  *
00008  *  Last modified:
00009  *     $Date: 2006-08-08 20:36:53 +0200 (Tue, 08 Aug 2006) $ by $Author: schulte $
00010  *     $Revision: 3538 $
00011  *
00012  *  This file is part of Gecode, the generic constraint
00013  *  development environment:
00014  *     http://www.gecode.org
00015  *
00016  *  See the file "LICENSE" for information on usage and
00017  *  redistribution of this file, and for a
00018  *     DISCLAIMER OF ALL WARRANTIES.
00019  *
00020  */
00021 
00022 namespace Gecode { namespace Int { namespace Count {
00023 
00024   /*
00025    * General baseclass
00026    *
00027    */
00028 
00029   template <class VX, class VY>
00030   forceinline
00031   BaseInt<VX,VY>::BaseInt(Space* home, 
00032                           ViewArray<VX>& x0, int n_s0, VY y0, int c0)
00033     : Propagator(home), x(x0), n_s(n_s0), y(y0), c(c0) {
00034     for (int i=n_s; i--; )
00035       x[i].subscribe(home,this,PC_INT_DOM);
00036     y.subscribe(home,this,PC_INT_DOM);
00037   }
00038 
00039   template <class VX, class VY>
00040   size_t
00041   BaseInt<VX,VY>::dispose(Space* home) {
00042     assert(!home->failed());
00043     for (int i=n_s; i--; )
00044       x[i].cancel(home,this,PC_INT_DOM);
00045     y.cancel(home,this,PC_INT_DOM);
00046     (void) Propagator::dispose(home);
00047     return sizeof(*this);
00048   }
00049 
00050   template <class VX, class VY>
00051   forceinline
00052   BaseInt<VX,VY>::BaseInt(Space* home, bool share, BaseInt<VX,VY>& p)
00053     : Propagator(home,share,p), n_s(p.n_s), c(p.c) {
00054     x.update(home,share,p.x);
00055     y.update(home,share,p.y);
00056   }
00057 
00058   template <class VX, class VY>
00059   PropCost
00060   BaseInt<VX,VY>::cost(void) const {
00061     return cost_lo(x.size(),PC_LINEAR_LO);
00062   }
00063 
00064   /*
00065    * Equal propagator (integer rhs)
00066    *
00067    */
00068   template <class VX, class VY>
00069   forceinline
00070   EqInt<VX,VY>::EqInt(Space* home, ViewArray<VX>& x, int n_s, VY y, int c)
00071     : BaseInt<VX,VY>(home,x,n_s,y,c) {}
00072 
00073   template <class VX, class VY>
00074   ExecStatus
00075   EqInt<VX,VY>::post(Space* home, ViewArray<VX>& x, VY y, int c) {
00076     // Eliminate decided views
00077     int n_x = x.size();
00078     for (int i=n_x; i--; )
00079       switch (holds(x[i],y)) {
00080       case RT_FALSE:
00081         x[i] = x[--n_x]; break;
00082       case RT_TRUE:
00083         x[i] = x[--n_x]; c--; break;
00084       case RT_MAYBE:
00085         break;
00086       default: 
00087         GECODE_NEVER;
00088       }
00089     x.size(n_x);
00090     // RHS too small or too large
00091     if ((c < 0) || (c > n_x))
00092       return ES_FAILED;
00093     // All views must be different
00094     if (c == 0) {
00095       ExecStatus es = post_false(home,x,y);
00096       return (es == ES_SUBSUMED) ? ES_OK : es;
00097     }
00098     // All views must be equal
00099     if (c == n_x) {
00100       ExecStatus es = post_true(home,x,y);
00101       return (es == ES_SUBSUMED) ? ES_OK : es;
00102     }
00103     // Compute how many subscriptions must be created
00104     int n_s = std::max(c,n_x-c)+1;
00105     assert(n_s <= n_x);
00106     (void) new (home) EqInt<VX,VY>(home,x,n_s,y,c);
00107     return ES_OK;
00108   }
00109 
00110   template <class VX, class VY>
00111   forceinline
00112   EqInt<VX,VY>::EqInt(Space* home, bool share, EqInt<VX,VY>& p)
00113     : BaseInt<VX,VY>(home,share,p) {}
00114 
00115   template <class VX, class VY>
00116   Actor*
00117   EqInt<VX,VY>::copy(Space* home, bool share) {
00118     return new (home) EqInt<VX,VY>(home,share,*this);
00119   }
00120 
00121   template <class VX, class VY>
00122   ExecStatus
00123   EqInt<VX,VY>::propagate(Space* home) {
00124     // Eliminate decided views from subscribed views
00125     int n_x = x.size();
00126     for (int i=n_s; i--; )
00127       switch (holds(x[i],y)) {
00128       case RT_FALSE:
00129         x[i].cancel(home,this,PC_INT_DOM);
00130         x[i]=x[--n_s]; x[n_s]=x[--n_x]; 
00131         break;
00132       case RT_TRUE:
00133         x[i].cancel(home,this,PC_INT_DOM);
00134         x[i]=x[--n_s]; x[n_s]=x[--n_x]; c--; 
00135         break;
00136       case RT_MAYBE:
00137         break;
00138       default: 
00139         GECODE_NEVER;
00140       }
00141     x.size(n_x);
00142     if ((c < 0) || (c > n_x))
00143       return ES_FAILED;
00144     // Eliminate decided views from unsubscribed views
00145     for (int i=n_x; i-- > n_s; )
00146       switch (holds(x[i],y)) {
00147       case RT_FALSE: x[i]=x[--n_x]; break;
00148       case RT_TRUE:  x[i]=x[--n_x]; c--; break;
00149       case RT_MAYBE: break;
00150       default:       GECODE_NEVER;
00151       }
00152     x.size(n_x);
00153     if ((c < 0) || (c > n_x))
00154       return ES_FAILED;
00155     if (c == 0)
00156       // All views must be different
00157       return post_false(home,x,y);
00158     if (c == n_x)
00159       // All views must be equal
00160       return post_true(home,x,y);
00161     int m = std::max(c,n_x-c)+1;
00162     assert(m <= n_x);
00163     // Now, there must be new subscriptions from x[n_s] up to x[m-1]
00164     while (n_s < m)
00165       x[n_s++].subscribe(home,this,PC_INT_DOM,false);
00166     return ES_FIX;
00167   }
00168 
00169   /*
00170    * Greater or equal propagator (integer rhs)
00171    *
00172    */
00173   template <class VX, class VY>
00174   forceinline
00175   GqInt<VX,VY>::GqInt(Space* home, ViewArray<VX>& x, int n_s, VY y, int c)
00176     : BaseInt<VX,VY>(home,x,n_s,y,c) {}
00177 
00178   template <class VX, class VY>
00179   ExecStatus
00180   GqInt<VX,VY>::post(Space* home, ViewArray<VX>& x, VY y, int c) {
00181     // Eliminate decided views
00182     int n_x = x.size();
00183     for (int i=n_x; i--; )
00184       switch (holds(x[i],y)) {
00185       case RT_FALSE:
00186         x[i] = x[--n_x]; break;
00187       case RT_TRUE:
00188         x[i] = x[--n_x]; c--; break;
00189       case RT_MAYBE:
00190         break;
00191       default: 
00192         GECODE_NEVER;
00193       }
00194     x.size(n_x);
00195     // RHS too large
00196     if (n_x < c)
00197       return ES_FAILED;
00198     // Whatever the x[i] take for values, the inequality is subsumed
00199     if (c <= 0)
00200       return ES_OK;
00201     // All views must be equal
00202     if (c == n_x) {
00203       ExecStatus es = post_true(home,x,y);
00204       return (es == ES_SUBSUMED) ? ES_OK : es;
00205     }
00206     (void) new (home) GqInt<VX,VY>(home,x,c+1,y,c);
00207     return ES_OK;
00208   }
00209 
00210   template <class VX, class VY>
00211   forceinline
00212   GqInt<VX,VY>::GqInt(Space* home, bool share, GqInt<VX,VY>& p)
00213     : BaseInt<VX,VY>(home,share,p) {}
00214 
00215   template <class VX, class VY>
00216   Actor*
00217   GqInt<VX,VY>::copy(Space* home, bool share) {
00218     return new (home) GqInt<VX,VY>(home,share,*this);
00219   }
00220 
00221   template <class VX, class VY>
00222   ExecStatus
00223   GqInt<VX,VY>::propagate(Space* home) {
00224     // Eliminate decided views from subscribed views
00225     int n_x = x.size();
00226     for (int i=n_s; i--; )
00227       switch (holds(x[i],y)) {
00228       case RT_FALSE:
00229         x[i].cancel(home,this,PC_INT_DOM);
00230         x[i]=x[--n_s]; x[n_s]=x[--n_x]; 
00231         break;
00232       case RT_TRUE:
00233         x[i].cancel(home,this,PC_INT_DOM);
00234         x[i]=x[--n_s]; x[n_s]=x[--n_x]; c--; 
00235         break;
00236       case RT_MAYBE:
00237         break;
00238       default: 
00239         GECODE_NEVER;
00240       }
00241     x.size(n_x);
00242     if (n_x < c)
00243       return ES_FAILED;
00244     if (c <= 0)
00245       return ES_SUBSUMED;
00246     // Eliminate decided views from unsubscribed views
00247     for (int i=n_x; i-- > n_s; )
00248       switch (holds(x[i],y)) {
00249       case RT_FALSE: x[i]=x[--n_x]; break;
00250       case RT_TRUE:  x[i]=x[--n_x]; c--; break;
00251       case RT_MAYBE: break;
00252       default:       GECODE_NEVER;
00253       }
00254     x.size(n_x);
00255     if (n_x < c)
00256       return ES_FAILED;
00257     if (c <= 0)
00258       return ES_SUBSUMED;
00259     if (c == n_x)
00260       // All views must be equal
00261       return post_true(home,x,y);
00262     // Now, there must be new subscriptions from x[n_s] up to x[c+1]
00263     while (n_s <= c)
00264       x[n_s++].subscribe(home,this,PC_INT_DOM,false);
00265     return ES_FIX;
00266   }
00267 
00268   /*
00269    * Less or equal propagator (integer rhs)
00270    *
00271    */
00272   template <class VX, class VY>
00273   forceinline
00274   LqInt<VX,VY>::LqInt(Space* home, ViewArray<VX>& x, int n_s, VY y, int c)
00275     : BaseInt<VX,VY>(home,x,n_s,y,c) {}
00276 
00277   template <class VX, class VY>
00278   ExecStatus
00279   LqInt<VX,VY>::post(Space* home, ViewArray<VX>& x, VY y, int c) {
00280     // Eliminate decided views
00281     int n_x = x.size();
00282     for (int i=n_x; i--; )
00283       switch (holds(x[i],y)) {
00284       case RT_FALSE:
00285         x[i] = x[--n_x]; break;
00286       case RT_TRUE:
00287         x[i] = x[--n_x]; c--; break;
00288       case RT_MAYBE:
00289         break;
00290       default: 
00291         GECODE_NEVER;
00292       }
00293     x.size(n_x);
00294     if (c < 0)
00295       return ES_FAILED;
00296     if (c >= n_x)
00297       return ES_OK;
00298     // All views must be different
00299     if (c == 0) {
00300       ExecStatus es = post_false(home,x,y);
00301       return (es == ES_SUBSUMED) ? ES_OK : es;
00302     }
00303     (void) new (home) LqInt<VX,VY>(home,x,n_x-c+1,y,c);
00304     return ES_OK;
00305   }
00306 
00307   template <class VX, class VY>
00308   forceinline
00309   LqInt<VX,VY>::LqInt(Space* home, bool share, LqInt<VX,VY>& p)
00310     : BaseInt<VX,VY>(home,share,p) {}
00311 
00312   template <class VX, class VY>
00313   Actor*
00314   LqInt<VX,VY>::copy(Space* home, bool share) {
00315     return new (home) LqInt<VX,VY>(home,share,*this);
00316   }
00317 
00318   template <class VX, class VY>
00319   ExecStatus
00320   LqInt<VX,VY>::propagate(Space* home) {
00321     // Eliminate decided views from subscribed views
00322     int n_x = x.size();
00323     for (int i=n_s; i--; )
00324       switch (holds(x[i],y)) {
00325       case RT_FALSE:
00326         x[i].cancel(home,this,PC_INT_DOM);
00327         x[i]=x[--n_s]; x[n_s]=x[--n_x]; 
00328         break;
00329       case RT_TRUE:
00330         x[i].cancel(home,this,PC_INT_DOM);
00331         x[i]=x[--n_s]; x[n_s]=x[--n_x]; c--; 
00332         break;
00333       case RT_MAYBE:
00334         break;
00335       default: 
00336         GECODE_NEVER;
00337       }
00338     x.size(n_x);
00339     if (c < 0)
00340       return ES_FAILED;
00341     if (c >= n_x)
00342       return ES_SUBSUMED;
00343     // Eliminate decided views from unsubscribed views
00344     for (int i=n_x; i-- > n_s; )
00345       switch (holds(x[i],y)) {
00346       case RT_FALSE: x[i]=x[--n_x]; break;
00347       case RT_TRUE:  x[i]=x[--n_x]; c--; break;
00348       case RT_MAYBE: break;
00349       default:       GECODE_NEVER;
00350       }
00351     x.size(n_x);
00352     if (c < 0)
00353       return ES_FAILED;
00354     if (c >= n_x)
00355       return ES_SUBSUMED;
00356     if (c == 0)
00357       // All views must be different
00358       return post_false(home,x,y);
00359     // Now, there must be new subscriptions from x[n_s] up to x[n_x-c+1]
00360     int m = n_x-c;
00361     while (n_s <= m)
00362       x[n_s++].subscribe(home,this,PC_INT_DOM,false);
00363     return ES_FIX;
00364   }
00365 
00366   /*
00367    * Not-equal propagator (integer rhs)
00368    *
00369    */
00370   template<class VX, class VY>
00371   forceinline
00372   NqInt<VX,VY>::NqInt(Space* home, ViewArray<VX>& x0, VY y0, int c0)
00373     : BinaryPropagator<VX,PC_INT_DOM>(home,
00374                                       x0[x0.size()-2],
00375                                       x0[x0.size()-1]), x(x0), y(y0), c(c0) {
00376     assert(x.size() >= 2);
00377     x.size(x.size()-2);
00378     y.subscribe(home,this,PC_INT_DOM);
00379   }
00380 
00381   template <class VX, class VY>
00382   size_t
00383   NqInt<VX,VY>::dispose(Space* home) {
00384     assert(!home->failed());
00385     y.cancel(home,this,PC_INT_DOM);
00386     (void) BinaryPropagator<VX,PC_INT_DOM>::dispose(home);
00387     return sizeof(*this);
00388   }
00389 
00390   template<class VX, class VY>
00391   forceinline
00392   NqInt<VX,VY>::NqInt(Space* home, bool share, NqInt<VX,VY>& p)
00393     : BinaryPropagator<VX,PC_INT_DOM>(home,share,p), c(p.c) {
00394     x.update(home,share,p.x);
00395     y.update(home,share,p.y);
00396   }
00397 
00398   template<class VX, class VY>
00399   forceinline ExecStatus
00400   NqInt<VX,VY>::post(Space* home, ViewArray<VX>& x, VY y, int c) {
00401     int n = x.size();
00402     for (int i=n; i--; )
00403       switch (holds(x[i],y)) {
00404       case RT_FALSE: x[i]=x[--n]; break;
00405       case RT_TRUE:  x[i]=x[--n]; c--; break;
00406       case RT_MAYBE: break;
00407       default:       GECODE_NEVER;
00408       }
00409     x.size(n);
00410     if ((n < c) || (c < 0))
00411       return ES_OK;
00412     if (n == 0)
00413       return (c == 0) ? ES_FAILED : ES_OK;
00414     if (n == 1) {
00415       ExecStatus es = (c == 1) ?
00416         post_false(home,x[0],y) : post_true(home,x[0],y);
00417       return (es == ES_SUBSUMED) ? ES_OK : es;
00418     }
00419     (void) new (home) NqInt(home,x,y,c);
00420     return ES_OK;
00421   }
00422 
00423   template<class VX, class VY>
00424   Actor*
00425   NqInt<VX,VY>::copy(Space* home, bool share) {
00426     return new (home) NqInt<VX,VY>(home,share,*this);
00427   }
00428 
00429   template<class VX, class VY>
00430   PropCost
00431   NqInt<VX,VY>::cost(void) const {
00432     return PC_LINEAR_LO;
00433   }
00434 
00435   template<class VX, class VY>
00436   forceinline bool
00437   NqInt<VX,VY>::resubscribe(Space* home, VX& z) {
00438     switch (holds(z,y)) {
00439     case RT_FALSE: break;
00440     case RT_TRUE:  c--; break;
00441     case RT_MAYBE: return true;
00442     default:       GECODE_NEVER;
00443     }
00444     int n = x.size();
00445     for (int i=n; i--; )
00446       switch (holds(x[i],y)) {
00447       case RT_FALSE: 
00448         x[i]=x[--n]; 
00449         break;
00450       case RT_TRUE:  
00451         x[i]=x[--n]; c--; 
00452         break;
00453       case RT_MAYBE: 
00454         // New undecided view found
00455         z.cancel(home,this,PC_INT_DOM);
00456         z=x[i]; x[i]=x[--n]; 
00457         x.size(n);
00458         z.subscribe(home,this,PC_INT_DOM,false);
00459         return true;
00460       default:       
00461         GECODE_NEVER;
00462       }
00463     // All views have been decided
00464     x.size(0);
00465     return false;
00466   }
00467 
00468   template<class VX, class VY>
00469   ExecStatus
00470   NqInt<VX,VY>::propagate(Space* home) {
00471     bool s0 = resubscribe(home,x0);
00472     bool s1 = resubscribe(home,x1);
00473     int n = x.size() + s0 + s1;
00474     if ((n < c) || (c < 0))
00475       return ES_SUBSUMED;
00476     if (n == 0)
00477       return (c == 0) ? ES_FAILED : ES_SUBSUMED;
00478     if (n == 1) {
00479       if (s0) {
00480         return (c == 1) ? 
00481           post_false(home,x0,y) : post_true(home,x0,y);
00482       } else {
00483         assert(s1);
00484         return (c == 1) ? 
00485           post_false(home,x1,y) : post_true(home,x1,y);
00486       }
00487       return ES_SUBSUMED;
00488     }
00489     return ES_FIX;
00490   }
00491 
00492 }}}
00493 
00494 // STATISTICS: int-prop
00495