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 CpltSetVarImp::CpltSetVarImp(Space* home,
00043 int glbMin, int glbMax, int lubMin, int lubMax,
00044 unsigned int cardMin, unsigned int cardMax)
00045 : CpltSetVarImpBase(home), domain(bdd_true()),
00046 min(lubMin), max(lubMax), _assigned(false) {
00047
00048 IntSet glb(glbMin, glbMax);
00049 IntSet lub(lubMin, lubMax);
00050 testConsistency(glb, lub, cardMin, cardMax, "CpltSetVarImp");
00051
00052 _offset = manager.allocate(tableWidth());
00053
00054 for (int i = glbMax; i >= glbMin; i--) {
00055 domain &= element(i - min);
00056 }
00057
00058 unsigned int range = tableWidth();
00059 domain &= cardcheck(range, _offset,
00060 static_cast<int> (cardMin),
00061 static_cast<int> (cardMax));
00062
00063 assert(!manager.cfalse(domain));
00064 }
00065
00066 CpltSetVarImp::CpltSetVarImp(Space* home,
00067 int glbMin, int glbMax, const IntSet& lubD,
00068 unsigned int cardMin, unsigned int cardMax)
00069 : CpltSetVarImpBase(home), domain(bdd_true()),
00070 min(lubD.min()), max(lubD.max()),
00071 _assigned(false) {
00072
00073 IntSet glb(glbMin, glbMax);
00074 testConsistency(glb, lubD, cardMin, cardMax, "CpltSetVarImp");
00075
00076 IntSetRanges lub(lubD);
00077 Iter::Ranges::ToValues<IntSetRanges> lval(lub);
00078 Iter::Ranges::ValCache<Iter::Ranges::ToValues<IntSetRanges> > vc(lval);
00079
00080 _offset = manager.allocate(tableWidth());
00081 vc.last();
00082
00083 int c = glbMax;
00084 for (int i = max; i >= min; i--) {
00085 if (i != vc.val()) {
00086 if (c >= glbMin && c == i) {
00087 throw CpltSet::GlbLubSpecNoSubset("CpltSetVarImp");
00088 }
00089 domain &= elementNeg(i - min);
00090 } else {
00091 if (c >= glbMin && c == i) {
00092 domain &= element(i - min);
00093 c--;
00094 }
00095 --vc;
00096 }
00097 }
00098
00099 unsigned int range = tableWidth();
00100 domain &= cardcheck(range, _offset,
00101 static_cast<int> (cardMin),
00102 static_cast<int> (cardMax));
00103
00104 assert(!manager.cfalse(domain));
00105 }
00106
00107 CpltSetVarImp::CpltSetVarImp(Space* home,
00108 const IntSet& glbD, int lubMin, int lubMax,
00109 unsigned int cardMin, unsigned int cardMax)
00110 : CpltSetVarImpBase(home), domain(bdd_true()),
00111 min(lubMin), max(lubMax), _assigned(false) {
00112
00113 IntSet lub(lubMin, lubMax);
00114 testConsistency(glbD, lub, cardMin, cardMax, "CpltSetVarImp");
00115
00116 IntSetRanges glb(glbD);
00117 Iter::Ranges::ToValues<IntSetRanges> gval(glb);
00118 Iter::Ranges::ValCache<Iter::Ranges::ToValues<IntSetRanges> > vc(gval);
00119
00120 vc.last();
00121 _offset = manager.allocate(tableWidth());
00122
00123 for (vc.last(); vc(); --vc) {
00124 domain &= element(vc.val() - min);
00125 }
00126
00127 unsigned int range = tableWidth();
00128 domain &= cardcheck(range, _offset,
00129 static_cast<int> (cardMin),
00130 static_cast<int> (cardMax));
00131
00132 assert(!manager.cfalse(domain));
00133 }
00134
00135 CpltSetVarImp::CpltSetVarImp(Space* home,
00136 const IntSet& glbD,const IntSet& lubD,
00137 unsigned int cardMin, unsigned int cardMax)
00138 : CpltSetVarImpBase(home), domain(bdd_true()),
00139 min(lubD.min()), max(lubD.max()),
00140 _assigned(false) {
00141
00142 testConsistency(glbD, lubD, cardMin, cardMax, "CpltSetVarImp");
00143
00144 IntSetRanges glb(glbD);
00145 Iter::Ranges::ToValues<IntSetRanges> gval(glb);
00146 Iter::Ranges::ValCache<Iter::Ranges::ToValues<IntSetRanges> >
00147 vcglb(gval);
00148 IntSetRanges lub(lubD);
00149 Iter::Ranges::ToValues<IntSetRanges> lval(lub);
00150 Iter::Ranges::ValCache<Iter::Ranges::ToValues<IntSetRanges> >
00151 vclub(lval);
00152
00153 _offset = manager.allocate(tableWidth());
00154
00155 vcglb.last();
00156 vclub.last();
00157
00158 for (int i = max; i >= min; i--) {
00159 if (i != vclub.val()) {
00160 if (vcglb() && vcglb.val() == i) {
00161 throw CpltSet::GlbLubSpecNoSubset("CpltSetVarImp");
00162 }
00163 domain &= elementNeg(i - min);
00164 } else {
00165 if (vcglb() && vcglb.val() == i) {
00166 domain &= element(i - min);
00167 }
00168 --vclub;
00169 }
00170 }
00171
00172 unsigned int range = tableWidth();
00173 domain &= cardcheck(range, _offset,
00174 static_cast<int> (cardMin),
00175 static_cast<int> (cardMax));
00176
00177 assert(!manager.cfalse(domain));
00178 }
00179
00180
00181 CpltSetVarImp::CpltSetVarImp(Space* home, bool share, CpltSetVarImp& x)
00182 : CpltSetVarImpBase(home,share,x),
00183 domain(x.domain), min(x.min), max(x.max),
00184 _offset(x._offset), _assigned(false) {
00185 }
00186
00187 inline void
00188 CpltSetVarImp::dispose(Space*) {
00189 manager.dispose(domain);
00190
00191 if (!(_offset == 0 &&
00192 min == Set::Limits::min &&
00193 max == Set::Limits::max)
00194 ) {
00195 manager.dispose(_offset, (int) tableWidth());
00196 }
00197 }
00198
00199 CpltSetVarImp*
00200 CpltSetVarImp::perform_copy(Space* home, bool share) {
00201 CpltSetVarImp* ptr = new (home) CpltSetVarImp(home,share,*this);
00202 return ptr;
00203 }
00204
00205 Reflection::Arg*
00206 CpltSetVarImp::spec(const Space*, Reflection::VarMap&) const {
00207
00208 return NULL;
00209 }
00210
00211
00212
00213 bool
00214 CpltSetVarImp::assigned(void) {
00215 if (!_assigned) {
00216
00217 bool cond1 = (unsigned int) manager.bddpath(domain) == 1;
00218
00219
00220
00221 bool cond2 = (unsigned int) manager.bddsize(domain) == tableWidth();
00222 _assigned = cond1 && cond2;
00223 }
00224 return _assigned;
00225 }
00226
00227 ModEvent
00228 CpltSetVarImp::intersect(Space* home, bdd& d) {
00229 bool assigned_before = assigned();
00230 bdd olddom = domain;
00231 domain &= d;
00232
00233 bool assigned_new = assigned();
00234 if (manager.cfalse(domain))
00235 return ME_CPLTSET_FAILED;
00236
00237 ModEvent me = ME_CPLTSET_NONE;
00238 if (assigned_new) {
00239 if (assigned_before) {
00240 me = ME_CPLTSET_NONE;
00241 return me;
00242 } else {
00243 me = ME_CPLTSET_VAL;
00244 }
00245 Delta d;
00246 return notify(home, me, &d);
00247 } else {
00248 if (olddom != domain) {
00249 me = ME_CPLTSET_DOM;
00250 Delta d;
00251 return notify(home, me, &d);
00252 }
00253 }
00254 return me;
00255 }
00256
00257 ModEvent
00258 CpltSetVarImp::exclude(Space* home, int a, int b) {
00259
00260 if (a > max || b < min)
00261 return ME_CPLTSET_NONE;
00262
00263 int mi = std::max(min, a);
00264 int ma = std::min(b, max);
00265
00266 bdd notinlub = bdd_true();
00267
00268 for (int i = ma; i >= mi; i--)
00269 notinlub &= elementNeg(i - min);
00270
00271 return intersect(home, notinlub);
00272 }
00273
00274 ModEvent
00275 CpltSetVarImp::include(Space* home, int a, int b) {
00276 if (a < min || b > max)
00277 return ME_CPLTSET_FAILED;
00278
00279 bdd in_glb = bdd_true();
00280 for (int i = b; i >= a; i--)
00281 in_glb &= element(i - min);
00282
00283 return intersect(home, in_glb);
00284 }
00285
00286 ModEvent
00287 CpltSetVarImp::nq(Space* home, int a, int b) {
00288 if (b < min || a > max)
00289 return ME_CPLTSET_NONE;
00290
00291 Iter::Ranges::Singleton m(a, b);
00292 bdd ass = !(iterToBdd(m));
00293 return intersect(home, ass);
00294 }
00295
00296 ModEvent
00297 CpltSetVarImp::eq(Space* home, int a, int b) {
00298 if (b < min || a > max)
00299 return ME_CPLTSET_FAILED;
00300
00301 Iter::Ranges::Singleton m(a, b);
00302 bdd ass = iterToBdd(m);
00303 return intersect(home, ass);
00304 }
00305
00306 ModEvent
00307 CpltSetVarImp::intersect(Space* home, int a, int b) {
00308 ModEvent me_left = exclude(home, Set::Limits::min, a - 1);
00309
00310 if (me_failed(me_left) || me_left == ME_CPLTSET_VAL)
00311 return me_left;
00312
00313 ModEvent me_right = exclude(home, b + 1, Set::Limits::max);
00314
00315 if (me_failed(me_right) || me_right == ME_CPLTSET_VAL)
00316 return me_right;
00317
00318 if (me_left > 0 || me_right > 0)
00319 return ME_CPLTSET_DOM;
00320
00321 return ME_CPLTSET_NONE;
00322 }
00323
00324 ModEvent
00325 CpltSetVarImp::cardinality(Space* home, int l, int u) {
00326 unsigned int maxcard = tableWidth();
00327
00328 bdd c = cardcheck(maxcard, _offset, l, u);
00329 return intersect(home, c);
00330 }
00331
00332 bool
00333 CpltSetVarImp::knownIn(int v) const {
00334 if (manager.ctrue(domain))
00335 return false;
00336 if (v<min || v>max)
00337 return false;
00338 bdd bv = manager.negbddpos(_offset+v-min);
00339 return (manager.cfalse(domain & bv));
00340 }
00341
00342 bool
00343 CpltSetVarImp::knownOut(int v) const {
00344 if (manager.ctrue(domain))
00345 return false;
00346 if (v<min || v>max)
00347 return false;
00348 bdd bv = manager.bddpos(_offset+v-min);
00349 return (manager.cfalse(domain & bv));
00350 }
00351
00352 inline int
00353 CpltSetVarImp::lubMaxN(int n) const {
00354 if (manager.ctrue(domain))
00355 return initialLubMax() - n;
00356
00357 GECODE_AUTOARRAY(NodeStatus, status, tableWidth());
00358 DomBddIterator iter(this);
00359
00360 if (!iter())
00361 return MAX_OF_EMPTY;
00362
00363 for (int i = 0; iter(); i++, ++iter) {
00364 status[i] = iter.status();
00365 }
00366 int c = 0;
00367 for (int j = tableWidth() - 1; j--; ) {
00368 if (status[j] != FIX_NOT_LUB) {
00369 if (c == n) {
00370 c = j;
00371 break;
00372 }
00373 c++;
00374 }
00375 }
00376 return initialLubMax() - c;
00377 }
00378
00379 unsigned int
00380 CpltSetVarImp::lubSize(void) const {
00381 if (manager.ctrue(domain))
00382 return tableWidth();
00383
00384 BddIterator iter(domain);
00385 int out = 0;
00386 while (iter()) {
00387 if (iter.status() == FIX_NOT_LUB)
00388 out++;
00389 ++iter;
00390 }
00391 return tableWidth() - out;
00392 }
00393
00394 int
00395 CpltSetVarImp::glbMin(void) const {
00396 if (manager.ctrue(domain))
00397 return initialLubMin();
00398
00399 BddIterator iter(domain);
00400 while (iter()) {
00401 if (iter.status() == FIX_GLB) {
00402 int idx = iter.label() - offset();
00403 return initialLubMin() + idx;
00404 }
00405 ++iter;
00406 }
00407 return MIN_OF_EMPTY;
00408 }
00409
00410 int
00411 CpltSetVarImp::glbMax(void) const {
00412 if (manager.ctrue(domain))
00413 return initialLubMax();
00414
00415 BddIterator iter(domain);
00416 int lastglb = -1;
00417 while (iter()) {
00418 if (iter.status() == FIX_GLB) {
00419 int idx = iter.label() - offset();
00420 lastglb = initialLubMin() + idx;
00421 }
00422 ++iter;
00423 }
00424 return (lastglb == -1) ? MAX_OF_EMPTY : lastglb;
00425 }
00426
00427 unsigned int
00428 CpltSetVarImp::glbSize(void) const {
00429 if (manager.ctrue(domain)) { return 0; }
00430 BddIterator iter(domain);
00431 int size = 0;
00432 while (iter()) {
00433 if (iter.status() == FIX_GLB) { size++; }
00434 ++iter;
00435 }
00436 return size;
00437 }
00438
00439 int
00440 CpltSetVarImp::unknownMin(void) const {
00441 if (manager.ctrue(domain)) { return initialLubMin(); }
00442 BddIterator iter(domain);
00443 while (iter()) {
00444 NodeStatus status = iter.status();
00445 if (status == FIX_UNKNOWN || status == UNDET) {
00446 int idx = iter.label() - offset();
00447 return initialLubMin() + idx;
00448 }
00449 ++iter;
00450 }
00451 return MIN_OF_EMPTY;
00452 }
00453
00454 int
00455 CpltSetVarImp::unknownMax(void) const {
00456 if (manager.ctrue(domain))
00457 return initialLubMax();
00458
00459 BddIterator iter(domain);
00460 int lastunknown = -1;
00461 while (iter()) {
00462 NodeStatus status = iter.status();
00463 if (status == FIX_UNKNOWN || status == UNDET) {
00464 int idx = iter.label() - offset();
00465 lastunknown = initialLubMin() + idx;
00466 }
00467 ++iter;
00468 }
00469 return (lastunknown == -1) ? MAX_OF_EMPTY : lastunknown;
00470 }
00471
00472 unsigned int
00473 CpltSetVarImp::unknownSize(void) const {
00474 int size = tableWidth();
00475 if (manager.ctrue(domain))
00476 return size;
00477
00478 BddIterator iter(domain);
00479 while (iter()) {
00480 NodeStatus status = iter.status();
00481 if (status == FIX_GLB || status == FIX_NOT_LUB) { size--; }
00482 ++iter;
00483 }
00484 return size;
00485 }
00486
00487 int
00488 CpltSetVarImp::lubMin(void) const {
00489 if (manager.ctrue(domain)) { return initialLubMin(); }
00490 Gecode::Set::LubRanges<CpltSetVarImp*> lub(this);
00491 return !lub() ? MIN_OF_EMPTY : lub.min();
00492 }
00493
00494 int
00495 CpltSetVarImp::lubMax(void) const {
00496 if (manager.ctrue(domain)) { return initialLubMax(); }
00497 Gecode::Set::LubRanges<CpltSetVarImp*> lub(this);
00498 if (!lub()) { return MAX_OF_EMPTY; }
00499 int maxlub = initialLubMax();
00500 while (lub()) {
00501 maxlub = lub.max();
00502 ++lub;
00503 }
00504 return maxlub;
00505 }
00506
00507 int
00508 CpltSetVarImp::lubMinN(int n) const {
00509 if (manager.ctrue(domain))
00510 return initialLubMin() + n;
00511
00512 Gecode::Set::LubRanges<CpltSetVarImp*> lub(this);
00513
00514 if (!lub())
00515 return MIN_OF_EMPTY;
00516
00517 while (lub()) {
00518 if (n < (int) lub.width()) {
00519 return lub.min() + n;
00520 } else {
00521 n -= lub.width();
00522 }
00523 ++lub;
00524 }
00525
00526
00527 return MIN_OF_EMPTY;
00528 }
00529
00530
00531 void
00532 BddIterator::init(const bdd& b) {
00533 markref = 0;
00534 c = b;
00535 n = manager.bddsize(c);
00536 l = 0;
00537 r = n - 1;
00538 bypassed = false;
00539 onlyleaves = false;
00540 singleton = (n == 1);
00541 _level = -1;
00542
00543 if (!manager.leaf(c)) {
00544 SharedArray<bdd> dummy(n);
00545 nodes = dummy;
00546
00547 for (int i = n; i--; ){
00548 new (&nodes[i]) bdd;
00549 nodes[i].init();
00550 }
00551
00552 assert(!manager.leaf(c));
00553
00554 nodes[l] = c;
00555 manager.mark(nodes[l]);
00556 markref++;
00557 l++;
00558 }
00559 if (operator()()) {
00560 operator++();
00561 }
00562 }
00563
00564
00565 void
00566 BddIterator::cache_mark(void) {
00567
00568 if (l > 0) {
00569 for (int i = 0; i < l; i++) {
00570 if (!manager.marked(nodes[i])) {
00571 manager.mark(nodes[i]);
00572 markref++;
00573 }
00574 }
00575 }
00576
00577 if (r < n - 1) {
00578 for (int i = r + 1; i < n; i++) {
00579 if (!manager.marked(nodes[i])) {
00580 manager.mark(nodes[i]);
00581 markref++;
00582 }
00583 }
00584 }
00585 }
00586
00587
00588 void
00589 BddIterator::cache_unmark(void) {
00590 if (l > 0) {
00591 for (int i = 0; i < l; i++) {
00592 if (manager.marked(nodes[i])) {
00593 manager.unmark(nodes[i]);
00594 markref--;
00595 }
00596 }
00597 }
00598 if (r < n - 1) {
00599 for (int i = r + 1; i < n; i++) {
00600 if (manager.marked(nodes[i])) {
00601 manager.unmark(nodes[i]);
00602 markref--;
00603 }
00604 }
00605 }
00606 }
00607
00608
00609 void
00610 BddIterator::operator++(void) {
00611 if (empty()) {
00612 singleton = false;
00613 cache_unmark();
00614 assert(markref == 0);
00615 return;
00616 }
00617
00618
00619
00620
00621 if (onlyleaves || bypassed) {
00622 flag = UNDET;
00623 } else {
00624
00625 flag = INIT;
00626 }
00627
00628
00629 cache_mark();
00630 if (l > 0) {
00631 _level++;
00632 }
00633
00634 bool stackleft = false;
00635 while (l > 0) {
00636 stackleft = true;
00637
00638
00639
00640
00641
00642
00643
00644
00645
00646 while ((l > 1) &&
00647 manager.bddidx(nodes[l - 1]) < manager.bddidx(nodes[l - 2])) {
00648 int shift = l - 2;
00649 int norm = l - 1;
00650 manager.unmark(nodes[shift]); markref--;
00651 flag = UNDET;
00652 if (r == n - 1) {
00653 nodes[r] = nodes[shift];
00654 manager.mark(nodes[r]); markref++;
00655 } else {
00656 for (int i = r; i < n - 1; i++) {
00657 nodes[i] = nodes[i + 1];
00658 }
00659 nodes[n - 1] = nodes[shift];
00660 manager.mark(nodes[n - 1]); markref++;
00661 }
00662 r--;
00663 nodes[shift] = nodes[norm];
00664 nodes[norm].init();
00665 l--;
00666 }
00667
00668 while ((l > 1) &&
00669 manager.bddidx(nodes[l - 1]) > manager.bddidx(nodes[l - 2])) {
00670 int shift = l - 1;
00671 manager.unmark(nodes[shift]); markref--;
00672 flag = UNDET;
00673 if (r == n - 1) {
00674 nodes[r] = nodes[shift];
00675 manager.mark(nodes[r]); markref++;
00676 } else {
00677 for (int i = r; i < n - 1; i++) {
00678 nodes[i] = nodes[i + 1];
00679 }
00680 nodes[n - 1] = nodes[shift];
00681 manager.mark(nodes[n - 1]); markref++;
00682 }
00683 r--;
00684 nodes[shift].init();
00685 l--;
00686 }
00687
00688 l--;
00689 manager.unmark(nodes[l]);
00690 markref--;
00691 cur = nodes[l];
00692 assert(!manager.marked(cur));
00693 nodes[l].init();
00694
00695
00696
00697 if (!manager.leaf(cur)) {
00698 bdd t = manager.iftrue(cur);
00699 bdd f = manager.iffalse(cur);
00700
00701 bool fixed_glb = manager.cfalse(f);
00702 bool fixed_not_lub = manager.cfalse(t);
00703
00704 bool leaf_t = manager.leaf(t);
00705 bool leaf_f = manager.leaf(f);
00706
00707 if (flag != UNDET) {
00708
00709 if (fixed_not_lub) {
00710 if (flag > INIT && flag != FIX_NOT_LUB) {
00711
00712 flag = UNDET;
00713 } else {
00714 flag = FIX_NOT_LUB;
00715 }
00716 } else {
00717
00718 if (fixed_glb) {
00719 if (flag > INIT && flag != FIX_GLB) {
00720
00721 flag = UNDET;
00722 } else {
00723 flag = FIX_GLB;
00724 }
00725 } else {
00726 if (flag > INIT && flag != FIX_UNKNOWN) {
00727
00728 flag = UNDET;
00729 } else {
00730
00731 flag = FIX_UNKNOWN;
00732 }
00733 }
00734 }
00735 }
00736
00737 if (!leaf_t) {
00738 if (!manager.marked(t)) {
00739
00740
00741 nodes[r] = t;
00742 manager.mark(nodes[r]);
00743 markref++;
00744 r--;
00745 }
00746
00747 if (manager.ctrue(f)) {
00748 bypassed = true;
00749 }
00750 } else {
00751
00752
00753
00754 onlyleaves |= leaf_f;
00755 }
00756
00757 if (!leaf_f) {
00758 if (!manager.marked(f)) {
00759 nodes[r] = f;
00760 manager.mark(nodes[r]);
00761 markref++;
00762 r--;
00763 }
00764 if (manager.ctrue(t)) {
00765
00766 bypassed = true;
00767
00768
00769
00770 }
00771 }
00772 }
00773 if (empty()) {
00774
00775
00776 singleton = true;
00777 }
00778 }
00779
00780
00781
00782 if (stackleft) {
00783 cache_unmark();
00784 assert(markref == 0);
00785 return;
00786 }
00787
00788 if (r < n - 1) {
00789 _level++;
00790 }
00791
00792
00793 while (r < n - 1) {
00794 while ((r < n - 2) && manager.bddidx(nodes[r + 1]) <
00795 manager.bddidx(nodes[r + 2])) {
00796 int shift = r + 2;
00797 int norm = r + 1;
00798 manager.unmark(nodes[shift]); markref--;
00799 flag = UNDET;
00800 if (l == 0) {
00801 nodes[l] = nodes[shift];
00802 manager.mark(nodes[l]); markref++;
00803 } else {
00804 for (int i = l; i > 0; i--) {
00805 nodes[i] = nodes[i - 1];
00806 }
00807 nodes[0] = nodes[shift];
00808 manager.mark(nodes[0]); markref++;
00809 }
00810 l++;
00811 nodes[shift] = nodes[norm];
00812 nodes[norm].init();
00813 r++;
00814 }
00815 while ((r < n - 2) && manager.bddidx(nodes[r + 1]) >
00816 manager.bddidx(nodes[r + 2])) {
00817 int shift = r + 1;
00818 manager.unmark(nodes[shift]); markref--;
00819 flag = UNDET;
00820 if (l == 0) {
00821 nodes[l] = nodes[shift];
00822 manager.mark(nodes[l]); markref++;
00823 } else {
00824 for (int i = l; i > 0; i--) {
00825 nodes[i] = nodes[i - 1];
00826 }
00827 nodes[0] = nodes[shift];
00828 manager.mark(nodes[0]); markref++;
00829 }
00830 l++;
00831 nodes[shift].init();
00832 r++;
00833 }
00834
00835 r++;
00836 manager.unmark(nodes[r]);
00837 markref--;
00838 cur = nodes[r];
00839 assert(!manager.marked(cur));
00840
00841 nodes[r].init();
00842
00843
00844 if (!manager.leaf(cur)) {
00845 bdd t = manager.iftrue(cur);
00846 bdd f = manager.iffalse(cur);
00847
00848 bool fixed_glb = manager.cfalse(f);
00849 bool fixed_not_lub = manager.cfalse(t);
00850
00851 bool leaf_t = manager.leaf(t);
00852 bool leaf_f = manager.leaf(f);
00853
00854 if (flag != UNDET) {
00855 if (fixed_not_lub) {
00856 if (flag > INIT && flag != FIX_NOT_LUB) {
00857 flag = UNDET;
00858 } else {
00859 flag = FIX_NOT_LUB;
00860 }
00861 } else {
00862 if (fixed_glb) {
00863 if (flag > INIT && flag != FIX_GLB) {
00864 flag = UNDET;
00865 } else {
00866 flag = FIX_GLB;
00867 }
00868 } else {
00869 if (flag > INIT && flag != FIX_UNKNOWN) {
00870 flag = UNDET;
00871 } else {
00872 flag = FIX_UNKNOWN;
00873 }
00874 }
00875 }
00876 }
00877
00878 if (!leaf_t) {
00879 if (!manager.marked(t)) {
00880 nodes[l] = t;
00881 manager.mark(nodes[l]);
00882 markref++;
00883 l++;
00884 }
00885
00886
00887 if (manager.ctrue(f)) {
00888 bypassed = true;
00889 }
00890 } else {
00891
00892
00893
00894 onlyleaves |= leaf_f;
00895 }
00896
00897 if (!leaf_f) {
00898 if (!manager.marked(f)) {
00899 nodes[l] = f;
00900 manager.mark(nodes[l]);
00901 markref++;
00902 l++;
00903 }
00904
00905 if (manager.ctrue(t)) {
00906 bypassed = true;
00907 }
00908 }
00909 }
00910 if (empty()) {
00911
00912
00913 singleton = true;
00914 }
00915 }
00916
00917 cache_unmark();
00918 assert(markref == 0);
00919 }
00920
00921
00922 GECODE_CPLTSET_EXPORT VarDisposer<CpltSetVarImp> vtd;
00923
00924 }}
00925
00926