bool-post.cpp
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 * Tias Guns <tias.guns@cs.kuleuven.be> 00006 * 00007 * Copyright: 00008 * Christian Schulte, 2002 00009 * Tias Guns, 2009 00010 * 00011 * Last modified: 00012 * $Date: 2010-03-03 17:40:32 +0100 (Wed, 03 Mar 2010) $ by $Author: schulte $ 00013 * $Revision: 10365 $ 00014 * 00015 * This file is part of Gecode, the generic constraint 00016 * development environment: 00017 * http://www.gecode.org 00018 * 00019 * Permission is hereby granted, free of charge, to any person obtaining 00020 * a copy of this software and associated documentation files (the 00021 * "Software"), to deal in the Software without restriction, including 00022 * without limitation the rights to use, copy, modify, merge, publish, 00023 * distribute, sublicense, and/or sell copies of the Software, and to 00024 * permit persons to whom the Software is furnished to do so, subject to 00025 * the following conditions: 00026 * 00027 * The above copyright notice and this permission notice shall be 00028 * included in all copies or substantial portions of the Software. 00029 * 00030 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 00031 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 00032 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 00033 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE 00034 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION 00035 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION 00036 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 00037 * 00038 */ 00039 00040 #include <gecode/int/linear.hh> 00041 00042 namespace Gecode { namespace Int { namespace Linear { 00043 00045 inline IntRelType 00046 inverse(const IntRelType r) { 00047 switch (r) { 00048 case IRT_EQ: return IRT_NQ; break; 00049 case IRT_NQ: return IRT_EQ; break; 00050 case IRT_GQ: return IRT_LE; break; 00051 case IRT_LQ: return IRT_GR; break; 00052 case IRT_LE: return IRT_GQ; break; 00053 case IRT_GR: return IRT_LQ; break; 00054 default: GECODE_NEVER; 00055 } 00056 throw UnknownRelation("Int::linear"); 00057 } 00058 00060 inline void 00061 eliminate(Term<BoolView>* t, int &n, double& d) { 00062 for (int i=n; i--; ) 00063 if (t[i].x.one()) { 00064 d -= t[i].a; t[i]=t[--n]; 00065 } else if (t[i].x.zero()) { 00066 t[i]=t[--n]; 00067 } 00068 00069 Limits::check(d,"Int::linear"); 00070 } 00071 00073 inline void 00074 rewrite(IntRelType &r, double &d) { 00075 switch (r) { 00076 case IRT_EQ: case IRT_NQ: case IRT_LQ: case IRT_GQ: 00077 break; 00078 case IRT_LE: 00079 d--; r = IRT_LQ; break; 00080 case IRT_GR: 00081 d++; r = IRT_GQ; break; 00082 default: 00083 throw UnknownRelation("Int::linear"); 00084 } 00085 } 00086 00087 void 00088 post_pos_unit(Home home, 00089 Term<BoolView>* t_p, int n_p, 00090 IntRelType r, IntView y, int c) { 00091 switch (r) { 00092 case IRT_EQ: 00093 { 00094 ViewArray<BoolView> x(home,n_p); 00095 for (int i=n_p; i--; ) 00096 x[i]=t_p[i].x; 00097 GECODE_ES_FAIL((EqBoolView<BoolView,IntView> 00098 ::post(home,x,y,c))); 00099 } 00100 break; 00101 case IRT_NQ: 00102 { 00103 ViewArray<BoolView> x(home,n_p); 00104 for (int i=n_p; i--; ) 00105 x[i]=t_p[i].x; 00106 GECODE_ES_FAIL((NqBoolView<BoolView,IntView> 00107 ::post(home,x,y,c))); 00108 } 00109 break; 00110 case IRT_GQ: 00111 { 00112 ViewArray<BoolView> x(home,n_p); 00113 for (int i=n_p; i--; ) 00114 x[i]=t_p[i].x; 00115 GECODE_ES_FAIL((GqBoolView<BoolView,IntView> 00116 ::post(home,x,y,c))); 00117 } 00118 break; 00119 case IRT_LQ: 00120 { 00121 ViewArray<NegBoolView> x(home,n_p); 00122 for (int i=n_p; i--; ) 00123 x[i]=NegBoolView(t_p[i].x); 00124 MinusView z(y); 00125 GECODE_ES_FAIL((GqBoolView<NegBoolView,MinusView> 00126 ::post(home,x,z,n_p-c))); 00127 } 00128 break; 00129 default: GECODE_NEVER; 00130 } 00131 } 00132 00133 void 00134 post_pos_unit(Home home, 00135 Term<BoolView>* t_p, int n_p, 00136 IntRelType r, ZeroIntView, int c) { 00137 switch (r) { 00138 case IRT_EQ: 00139 { 00140 ViewArray<BoolView> x(home,n_p); 00141 for (int i=n_p; i--; ) 00142 x[i]=t_p[i].x; 00143 GECODE_ES_FAIL((EqBoolInt<BoolView>::post(home,x,c))); 00144 } 00145 break; 00146 case IRT_NQ: 00147 { 00148 ViewArray<BoolView> x(home,n_p); 00149 for (int i=n_p; i--; ) 00150 x[i]=t_p[i].x; 00151 GECODE_ES_FAIL((NqBoolInt<BoolView>::post(home,x,c))); 00152 } 00153 break; 00154 case IRT_GQ: 00155 { 00156 ViewArray<BoolView> x(home,n_p); 00157 for (int i=n_p; i--; ) 00158 x[i]=t_p[i].x; 00159 GECODE_ES_FAIL((GqBoolInt<BoolView>::post(home,x,c))); 00160 } 00161 break; 00162 case IRT_LQ: 00163 { 00164 ViewArray<NegBoolView> x(home,n_p); 00165 for (int i=n_p; i--; ) 00166 x[i]=NegBoolView(t_p[i].x); 00167 GECODE_ES_FAIL((GqBoolInt<NegBoolView>::post(home,x,n_p-c))); 00168 } 00169 break; 00170 default: GECODE_NEVER; 00171 } 00172 } 00173 00174 void 00175 post_pos_unit(Home home, 00176 Term<BoolView>* t_p, int n_p, 00177 IntRelType r, int c, BoolView b, 00178 IntConLevel) { 00179 switch (r) { 00180 case IRT_EQ: 00181 { 00182 ViewArray<BoolView> x(home,n_p); 00183 for (int i=n_p; i--; ) 00184 x[i]=t_p[i].x; 00185 GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView>::post(home,x,c,b))); 00186 } 00187 break; 00188 case IRT_NQ: 00189 { 00190 ViewArray<BoolView> x(home,n_p); 00191 for (int i=n_p; i--; ) 00192 x[i]=t_p[i].x; 00193 NegBoolView nb(b); 00194 GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView>::post(home,x,c,nb))); 00195 } 00196 break; 00197 case IRT_GQ: 00198 { 00199 ViewArray<BoolView> x(home,n_p); 00200 for (int i=n_p; i--; ) 00201 x[i]=t_p[i].x; 00202 GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView>::post(home,x,c,b))); 00203 } 00204 break; 00205 case IRT_LQ: 00206 { 00207 ViewArray<NegBoolView> x(home,n_p); 00208 for (int i=n_p; i--; ) 00209 x[i]=NegBoolView(t_p[i].x); 00210 GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView>::post(home,x,n_p-c,b))); 00211 } 00212 break; 00213 default: GECODE_NEVER; 00214 } 00215 } 00216 00217 void 00218 post_neg_unit(Home home, 00219 Term<BoolView>* t_n, int n_n, 00220 IntRelType r, IntView y, int c) { 00221 switch (r) { 00222 case IRT_EQ: 00223 { 00224 ViewArray<BoolView> x(home,n_n); 00225 for (int i=n_n; i--; ) 00226 x[i]=t_n[i].x; 00227 MinusView z(y); 00228 GECODE_ES_FAIL((EqBoolView<BoolView,MinusView> 00229 ::post(home,x,z,-c))); 00230 } 00231 break; 00232 case IRT_NQ: 00233 { 00234 ViewArray<BoolView> x(home,n_n); 00235 for (int i=n_n; i--; ) 00236 x[i]=t_n[i].x; 00237 MinusView z(y); 00238 GECODE_ES_FAIL((NqBoolView<BoolView,MinusView> 00239 ::post(home,x,z,-c))); 00240 } 00241 break; 00242 case IRT_GQ: 00243 { 00244 ViewArray<NegBoolView> x(home,n_n); 00245 for (int i=n_n; i--; ) 00246 x[i]=NegBoolView(t_n[i].x); 00247 GECODE_ES_FAIL((GqBoolView<NegBoolView,IntView> 00248 ::post(home,x,y,n_n+c))); 00249 } 00250 break; 00251 case IRT_LQ: 00252 { 00253 ViewArray<BoolView> x(home,n_n); 00254 for (int i=n_n; i--; ) 00255 x[i]=t_n[i].x; 00256 MinusView z(y); 00257 GECODE_ES_FAIL((GqBoolView<BoolView,MinusView> 00258 ::post(home,x,z,-c))); 00259 } 00260 break; 00261 default: GECODE_NEVER; 00262 } 00263 } 00264 00265 void 00266 post_neg_unit(Home home, 00267 Term<BoolView>* t_n, int n_n, 00268 IntRelType r, ZeroIntView, int c) { 00269 switch (r) { 00270 case IRT_EQ: 00271 { 00272 ViewArray<BoolView> x(home,n_n); 00273 for (int i=n_n; i--; ) 00274 x[i]=t_n[i].x; 00275 GECODE_ES_FAIL((EqBoolInt<BoolView>::post(home,x,-c))); 00276 } 00277 break; 00278 case IRT_NQ: 00279 { 00280 ViewArray<BoolView> x(home,n_n); 00281 for (int i=n_n; i--; ) 00282 x[i]=t_n[i].x; 00283 GECODE_ES_FAIL((NqBoolInt<BoolView>::post(home,x,-c))); 00284 } 00285 break; 00286 case IRT_GQ: 00287 { 00288 ViewArray<NegBoolView> x(home,n_n); 00289 for (int i=n_n; i--; ) 00290 x[i]=NegBoolView(t_n[i].x); 00291 GECODE_ES_FAIL((GqBoolInt<NegBoolView>::post(home,x,n_n+c))); 00292 } 00293 break; 00294 case IRT_LQ: 00295 { 00296 ViewArray<BoolView> x(home,n_n); 00297 for (int i=n_n; i--; ) 00298 x[i]=t_n[i].x; 00299 GECODE_ES_FAIL((GqBoolInt<BoolView>::post(home,x,-c))); 00300 } 00301 break; 00302 default: GECODE_NEVER; 00303 } 00304 } 00305 00306 void 00307 post_neg_unit(Home home, 00308 Term<BoolView>* t_n, int n_n, 00309 IntRelType r, int c, BoolView b, 00310 IntConLevel) { 00311 switch (r) { 00312 case IRT_EQ: 00313 { 00314 ViewArray<BoolView> x(home,n_n); 00315 for (int i=n_n; i--; ) 00316 x[i]=t_n[i].x; 00317 GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView>::post(home,x,-c,b))); 00318 } 00319 break; 00320 case IRT_NQ: 00321 { 00322 ViewArray<BoolView> x(home,n_n); 00323 for (int i=n_n; i--; ) 00324 x[i]=t_n[i].x; 00325 NegBoolView nb(b); 00326 GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView>::post(home,x,-c,nb))); 00327 } 00328 break; 00329 case IRT_GQ: 00330 { 00331 ViewArray<NegBoolView> x(home,n_n); 00332 for (int i=n_n; i--; ) 00333 x[i]=NegBoolView(t_n[i].x); 00334 GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView>::post(home,x,n_n+c,b))); 00335 } 00336 break; 00337 case IRT_LQ: 00338 { 00339 ViewArray<BoolView> x(home,n_n); 00340 for (int i=n_n; i--; ) 00341 x[i]=t_n[i].x; 00342 GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView>::post(home,x,-c,b))); 00343 } 00344 break; 00345 default: GECODE_NEVER; 00346 } 00347 } 00348 00349 void 00350 post_mixed(Home home, 00351 Term<BoolView>* t_p, int n_p, 00352 Term<BoolView>* t_n, int n_n, 00353 IntRelType r, IntView y, int c) { 00354 ScaleBoolArray b_p(home,n_p); 00355 { 00356 ScaleBool* f=b_p.fst(); 00357 for (int i=n_p; i--; ) { 00358 f[i].x=t_p[i].x; f[i].a=t_p[i].a; 00359 } 00360 } 00361 ScaleBoolArray b_n(home,n_n); 00362 { 00363 ScaleBool* f=b_n.fst(); 00364 for (int i=n_n; i--; ) { 00365 f[i].x=t_n[i].x; f[i].a=t_n[i].a; 00366 } 00367 } 00368 switch (r) { 00369 case IRT_EQ: 00370 GECODE_ES_FAIL( 00371 (EqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView> 00372 ::post(home,b_p,b_n,y,c))); 00373 break; 00374 case IRT_NQ: 00375 GECODE_ES_FAIL( 00376 (NqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView> 00377 ::post(home,b_p,b_n,y,c))); 00378 break; 00379 case IRT_LQ: 00380 GECODE_ES_FAIL( 00381 (LqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView> 00382 ::post(home,b_p,b_n,y,c))); 00383 break; 00384 case IRT_GQ: 00385 { 00386 MinusView m(y); 00387 GECODE_ES_FAIL( 00388 (LqBoolScale<ScaleBoolArray,ScaleBoolArray,MinusView> 00389 ::post(home,b_n,b_p,m,-c))); 00390 } 00391 break; 00392 default: 00393 GECODE_NEVER; 00394 } 00395 } 00396 00397 00398 void 00399 post_mixed(Home home, 00400 Term<BoolView>* t_p, int n_p, 00401 Term<BoolView>* t_n, int n_n, 00402 IntRelType r, ZeroIntView y, int c) { 00403 ScaleBoolArray b_p(home,n_p); 00404 { 00405 ScaleBool* f=b_p.fst(); 00406 for (int i=n_p; i--; ) { 00407 f[i].x=t_p[i].x; f[i].a=t_p[i].a; 00408 } 00409 } 00410 ScaleBoolArray b_n(home,n_n); 00411 { 00412 ScaleBool* f=b_n.fst(); 00413 for (int i=n_n; i--; ) { 00414 f[i].x=t_n[i].x; f[i].a=t_n[i].a; 00415 } 00416 } 00417 switch (r) { 00418 case IRT_EQ: 00419 GECODE_ES_FAIL( 00420 (EqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView> 00421 ::post(home,b_p,b_n,y,c))); 00422 break; 00423 case IRT_NQ: 00424 GECODE_ES_FAIL( 00425 (NqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView> 00426 ::post(home,b_p,b_n,y,c))); 00427 break; 00428 case IRT_LQ: 00429 GECODE_ES_FAIL( 00430 (LqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView> 00431 ::post(home,b_p,b_n,y,c))); 00432 break; 00433 case IRT_GQ: 00434 GECODE_ES_FAIL( 00435 (LqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView> 00436 ::post(home,b_n,b_p,y,-c))); 00437 break; 00438 default: 00439 GECODE_NEVER; 00440 } 00441 } 00442 00443 template<class View> 00444 forceinline void 00445 post_all(Home home, 00446 Term<BoolView>* t, int n, 00447 IntRelType r, View x, int c) { 00448 00449 Limits::check(c,"Int::linear"); 00450 00451 double d = c; 00452 00453 eliminate(t,n,d); 00454 00455 rewrite(r,d); 00456 00457 c = static_cast<int>(d); 00458 00459 Term<BoolView> *t_p, *t_n; 00460 int n_p, n_n; 00461 bool unit = normalize<BoolView>(t,n,t_p,n_p,t_n,n_n); 00462 00463 if (n == 0) { 00464 switch (r) { 00465 case IRT_EQ: GECODE_ME_FAIL(x.eq(home,-c)); break; 00466 case IRT_NQ: GECODE_ME_FAIL(x.nq(home,-c)); break; 00467 case IRT_GQ: GECODE_ME_FAIL(x.lq(home,-c)); break; 00468 case IRT_LQ: GECODE_ME_FAIL(x.gq(home,-c)); break; 00469 default: GECODE_NEVER; 00470 } 00471 return; 00472 } 00473 00474 // Check for overflow 00475 { 00476 double sl = x.max()+c; 00477 double su = x.min()+c; 00478 for (int i=n_p; i--; ) 00479 su -= t_p[i].a; 00480 for (int i=n_n; i--; ) 00481 sl += t_n[i].a; 00482 Limits::check(sl,"Int::linear"); 00483 Limits::check(su,"Int::linear"); 00484 } 00485 00486 if (unit && (n_n == 0)) { 00488 post_pos_unit(home,t_p,n_p,r,x,c); 00489 } else if (unit && (n_p == 0)) { 00490 // All coefficients are -1 00491 post_neg_unit(home,t_n,n_n,r,x,c); 00492 } else { 00493 // Mixed coefficients 00494 post_mixed(home,t_p,n_p,t_n,n_n,r,x,c); 00495 } 00496 } 00497 00498 00499 void 00500 post(Home home, 00501 Term<BoolView>* t, int n, IntRelType r, IntView x, int c, 00502 IntConLevel) { 00503 post_all(home,t,n,r,x,c); 00504 } 00505 00506 void 00507 post(Home home, 00508 Term<BoolView>* t, int n, IntRelType r, int c, 00509 IntConLevel) { 00510 ZeroIntView x; 00511 post_all(home,t,n,r,x,c); 00512 } 00513 00514 void 00515 post(Home home, 00516 Term<BoolView>* t, int n, IntRelType r, IntView x, BoolView b, 00517 IntConLevel icl) { 00518 int l, u; 00519 estimate(t,n,0,l,u); 00520 IntVar z(home,l,u); IntView zv(z); 00521 post_all(home,t,n,IRT_EQ,zv,0); 00522 rel(home,z,r,x,b,icl); 00523 } 00524 00525 void 00526 post(Home home, 00527 Term<BoolView>* t, int n, IntRelType r, int c, BoolView b, 00528 IntConLevel icl) { 00529 00530 if (b.one()) 00531 return post(home,t,n,r,c,icl); 00532 if (b.zero()) 00533 return post(home,t,n,inverse(r),c,icl); 00534 00535 Limits::check(c,"Int::linear"); 00536 00537 double d = c; 00538 00539 eliminate(t,n,d); 00540 00541 rewrite(r,d); 00542 00543 c = static_cast<int>(d); 00544 00545 if (n == 0) { 00546 bool fail = false; 00547 switch (r) { 00548 case IRT_EQ: fail = (0 != c); break; 00549 case IRT_NQ: fail = (0 == c); break; 00550 case IRT_GQ: fail = (0 < c); break; 00551 case IRT_LQ: fail = (0 > c); break; 00552 default: GECODE_NEVER; 00553 } 00554 if ((fail ? b.zero(home) : b.one(home)) == ME_INT_FAILED) 00555 home.fail(); 00556 return; 00557 } 00558 00559 Term<BoolView> *t_p, *t_n; 00560 int n_p, n_n; 00561 bool unit = normalize<BoolView>(t,n,t_p,n_p,t_n,n_n); 00562 00563 // Check for overflow 00564 { 00565 double sl = c; 00566 double su = c; 00567 for (int i=n_p; i--; ) 00568 su -= t_p[i].a; 00569 for (int i=n_n; i--; ) 00570 sl += t_n[i].a; 00571 Limits::check(sl,"Int::linear"); 00572 Limits::check(su,"Int::linear"); 00573 } 00574 00575 if (unit && (n_n == 0)) { 00577 post_pos_unit(home,t_p,n_p,r,c,b,icl); 00578 } else if (unit && (n_p == 0)) { 00579 // All coefficients are -1 00580 post_neg_unit(home,t_n,n_n,r,c,b,icl); 00581 } else { 00582 // Mixed coefficients 00583 /* 00584 * Denormalize: Make all t_n coefficients negative again 00585 * (t_p and t_n are shared in t) 00586 */ 00587 for (int i=n_n; i--; ) 00588 t_n[i].a = -t_n[i].a; 00589 00590 // Note: still slow implementation 00591 int l, u; 00592 estimate(t,n,0,l,u); 00593 IntVar z(home,l,u); IntView zv(z); 00594 post_all(home,t,n,IRT_EQ,zv,0); 00595 rel(home,z,r,c,b,icl); 00596 } 00597 } 00598 00599 }}} 00600 00601 // STATISTICS: int-post 00602