bool-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-09-06 15:51:28 +0200 (Wed, 06 Sep 2006) $ by $Author: schulte $
00010  *     $Revision: 3604 $
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 #include <algorithm>
00023 
00024 #include "gecode/int/bool.hh"
00025 
00026 namespace Gecode { namespace Int { namespace Linear {
00027 
00028   /*
00029    * Baseclass for integer Boolean sum
00030    *
00031    */
00032   template <class VX>
00033   forceinline
00034   LinBoolInt<VX>::LinBoolInt(Space* home, ViewArray<VX>& x0,
00035                              int n_s0, int c0)
00036     : Propagator(home), x(x0), n_s(n_s0), c(c0) {
00037     for (int i=n_s; i--; )
00038       x[i].subscribe(home,this,PC_INT_VAL);
00039   }
00040 
00041   template <class VX>
00042   size_t
00043   LinBoolInt<VX>::dispose(Space* home) {
00044     assert(!home->failed());
00045     for (int i=n_s; i--; )
00046       x[i].cancel(home,this,PC_INT_VAL);
00047     (void) Propagator::dispose(home);
00048     return sizeof(*this);
00049   }
00050 
00051   template <class VX>
00052   forceinline
00053   LinBoolInt<VX>::LinBoolInt(Space* home, bool share, LinBoolInt<VX>& p)
00054     : Propagator(home,share,p), x(home,p.x.size()), n_s(p.n_s) {
00055     // Update views not assigned and subscribed to
00056     for (int i=n_s; i--; )
00057       x[i].update(home,share,p.x[i]);
00058     // Eliminate assigned but not subscribed views in original
00059     // and update remaining ones
00060     int n_x = p.x.size();
00061     int p_c = p.c;
00062     for (int i=n_x; i-- > n_s; )
00063       if (p.x[i].zero()) {
00064         n_x--;
00065         p.x[i]=p.x[n_x]; x[i]=x[n_x];
00066       } else if (p.x[i].one()) {
00067         n_x--; p_c--;
00068         p.x[i]=p.x[n_x]; x[i]=x[n_x];
00069       } else {
00070         x[i].update(home,share,p.x[i]);
00071       }
00072     p.c = p_c; c = p_c;
00073     p.x.size(n_x); x.size(n_x);
00074   }
00075 
00076   template <class VX>
00077   PropCost
00078   LinBoolInt<VX>::cost(void) const {
00079     return cost_lo(x.size(),PC_LINEAR_LO);
00080   }
00081 
00082 
00083   /*
00084    * Less or equal propagator (integer rhs)
00085    *
00086    */
00087 
00088   template <class VX>
00089   forceinline
00090   GqBoolInt<VX>::GqBoolInt(Space* home, ViewArray<VX>& x,
00091                            int n_s, int c)
00092     : LinBoolInt<VX>(home,x,n_s,c) {}
00093 
00094   template <class VX>
00095   ExecStatus
00096   GqBoolInt<VX>::post(Space* home, ViewArray<VX>& x, int c) {
00097     if (c == 1)
00098       return Bool::NaryOrTrue<VX>::post(home,x);
00099     // Eliminate assigned views
00100     int n_x = x.size();
00101     for (int i=n_x; i--; )
00102       if (x[i].zero()) {
00103         x[i] = x[--n_x];
00104       } else if (x[i].one()) {
00105         x[i] = x[--n_x]; c--;
00106       }
00107     // RHS too large
00108     if (n_x < c)
00109       return ES_FAILED;
00110     // Whatever the x[i] take for values, the inequality is subsumed
00111     if (c <= 0)
00112       return ES_OK;
00113     // All views must be one to satisfy inequality
00114     if (c == n_x) {
00115       for (int i=n_x; i--; )
00116         x[i].t_one_none(home);
00117       return ES_OK;
00118     }
00119     // This is the needed invariant as c+1 subscriptions must be created
00120     assert(n_x > c);
00121     x.size(n_x);
00122     (void) new (home) GqBoolInt<VX>(home,x,c+1,c);
00123     return ES_OK;
00124   }
00125 
00126   template <class VX>
00127   forceinline
00128   GqBoolInt<VX>::GqBoolInt(Space* home, bool share, GqBoolInt<VX>& p)
00129     : LinBoolInt<VX>(home,share,p) {}
00130 
00131   template <class VX>
00132   Actor*
00133   GqBoolInt<VX>::copy(Space* home, bool share) {
00134     return new (home) GqBoolInt<VX>(home,share,*this);
00135   }
00136 
00137   template <class VX>
00138   ExecStatus
00139   GqBoolInt<VX>::propagate(Space* home) {
00140     // Eliminate assigned views from subscribed views
00141     int n_x = x.size();
00142     for (int i=n_s; i--; )
00143       if (x[i].zero()) {
00144         x[i]=x[--n_s]; x[n_s]=x[--n_x];
00145       } else if (x[i].one()) {
00146         x[i]=x[--n_s]; x[n_s]=x[--n_x]; c--;
00147       }
00148     x.size(n_x);
00149     if (n_x < c)
00150       return ES_FAILED;
00151     if (c <= 0)
00152       return ES_SUBSUMED;
00153     // Find unassigned variables to subscribe to
00154     while ((n_s < n_x) && (n_s <= c)) 
00155       if (x[n_s].zero()) {
00156         x[n_s]=x[--n_x];
00157       } else if (x[n_s].one()) {
00158         x[n_s]=x[--n_x]; c--;
00159       } else {
00160         x[n_s++].subscribe(home,this,PC_INT_VAL,false);
00161       }
00162     x.size(n_x);
00163     if (n_x < c)
00164       return ES_FAILED;
00165     if (c <= 0)
00166       return ES_SUBSUMED;
00167     if (c == n_x) {
00168       // These are known to be not assigned
00169       for (int i=n_s; i--; )
00170         x[i].t_one_none(home);
00171       // These are not known to be assigned
00172       for (int i=n_s+1; i<n_x; i++)
00173         x[i].t_one(home);
00174       // Fix number of subscriptions such that cancelling subscriptions work
00175       n_s = 0;
00176       return ES_SUBSUMED;
00177     }
00178     return ES_FIX;
00179   }
00180 
00181 
00182   /*
00183    * Equal propagator (integer rhs)
00184    *
00185    */
00186   template <class VX>
00187   forceinline
00188   EqBoolInt<VX>::EqBoolInt(Space* home, ViewArray<VX>& x,
00189                            int n_s, int c)
00190     : LinBoolInt<VX>(home,x,n_s,c) {}
00191 
00192   template <class VX>
00193   ExecStatus
00194   EqBoolInt<VX>::post(Space* home, ViewArray<VX>& x, int c) {
00195     // Eliminate assigned views
00196     int n_x = x.size();
00197     for (int i=n_x; i--; )
00198       if (x[i].zero()) {
00199         x[i] = x[--n_x];
00200       } else if (x[i].one()) {
00201         x[i] = x[--n_x]; c--;
00202       }
00203     // RHS too small or too large
00204     if ((c < 0) || (c > n_x))
00205       return ES_FAILED;
00206     // All views must be zero to satisfy equality
00207     if (c == 0) {
00208       for (int i=n_x; i--; )
00209         x[i].t_zero_none(home);
00210       return ES_OK;
00211     }
00212     // All views must be one to satisfy equality
00213     if (c == n_x) {
00214       for (int i=n_x; i--; )
00215         x[i].t_one_none(home);
00216       return ES_OK;
00217     }
00218     x.size(n_x);
00219     // Compute how many subscriptions must be created
00220     int n_s = std::max(c,n_x-c)+1;
00221     assert(n_s <= n_x);
00222     (void) new (home) EqBoolInt<VX>(home,x,n_s,c);
00223     return ES_OK;
00224   }
00225 
00226   template <class VX>
00227   forceinline
00228   EqBoolInt<VX>::EqBoolInt(Space* home, bool share, EqBoolInt<VX>& p)
00229     : LinBoolInt<VX>(home,share,p) {}
00230 
00231   template <class VX>
00232   Actor*
00233   EqBoolInt<VX>::copy(Space* home, bool share) {
00234     return new (home) EqBoolInt<VX>(home,share,*this);
00235   }
00236 
00237   template <class VX>
00238   ExecStatus
00239   EqBoolInt<VX>::propagate(Space* home) {
00240     // Eliminate assigned views from subscribed views
00241     int n_x = x.size();
00242     for (int i=n_s; i--; )
00243       if (x[i].zero()) {
00244         x[i]=x[--n_s]; x[n_s]=x[--n_x];
00245       } else if (x[i].one()) {
00246         x[i]=x[--n_s]; x[n_s]=x[--n_x]; c--;
00247       }
00248     x.size(n_x);
00249     if ((c < 0) || (c > n_x))
00250       return ES_FAILED;
00251     // Find unassigned variables to subscribe to
00252     while ((n_s < n_x) && ((n_s <= c) || (n_s <= n_x-c))) 
00253       if (x[n_s].zero()) {
00254         x[n_s]=x[--n_x];
00255       } else if (x[n_s].one()) {
00256         x[n_s]=x[--n_x]; c--;
00257       } else {
00258         x[n_s++].subscribe(home,this,PC_INT_VAL,false);
00259       }
00260     x.size(n_x);
00261     if ((c < 0) || (c > n_x))
00262       return ES_FAILED;
00263     if (c == 0) {
00264       // These are known to be not assigned
00265       for (int i=n_s; i--; )
00266         x[i].t_zero_none(home);
00267       // These are not known to be assigned
00268       for (int i=n_s+1; i<n_x; i++)
00269         x[i].t_zero(home);
00270       // Fix number of subscriptions such that cancelling subscriptions work
00271       n_s = 0;
00272       return ES_SUBSUMED;
00273     }
00274     if (c == n_x) {
00275       // These are known to be not assigned
00276       for (int i=n_s; i--; )
00277         x[i].t_one_none(home);
00278       // These are not known to be assigned
00279       for (int i=n_s+1; i<n_x; i++)
00280         x[i].t_one(home);
00281       // Fix number of subscriptions such that cancelling subscriptions work
00282       n_s = 0;
00283       return ES_SUBSUMED;
00284     }
00285     return ES_FIX;
00286   }
00287 
00288 
00289   /*
00290    * Integer disequal to Boolean sum
00291    *
00292    */
00293 
00294   template<class VX>
00295   forceinline
00296   NqBoolInt<VX>::NqBoolInt(Space* home, ViewArray<VX>& b, int c0)
00297     : BinaryPropagator<VX,PC_INT_VAL>(home,
00298                                       b[b.size()-2],
00299                                       b[b.size()-1]), x(b), c(c0) {
00300     assert(x.size() >= 2);
00301     x.size(x.size()-2);
00302   }
00303 
00304   template<class VX>
00305   forceinline
00306   NqBoolInt<VX>::NqBoolInt(Space* home, bool share, NqBoolInt<VX>& p)
00307     : BinaryPropagator<VX,PC_INT_VAL>(home,share,p), x(home,p.x.size()) {
00308     // Eliminate all zeros and ones in original and update
00309     int n = p.x.size();
00310     int p_c = p.c;
00311     for (int i=n; i--; )
00312       if (p.x[i].zero()) {
00313         n--; p.x[i]=p.x[n]; x[i]=x[n];
00314       } else if (p.x[i].one()) {
00315         n--; p_c--; p.x[i]=p.x[n]; x[i]=x[n];
00316       } else {
00317         x[i].update(home,share,p.x[i]);
00318       }
00319     c = p_c; p.c = p_c;
00320     x.size(n); p.x.size(n);
00321   }
00322 
00323   template<class VX>
00324   forceinline ExecStatus
00325   NqBoolInt<VX>::post(Space* home, ViewArray<VX>& x, int c) {
00326     int n = x.size();
00327     for (int i=n; i--; )
00328       if (x[i].one()) {
00329         x[i]=x[--n]; c--;
00330       } else if (x[i].zero()) {
00331         x[i]=x[--n];
00332       }
00333     x.size(n);
00334     if ((n < c) || (c < 0))
00335       return ES_OK;
00336     if (n == 0)
00337       return (c == 0) ? ES_FAILED : ES_OK;
00338     if (n == 1) {
00339       if (c == 1)
00340         x[0].t_zero_none(home);
00341       else
00342         x[0].t_one_none(home);
00343       return ES_OK;
00344     }
00345     (void) new (home) NqBoolInt(home,x,c);
00346     return ES_OK;
00347   }
00348 
00349   template<class VX>
00350   Actor*
00351   NqBoolInt<VX>::copy(Space* home, bool share) {
00352     return new (home) NqBoolInt<VX>(home,share,*this);
00353   }
00354 
00355   template<class VX>
00356   PropCost
00357   NqBoolInt<VX>::cost(void) const {
00358     return PC_LINEAR_LO;
00359   }
00360 
00361   template<class VX>
00362   forceinline bool
00363   NqBoolInt<VX>::resubscribe(Space* home, VX& y) {
00364     if (y.one())
00365       c--;
00366     int n = x.size();
00367     for (int i=n; i--; )
00368       if (x[i].one()) {
00369         c--; x[i]=x[--n];
00370       } else if (x[i].zero()) {
00371         x[i] = x[--n];
00372       } else {
00373         // New unassigned view found
00374         assert(!x[i].zero() && !x[i].one());
00375         // Move to y and subscribe
00376         y=x[i]; x[i]=x[--n]; 
00377         x.size(n);
00378         y.subscribe(home,this,PC_INT_VAL,false);
00379         return true;
00380       }
00381     // All views have been assigned!
00382     x.size(0);
00383     return false;
00384   }
00385 
00386   template<class VX>
00387   ExecStatus
00388   NqBoolInt<VX>::propagate(Space* home) {
00389     bool s0 = true; 
00390     if (x0.zero() || x0.one())
00391       s0 = resubscribe(home,x0);
00392     bool s1 = true;
00393     if (x1.zero() || x1.one())
00394       s1 = resubscribe(home,x1);
00395     int n = x.size() + s0 + s1;
00396     if ((n < c) || (c < 0))
00397       return ES_SUBSUMED;
00398     if (n == 0)
00399       return (c == 0) ? ES_FAILED : ES_SUBSUMED;
00400     if (n == 1) {
00401       if (s0) {
00402         if (c == 1)
00403           x0.t_zero_none(home);
00404         else
00405           x0.t_one_none(home);
00406       } else {
00407         assert(s1);
00408         if (c == 1)
00409           x1.t_zero_none(home);
00410         else
00411           x1.t_one_none(home);
00412       }
00413       return ES_SUBSUMED;
00414     }
00415     return ES_FIX;
00416   }
00417 
00418 
00419 }}}
00420 
00421 // STATISTICS: int-prop
00422