int-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 * 00006 * Copyright: 00007 * Christian Schulte, 2002 00008 * 00009 * Last modified: 00010 * $Date: 2010-08-02 14:34:35 +0200 (Mon, 02 Aug 2010) $ by $Author: tack $ 00011 * $Revision: 11321 $ 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 #include <cfloat> 00039 #include <algorithm> 00040 00041 #include <gecode/int/rel.hh> 00042 #include <gecode/int/linear.hh> 00043 00044 namespace Gecode { namespace Int { namespace Linear { 00045 00047 inline void 00048 eliminate(Term<IntView>* t, int &n, double& d) { 00049 for (int i=n; i--; ) 00050 if (t[i].x.assigned()) { 00051 d -= t[i].a * static_cast<double>(t[i].x.val()); 00052 t[i]=t[--n]; 00053 } 00054 if ((d < Limits::double_min) || (d > Limits::double_max)) 00055 throw OutOfLimits("Int::linear"); 00056 } 00057 00059 inline void 00060 rewrite(IntRelType &r, double &d, 00061 Term<IntView>* &t_p, int &n_p, 00062 Term<IntView>* &t_n, int &n_n) { 00063 switch (r) { 00064 case IRT_EQ: case IRT_NQ: case IRT_LQ: 00065 break; 00066 case IRT_LE: 00067 d--; r = IRT_LQ; break; 00068 case IRT_GR: 00069 d++; /* fall through */ 00070 case IRT_GQ: 00071 r = IRT_LQ; 00072 std::swap(n_p,n_n); std::swap(t_p,t_n); d = -d; 00073 break; 00074 default: 00075 throw UnknownRelation("Int::linear"); 00076 } 00077 } 00078 00080 inline bool 00081 precision(Term<IntView>* t_p, int n_p, 00082 Term<IntView>* t_n, int n_n, 00083 double d) { 00084 double sl = 0.0; 00085 double su = 0.0; 00086 00087 for (int i = n_p; i--; ) { 00088 sl += t_p[i].a * static_cast<double>(t_p[i].x.min()); 00089 su += t_p[i].a * static_cast<double>(t_p[i].x.max()); 00090 } 00091 for (int i = n_n; i--; ) { 00092 sl -= t_n[i].a * static_cast<double>(t_n[i].x.max()); 00093 su -= t_n[i].a * static_cast<double>(t_n[i].x.min()); 00094 } 00095 sl -= d; 00096 su -= d; 00097 00098 if ((sl < Limits::double_min) || (su > Limits::double_max)) 00099 throw OutOfLimits("Int::linear"); 00100 00101 bool is_ip = (sl >= Limits::min) && (su <= Limits::max); 00102 00103 for (int i = n_p; i--; ) { 00104 if (sl - t_p[i].a * static_cast<double>(t_p[i].x.min()) 00105 < Limits::double_min) 00106 throw OutOfLimits("Int::linear"); 00107 if (sl - t_p[i].a * static_cast<double>(t_p[i].x.min()) < Limits::min) 00108 is_ip = false; 00109 if (su - t_p[i].a * static_cast<double>(t_p[i].x.max()) 00110 > Limits::double_max) 00111 throw OutOfLimits("Int::linear"); 00112 if (su - t_p[i].a * static_cast<double>(t_p[i].x.max()) > Limits::max) 00113 is_ip = false; 00114 } 00115 for (int i = n_n; i--; ) { 00116 if (sl + t_n[i].a * static_cast<double>(t_n[i].x.min()) 00117 < Limits::double_min) 00118 throw OutOfLimits("Int::linear"); 00119 if (sl + t_n[i].a * static_cast<double>(t_n[i].x.min()) < Limits::min) 00120 is_ip = false; 00121 if (su + t_n[i].a * static_cast<double>(t_n[i].x.max()) 00122 > Limits::double_max) 00123 throw OutOfLimits("Int::linear"); 00124 if (su + t_n[i].a * static_cast<double>(t_n[i].x.max()) > Limits::max) 00125 is_ip = false; 00126 } 00127 return is_ip; 00128 } 00129 00134 template<class Val, class View> 00135 forceinline void 00136 post_nary(Home home, 00137 ViewArray<View>& x, ViewArray<View>& y, IntRelType r, Val c) { 00138 switch (r) { 00139 case IRT_EQ: 00140 GECODE_ES_FAIL((Eq<Val,View,View >::post(home,x,y,c))); 00141 break; 00142 case IRT_NQ: 00143 GECODE_ES_FAIL((Nq<Val,View,View >::post(home,x,y,c))); 00144 break; 00145 case IRT_LQ: 00146 GECODE_ES_FAIL((Lq<Val,View,View >::post(home,x,y,c))); 00147 break; 00148 default: GECODE_NEVER; 00149 } 00150 } 00151 00152 00154 #define GECODE_INT_PL_BIN(CLASS) \ 00155 switch (n_p) { \ 00156 case 2: \ 00157 GECODE_ES_FAIL((CLASS<int,IntView,IntView>::post \ 00158 (home,t_p[0].x,t_p[1].x,c))); \ 00159 break; \ 00160 case 1: \ 00161 GECODE_ES_FAIL((CLASS<int,IntView,MinusView>::post \ 00162 (home,t_p[0].x,MinusView(t_n[0].x),c))); \ 00163 break; \ 00164 case 0: \ 00165 GECODE_ES_FAIL((CLASS<int,MinusView,MinusView>::post \ 00166 (home,MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \ 00167 break; \ 00168 default: GECODE_NEVER; \ 00169 } 00170 00172 #define GECODE_INT_PL_TER(CLASS) \ 00173 switch (n_p) { \ 00174 case 3: \ 00175 GECODE_ES_FAIL((CLASS<int,IntView,IntView,IntView>::post \ 00176 (home,t_p[0].x,t_p[1].x,t_p[2].x,c))); \ 00177 break; \ 00178 case 2: \ 00179 GECODE_ES_FAIL((CLASS<int,IntView,IntView,MinusView>::post \ 00180 (home,t_p[0].x,t_p[1].x, \ 00181 MinusView(t_n[0].x),c))); \ 00182 break; \ 00183 case 1: \ 00184 GECODE_ES_FAIL((CLASS<int,IntView,MinusView,MinusView>::post \ 00185 (home,t_p[0].x, \ 00186 MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \ 00187 break; \ 00188 case 0: \ 00189 GECODE_ES_FAIL((CLASS<int,MinusView,MinusView,MinusView>::post \ 00190 (home,MinusView(t_n[0].x), \ 00191 MinusView(t_n[1].x),MinusView(t_n[2].x),c))); \ 00192 break; \ 00193 default: GECODE_NEVER; \ 00194 } 00195 00196 void 00197 post(Home home, Term<IntView>* t, int n, IntRelType r, int c, 00198 IntConLevel icl) { 00199 00200 Limits::check(c,"Int::linear"); 00201 00202 double d = c; 00203 00204 eliminate(t,n,d); 00205 00206 Term<IntView> *t_p, *t_n; 00207 int n_p, n_n; 00208 bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n); 00209 00210 rewrite(r,d,t_p,n_p,t_n,n_n); 00211 00212 if (n == 0) { 00213 switch (r) { 00214 case IRT_EQ: if (d != 0.0) home.fail(); break; 00215 case IRT_NQ: if (d == 0.0) home.fail(); break; 00216 case IRT_LQ: if (d < 0.0) home.fail(); break; 00217 default: GECODE_NEVER; 00218 } 00219 return; 00220 } 00221 00222 if (n == 1) { 00223 if (n_p == 1) { 00224 DoubleScaleView y(t_p[0].a,t_p[0].x); 00225 switch (r) { 00226 case IRT_EQ: GECODE_ME_FAIL(y.eq(home,d)); break; 00227 case IRT_NQ: GECODE_ME_FAIL(y.nq(home,d)); break; 00228 case IRT_LQ: GECODE_ME_FAIL(y.lq(home,d)); break; 00229 default: GECODE_NEVER; 00230 } 00231 } else { 00232 DoubleScaleView y(t_n[0].a,t_n[0].x); 00233 switch (r) { 00234 case IRT_EQ: GECODE_ME_FAIL(y.eq(home,-d)); break; 00235 case IRT_NQ: GECODE_ME_FAIL(y.nq(home,-d)); break; 00236 case IRT_LQ: GECODE_ME_FAIL(y.gq(home,-d)); break; 00237 default: GECODE_NEVER; 00238 } 00239 } 00240 return; 00241 } 00242 00243 bool is_ip = precision(t_p,n_p,t_n,n_n,d); 00244 00245 if (is_unit && is_ip && (icl != ICL_DOM)) { 00246 // Unit coefficients with integer precision 00247 c = static_cast<int>(d); 00248 if (n == 2) { 00249 switch (r) { 00250 case IRT_EQ: GECODE_INT_PL_BIN(EqBin); break; 00251 case IRT_NQ: GECODE_INT_PL_BIN(NqBin); break; 00252 case IRT_LQ: GECODE_INT_PL_BIN(LqBin); break; 00253 default: GECODE_NEVER; 00254 } 00255 } else if (n == 3) { 00256 switch (r) { 00257 case IRT_EQ: GECODE_INT_PL_TER(EqTer); break; 00258 case IRT_NQ: GECODE_INT_PL_TER(NqTer); break; 00259 case IRT_LQ: GECODE_INT_PL_TER(LqTer); break; 00260 default: GECODE_NEVER; 00261 } 00262 } else { 00263 ViewArray<IntView> x(home,n_p); 00264 for (int i = n_p; i--; ) 00265 x[i] = t_p[i].x; 00266 ViewArray<IntView> y(home,n_n); 00267 for (int i = n_n; i--; ) 00268 y[i] = t_n[i].x; 00269 post_nary<int,IntView>(home,x,y,r,c); 00270 } 00271 } else if (is_ip) { 00272 if (n==2 && is_unit && icl == ICL_DOM && r == IRT_EQ) { 00273 // Binary domain-consistent equality 00274 c = static_cast<int>(d); 00275 if (c==0) { 00276 switch (n_p) { 00277 case 2: { 00278 IntView x(t_p[0].x); 00279 MinusView y(t_p[1].x); 00280 GECODE_ES_FAIL( 00281 (Rel::EqDom<IntView,MinusView>::post(home,x,y))); 00282 break; 00283 } 00284 case 1: { 00285 IntView x(t_p[0].x); 00286 IntView y(t_n[0].x); 00287 GECODE_ES_FAIL( 00288 (Rel::EqDom<IntView,IntView>::post(home,x,y))); 00289 break; 00290 } 00291 case 0: { 00292 IntView x(t_n[0].x); 00293 MinusView y(t_n[1].x); 00294 GECODE_ES_FAIL( 00295 (Rel::EqDom<IntView,MinusView>::post(home,x,y))); 00296 break; 00297 } 00298 default: 00299 GECODE_NEVER; 00300 } 00301 } else { 00302 switch (n_p) { 00303 case 2: { 00304 MinusView x(t_p[0].x); 00305 OffsetView y(t_p[1].x, -c); 00306 GECODE_ES_FAIL( 00307 (Rel::EqDom<MinusView,OffsetView>::post(home,x,y))); 00308 break; 00309 } 00310 case 1: { 00311 IntView x(t_p[0].x); 00312 OffsetView y(t_n[0].x, c); 00313 GECODE_ES_FAIL( 00314 (Rel::EqDom<IntView,OffsetView>::post(home,x,y))); 00315 break; 00316 } 00317 case 0: { 00318 MinusView x(t_n[0].x); 00319 OffsetView y(t_n[1].x, c); 00320 GECODE_ES_FAIL( 00321 (Rel::EqDom<MinusView,OffsetView>::post(home,x,y))); 00322 break; 00323 } 00324 default: 00325 GECODE_NEVER; 00326 } 00327 } 00328 } else { 00329 // Arbitrary coefficients with integer precision 00330 c = static_cast<int>(d); 00331 ViewArray<IntScaleView> x(home,n_p); 00332 for (int i = n_p; i--; ) 00333 x[i] = IntScaleView(t_p[i].a,t_p[i].x); 00334 ViewArray<IntScaleView> y(home,n_n); 00335 for (int i = n_n; i--; ) 00336 y[i] = IntScaleView(t_n[i].a,t_n[i].x); 00337 if ((icl == ICL_DOM) && (r == IRT_EQ)) { 00338 GECODE_ES_FAIL((DomEq<int,IntScaleView>::post(home,x,y,c))); 00339 } else { 00340 post_nary<int,IntScaleView>(home,x,y,r,c); 00341 } 00342 } 00343 } else { 00344 // Arbitrary coefficients with double precision 00345 ViewArray<DoubleScaleView> x(home,n_p); 00346 for (int i = n_p; i--; ) 00347 x[i] = DoubleScaleView(t_p[i].a,t_p[i].x); 00348 ViewArray<DoubleScaleView> y(home,n_n); 00349 for (int i = n_n; i--; ) 00350 y[i] = DoubleScaleView(t_n[i].a,t_n[i].x); 00351 if ((icl == ICL_DOM) && (r == IRT_EQ)) { 00352 GECODE_ES_FAIL((DomEq<double,DoubleScaleView>::post(home,x,y,d))); 00353 } else { 00354 post_nary<double,DoubleScaleView>(home,x,y,r,d); 00355 } 00356 } 00357 } 00358 00359 #undef GECODE_INT_PL_BIN 00360 #undef GECODE_INT_PL_TER 00361 00362 00367 template<class Val, class View> 00368 forceinline void 00369 post_nary(Home home, 00370 ViewArray<View>& x, ViewArray<View>& y, 00371 IntRelType r, Val c, BoolView b) { 00372 switch (r) { 00373 case IRT_EQ: 00374 GECODE_ES_FAIL((ReEq<Val,View,View,BoolView>::post(home,x,y,c,b))); 00375 break; 00376 case IRT_NQ: 00377 { 00378 NegBoolView n(b); 00379 GECODE_ES_FAIL((ReEq<Val,View,View,NegBoolView>::post 00380 (home,x,y,c,n))); 00381 } 00382 break; 00383 case IRT_LQ: 00384 GECODE_ES_FAIL((ReLq<Val,View,View>::post(home,x,y,c,b))); 00385 break; 00386 default: GECODE_NEVER; 00387 } 00388 } 00389 00390 void 00391 post(Home home, 00392 Term<IntView>* t, int n, IntRelType r, int c, BoolView b, 00393 IntConLevel) { 00394 00395 Limits::check(c,"Int::linear"); 00396 00397 double d = c; 00398 00399 eliminate(t,n,d); 00400 00401 Term<IntView> *t_p, *t_n; 00402 int n_p, n_n; 00403 bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n); 00404 00405 rewrite(r,d,t_p,n_p,t_n,n_n); 00406 00407 if (n == 0) { 00408 bool fail = false; 00409 switch (r) { 00410 case IRT_EQ: fail = (d != 0.0); break; 00411 case IRT_NQ: fail = (d == 0.0); break; 00412 case IRT_LQ: fail = (0.0 > d); break; 00413 default: GECODE_NEVER; 00414 } 00415 if ((fail ? b.zero(home) : b.one(home)) == ME_INT_FAILED) 00416 home.fail(); 00417 return; 00418 } 00419 00420 bool is_ip = precision(t_p,n_p,t_n,n_n,d); 00421 00422 if (is_unit && is_ip) { 00423 c = static_cast<int>(d); 00424 if (n == 1) { 00425 switch (r) { 00426 case IRT_EQ: 00427 if (n_p == 1) { 00428 GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,BoolView>::post 00429 (home,t_p[0].x,c,b))); 00430 } else { 00431 GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,BoolView>::post 00432 (home,t_n[0].x,-c,b))); 00433 } 00434 break; 00435 case IRT_NQ: 00436 { 00437 NegBoolView nb(b); 00438 if (n_p == 1) { 00439 GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,NegBoolView>::post 00440 (home,t_p[0].x,c,nb))); 00441 } else { 00442 GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,NegBoolView>::post 00443 (home,t_n[0].x,-c,nb))); 00444 } 00445 } 00446 break; 00447 case IRT_LQ: 00448 if (n_p == 1) { 00449 GECODE_ES_FAIL((Rel::ReLqInt<IntView,BoolView>::post 00450 (home,t_p[0].x,c,b))); 00451 } else { 00452 NegBoolView nb(b); 00453 GECODE_ES_FAIL((Rel::ReLqInt<IntView,NegBoolView>::post 00454 (home,t_n[0].x,-c-1,nb))); 00455 } 00456 break; 00457 default: GECODE_NEVER; 00458 } 00459 } else if (n == 2) { 00460 switch (r) { 00461 case IRT_EQ: 00462 switch (n_p) { 00463 case 2: 00464 GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView>::post 00465 (home,t_p[0].x,t_p[1].x,c,b))); 00466 break; 00467 case 1: 00468 GECODE_ES_FAIL((ReEqBin<int,IntView,MinusView,BoolView>::post 00469 (home,t_p[0].x,MinusView(t_n[0].x),c,b))); 00470 break; 00471 case 0: 00472 GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView>::post 00473 (home,t_n[0].x,t_n[1].x,-c,b))); 00474 break; 00475 default: GECODE_NEVER; 00476 } 00477 break; 00478 case IRT_NQ: 00479 { 00480 NegBoolView nb(b); 00481 switch (n_p) { 00482 case 2: 00483 GECODE_ES_FAIL( 00484 (ReEqBin<int,IntView,IntView,NegBoolView>::post 00485 (home,t_p[0].x,t_p[1].x,c,nb))); 00486 break; 00487 case 1: 00488 GECODE_ES_FAIL( 00489 (ReEqBin<int,IntView,MinusView,NegBoolView>::post 00490 (home,t_p[0].x,MinusView(t_n[0].x),c, 00491 NegBoolView(b)))); 00492 break; 00493 case 0: 00494 GECODE_ES_FAIL( 00495 (ReEqBin<int,IntView,IntView,NegBoolView>::post 00496 (home,t_p[0].x,t_p[1].x,-c,NegBoolView(b)))); 00497 break; 00498 default: GECODE_NEVER; 00499 } 00500 } 00501 break; 00502 case IRT_LQ: 00503 switch (n_p) { 00504 case 2: 00505 GECODE_ES_FAIL((ReLqBin<int,IntView,IntView>::post 00506 (home,t_p[0].x,t_p[1].x,c,b))); 00507 break; 00508 case 1: 00509 GECODE_ES_FAIL((ReLqBin<int,IntView,MinusView>::post 00510 (home,t_p[0].x,MinusView(t_n[0].x),c,b))); 00511 break; 00512 case 0: 00513 GECODE_ES_FAIL((ReLqBin<int,MinusView,MinusView>::post 00514 (home,MinusView(t_n[0].x), 00515 MinusView(t_n[1].x),c,b))); 00516 break; 00517 default: GECODE_NEVER; 00518 } 00519 break; 00520 default: GECODE_NEVER; 00521 } 00522 } else { 00523 ViewArray<IntView> x(home,n_p); 00524 for (int i = n_p; i--; ) 00525 x[i] = t_p[i].x; 00526 ViewArray<IntView> y(home,n_n); 00527 for (int i = n_n; i--; ) 00528 y[i] = t_n[i].x; 00529 post_nary<int,IntView>(home,x,y,r,c,b); 00530 } 00531 } else if (is_ip) { 00532 // Arbitrary coefficients with integer precision 00533 c = static_cast<int>(d); 00534 ViewArray<IntScaleView> x(home,n_p); 00535 for (int i = n_p; i--; ) 00536 x[i] = IntScaleView(t_p[i].a,t_p[i].x); 00537 ViewArray<IntScaleView> y(home,n_n); 00538 for (int i = n_n; i--; ) 00539 y[i] = IntScaleView(t_n[i].a,t_n[i].x); 00540 post_nary<int,IntScaleView>(home,x,y,r,c,b); 00541 } else { 00542 // Arbitrary coefficients with double precision 00543 ViewArray<DoubleScaleView> x(home,n_p); 00544 for (int i = n_p; i--; ) 00545 x[i] = DoubleScaleView(t_p[i].a,t_p[i].x); 00546 ViewArray<DoubleScaleView> y(home,n_n); 00547 for (int i = n_n; i--; ) 00548 y[i] = DoubleScaleView(t_n[i].a,t_n[i].x); 00549 post_nary<double,DoubleScaleView>(home,x,y,r,d,b); 00550 } 00551 } 00552 00553 }}} 00554 00555 // STATISTICS: int-post