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
00039
00040 #include <gecode/minimodel.hh>
00041
00042 #ifdef GECODE_HAS_SET_VARS
00043
00044 namespace Gecode {
00045
00046 namespace {
00048 static bool same(SetExpr::NodeType t0, SetExpr::NodeType t1) {
00049 return (t0==t1) || (t1==SetExpr::NT_VAR) ||
00050 (t1==SetExpr::NT_CONST) || (t1==SetExpr::NT_LEXP);
00051 }
00052 }
00053
00055 class SetExpr::Node {
00056 public:
00058 unsigned int use;
00060 int same;
00062 NodeType t;
00064 Node *l, *r;
00066 SetVar x;
00068 IntSet s;
00070 LinIntExpr e;
00071
00073 Node(void);
00075 GECODE_MINIMODEL_EXPORT
00076 bool decrement(void);
00078 static void* operator new(size_t size);
00080 static void operator delete(void* p, size_t size);
00081 };
00082
00083
00084
00085
00086
00087 SetExpr::Node::Node(void) : use(1) {}
00088
00089 void*
00090 SetExpr::Node::operator new(size_t size) {
00091 return heap.ralloc(size);
00092 }
00093 void
00094 SetExpr::Node::operator delete(void* p, size_t) {
00095 heap.rfree(p);
00096 }
00097
00098 bool
00099 SetExpr::Node::decrement(void) {
00100 if (--use == 0) {
00101 if ((l != NULL) && l->decrement())
00102 delete l;
00103 if ((r != NULL) && r->decrement())
00104 delete r;
00105 return true;
00106 }
00107 return false;
00108 }
00109
00110 namespace {
00112 class NNF {
00113 public:
00114 typedef SetExpr::NodeType NodeType;
00115 typedef SetExpr::Node Node;
00117 NodeType t;
00119 int p;
00121 int n;
00123 union {
00125 struct {
00127 NNF* l;
00129 NNF* r;
00130 } b;
00132 struct {
00134 Node* x;
00135 } a;
00136 } u;
00138 bool neg;
00140 static NNF* nnf(Region& r, Node* n, bool neg);
00142 void post(Home home, NodeType t, SetVarArgs& b, int& i) const;
00144 void post(Home home, SetRelType srt, SetVar s) const;
00146 void post(Home home, SetRelType srt, SetVar s, BoolVar b) const;
00148 void post(Home home, SetRelType srt, const NNF* n) const;
00150 void post(Home home, BoolVar b, bool t, SetRelType srt,
00151 const NNF* n) const;
00153 static void* operator new(size_t s, Region& r);
00155 static void operator delete(void*);
00157 static void operator delete(void*, Region&);
00158 };
00159
00160
00161
00162
00163
00164 forceinline void
00165 NNF::operator delete(void*) {}
00166
00167 forceinline void
00168 NNF::operator delete(void*, Region&) {}
00169
00170 forceinline void*
00171 NNF::operator new(size_t s, Region& r) {
00172 return r.ralloc(s);
00173 }
00174
00175 void
00176 NNF::post(Home home, SetRelType srt, SetVar s) const {
00177 switch (t) {
00178 case SetExpr::NT_VAR:
00179 if (neg) {
00180 switch (srt) {
00181 case SRT_EQ:
00182 rel(home, u.a.x->x, SRT_CMPL, s);
00183 break;
00184 case SRT_CMPL:
00185 rel(home, u.a.x->x, SRT_EQ, s);
00186 break;
00187 default:
00188 SetVar bc(home,IntSet::empty,
00189 IntSet(Set::Limits::min,Set::Limits::max));
00190 rel(home, s, SRT_CMPL, bc);
00191 rel(home, u.a.x->x, srt, bc);
00192 break;
00193 }
00194 } else
00195 rel(home, u.a.x->x, srt, s);
00196 break;
00197 case SetExpr::NT_CONST:
00198 {
00199 IntSet ss;
00200 if (neg) {
00201 IntSetRanges sr(u.a.x->s);
00202 Set::RangesCompl<IntSetRanges> src(sr);
00203 ss = IntSet(src);
00204 } else {
00205 ss = u.a.x->s;
00206 }
00207 switch (srt) {
00208 case SRT_SUB: srt = SRT_SUP; break;
00209 case SRT_SUP: srt = SRT_SUB; break;
00210 default: break;
00211 }
00212 dom(home, s, srt, ss);
00213 }
00214 break;
00215 case SetExpr::NT_LEXP:
00216 {
00217 IntVar iv = u.a.x->e.post(home,ICL_DEF);
00218 if (neg) {
00219 SetVar ic(home,IntSet::empty,
00220 IntSet(Set::Limits::min,Set::Limits::max));
00221 rel(home, iv, SRT_CMPL, ic);
00222 rel(home,ic,srt,s);
00223 } else {
00224 rel(home,iv,srt,s);
00225 }
00226 }
00227 break;
00228 case SetExpr::NT_INTER:
00229 {
00230 SetVarArgs bs(p+n);
00231 int i=0;
00232 post(home, SetExpr::NT_INTER, bs, i);
00233 if (i == 2) {
00234 rel(home, bs[0], SOT_INTER, bs[1], srt, s);
00235 } else {
00236 if (srt == SRT_EQ)
00237 rel(home, SOT_INTER, bs, s);
00238 else {
00239 SetVar bc(home,IntSet::empty,
00240 IntSet(Set::Limits::min,Set::Limits::max));
00241 rel(home, SOT_INTER, bs, bc);
00242 rel(home, bc, srt, s);
00243 }
00244 }
00245 }
00246 break;
00247 case SetExpr::NT_UNION:
00248 {
00249 SetVarArgs bs(p+n);
00250 int i=0;
00251 post(home, SetExpr::NT_UNION, bs, i);
00252 if (i == 2) {
00253 rel(home, bs[0], SOT_UNION, bs[1], srt, s);
00254 } else {
00255 if (srt == SRT_EQ)
00256 rel(home, SOT_UNION, bs, s);
00257 else {
00258 SetVar bc(home,IntSet::empty,
00259 IntSet(Set::Limits::min,Set::Limits::max));
00260 rel(home, SOT_UNION, bs, bc);
00261 rel(home, bc, srt, s);
00262 }
00263 }
00264 }
00265 break;
00266 case SetExpr::NT_DUNION:
00267 {
00268 SetVarArgs bs(p+n);
00269 int i=0;
00270 post(home, SetExpr::NT_DUNION, bs, i);
00271
00272 if (i == 2) {
00273 if (neg) {
00274 if (srt == SRT_CMPL) {
00275 rel(home, bs[0], SOT_DUNION, bs[1], srt, s);
00276 } else {
00277 SetVar bc(home,IntSet::empty,
00278 IntSet(Set::Limits::min,Set::Limits::max));
00279 rel(home,s,SRT_CMPL,bc);
00280 rel(home, bs[0], SOT_DUNION, bs[1], srt, bc);
00281 }
00282 } else {
00283 rel(home, bs[0], SOT_DUNION, bs[1], srt, s);
00284 }
00285 } else {
00286 if (neg) {
00287 if (srt == SRT_CMPL) {
00288 rel(home, SOT_DUNION, bs, s);
00289 } else {
00290 SetVar br(home,IntSet::empty,
00291 IntSet(Set::Limits::min,Set::Limits::max));
00292 rel(home, SOT_DUNION, bs, br);
00293 if (srt == SRT_EQ)
00294 rel(home, br, SRT_CMPL, s);
00295 else {
00296 SetVar bc(home,IntSet::empty,
00297 IntSet(Set::Limits::min,Set::Limits::max));
00298 rel(home, br, srt, bc);
00299 rel(home, bc, SRT_CMPL, s);
00300 }
00301 }
00302 } else {
00303 if (srt == SRT_EQ)
00304 rel(home, SOT_DUNION, bs, s);
00305 else {
00306 SetVar br(home,IntSet::empty,
00307 IntSet(Set::Limits::min,Set::Limits::max));
00308 rel(home, SOT_DUNION, bs, br);
00309 rel(home, br, srt, s);
00310 }
00311 }
00312 }
00313 }
00314 break;
00315 default:
00316 GECODE_NEVER;
00317 }
00318 }
00319
00320 void
00321 NNF::post(Home home, SetRelType srt, SetVar s, BoolVar b) const {
00322 switch (t) {
00323 case SetExpr::NT_VAR:
00324 if (neg) {
00325 switch (srt) {
00326 case SRT_EQ:
00327 rel(home, u.a.x->x, SRT_CMPL, s, b);
00328 break;
00329 case SRT_CMPL:
00330 rel(home, u.a.x->x, SRT_EQ, s, b);
00331 break;
00332 default:
00333 SetVar bc(home,IntSet::empty,
00334 IntSet(Set::Limits::min,Set::Limits::max));
00335 rel(home, s, SRT_CMPL, bc);
00336 rel(home, u.a.x->x, srt, bc, b);
00337 break;
00338 }
00339 } else
00340 rel(home, u.a.x->x, srt, s, b);
00341 break;
00342 case SetExpr::NT_CONST:
00343 {
00344 IntSet ss;
00345 if (neg) {
00346 IntSetRanges sr(u.a.x->s);
00347 Set::RangesCompl<IntSetRanges> src(sr);
00348 ss = IntSet(src);
00349 } else {
00350 ss = u.a.x->s;
00351 }
00352 SetRelType invsrt;
00353 switch (srt) {
00354 case SRT_SUB: invsrt = SRT_SUP; break;
00355 case SRT_SUP: invsrt = SRT_SUB; break;
00356 case SRT_LQ: invsrt = SRT_GQ; break;
00357 case SRT_LE: invsrt = SRT_GR; break;
00358 case SRT_GQ: invsrt = SRT_LQ; break;
00359 case SRT_GR: invsrt = SRT_LE; break;
00360 case SRT_EQ:
00361 case SRT_NQ:
00362 case SRT_DISJ:
00363 case SRT_CMPL:
00364 invsrt = srt;
00365 break;
00366 default:
00367 invsrt = srt;
00368 GECODE_NEVER;
00369 }
00370 dom(home, s, invsrt, ss, b);
00371 }
00372 break;
00373 case SetExpr::NT_LEXP:
00374 {
00375 IntVar iv = u.a.x->e.post(home,ICL_DEF);
00376 if (neg) {
00377 SetVar ic(home,IntSet::empty,
00378 IntSet(Set::Limits::min,Set::Limits::max));
00379 rel(home, iv, SRT_CMPL, ic);
00380 rel(home,ic,srt,s,b);
00381 } else {
00382 rel(home,iv,srt,s,b);
00383 }
00384 }
00385 case SetExpr::NT_INTER:
00386 {
00387 SetVarArgs bs(p+n);
00388 int i=0;
00389 post(home, SetExpr::NT_INTER, bs, i);
00390 SetVar br(home,IntSet::empty,
00391 IntSet(Set::Limits::min,Set::Limits::max));
00392 rel(home, SOT_INTER, bs, br);
00393 rel(home, br, srt, s, b);
00394 }
00395 break;
00396 case SetExpr::NT_UNION:
00397 {
00398 SetVarArgs bs(p+n);
00399 int i=0;
00400 post(home, SetExpr::NT_UNION, bs, i);
00401 SetVar br(home,IntSet::empty,
00402 IntSet(Set::Limits::min,Set::Limits::max));
00403 rel(home, SOT_UNION, bs, br);
00404 rel(home, br, srt, s, b);
00405 }
00406 break;
00407 case SetExpr::NT_DUNION:
00408 {
00409 SetVarArgs bs(p+n);
00410 int i=0;
00411 post(home, SetExpr::NT_DUNION, bs, i);
00412
00413 if (neg) {
00414 SetVar br(home,IntSet::empty,
00415 IntSet(Set::Limits::min,Set::Limits::max));
00416 rel(home, SOT_DUNION, bs, br);
00417 if (srt == SRT_CMPL)
00418 rel(home, br, SRT_EQ, s, b);
00419 else if (srt == SRT_EQ)
00420 rel(home, br, SRT_CMPL, s, b);
00421 else {
00422 SetVar bc(home,IntSet::empty,
00423 IntSet(Set::Limits::min,Set::Limits::max));
00424 rel(home, br, srt, bc);
00425 rel(home, bc, SRT_CMPL, s, b);
00426 }
00427 } else {
00428 SetVar br(home,IntSet::empty,
00429 IntSet(Set::Limits::min,Set::Limits::max));
00430 rel(home, SOT_DUNION, bs, br);
00431 rel(home, br, srt, s, b);
00432 }
00433 }
00434 break;
00435 default:
00436 GECODE_NEVER;
00437 }
00438 }
00439
00440 void
00441 NNF::post(Home home, NodeType t, SetVarArgs& b, int& i) const {
00442 if (this->t != t) {
00443 switch (this->t) {
00444 case SetExpr::NT_VAR:
00445 if (neg) {
00446 SetVar xc(home,IntSet::empty,
00447 IntSet(Set::Limits::min,Set::Limits::max));
00448 rel(home, xc, SRT_CMPL, u.a.x->x);
00449 b[i++]=xc;
00450 } else {
00451 b[i++]=u.a.x->x;
00452 }
00453 break;
00454 default:
00455 {
00456 SetVar s(home,IntSet::empty,
00457 IntSet(Set::Limits::min,Set::Limits::max));
00458 post(home,SRT_EQ,s);
00459 b[i++] = s;
00460 }
00461 break;
00462 }
00463 } else {
00464 u.b.l->post(home, t, b, i);
00465 u.b.r->post(home, t, b, i);
00466 }
00467 }
00468
00469 void
00470 NNF::post(Home home, SetRelType srt, const NNF* n) const {
00471 if (n->t == SetExpr::NT_VAR && !n->neg) {
00472 post(home,srt,n->u.a.x->x);
00473 } else if (t == SetExpr::NT_VAR && !neg) {
00474 SetRelType n_srt;
00475 switch (srt) {
00476 case SRT_SUB: n_srt = SRT_SUP; break;
00477 case SRT_SUP: n_srt = SRT_SUB; break;
00478 default: n_srt = srt;
00479 }
00480 n->post(home,n_srt,this);
00481 } else {
00482 SetVar nx(home,IntSet::empty,
00483 IntSet(Set::Limits::min,Set::Limits::max));
00484 n->post(home,SRT_EQ,nx);
00485 post(home,srt,nx);
00486 }
00487 }
00488
00489 void
00490 NNF::post(Home home, BoolVar b, bool pt,
00491 SetRelType srt, const NNF* n) const {
00492 if (pt) {
00493 if (n->t == SetExpr::NT_VAR && !n->neg) {
00494 post(home,srt,n->u.a.x->x,b);
00495 } else if (t == SetExpr::NT_VAR && !neg) {
00496 SetRelType n_srt;
00497 switch (srt) {
00498 case SRT_SUB: n_srt = SRT_SUP; break;
00499 case SRT_SUP: n_srt = SRT_SUB; break;
00500 default: n_srt = srt;
00501 }
00502 n->post(home,b,true,n_srt,this);
00503 } else {
00504 SetVar nx(home,IntSet::empty,
00505 IntSet(Set::Limits::min,Set::Limits::max));
00506 n->post(home,SRT_EQ,nx);
00507 post(home,srt,nx,b);
00508 }
00509 } else if (srt == SRT_EQ) {
00510 post(home,b,true,SRT_NQ,n);
00511 } else if (srt == SRT_NQ) {
00512 post(home,b,true,SRT_EQ,n);
00513 } else {
00514 BoolVar nb(home,0,1);
00515 rel(home,b,IRT_NQ,nb);
00516 post(home,nb,true,srt,n);
00517 }
00518 }
00519
00520 NNF*
00521 NNF::nnf(Region& r, Node* n, bool neg) {
00522 switch (n->t) {
00523 case SetExpr::NT_VAR:
00524 case SetExpr::NT_CONST:
00525 case SetExpr::NT_LEXP:
00526 {
00527 NNF* x = new (r) NNF;
00528 x->t = n->t; x->neg = neg; x->u.a.x = n;
00529 if (neg) {
00530 x->p = 0; x->n = 1;
00531 } else {
00532 x->p = 1; x->n = 0;
00533 }
00534 return x;
00535 }
00536 case SetExpr::NT_CMPL:
00537 return nnf(r,n->l,!neg);
00538 case SetExpr::NT_INTER:
00539 case SetExpr::NT_UNION:
00540 case SetExpr::NT_DUNION:
00541 {
00542 NodeType t; bool xneg;
00543 if (n->t == SetExpr::NT_DUNION) {
00544 t = n->t; xneg = neg; neg = false;
00545 } else {
00546 t = ((n->t == SetExpr::NT_INTER) == neg) ?
00547 SetExpr::NT_UNION : SetExpr::NT_INTER;
00548 xneg = false;
00549 }
00550 NNF* x = new (r) NNF;
00551 x->neg = xneg;
00552 x->t = t;
00553 x->u.b.l = nnf(r,n->l,neg);
00554 x->u.b.r = nnf(r,n->r,neg);
00555 int p_l, n_l;
00556 if ((x->u.b.l->t == t) || (x->u.b.l->t == SetExpr::NT_VAR)) {
00557 p_l=x->u.b.l->p; n_l=x->u.b.l->n;
00558 } else {
00559 p_l=1; n_l=0;
00560 }
00561 int p_r, n_r;
00562 if ((x->u.b.r->t == t) || (x->u.b.r->t == SetExpr::NT_VAR)) {
00563 p_r=x->u.b.r->p; n_r=x->u.b.r->n;
00564 } else {
00565 p_r=1; n_r=0;
00566 }
00567 x->p = p_l+p_r;
00568 x->n = n_l+n_r;
00569 return x;
00570 }
00571 default:
00572 GECODE_NEVER;
00573 }
00574 GECODE_NEVER;
00575 return NULL;
00576 }
00577 }
00578
00579 SetExpr::SetExpr(const SetVar& x) : n(new Node) {
00580 n->same = 1;
00581 n->t = NT_VAR;
00582 n->l = NULL;
00583 n->r = NULL;
00584 n->x = x;
00585 }
00586
00587 SetExpr::SetExpr(const IntSet& s) : n(new Node) {
00588 n->same = 1;
00589 n->t = NT_CONST;
00590 n->l = NULL;
00591 n->r = NULL;
00592 n->s = s;
00593 }
00594
00595 SetExpr::SetExpr(const LinIntExpr& e) : n(new Node) {
00596 n->same = 1;
00597 n->t = NT_LEXP;
00598 n->l = NULL;
00599 n->r = NULL;
00600 n->e = e;
00601 }
00602
00603 SetExpr::SetExpr(const SetExpr& l, NodeType t, const SetExpr& r)
00604 : n(new Node) {
00605 int ls = same(t,l.n->t) ? l.n->same : 1;
00606 int rs = same(t,r.n->t) ? r.n->same : 1;
00607 n->same = ls+rs;
00608 n->t = t;
00609 n->l = l.n;
00610 n->l->use++;
00611 n->r = r.n;
00612 n->r->use++;
00613 }
00614
00615 SetExpr::SetExpr(const SetExpr& l, NodeType t) {
00616 (void) t;
00617 assert(t == NT_CMPL);
00618 if (l.n->t == NT_CMPL) {
00619 n = l.n->l;
00620 n->use++;
00621 } else {
00622 n = new Node;
00623 n->same = 1;
00624 n->t = NT_CMPL;
00625 n->l = l.n;
00626 n->l->use++;
00627 n->r = NULL;
00628 }
00629 }
00630
00631 const SetExpr&
00632 SetExpr::operator =(const SetExpr& e) {
00633 if (this != &e) {
00634 if (n != NULL && n->decrement())
00635 delete n;
00636 n = e.n;
00637 n->use++;
00638 }
00639 return *this;
00640 }
00641
00642 SetExpr::~SetExpr(void) {
00643 if (n != NULL && n->decrement())
00644 delete n;
00645 }
00646
00647 SetExpr::SetExpr(const SetExpr& e) : n(e.n) {
00648 n->use++;
00649 }
00650
00651 SetVar
00652 SetExpr::post(Home home) const {
00653 Region r(home);
00654 SetVar s(home,IntSet::empty,
00655 IntSet(Set::Limits::min,Set::Limits::max));
00656 NNF::nnf(r,n,false)->post(home,SRT_EQ,s);
00657 return s;
00658 }
00659
00660 void
00661 SetExpr::post(Home home, SetRelType srt, const SetExpr& e) const {
00662 Region r(home);
00663 return NNF::nnf(r,n,false)->post(home,srt,NNF::nnf(r,e.n,false));
00664 }
00665 void
00666 SetExpr::post(Home home, BoolVar b, bool t,
00667 SetRelType srt, const SetExpr& e) const {
00668 Region r(home);
00669 return NNF::nnf(r,n,false)->post(home,b,t,srt,
00670 NNF::nnf(r,e.n,false));
00671 }
00672
00673 SetExpr
00674 operator &(const SetExpr& l, const SetExpr& r) {
00675 return SetExpr(l,SetExpr::NT_INTER,r);
00676 }
00677 SetExpr
00678 operator |(const SetExpr& l, const SetExpr& r) {
00679 return SetExpr(l,SetExpr::NT_UNION,r);
00680 }
00681 SetExpr
00682 operator +(const SetExpr& l, const SetExpr& r) {
00683 return SetExpr(l,SetExpr::NT_DUNION,r);
00684 }
00685 SetExpr
00686 operator -(const SetExpr& e) {
00687 return SetExpr(e,SetExpr::NT_CMPL);
00688 }
00689 SetExpr
00690 operator -(const SetExpr& l, const SetExpr& r) {
00691 return SetExpr(l,SetExpr::NT_INTER,-r);
00692 }
00693 SetExpr
00694 singleton(const LinIntExpr& e) {
00695 return SetExpr(e);
00696 }
00697
00698 SetExpr
00699 inter(const SetVarArgs& x) {
00700 if (x.size() == 0)
00701 return SetExpr(IntSet(Set::Limits::min,Set::Limits::max));
00702 SetExpr r(x[0]);
00703 for (int i=1; i<x.size(); i++)
00704 r = (r & x[i]);
00705 return r;
00706 }
00707 SetExpr
00708 setunion(const SetVarArgs& x) {
00709 if (x.size() == 0)
00710 return SetExpr(IntSet::empty);
00711 SetExpr r(x[0]);
00712 for (int i=1; i<x.size(); i++)
00713 r = (r | x[i]);
00714 return r;
00715 }
00716 SetExpr
00717 setdunion(const SetVarArgs& x) {
00718 if (x.size() == 0)
00719 return SetExpr(IntSet::empty);
00720 SetExpr r(x[0]);
00721 for (int i=1; i<x.size(); i++)
00722 r = (r + x[i]);
00723 return r;
00724 }
00725
00726 namespace MiniModel {
00728 class GECODE_MINIMODEL_EXPORT SetNonLinIntExpr : public NonLinIntExpr {
00729 public:
00731 enum SetNonLinIntExprType {
00732 SNLE_CARD,
00733 SNLE_MIN,
00734 SNLE_MAX
00735 } t;
00737 SetExpr e;
00739 SetNonLinIntExpr(const SetExpr& e0, SetNonLinIntExprType t0)
00740 : t(t0), e(e0) {}
00742 virtual IntVar post(Home home, IntVar* ret, IntConLevel) const {
00743 IntVar m = result(home,ret);
00744 switch (t) {
00745 case SNLE_CARD:
00746 cardinality(home, e.post(home), m);
00747 break;
00748 case SNLE_MIN:
00749 min(home, e.post(home), m);
00750 break;
00751 case SNLE_MAX:
00752 max(home, e.post(home), m);
00753 break;
00754 default:
00755 GECODE_NEVER;
00756 break;
00757 }
00758 return m;
00759 }
00760 virtual void post(Home home, IntRelType irt, int c,
00761 IntConLevel icl) const {
00762 if (t==SNLE_CARD && irt!=IRT_NQ) {
00763 switch (irt) {
00764 case IRT_LQ:
00765 cardinality(home, e.post(home),
00766 0U,
00767 static_cast<unsigned int>(c));
00768 break;
00769 case IRT_LE:
00770 cardinality(home, e.post(home),
00771 0U,
00772 static_cast<unsigned int>(c-1));
00773 break;
00774 case IRT_GQ:
00775 cardinality(home, e.post(home),
00776 static_cast<unsigned int>(c),
00777 Set::Limits::card);
00778 break;
00779 case IRT_GR:
00780 cardinality(home, e.post(home),
00781 static_cast<unsigned int>(c+1),
00782 Set::Limits::card);
00783 break;
00784 case IRT_EQ:
00785 cardinality(home, e.post(home),
00786 static_cast<unsigned int>(c),
00787 static_cast<unsigned int>(c));
00788 break;
00789 default:
00790 GECODE_NEVER;
00791 }
00792 } else if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) {
00793 c = (irt==IRT_GQ ? c : c+1);
00794 dom(home, e.post(home), SRT_SUB, c, Set::Limits::max);
00795 } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) {
00796 c = (irt==IRT_LQ ? c : c-1);
00797 dom(home, e.post(home), SRT_SUB, Set::Limits::min, c);
00798 } else {
00799 rel(home, post(home,NULL,icl), irt, c);
00800 }
00801 }
00802 virtual void post(Home home, IntRelType irt, int c,
00803 BoolVar b, IntConLevel icl) const {
00804 if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) {
00805 c = (irt==IRT_GQ ? c : c+1);
00806 dom(home, e.post(home), SRT_SUB, c, Set::Limits::max, b);
00807 } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) {
00808 c = (irt==IRT_LQ ? c : c-1);
00809 dom(home, e.post(home), SRT_SUB, Set::Limits::min, c, b);
00810 } else {
00811 rel(home, post(home,NULL,icl), irt, c, b);
00812 }
00813 }
00814 };
00815 }
00816
00817 LinIntExpr
00818 cardinality(const SetExpr& e) {
00819 return LinIntExpr(new MiniModel::SetNonLinIntExpr(e,
00820 MiniModel::SetNonLinIntExpr::SNLE_CARD));
00821 }
00822 LinIntExpr
00823 min(const SetExpr& e) {
00824 return LinIntExpr(new MiniModel::SetNonLinIntExpr(e,
00825 MiniModel::SetNonLinIntExpr::SNLE_MIN));
00826 }
00827 LinIntExpr
00828 max(const SetExpr& e) {
00829 return LinIntExpr(new MiniModel::SetNonLinIntExpr(e,
00830 MiniModel::SetNonLinIntExpr::SNLE_MAX));
00831 }
00832
00833
00834
00835
00836
00837 SetVar
00838 expr(Home home, const SetExpr& e) {
00839 if (!home.failed())
00840 return e.post(home);
00841 SetVar x(home,IntSet::empty,IntSet::empty);
00842 return x;
00843 }
00844
00845
00846 }
00847
00848 #endif
00849
00850