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: 2010-03-03 17:32:21 +0100 (Wed, 03 Mar 2010) $ by $Author: schulte $ 00011 * $Revision: 10364 $ 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 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, 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 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 ExecStatus 00331 Clause<VX,VY>::propagate(Space& home, const ModEventDelta&) { 00332 if (z.one()) 00333 GECODE_REWRITE(*this,(ClauseTrue<VX,VY>::post(home(*this),x,y))); 00334 if (z.zero()) { 00335 for (int i = x.size(); i--; ) 00336 GECODE_ME_CHECK(x[i].zero(home)); 00337 for (int i = y.size(); i--; ) 00338 GECODE_ME_CHECK(y[i].zero(home)); 00339 c.dispose(home); 00340 } else if (n_zero == x.size() + y.size()) { 00341 GECODE_ME_CHECK(z.zero_none(home)); 00342 c.dispose(home); 00343 } else { 00344 // There is exactly one view which is one 00345 GECODE_ME_CHECK(z.one_none(home)); 00346 } 00347 return home.ES_SUBSUMED(*this); 00348 } 00349 00350 }}} 00351 00352 // STATISTICS: int-prop 00353