00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 #include "int/rel.hh"
00023 #include "int/linear.hh"
00024
00025 #include "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 int n_p, n_n;
00164 bool is_unit = preprocess(e,n,r,c,n_p,n_n);
00165 if (n == 0) {
00166 switch (r) {
00167 case IRT_EQ: if (c != 0) home->fail(); break;
00168 case IRT_NQ: if (c == 0) home->fail(); break;
00169 case IRT_LQ: if (0 > c) home->fail(); break;
00170 default: assert(0);
00171 }
00172 return;
00173 }
00174 if (n == 1) {
00175 if (e[0].a > 0) {
00176 DoubleScaleView y(e[0].a,e[0].x);
00177 switch (r) {
00178 case IRT_EQ: GECODE_ME_FAIL(home,y.eq(home,c)); break;
00179 case IRT_NQ: GECODE_ME_FAIL(home,y.nq(home,c)); break;
00180 case IRT_LQ: GECODE_ME_FAIL(home,y.lq(home,c)); break;
00181 default: assert(0);
00182 }
00183 } else {
00184 DoubleScaleView y(-e[0].a,e[0].x);
00185 switch (r) {
00186 case IRT_EQ: GECODE_ME_FAIL(home,y.eq(home,-c)); break;
00187 case IRT_NQ: GECODE_ME_FAIL(home,y.nq(home,-c)); break;
00188 case IRT_LQ: GECODE_ME_FAIL(home,y.gq(home,-c)); break;
00189 default: assert(0);
00190 }
00191 }
00192 return;
00193 }
00194 bool is_ip = int_precision(e,n,c);
00195 if (is_unit && is_ip) {
00196 if (n == 2) {
00197 switch (r) {
00198 case IRT_LQ:
00199 switch (n_p) {
00200 case 2:
00201 if (LqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c)
00202 == ES_FAILED) home->fail();
00203 break;
00204 case 1:
00205 if (LqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c)
00206 == ES_FAILED) home->fail();
00207 break;
00208 case 0:
00209 if (LqBin<int,MinusView,MinusView>::post(home,e[0].x,e[1].x,c)
00210 == ES_FAILED) home->fail();
00211 break;
00212 default:
00213 assert(0);
00214 }
00215 break;
00216 case IRT_EQ:
00217 switch (n_p) {
00218 case 2:
00219 if (EqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c)
00220 == ES_FAILED) home->fail();
00221 break;
00222 case 1:
00223 if (EqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c)
00224 == ES_FAILED) home->fail();
00225 break;
00226 case 0:
00227 if (EqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,-c)
00228 == ES_FAILED) home->fail();
00229 break;
00230 default:
00231 assert(0);
00232 }
00233 break;
00234 case IRT_NQ:
00235 switch (n_p) {
00236 case 2:
00237 if (NqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c)
00238 == ES_FAILED) home->fail();
00239 break;
00240 case 1:
00241 if (NqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c)
00242 == ES_FAILED) home->fail();
00243 break;
00244 case 0:
00245 if (NqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,-c)
00246 == ES_FAILED) home->fail();
00247 break;
00248 default:
00249 assert(0);
00250 }
00251 break;
00252 default:
00253 assert(0);
00254 }
00255 } else if (n == 3) {
00256 switch (r) {
00257 case IRT_LQ:
00258 switch (n_p) {
00259 case 3:
00260 if (LqTer<int,IntView,IntView,IntView>::post
00261 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00262 break;
00263 case 2:
00264 if (LqTer<int,IntView,IntView,MinusView>::post
00265 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00266 break;
00267 case 1:
00268 if (LqTer<int,IntView,MinusView,MinusView>::post
00269 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00270 break;
00271 case 0:
00272 if (LqTer<int,MinusView,MinusView,MinusView>::post
00273 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00274 break;
00275 default:
00276 assert(0);
00277 }
00278 break;
00279 case IRT_EQ:
00280 switch (n_p) {
00281 case 3:
00282 if (EqTer<int,IntView,IntView,IntView>::post
00283 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00284 break;
00285 case 2:
00286 if (EqTer<int,IntView,IntView,MinusView>::post
00287 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00288 break;
00289 case 1:
00290 if (EqTer<int,IntView,IntView,MinusView>::post
00291 (home,e[1].x,e[2].x,e[0].x,-c) == ES_FAILED) home->fail();
00292 break;
00293 case 0:
00294 if (EqTer<int,IntView,IntView,IntView>::post
00295 (home,e[0].x,e[1].x,e[2].x,-c) == ES_FAILED) home->fail();
00296 break;
00297 default:
00298 assert(0);
00299 }
00300 break;
00301 case IRT_NQ:
00302 switch (n_p) {
00303 case 3:
00304 if (NqTer<int,IntView,IntView,IntView>::post
00305 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00306 break;
00307 case 2:
00308 if (NqTer<int,IntView,IntView,MinusView>::post
00309 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00310 break;
00311 case 1:
00312 if (NqTer<int,IntView,IntView,MinusView>::post
00313 (home,e[1].x,e[2].x,e[0].x,-c) == ES_FAILED) home->fail();
00314 break;
00315 case 0:
00316 if (NqTer<int,IntView,IntView,IntView>::post
00317 (home,e[0].x,e[1].x,e[2].x,-c) == ES_FAILED) home->fail();
00318 break;
00319 default:
00320 assert(0);
00321 }
00322 break;
00323 default:
00324 assert(0);
00325 }
00326 } else {
00327 ViewArray<IntView> x(home,n_p);
00328 for (int i = n_p; i--; ) x[i] = e[i].x;
00329 ViewArray<IntView> y(home,n_n);
00330 for (int i = n_n; i--; ) y[i] = e[i+n_p].x;
00331 post_nary<int,IntView>(home,x,y,r,c);
00332 }
00333 } else {
00334 if (is_ip) {
00335 ViewArray<IntScaleView> x(home,n_p);
00336 for (int i = n_p; i--; )
00337 x[i].init(e[i].a,e[i].x);
00338 ViewArray<IntScaleView> y(home,n_n);
00339 for (int i = n_n; i--; )
00340 y[i].init(-e[i+n_p].a,e[i+n_p].x);
00341 post_nary<int,IntScaleView>(home,x,y,r,c);
00342 } else {
00343 ViewArray<DoubleScaleView> x(home,n_p);
00344 for (int i = n_p; i--; )
00345 x[i].init(e[i].a,e[i].x);
00346 ViewArray<DoubleScaleView> y(home,n_n);
00347 for (int i = n_n; i--; )
00348 y[i].init(-e[i+n_p].a,e[i+n_p].x);
00349 post_nary<double,DoubleScaleView>(home,x,y,r,c);
00350 }
00351 }
00352 }
00353
00354
00355
00356
00357
00358
00359
00360
00361 template <class Val, class View>
00362 forceinline void
00363 post_nary(Space* home,
00364 ViewArray<View>& x, ViewArray<View>& y, IntRelType r, Val c, BoolView b) {
00365 switch (r) {
00366 case IRT_LQ:
00367 if (ReLq<Val,View,View>::post(home,x,y,c,b) == ES_FAILED)
00368 home->fail();
00369 break;
00370 case IRT_EQ:
00371 if (ReEq<Val,View,View,BoolView>::post(home,x,y,c,b) == ES_FAILED)
00372 home->fail();
00373 break;
00374 case IRT_NQ:
00375 {
00376 NegBoolView n(b);
00377 if (ReEq<Val,View,View,NegBoolView>::post(home,x,y,c,n) == ES_FAILED)
00378 home->fail();
00379 }
00380 break;
00381 default:
00382 assert(0);
00383 }
00384 }
00385
00386 void
00387 post(Space* home,
00388 Term e[], int n, IntRelType r, int c, BoolView b) {
00389 int n_p, n_n;
00390 bool is_unit = preprocess(e,n,r,c,n_p,n_n);
00391 if (n == 0) {
00392 bool fail = false;
00393 switch (r) {
00394 case IRT_EQ: fail = (c != 0); break;
00395 case IRT_NQ: fail = (c == 0); break;
00396 case IRT_LQ: fail = (0 > c); break;
00397 default: assert(0);
00398 }
00399 if ((fail ? b.t_zero(home) : b.t_one(home)) == ME_INT_FAILED)
00400 home->fail();
00401 return;
00402 }
00403 bool is_ip = int_precision(e,n,c);
00404 if (is_unit && is_ip) {
00405 if (n == 1) {
00406 switch (r) {
00407 case IRT_EQ:
00408 if (e[0].a == 1) {
00409 if (Rel::ReEqBndInt<IntView,BoolView>::post(home,e[0].x,c,b)
00410 == ES_FAILED)
00411 home->fail();
00412 } else {
00413 if (Rel::ReEqBndInt<IntView,BoolView>::post(home,e[0].x,-c,b)
00414 == ES_FAILED)
00415 home->fail();
00416 }
00417 break;
00418 case IRT_NQ:
00419 {
00420 NegBoolView n(b);
00421 if (e[0].a == 1) {
00422 if (Rel::ReEqBndInt<IntView,NegBoolView>::post(home,e[0].x,c,n)
00423 == ES_FAILED)
00424 home->fail();
00425 } else {
00426 if (Rel::ReEqBndInt<IntView,NegBoolView>::post(home,e[0].x,-c,n)
00427 == ES_FAILED)
00428 home->fail();
00429 }
00430 }
00431 break;
00432 case IRT_LQ:
00433 if (e[0].a == 1) {
00434 if (Rel::ReLqInt<IntView,BoolView>::post(home,e[0].x,c,b)
00435 == ES_FAILED)
00436 home->fail();
00437 } else {
00438 NegBoolView n(b);
00439 if (Rel::ReLqInt<IntView,NegBoolView>::post(home,e[0].x,-c-1,n)
00440 == ES_FAILED)
00441 home->fail();
00442 }
00443 break;
00444 default:
00445 assert(false);
00446 }
00447 } else if (n == 2) {
00448 switch (r) {
00449 case IRT_LQ:
00450 switch (n_p) {
00451 case 2:
00452 if (ReLqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c,b)
00453 == ES_FAILED) home->fail();
00454 break;
00455 case 1:
00456 if (ReLqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c,b)
00457 == ES_FAILED) home->fail();
00458 break;
00459 case 0:
00460 if (ReLqBin<int,MinusView,MinusView>::post(home,e[0].x,e[1].x,c,b)
00461 == ES_FAILED) home->fail();
00462 break;
00463 default:
00464 assert(0);
00465 }
00466 break;
00467 case IRT_EQ:
00468 switch (n_p) {
00469 case 2:
00470 if (ReEqBin<int,IntView,IntView,BoolView>::post
00471 (home,e[0].x,e[1].x,c,b)
00472 == ES_FAILED) home->fail();
00473 break;
00474 case 1:
00475 if (ReEqBin<int,IntView,MinusView,BoolView>::post
00476 (home,e[0].x,e[1].x,c,b)
00477 == ES_FAILED) home->fail();
00478 break;
00479 case 0:
00480 if (ReEqBin<int,IntView,IntView,BoolView>::post
00481 (home,e[0].x,e[1].x,-c,b)
00482 == ES_FAILED) home->fail();
00483 break;
00484 default:
00485 assert(0);
00486 }
00487 break;
00488 case IRT_NQ:
00489 {
00490 NegBoolView n(b);
00491 switch (n_p) {
00492 case 2:
00493 if (ReEqBin<int,IntView,IntView,NegBoolView>::post
00494 (home,e[0].x,e[1].x,c,n)
00495 == ES_FAILED) home->fail();
00496 break;
00497 case 1:
00498 if (ReEqBin<int,IntView,MinusView,NegBoolView>::post
00499 (home,e[0].x,e[1].x,c,b)
00500 == ES_FAILED) home->fail();
00501 break;
00502 case 0:
00503 if (ReEqBin<int,IntView,IntView,NegBoolView>::post
00504 (home,e[0].x,e[1].x,-c,b)
00505 == ES_FAILED) home->fail();
00506 break;
00507 default:
00508 assert(0);
00509 }
00510 }
00511 break;
00512 default:
00513 assert(0);
00514 }
00515 } else {
00516 ViewArray<IntView> x(home,n_p);
00517 for (int i = n_p; i--; ) x[i] = e[i].x;
00518 ViewArray<IntView> y(home,n_n);
00519 for (int i = n_n; i--; ) y[i] = e[i+n_p].x;
00520 post_nary<int,IntView>(home,x,y,r,c,b);
00521 }
00522 } else {
00523 if (is_ip) {
00524 ViewArray<IntScaleView> x(home,n_p);
00525 for (int i = n_p; i--; )
00526 x[i].init(e[i].a,e[i].x);
00527 ViewArray<IntScaleView> y(home,n_n);
00528 for (int i = n_n; i--; )
00529 y[i].init(-e[i+n_p].a,e[i+n_p].x);
00530 post_nary<int,IntScaleView>(home,x,y,r,c,b);
00531 } else {
00532 ViewArray<DoubleScaleView> x(home,n_p);
00533 for (int i = n_p; i--; )
00534 x[i].init(e[i].a,e[i].x);
00535 ViewArray<DoubleScaleView> y(home,n_n);
00536 for (int i = n_n; i--; )
00537 y[i].init(-e[i+n_p].a,e[i+n_p].x);
00538 post_nary<double,DoubleScaleView>(home,x,y,r,c,b);
00539 }
00540 }
00541 }
00542
00543 }}}
00544
00545
00546