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: GECODE_NEVER;
00157 }
00158 }
00159
00160 void
00161 post(Space* home, Term e[], int n, IntRelType r, int c,
00162 IntConLevel icl) {
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: GECODE_NEVER;
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: GECODE_NEVER;
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: GECODE_NEVER;
00190 }
00191 }
00192 return;
00193 }
00194 bool is_ip = int_precision(e,n,c);
00195 if (is_unit && is_ip && (icl != ICL_DOM)) {
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: GECODE_NEVER;
00213 }
00214 break;
00215 case IRT_EQ:
00216 switch (n_p) {
00217 case 2:
00218 if (EqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c)
00219 == ES_FAILED) home->fail();
00220 break;
00221 case 1:
00222 if (EqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c)
00223 == ES_FAILED) home->fail();
00224 break;
00225 case 0:
00226 if (EqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,-c)
00227 == ES_FAILED) home->fail();
00228 break;
00229 default: GECODE_NEVER;
00230 }
00231 break;
00232 case IRT_NQ:
00233 switch (n_p) {
00234 case 2:
00235 if (NqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c)
00236 == ES_FAILED) home->fail();
00237 break;
00238 case 1:
00239 if (NqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c)
00240 == ES_FAILED) home->fail();
00241 break;
00242 case 0:
00243 if (NqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,-c)
00244 == ES_FAILED) home->fail();
00245 break;
00246 default: GECODE_NEVER;
00247 }
00248 break;
00249 default: GECODE_NEVER;
00250 }
00251 } else if (n == 3) {
00252 switch (r) {
00253 case IRT_LQ:
00254 switch (n_p) {
00255 case 3:
00256 if (LqTer<int,IntView,IntView,IntView>::post
00257 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00258 break;
00259 case 2:
00260 if (LqTer<int,IntView,IntView,MinusView>::post
00261 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00262 break;
00263 case 1:
00264 if (LqTer<int,IntView,MinusView,MinusView>::post
00265 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00266 break;
00267 case 0:
00268 if (LqTer<int,MinusView,MinusView,MinusView>::post
00269 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00270 break;
00271 default: GECODE_NEVER;
00272 }
00273 break;
00274 case IRT_EQ:
00275 switch (n_p) {
00276 case 3:
00277 if (EqTer<int,IntView,IntView,IntView>::post
00278 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00279 break;
00280 case 2:
00281 if (EqTer<int,IntView,IntView,MinusView>::post
00282 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00283 break;
00284 case 1:
00285 if (EqTer<int,IntView,IntView,MinusView>::post
00286 (home,e[1].x,e[2].x,e[0].x,-c) == ES_FAILED) home->fail();
00287 break;
00288 case 0:
00289 if (EqTer<int,IntView,IntView,IntView>::post
00290 (home,e[0].x,e[1].x,e[2].x,-c) == ES_FAILED) home->fail();
00291 break;
00292 default: GECODE_NEVER;
00293 }
00294 break;
00295 case IRT_NQ:
00296 switch (n_p) {
00297 case 3:
00298 if (NqTer<int,IntView,IntView,IntView>::post
00299 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00300 break;
00301 case 2:
00302 if (NqTer<int,IntView,IntView,MinusView>::post
00303 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00304 break;
00305 case 1:
00306 if (NqTer<int,IntView,IntView,MinusView>::post
00307 (home,e[1].x,e[2].x,e[0].x,-c) == ES_FAILED) home->fail();
00308 break;
00309 case 0:
00310 if (NqTer<int,IntView,IntView,IntView>::post
00311 (home,e[0].x,e[1].x,e[2].x,-c) == ES_FAILED) home->fail();
00312 break;
00313 default: GECODE_NEVER;
00314 }
00315 break;
00316 default: GECODE_NEVER;
00317 }
00318 } else {
00319 ViewArray<IntView> x(home,n_p);
00320 for (int i = n_p; i--; ) x[i] = e[i].x;
00321 ViewArray<IntView> y(home,n_n);
00322 for (int i = n_n; i--; ) y[i] = e[i+n_p].x;
00323 post_nary<int,IntView>(home,x,y,r,c);
00324 }
00325 } else {
00326 if (is_ip) {
00327 ViewArray<IntScaleView> x(home,n_p);
00328 for (int i = n_p; i--; )
00329 x[i].init(e[i].a,e[i].x);
00330 ViewArray<IntScaleView> y(home,n_n);
00331 for (int i = n_n; i--; )
00332 y[i].init(-e[i+n_p].a,e[i+n_p].x);
00333 if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00334 if (DomEq<int,IntScaleView>::post(home,x,y,c) == ES_FAILED)
00335 home->fail();
00336 } else {
00337 post_nary<int,IntScaleView>(home,x,y,r,c);
00338 }
00339 } else {
00340 ViewArray<DoubleScaleView> x(home,n_p);
00341 for (int i = n_p; i--; )
00342 x[i].init(e[i].a,e[i].x);
00343 ViewArray<DoubleScaleView> y(home,n_n);
00344 for (int i = n_n; i--; )
00345 y[i].init(-e[i+n_p].a,e[i+n_p].x);
00346 if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00347 if (DomEq<double,DoubleScaleView>::post(home,x,y,c) == ES_FAILED)
00348 home->fail();
00349 } else {
00350 post_nary<double,DoubleScaleView>(home,x,y,r,c);
00351 }
00352 }
00353 }
00354 }
00355
00356
00357
00358
00359
00360
00361
00362
00363 template <class Val, class View>
00364 forceinline void
00365 post_nary(Space* home,
00366 ViewArray<View>& x, ViewArray<View>& y, IntRelType r, Val c, BoolView b) {
00367 switch (r) {
00368 case IRT_LQ:
00369 if (ReLq<Val,View,View>::post(home,x,y,c,b) == ES_FAILED)
00370 home->fail();
00371 break;
00372 case IRT_EQ:
00373 if (ReEq<Val,View,View,BoolView>::post(home,x,y,c,b) == ES_FAILED)
00374 home->fail();
00375 break;
00376 case IRT_NQ:
00377 {
00378 NegBoolView n(b);
00379 if (ReEq<Val,View,View,NegBoolView>::post(home,x,y,c,n) == ES_FAILED)
00380 home->fail();
00381 }
00382 break;
00383 default: GECODE_NEVER;
00384 }
00385 }
00386
00387 void
00388 post(Space* home,
00389 Term e[], int n, IntRelType r, int c, BoolView b) {
00390 int n_p, n_n;
00391 bool is_unit = preprocess(e,n,r,c,n_p,n_n);
00392 if (n == 0) {
00393 bool fail = false;
00394 switch (r) {
00395 case IRT_EQ: fail = (c != 0); break;
00396 case IRT_NQ: fail = (c == 0); break;
00397 case IRT_LQ: fail = (0 > c); break;
00398 default: GECODE_NEVER;
00399 }
00400 if ((fail ? b.t_zero(home) : b.t_one(home)) == ME_INT_FAILED)
00401 home->fail();
00402 return;
00403 }
00404 bool is_ip = int_precision(e,n,c);
00405 if (is_unit && is_ip) {
00406 if (n == 1) {
00407 switch (r) {
00408 case IRT_EQ:
00409 if (e[0].a == 1) {
00410 if (Rel::ReEqBndInt<IntView,BoolView>::post(home,e[0].x,c,b)
00411 == ES_FAILED)
00412 home->fail();
00413 } else {
00414 if (Rel::ReEqBndInt<IntView,BoolView>::post(home,e[0].x,-c,b)
00415 == ES_FAILED)
00416 home->fail();
00417 }
00418 break;
00419 case IRT_NQ:
00420 {
00421 NegBoolView n(b);
00422 if (e[0].a == 1) {
00423 if (Rel::ReEqBndInt<IntView,NegBoolView>::post(home,e[0].x,c,n)
00424 == ES_FAILED)
00425 home->fail();
00426 } else {
00427 if (Rel::ReEqBndInt<IntView,NegBoolView>::post(home,e[0].x,-c,n)
00428 == ES_FAILED)
00429 home->fail();
00430 }
00431 }
00432 break;
00433 case IRT_LQ:
00434 if (e[0].a == 1) {
00435 if (Rel::ReLqInt<IntView,BoolView>::post(home,e[0].x,c,b)
00436 == ES_FAILED)
00437 home->fail();
00438 } else {
00439 NegBoolView n(b);
00440 if (Rel::ReLqInt<IntView,NegBoolView>::post(home,e[0].x,-c-1,n)
00441 == ES_FAILED)
00442 home->fail();
00443 }
00444 break;
00445 default: GECODE_NEVER;
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: GECODE_NEVER;
00464 }
00465 break;
00466 case IRT_EQ:
00467 switch (n_p) {
00468 case 2:
00469 if (ReEqBin<int,IntView,IntView,BoolView>::post
00470 (home,e[0].x,e[1].x,c,b)
00471 == ES_FAILED) home->fail();
00472 break;
00473 case 1:
00474 if (ReEqBin<int,IntView,MinusView,BoolView>::post
00475 (home,e[0].x,e[1].x,c,b)
00476 == ES_FAILED) home->fail();
00477 break;
00478 case 0:
00479 if (ReEqBin<int,IntView,IntView,BoolView>::post
00480 (home,e[0].x,e[1].x,-c,b)
00481 == ES_FAILED) home->fail();
00482 break;
00483 default: GECODE_NEVER;
00484 }
00485 break;
00486 case IRT_NQ:
00487 {
00488 NegBoolView n(b);
00489 switch (n_p) {
00490 case 2:
00491 if (ReEqBin<int,IntView,IntView,NegBoolView>::post
00492 (home,e[0].x,e[1].x,c,n)
00493 == ES_FAILED) home->fail();
00494 break;
00495 case 1:
00496 if (ReEqBin<int,IntView,MinusView,NegBoolView>::post
00497 (home,e[0].x,e[1].x,c,b)
00498 == ES_FAILED) home->fail();
00499 break;
00500 case 0:
00501 if (ReEqBin<int,IntView,IntView,NegBoolView>::post
00502 (home,e[0].x,e[1].x,-c,b)
00503 == ES_FAILED) home->fail();
00504 break;
00505 default: GECODE_NEVER;
00506 }
00507 }
00508 break;
00509 default: GECODE_NEVER;
00510 }
00511 } else {
00512 ViewArray<IntView> x(home,n_p);
00513 for (int i = n_p; i--; ) x[i] = e[i].x;
00514 ViewArray<IntView> y(home,n_n);
00515 for (int i = n_n; i--; ) y[i] = e[i+n_p].x;
00516 post_nary<int,IntView>(home,x,y,r,c,b);
00517 }
00518 } else {
00519 if (is_ip) {
00520 ViewArray<IntScaleView> x(home,n_p);
00521 for (int i = n_p; i--; )
00522 x[i].init(e[i].a,e[i].x);
00523 ViewArray<IntScaleView> y(home,n_n);
00524 for (int i = n_n; i--; )
00525 y[i].init(-e[i+n_p].a,e[i+n_p].x);
00526 post_nary<int,IntScaleView>(home,x,y,r,c,b);
00527 } else {
00528 ViewArray<DoubleScaleView> x(home,n_p);
00529 for (int i = n_p; i--; )
00530 x[i].init(e[i].a,e[i].x);
00531 ViewArray<DoubleScaleView> y(home,n_n);
00532 for (int i = n_n; i--; )
00533 y[i].init(-e[i+n_p].a,e[i+n_p].x);
00534 post_nary<double,DoubleScaleView>(home,x,y,r,c,b);
00535 }
00536 }
00537 }
00538
00539 }}}
00540
00541
00542
