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