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