00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038 #include "gecode/cpltset/propagators.hh"
00039
00040 using namespace Gecode::CpltSet;
00041
00042 namespace Gecode {
00043
00044 namespace CpltSet { namespace Rel {
00045
00051 template <class View>
00052 void rel_post(Space* home, View x, CpltSetRelType r, View y) {
00053
00054 if (home->failed()) return;
00055
00056
00057
00058 unsigned int xoff = x.offset();
00059 unsigned int yoff = y.offset();
00060 unsigned int tab = std::max(x.tableWidth(), y.tableWidth());
00061
00062
00063 bdd d0 = bdd_true();
00064
00065 switch(r) {
00066 case SRT_LE:
00067 {
00068 d0 = lexlt(xoff, yoff, tab, tab - 1);
00069 }
00070 break;
00071 case SRT_GR:
00072 {
00073 d0 = lexlt(yoff, xoff, tab, tab - 1);
00074 }
00075 break;
00076 case SRT_LQ:
00077 {
00078 d0 = lexlq(xoff, yoff, tab, tab - 1);
00079 }
00080 break;
00081 case SRT_GQ:
00082 {
00083 d0 = lexlt(yoff, xoff, tab, tab - 1);
00084 }
00085 break;
00086 case SRT_LE_REV:
00087 {
00088 d0 = lexltrev(xoff, yoff, tab, 0);
00089 }
00090 break;
00091 case SRT_GR_REV:
00092 {
00093 d0 = lexltrev(yoff, xoff, tab, 0);
00094 }
00095 break;
00096 case SRT_LQ_REV:
00097 {
00098 d0 = lexlqrev(xoff, yoff, tab, 0);
00099 }
00100 break;
00101 case SRT_GQ_REV:
00102 {
00103 d0 = lexltrev(yoff, xoff, tab, 0);
00104 }
00105 break;
00106 default:
00107 {
00108 throw CpltSet::InvalidRelation (" COMPL = EQ NEG y ??? ");
00109 return;
00110 }
00111 }
00112
00113 GECODE_ES_FAIL(home,
00114 (BinaryCpltSetPropagator<View,View>::post(home, x, y, d0)));
00115 }
00116
00117 template <class View>
00118 void rel_post(Space* home, View x, SetRelType r, View y) {
00119
00120 if (home->failed()) return;
00121
00122
00123
00124 unsigned int tab = std::max(x.tableWidth(), y.tableWidth());
00125
00126
00127 bdd d0 = bdd_true();
00128
00129 switch(r) {
00130 case SRT_SUB:
00131 {
00132 for (int i = 0; i < (int) tab; i++) {
00133 d0 &= (x.element(i)) >>= (y.element(i));
00134 }
00135 }
00136 break;
00137 case SRT_SUP:
00138 {
00139 for (int i = 0; i < (int) tab; i++) {
00140 d0 &= (y.element(i)) >>= (x.element(i));
00141 }
00142 }
00143 break;
00144
00145 case SRT_DISJ:
00146 {
00147 Set::LubRanges<View> lubx(x);
00148 Set::LubRanges<View> luby(y);
00149 Gecode::Iter::Ranges::Inter<Set::LubRanges<View>,
00150 Set::LubRanges<View> > inter(lubx, luby);
00151 Gecode::Iter::Ranges::ToValues<
00152 Gecode::Iter::Ranges::Inter<Set::LubRanges<View>,
00153 Set::LubRanges<View> > > ival(inter);
00154
00155 Gecode::Iter::Ranges::ValCache<
00156 Gecode::Iter::Ranges::ToValues<
00157 Gecode::Iter::Ranges::Inter<Set::LubRanges<View>,
00158 Set::LubRanges<View> > > > cache(ival);
00159
00160 if (!cache()) {
00161 return;
00162 } else {
00163 cache.last();
00164 for (; cache(); --cache) {
00165 int v = cache.min();
00166 int minx = x.initialLubMin();
00167 int miny = y.initialLubMin();
00168 d0 &= (!(x.element(v - minx) & y.element(v - miny)));
00169 }
00170 }
00171 GECODE_ES_FAIL(home, (BinRelDisj<View,View>::post(home, x, y, d0)));
00172 return;
00173 }
00174 break;
00175 case SRT_EQ:
00176 {
00177 int xshift = 0;
00178 for (int i = 0; i < (int) tab; i++) {
00179 if (y.initialLubMin() + i < x.initialLubMin() ||
00180 y.initialLubMin() + i > x.initialLubMax()) {
00181 d0 &= (bdd_false() % y.element(i));
00182 xshift++;
00183 } else {
00184 d0 &= (x.element(i - xshift) % y.element(i));
00185 }
00186 }
00187 }
00188 break;
00189 case SRT_NQ:
00190 {
00191 Set::LubRanges<View> lubx(x);
00192 Set::LubRanges<View> luby(y);
00193 Gecode::Iter::Ranges::Inter<Set::LubRanges<View>,
00194 Set::LubRanges<View> > inter(lubx, luby);
00195 Gecode::Iter::Ranges::ToValues<
00196 Gecode::Iter::Ranges::Inter<Set::LubRanges<View>,
00197 Set::LubRanges<View> > > ival(inter);
00198 if (!ival()) {
00199 return;
00200 } else {
00201 for (; ival(); ++ival) {
00202 int v = ival.val();
00203 assert(v >= x.initialLubMin());
00204 assert(v <= x.initialLubMax());
00205 d0 &= (x.element(v - x.initialLubMin()) %
00206 y.element(v - x.initialLubMax()));
00207 }
00208 }
00209 d0 = !d0;
00210 }
00211 break;
00212 default:
00213 {
00214 throw CpltSet::InvalidRelation (" COMPL = EQ NEG y ??? ");
00215 return;
00216 }
00217 }
00218
00219 GECODE_ES_FAIL(home,
00220 (BinaryCpltSetPropagator<View,View>::post(home, x, y, d0)));
00221 }
00222
00223 template <class View0, class View1>
00224 void rel_post(Space* home, View0 x, CpltSetRelType r, View1 s) {
00225 if (home->failed()) return;
00226
00227
00228
00229 unsigned int xoff = x.offset();
00230 unsigned int yoff = s.offset();
00231 unsigned int tab = std::max(x.tableWidth(), s.tableWidth());
00232
00233
00234 bdd d0 = bdd_true();
00235
00236 switch(r) {
00237
00238
00239
00240 case SRT_LE:
00241 {
00242 d0 = lexlt(xoff, yoff, tab, tab - 1);
00243 }
00244 break;
00245 case SRT_GR:
00246 {
00247 d0 = lexlt(yoff, xoff, tab, tab - 1);
00248 }
00249 break;
00250 case SRT_LQ:
00251 {
00252 d0 = lexlq(xoff, yoff, tab, tab - 1);
00253 }
00254 break;
00255 case SRT_GQ:
00256 {
00257 d0 = lexlt(yoff, xoff, tab, tab - 1);
00258 }
00259 break;
00260 default:
00261 {
00262 throw CpltSet::InvalidRelation (" COMPL = EQ NEG y ??? ");
00263 return;
00264 }
00265 }
00266
00267 GECODE_ES_FAIL(home,
00268 (BinaryCpltSetPropagator<View0, View1>::post(home, x, s, d0)));
00269 }
00270
00271
00272 template <class View0, class View1>
00273 void rel_post(Space* home, View0 x, SetRelType r, View1 s) {
00274 if (home->failed()) return;
00275
00276
00277
00278 unsigned int tab = std::max(x.tableWidth(), s.tableWidth());
00279
00280
00281 bdd d0 = bdd_true();
00282
00283 switch(r) {
00284 case SRT_SUB:
00285 {
00286
00287 int xshift = x.initialLubMin() - s.initialLubMin();
00288 for (int i = 0; i < (int) tab; i++) {
00289 if (s.initialLubMin() + i >= x.initialLubMin()) {
00290 if (s.initialLubMin() + i <= x.initialLubMax()) {
00291 d0 &= (x.element(i - xshift)) >>= (s.element(i));
00292 } else {
00293
00294 }
00295 } else {
00296
00297 }
00298 }
00299 }
00300
00301 if (s.assigned()) {
00302
00303 d0 &= s.dom();
00304 }
00305 break;
00306 case SRT_SUP:
00307 {
00308 for (int i = 0; i < (int) tab; i++) {
00309 d0 &= (s.element(i)) >>= (x.element(i));
00310 }
00311 }
00312 break;
00313 case SRT_DISJ:
00314 {
00315 for (int i = 0; i < (int) tab; i++) {
00316 d0 &= !(s.element(i) & x.element(i));
00317 }
00318 }
00319 break;
00320 case SRT_EQ:
00321 {
00322 int xshift = 0;
00323 for (int i = 0; i < (int) tab; i++) {
00324 if (s.initialLubMin() + i < x.initialLubMin() ||
00325 s.initialLubMin() + i > x.initialLubMax()) {
00326 d0 &= (bdd_false() % s.element(i));
00327 xshift++;
00328 } else {
00329 d0 &= (x.element(i - xshift) % s.element(i));
00330 }
00331 }
00332 }
00333 break;
00334 case SRT_NQ:
00335 {
00336 for (int i = 0; i < (int) tab; i++) {
00337 d0 &= ((x.element(i)) % (s.element(i)));
00338 }
00339 d0 = !d0;
00340 }
00341 break;
00342 default:
00343 {
00344 throw CpltSet::InvalidRelation (" COMPL = EQ NEG y ??? ");
00345 return;
00346 }
00347 }
00348
00349 GECODE_ES_FAIL(home,
00350 (BinaryCpltSetPropagator<View0, View1>::post(home, x, s, d0)));
00351 }
00352
00353
00354
00355 template <class View>
00356 void rel_post(Space*, ViewArray<View>&, CpltSetOpType,
00357 CpltSetRelType) {
00358 throw CpltSet::InvalidRelation(" no bdd rel implemented lex smaller ....");
00359 }
00360
00361
00362 template <class View>
00363 void rel_post(Space* home, ViewArray<View>& x, CpltSetOpType o,
00364 SetRelType r) {
00365 if (home->failed()) return;
00366
00367
00368
00369 int x0_tab = x[0].tableWidth();
00370
00371
00372 bdd d0 = bdd_true();
00373
00374 for (int i = x0_tab; i--; ) {
00375 bdd op = bdd_true();
00376 switch(o) {
00377 case SOT_SYMDIFF:
00378 {
00379 op = ((x[0].element(i) & (!x[1].element(i))) |
00380 (!x[0].element(i) & (x[1].element(i)))) ;
00381 break;
00382 }
00383 default:
00384 {
00385 throw CpltSet::InvalidRelation(" other op rel relations not yet implemented ");
00386 return;
00387 }
00388 }
00389 switch (r) {
00390 case SRT_EQ:
00391 {
00392 d0 &= (op % x[2].element(i));
00393 break;
00394 }
00395 default:
00396 {
00397 throw CpltSet::InvalidRelation(" other rel relations not yet implemented ");
00398 return;
00399 }
00400 }
00401 }
00402
00403 GECODE_ES_FAIL(home, NaryCpltSetPropagator<View>::post(home, x, d0));
00404 }
00405
00406
00407
00408 template <class View>
00409 void rel_post(Space*, ViewArray<View>&, SetOpType,
00410 CpltSetRelType) {
00411 throw CpltSet::InvalidRelation(" no bdd rel implemented lex smaller with setoptype....");
00412 }
00413
00414
00415
00416 template <class View>
00417 void rel_post(Space* home, ViewArray<View>& x,
00418 SetOpType o, SetRelType r) {
00419 if (home->failed()) return;
00420
00421
00422
00423 int x0_tab = x[0].tableWidth();
00424
00425
00426 bdd d0 = bdd_true();
00427
00428 for (int i = x0_tab; i--; ) {
00429 bdd op = bdd_true();
00430 switch(o) {
00431 case SOT_UNION:
00432 {
00433 op = (x[0].element(i) | x[1].element(i));
00434 break;
00435 }
00436 case SOT_DUNION:
00437 {
00438 op = (x[0].element(i) | x[1].element(i));
00439
00440 break;
00441 }
00442 case SOT_INTER:
00443 {
00444 op = x[0].element(i) & x[1].element(i);
00445 break;
00446 }
00447 case SOT_MINUS:
00448 {
00449 op = x[0].element(i) & (!x[1].element(i));
00450 break;
00451 }
00452 default:
00453 {
00454 GECODE_NEVER;
00455 return;
00456 }
00457 }
00458 switch (r) {
00459 case SRT_EQ:
00460 {
00461 d0 &= (op % x[2].element(i));
00462 if (o == SOT_DUNION)
00463 d0 &= !(x[0].element(i) & x[1].element(i));
00464 break;
00465 }
00466 default:
00467 {
00468 throw CpltSet::InvalidRelation(" other rel relations not yet implemented ");
00469 return;
00470 }
00471 }
00472 }
00473 GECODE_ES_FAIL(home, NaryCpltSetPropagator<View>::post(home, x, d0));
00474 }
00475
00476
00477 template <class Rel>
00478 void rel_con(Space* home, const CpltSetVar& x, Rel r,
00479 const CpltSetVar& y) {
00480 CpltSetView xv(x);
00481 CpltSetView yv(y);
00482 rel_post(home, xv, r, yv);
00483 }
00484
00485 template <class Rel, class Op>
00486 forceinline void
00487 rel_con_bdd(Space* home, const CpltSetVar& x, Op o, const CpltSetVar& y,
00488 Rel r, const CpltSetVar& z) {
00489 ViewArray<CpltSetView> bv(home, 3);
00490 bv[0] = x;
00491 bv[1] = y;
00492 bv[2] = z;
00493 rel_post(home, bv, o, r);
00494 }
00495
00496 }}
00497
00498 using namespace CpltSet::Rel;
00499
00500 void rel(Space* home, CpltSetVar x, CpltSetRelType r, CpltSetVar y) {
00501 rel_con(home, x, r, y);
00502 }
00503
00504 void rel(Space* home, CpltSetVar x, CpltSetOpType o, CpltSetVar y,
00505 CpltSetRelType r, CpltSetVar z) {
00506 rel_con_bdd(home, x, o, y, r, z);
00507 }
00508
00509 void rel(Space* home, CpltSetVar x, CpltSetOpType o, CpltSetVar y,
00510 SetRelType r, CpltSetVar z) {
00511 rel_con_bdd(home, x, o, y, r, z);
00512 }
00513
00514 void rel(Space* home, CpltSetVar x, SetOpType o, CpltSetVar y,
00515 CpltSetRelType r, CpltSetVar z) {
00516 rel_con_bdd(home, x, o, y, r, z);
00517 }
00518
00519 void rel(Space* home, CpltSetVar x, SetOpType o, CpltSetVar y, SetRelType r,
00520 CpltSetVar z) {
00521 rel_con_bdd(home, x, o, y, r, z);
00522 }
00523
00524 void rel(Space* home, CpltSetVar x, SetRelType r, CpltSetVar y) {
00525 rel_con(home, x, r, y);
00526 }
00527
00528 }
00529
00530