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-06-03 20:34:20 +0200 (Thu, 03 Jun 2010) $ by $Author: schulte $ 00011 * $Revision: 11017 $ 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 // Arbitrary coefficients with integer precision 00273 c = static_cast<int>(d); 00274 ViewArray<IntScaleView> x(home,n_p); 00275 for (int i = n_p; i--; ) 00276 x[i] = IntScaleView(t_p[i].a,t_p[i].x); 00277 ViewArray<IntScaleView> y(home,n_n); 00278 for (int i = n_n; i--; ) 00279 y[i] = IntScaleView(t_n[i].a,t_n[i].x); 00280 if ((icl == ICL_DOM) && (r == IRT_EQ)) { 00281 GECODE_ES_FAIL((DomEq<int,IntScaleView>::post(home,x,y,c))); 00282 } else { 00283 post_nary<int,IntScaleView>(home,x,y,r,c); 00284 } 00285 } else { 00286 // Arbitrary coefficients with double precision 00287 ViewArray<DoubleScaleView> x(home,n_p); 00288 for (int i = n_p; i--; ) 00289 x[i] = DoubleScaleView(t_p[i].a,t_p[i].x); 00290 ViewArray<DoubleScaleView> y(home,n_n); 00291 for (int i = n_n; i--; ) 00292 y[i] = DoubleScaleView(t_n[i].a,t_n[i].x); 00293 if ((icl == ICL_DOM) && (r == IRT_EQ)) { 00294 GECODE_ES_FAIL((DomEq<double,DoubleScaleView>::post(home,x,y,d))); 00295 } else { 00296 post_nary<double,DoubleScaleView>(home,x,y,r,d); 00297 } 00298 } 00299 } 00300 00301 #undef GECODE_INT_PL_BIN 00302 #undef GECODE_INT_PL_TER 00303 00304 00309 template<class Val, class View> 00310 forceinline void 00311 post_nary(Home home, 00312 ViewArray<View>& x, ViewArray<View>& y, 00313 IntRelType r, Val c, BoolView b) { 00314 switch (r) { 00315 case IRT_EQ: 00316 GECODE_ES_FAIL((ReEq<Val,View,View,BoolView>::post(home,x,y,c,b))); 00317 break; 00318 case IRT_NQ: 00319 { 00320 NegBoolView n(b); 00321 GECODE_ES_FAIL((ReEq<Val,View,View,NegBoolView>::post 00322 (home,x,y,c,n))); 00323 } 00324 break; 00325 case IRT_LQ: 00326 GECODE_ES_FAIL((ReLq<Val,View,View>::post(home,x,y,c,b))); 00327 break; 00328 default: GECODE_NEVER; 00329 } 00330 } 00331 00332 void 00333 post(Home home, 00334 Term<IntView>* t, int n, IntRelType r, int c, BoolView b, 00335 IntConLevel) { 00336 00337 Limits::check(c,"Int::linear"); 00338 00339 double d = c; 00340 00341 eliminate(t,n,d); 00342 00343 Term<IntView> *t_p, *t_n; 00344 int n_p, n_n; 00345 bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n); 00346 00347 rewrite(r,d,t_p,n_p,t_n,n_n); 00348 00349 if (n == 0) { 00350 bool fail = false; 00351 switch (r) { 00352 case IRT_EQ: fail = (d != 0.0); break; 00353 case IRT_NQ: fail = (d == 0.0); break; 00354 case IRT_LQ: fail = (0.0 > d); break; 00355 default: GECODE_NEVER; 00356 } 00357 if ((fail ? b.zero(home) : b.one(home)) == ME_INT_FAILED) 00358 home.fail(); 00359 return; 00360 } 00361 00362 bool is_ip = precision(t_p,n_p,t_n,n_n,d); 00363 00364 if (is_unit && is_ip) { 00365 c = static_cast<int>(d); 00366 if (n == 1) { 00367 switch (r) { 00368 case IRT_EQ: 00369 if (n_p == 1) { 00370 GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,BoolView>::post 00371 (home,t_p[0].x,c,b))); 00372 } else { 00373 GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,BoolView>::post 00374 (home,t_n[0].x,-c,b))); 00375 } 00376 break; 00377 case IRT_NQ: 00378 { 00379 NegBoolView nb(b); 00380 if (n_p == 1) { 00381 GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,NegBoolView>::post 00382 (home,t_p[0].x,c,nb))); 00383 } else { 00384 GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,NegBoolView>::post 00385 (home,t_n[0].x,-c,nb))); 00386 } 00387 } 00388 break; 00389 case IRT_LQ: 00390 if (n_p == 1) { 00391 GECODE_ES_FAIL((Rel::ReLqInt<IntView,BoolView>::post 00392 (home,t_p[0].x,c,b))); 00393 } else { 00394 NegBoolView nb(b); 00395 GECODE_ES_FAIL((Rel::ReLqInt<IntView,NegBoolView>::post 00396 (home,t_n[0].x,-c-1,nb))); 00397 } 00398 break; 00399 default: GECODE_NEVER; 00400 } 00401 } else if (n == 2) { 00402 switch (r) { 00403 case IRT_EQ: 00404 switch (n_p) { 00405 case 2: 00406 GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView>::post 00407 (home,t_p[0].x,t_p[1].x,c,b))); 00408 break; 00409 case 1: 00410 GECODE_ES_FAIL((ReEqBin<int,IntView,MinusView,BoolView>::post 00411 (home,t_p[0].x,MinusView(t_n[0].x),c,b))); 00412 break; 00413 case 0: 00414 GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView>::post 00415 (home,t_n[0].x,t_n[1].x,-c,b))); 00416 break; 00417 default: GECODE_NEVER; 00418 } 00419 break; 00420 case IRT_NQ: 00421 { 00422 NegBoolView nb(b); 00423 switch (n_p) { 00424 case 2: 00425 GECODE_ES_FAIL( 00426 (ReEqBin<int,IntView,IntView,NegBoolView>::post 00427 (home,t_p[0].x,t_p[1].x,c,nb))); 00428 break; 00429 case 1: 00430 GECODE_ES_FAIL( 00431 (ReEqBin<int,IntView,MinusView,NegBoolView>::post 00432 (home,t_p[0].x,MinusView(t_n[0].x),c, 00433 NegBoolView(b)))); 00434 break; 00435 case 0: 00436 GECODE_ES_FAIL( 00437 (ReEqBin<int,IntView,IntView,NegBoolView>::post 00438 (home,t_p[0].x,t_p[1].x,-c,NegBoolView(b)))); 00439 break; 00440 default: GECODE_NEVER; 00441 } 00442 } 00443 break; 00444 case IRT_LQ: 00445 switch (n_p) { 00446 case 2: 00447 GECODE_ES_FAIL((ReLqBin<int,IntView,IntView>::post 00448 (home,t_p[0].x,t_p[1].x,c,b))); 00449 break; 00450 case 1: 00451 GECODE_ES_FAIL((ReLqBin<int,IntView,MinusView>::post 00452 (home,t_p[0].x,MinusView(t_n[0].x),c,b))); 00453 break; 00454 case 0: 00455 GECODE_ES_FAIL((ReLqBin<int,MinusView,MinusView>::post 00456 (home,MinusView(t_n[0].x), 00457 MinusView(t_n[1].x),c,b))); 00458 break; 00459 default: GECODE_NEVER; 00460 } 00461 break; 00462 default: GECODE_NEVER; 00463 } 00464 } else { 00465 ViewArray<IntView> x(home,n_p); 00466 for (int i = n_p; i--; ) 00467 x[i] = t_p[i].x; 00468 ViewArray<IntView> y(home,n_n); 00469 for (int i = n_n; i--; ) 00470 y[i] = t_n[i].x; 00471 post_nary<int,IntView>(home,x,y,r,c,b); 00472 } 00473 } else if (is_ip) { 00474 // Arbitrary coefficients with integer precision 00475 c = static_cast<int>(d); 00476 ViewArray<IntScaleView> x(home,n_p); 00477 for (int i = n_p; i--; ) 00478 x[i] = IntScaleView(t_p[i].a,t_p[i].x); 00479 ViewArray<IntScaleView> y(home,n_n); 00480 for (int i = n_n; i--; ) 00481 y[i] = IntScaleView(t_n[i].a,t_n[i].x); 00482 post_nary<int,IntScaleView>(home,x,y,r,c,b); 00483 } else { 00484 // Arbitrary coefficients with double precision 00485 ViewArray<DoubleScaleView> x(home,n_p); 00486 for (int i = n_p; i--; ) 00487 x[i] = DoubleScaleView(t_p[i].a,t_p[i].x); 00488 ViewArray<DoubleScaleView> y(home,n_n); 00489 for (int i = n_n; i--; ) 00490 y[i] = DoubleScaleView(t_n[i].a,t_n[i].x); 00491 post_nary<double,DoubleScaleView>(home,x,y,r,d,b); 00492 } 00493 } 00494 00495 }}} 00496 00497 // STATISTICS: int-post