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.hh"
00039
00040 namespace Gecode { namespace CpltSet {
00041
00042 void
00043 conv_hull(bdd& robdd, bdd& hull) {
00044 if (manager.leaf(robdd)) { hull = robdd; return; }
00045 BddIterator bi(robdd);
00046 while(bi()) {
00047 int stat = bi.status();
00048 int lev = bi.label();
00049
00050
00051
00052 if (stat == FIX_GLB) { hull &= manager.bddpos(lev); }
00053 if (stat == FIX_NOT_LUB) { hull &= manager.negbddpos(lev); }
00054 ++bi;
00055 }
00056 return;
00057 }
00058
00059 bdd
00060 bdd_vars(bdd& robdd) {
00061 bdd allvars = bdd_true();
00062 BddIterator bi(robdd);
00063 while(bi()) {
00064 int lev = bi.label();
00065
00066
00067
00068 bdd cur = manager.bddpos(lev);
00069 assert(!manager.marked(cur));
00070 allvars &= cur;
00071 ++bi;
00072 }
00073 return allvars;
00074 }
00075
00076 bdd
00077 cardeq(int offset, int c, int n, int r) {
00078 GECODE_AUTOARRAY(bdd, layer, n);
00079 for (int i = n; i--;)
00080 layer[i].init();
00081
00082
00083 layer[0] = bdd_true();
00084 for (int i = 1; i <= c; i++) {
00085 layer[i].init();
00086 layer[i] = manager.bddpos(offset + r - i + 1);
00087 }
00088
00089
00090 for (int i = 1; i < n; i++) {
00091 layer[i] = manager.ite(layer[i], layer[i - 1], bdd_false());
00092 }
00093
00094
00095 for (int k = r + 1; --k; ) {
00096 int col = k;
00097 for (int i = 0; i < n; i++) {
00098 bdd t = bdd_true();
00099 if (i == 0) {
00100 t = bdd_false();
00101 } else {
00102 t = layer[i-1];
00103 }
00104 layer[i] = manager.ite(manager.bddpos(offset + col), t,layer[i]);
00105 col--;
00106 if (col < 0) { k = 1; break; }
00107 }
00108 }
00109 return layer[n - 1];
00110 }
00111
00112 bdd
00113 cardlqgq(int offset, int cl, int cr, int n, int r) {
00114 GECODE_AUTOARRAY(bdd, layer, n);
00115
00116
00117 for (int i = n; i--;)
00118 layer[i].init();
00119
00120
00121 layer[n - cl - 1] = bdd_true();
00122 int k = r;
00123 for (int i = n - cl ; i < n; i++) {
00124 layer[i] = manager.ite(manager.bddpos(offset + k), layer[i - 1],
00125 bdd_false());
00126 k--;
00127 }
00128
00129 for (k = r; k--; ) {
00130 int col = k;
00131
00132 for (int i = n - cl; i < n; i++) {
00133 bdd t = layer[i-1];
00134 layer[i] = manager.ite(manager.bddpos(offset + col), t, layer[i]);
00135 col--;
00136 if (col < r + 1 - cr) { k = 0; break;}
00137 }
00138 }
00139
00140 if (cr == r + 1) {
00141 return layer[n - 1];
00142 }
00143
00144 if (cr == r) {
00145 int col = r;
00146
00147 bdd t = bdd_true();
00148 bdd f = bdd_true();
00149 bdd zerot = bdd_false();
00150 bdd zerof = t;
00151 for (int i = 0; i < n; i++) {
00152 if (i == 0) {
00153 t = zerot;
00154 f = zerof;
00155 } else {
00156 t = layer[i-1];
00157 if (i > n - cl - 1) {
00158 f = layer[i];
00159 }
00160 }
00161 layer[i] = manager.ite(manager.bddpos(offset + col), t ,f);
00162 col--;
00163 if (col < 0) { break;}
00164 }
00165
00166 return layer[n- 1];
00167 }
00168
00169
00170
00171 int col = r;
00172 {
00173 bdd t = bdd_true();
00174 bdd f = bdd_true();
00175 for (int i = 0; i < n; i++) {
00176 if (i == 0) {
00177 t = bdd_false();
00178 } else {
00179 t = layer[i-1];
00180
00181 if (i > n - cl - 1 && cl > 0) {
00182 f = layer[i];
00183 }
00184 }
00185 layer[i] = manager.ite(manager.bddpos(offset + col), t ,f);
00186 col--;
00187 if (col < 0) { break;}
00188 }
00189 }
00190
00191
00192 for (k = r; --k; ) {
00193 int col = k;
00194 for (int i = 0; i < n; i++) {
00195 bdd t = bdd_true();
00196 if (i == 0) {
00197 t = bdd_false();
00198 } else {
00199 t = layer[i-1];
00200 }
00201 layer[i] = manager.ite(manager.bddpos(offset + col), t, layer[i]);
00202 col--;
00203 if (col < 0) { k = 1; break;}
00204 }
00205 }
00206 return layer[n - 1];
00207 }
00208
00209 bdd
00210 cardcheck(int xtab, int offset, int cl, int cr) {
00211 if (cr > xtab) {
00212 cr = xtab;
00213 }
00214 int r = xtab - 1;
00215 int n = cr + 1;
00216 if (cl > xtab || cl > cr)
00217 return bdd_false();
00218
00219 if (cr == 0) {
00220
00221 bdd empty = bdd_true();
00222 for (int i = xtab; i--; ) {
00223 empty &= manager.negbddpos(offset + i);
00224 }
00225 return empty;
00226 }
00227
00228 if (cl == cr) {
00229 if (cr == xtab) {
00230
00231 bdd full = bdd_true();
00232 for (int i = xtab; i--; ) {
00233 full &= manager.bddpos(offset + i);
00234 }
00235 return full;
00236 } else {
00237 return cardeq(offset, cr, n, r);
00238 }
00239 }
00240
00241
00242 if (cr == xtab) {
00243 if (cl == 0) {
00244 return bdd_true();
00245 }
00246 }
00247 return cardlqgq(offset, cl, cr, n, r);
00248 }
00249
00250 bdd
00251 lexlt(unsigned int& xoff, unsigned int& yoff, unsigned int& range, int n) {
00252 if (n < 0) { return bdd_false(); }
00253
00254 bdd cur = bdd_true();
00255 cur &= ((manager.negbddpos(xoff + n)) & (manager.bddpos(yoff + n)));
00256 cur |= ( ((manager.bddpos(xoff + n)) % (manager.bddpos(yoff + n))) &
00257 lexlt(xoff, yoff, range, n - 1));
00258 return cur;
00259 }
00260
00261 bdd
00262 lexlq(unsigned int& xoff, unsigned int& yoff, unsigned int& range, int n) {
00263 if (n < 0) { return bdd_true(); }
00264
00265 bdd cur = bdd_true();
00266 cur &= ((manager.negbddpos(xoff + n)) & (manager.bddpos(yoff + n)));
00267 cur |= ( ((manager.bddpos(xoff + n)) % (manager.bddpos(yoff + n))) &
00268 lexlq(xoff, yoff, range, n - 1));
00269 return cur;
00270 }
00271
00272
00273 bdd
00274 lexltrev(unsigned int& xoff, unsigned int& yoff,
00275 unsigned int& range, int n) {
00276 if (n > (int) range - 1) { return bdd_false(); }
00277 bdd cur = bdd_true();
00278 cur &= ((manager.negbddpos(xoff + n)) & (manager.bddpos(yoff + n)));
00279 cur |= ( ((manager.bddpos(xoff + n)) % (manager.bddpos(yoff + n))) &
00280 lexltrev(xoff, yoff, range, n + 1));
00281 return cur;
00282 }
00283
00284 bdd
00285 lexlqrev(unsigned int& xoff, unsigned int& yoff,
00286 unsigned int& range, int n) {
00287 if (n > static_cast<int> (range) - 1) { return bdd_true(); }
00288
00289 bdd cur = bdd_true();
00290 cur &= ((manager.negbddpos(xoff + n)) & (manager.bddpos(yoff + n)));
00291 cur |= ( ((manager.bddpos(xoff + n)) % (manager.bddpos(yoff + n))) &
00292 lexlqrev(xoff, yoff, range, n + 1));
00293 return cur;
00294 }
00295
00296
00297 void
00298 extcache_mark(Support::DynamicArray<bdd>& nodes,
00299 int n, int& l, int& r, int& markref) {
00300
00301 if (l > 0) {
00302 for (int i = 0; i < l; i++) {
00303 if (!manager.marked(nodes[i])) {
00304 manager.mark(nodes[i]);
00305 markref++;
00306 }
00307 }
00308 }
00309
00310 if (r < n - 1) {
00311 for (int i = r + 1; i < n; i++) {
00312 if (!manager.marked(nodes[i])) {
00313 manager.mark(nodes[i]);
00314 markref++;
00315 }
00316 }
00317 }
00318 }
00319
00320
00321 void
00322 extcache_unmark(Support::DynamicArray<bdd>& nodes,
00323 int n, int& l, int& r, int& markref) {
00324 if (l > 0) {
00325 for (int i = 0; i < l; i++) {
00326 if (manager.marked(nodes[i])) {
00327 manager.unmark(nodes[i]);
00328 markref--;
00329 }
00330 }
00331 }
00332 if (r < n - 1) {
00333 for (int i = r + 1; i < n; i++) {
00334 if (manager.marked(nodes[i])) {
00335 manager.unmark(nodes[i]);
00336 markref--;
00337 }
00338 }
00339 }
00340 }
00341
00342
00343
00344 void
00345 extcardbounds(int& markref, bdd&, int& n, int& l, int& r,
00346 bool& singleton, int& _level,
00347 Support::DynamicArray<bdd>& nodes,
00348 int& curmin, int& curmax) {
00349 bdd cur = bdd_true();
00350
00351 if (((l == 0) && (r == n - 1))) {
00352
00353 singleton = false;
00354 extcache_unmark(nodes, n, l, r, markref);
00355 assert(markref == 0);
00356 return;
00357 }
00358
00359
00360 extcache_mark(nodes, n, l, r,markref);
00361 if (l > 0) {
00362 _level++;
00363 }
00364
00365
00366 bool stackleft = false;
00367 while (l > 0) {
00368 stackleft = true;
00369
00370
00371
00372
00373
00374
00375
00376
00377 while ((l > 1) &&
00378 manager.bddidx(nodes[l - 1]) < manager.bddidx(nodes[l - 2])) {
00379 int shift = l - 2;
00380 int norm = l - 1;
00381 manager.unmark(nodes[shift]); markref--;
00382 if (r == n - 1) {
00383 nodes[r] = nodes[shift];
00384 manager.mark(nodes[r]); markref++;
00385 } else {
00386 for (int i = r; i < n - 1; i++) {
00387 nodes[i] = nodes[i + 1];
00388 }
00389 nodes[n - 1] = nodes[shift];
00390 manager.mark(nodes[n - 1]); markref++;
00391 }
00392 r--;
00393 nodes[shift] = nodes[norm];
00394 nodes[norm].init();
00395 l--;
00396 }
00397
00398 while ((l > 1) &&
00399 manager.bddidx(nodes[l - 1]) > manager.bddidx(nodes[l - 2])) {
00400 int shift = l - 1;
00401 manager.unmark(nodes[shift]); markref--;
00402 if (r == n - 1) {
00403 nodes[r] = nodes[shift];
00404 manager.mark(nodes[r]); markref++;
00405 } else {
00406 for (int i = r; i < n - 1; i++) {
00407 nodes[i] = nodes[i + 1];
00408 }
00409 nodes[n - 1] = nodes[shift];
00410 manager.mark(nodes[n - 1]); markref++;
00411 }
00412 r--;
00413 nodes[shift].init();
00414 l--;
00415 }
00416
00417 l--;
00418 manager.unmark(nodes[l]);
00419 markref--;
00420 cur = nodes[l];
00421 assert(!manager.marked(cur));
00422 nodes[l].init();
00423
00424
00425 if (!manager.leaf(cur)) {
00426 bdd t = manager.iftrue(cur);
00427 bdd f = manager.iffalse(cur);
00428
00429
00430 bool leaf_t = manager.leaf(t);
00431 bool leaf_f = manager.leaf(f);
00432
00433 if (!leaf_t) {
00434 if (!manager.marked(t)) {
00435
00436
00437 nodes[r] = t;
00438 manager.lbCard(t, manager.lbCard(cur) + 1);
00439 manager.ubCard(t, manager.ubCard(cur) + 1);
00440
00441 manager.mark(nodes[r]);
00442 markref++;
00443 r--;
00444 } else {
00445 int lc = std::min(manager.lbCard(cur) + 1, manager.lbCard(t));
00446 int uc = std::max(manager.ubCard(cur) + 1, manager.ubCard(t));
00447 manager.lbCard(t, lc);
00448 manager.ubCard(t, uc);
00449 }
00450 } else {
00451
00452 if (manager.ctrue(t)) {
00453 int minval = manager.lbCard(cur) + 1;
00454 int maxval = manager.ubCard(cur) + 1;
00455 curmin = std::min(curmin, minval);
00456 curmax = std::max(curmax, maxval);
00457
00458 }
00459 }
00460
00461 if (!leaf_f) {
00462 if (!manager.marked(f)) {
00463 nodes[r] = f;
00464 manager.lbCard(f, manager.lbCard(cur));
00465 manager.ubCard(f, manager.ubCard(cur));
00466 manager.mark(nodes[r]);
00467 markref++;
00468 r--;
00469 } else {
00470 int lc = std::min(manager.lbCard(cur), manager.lbCard(f));
00471 int uc = std::max(manager.ubCard(cur), manager.ubCard(f));
00472 manager.lbCard(f, lc);
00473 manager.ubCard(f, uc);
00474 }
00475 } else {
00476
00477 if (manager.ctrue(f)) {
00478 int minval = manager.lbCard(cur);
00479 int maxval = manager.ubCard(cur);
00480 curmin = std::min(curmin, minval);
00481 curmax = std::max(curmax, maxval);
00482 }
00483 }
00484 } else {
00485
00486 }
00487 if (((l == 0) && (r == n - 1))) {
00488
00489
00490 singleton = true;
00491 }
00492 }
00493
00494
00495
00496 if (stackleft) {
00497 extcache_unmark(nodes, n, l, r, markref);
00498 assert(markref == 0);
00499 return;
00500 }
00501
00502 if (r < n - 1) {
00503 _level++;
00504 }
00505
00506
00507 while (r < n - 1) {
00508 while ((r < n - 2) && manager.bddidx(nodes[r + 1]) <
00509 manager.bddidx(nodes[r + 2])) {
00510 int shift = r + 2;
00511 int norm = r + 1;
00512 manager.unmark(nodes[shift]); markref--;
00513 if (l == 0) {
00514 nodes[l] = nodes[shift];
00515 manager.mark(nodes[l]); markref++;
00516 } else {
00517 for (int i = l; i > 0; i--) {
00518 nodes[i] = nodes[i - 1];
00519 }
00520 nodes[0] = nodes[shift];
00521 manager.mark(nodes[0]); markref++;
00522 }
00523 l++;
00524 nodes[shift] = nodes[norm];
00525 nodes[norm].init();
00526 r++;
00527 }
00528
00529 while ((r < n - 2) && manager.bddidx(nodes[r + 1]) >
00530 manager.bddidx(nodes[r + 2])) {
00531 int shift = r + 1;
00532 manager.unmark(nodes[shift]); markref--;
00533 if (l == 0) {
00534 nodes[l] = nodes[shift];
00535 manager.mark(nodes[l]); markref++;
00536 } else {
00537 for (int i = l; i > 0; i--) {
00538 nodes[i] = nodes[i - 1];
00539 }
00540 nodes[0] = nodes[shift];
00541 manager.mark(nodes[0]); markref++;
00542 }
00543 l++;
00544 nodes[shift].init();
00545 r++;
00546 }
00547
00548
00549
00550 r++;
00551 manager.unmark(nodes[r]);
00552 markref--;
00553 cur = nodes[r];
00554 assert(!manager.marked(cur));
00555
00556 nodes[r].init();
00557
00558
00559 if (!manager.leaf(cur)) {
00560 bdd t = manager.iftrue(cur);
00561 bdd f = manager.iffalse(cur);
00562
00563 bool leaf_t = manager.leaf(t);
00564 bool leaf_f = manager.leaf(f);
00565
00566 if (!leaf_t) {
00567 if (!manager.marked(t)) {
00568 nodes[l] = t;
00569 manager.lbCard(t, manager.lbCard(cur) + 1);
00570 manager.ubCard(t, manager.ubCard(cur) + 1);
00571 manager.mark(nodes[l]);
00572 markref++;
00573 l++;
00574 } else {
00575 int lc = std::min(manager.lbCard(cur) + 1, manager.lbCard(t));
00576 int uc = std::max(manager.ubCard(cur) + 1, manager.ubCard(t));
00577 manager.lbCard(t, lc);
00578 manager.ubCard(t, uc);
00579 }
00580
00581 } else {
00582
00583 if (manager.ctrue(t)) {
00584 int minval = manager.lbCard(cur) + 1;
00585 int maxval = manager.ubCard(cur) + 1;
00586 curmin = std::min(curmin, minval);
00587 curmax = std::max(curmax, maxval);
00588 }
00589 }
00590
00591 if (!leaf_f) {
00592 if (!manager.marked(f)) {
00593 nodes[l] = f;
00594 manager.lbCard(f, manager.lbCard(cur));
00595 manager.ubCard(f, manager.ubCard(cur));
00596 manager.mark(nodes[l]);
00597 markref++;
00598 l++;
00599 } else {
00600 int lc = std::min(manager.lbCard(cur), manager.lbCard(f));
00601 int uc = std::max(manager.ubCard(cur), manager.ubCard(f));
00602 manager.lbCard(f, lc);
00603 manager.ubCard(f, uc);
00604 }
00605 } else {
00606
00607 if (manager.ctrue(f)) {
00608 int minval = manager.lbCard(cur);
00609 int maxval = manager.ubCard(cur);
00610 curmin = std::min(curmin, minval);
00611 curmax = std::max(curmax, maxval);
00612
00613 }
00614 }
00615 }
00616 if (((l == 0) && (r == n - 1))) {
00617
00618
00619 singleton = true;
00620 }
00621
00622 }
00623
00624 extcache_unmark(nodes, n, l, r, markref);
00625 assert(markref == 0);
00626 }
00627
00628 void getcardbounds(bdd& c, int& curmin, int& curmax) {
00629
00630 int markref = 0;
00631 int csize = manager.bddsize(c);
00632 int l = 0;
00633 int r = csize - 1;
00634 bool singleton = (csize == 1);
00635 int _level = -1;
00636 Support::DynamicArray<bdd> nodes(csize);
00637
00638
00639 if (!manager.leaf(c)) {
00640
00641 for (int i = csize; i--; ) {
00642 nodes[i].init();
00643 }
00644
00645 nodes[l] = c;
00646 manager.lbCard(nodes[l], 0);
00647 manager.ubCard(nodes[l], 0);
00648 manager.mark(nodes[l]);
00649 markref++;
00650 l++;
00651 } else {
00652
00653 std::cerr << "NOT IMPLEMENTED CARDOUTPUT FOR LEAF !\n";
00654 }
00655
00656
00657 if (! ((l == 0) && (r == csize - 1))
00658 || singleton) {
00659 while (! ((l == 0) && (r == csize - 1)) || singleton) {
00660 extcardbounds(markref, c, csize, l, r,
00661 singleton, _level, nodes,
00662 curmin, curmax
00663 );
00664 }
00665 }
00666 }
00668
00669
00670
00671 }}
00672
00673