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 dom(home, s, srt, ss, b);
00353 }
00354 break;
00355 case SetExpr::NT_LEXP:
00356 {
00357 IntVar iv = u.a.x->e.post(home,ICL_DEF);
00358 if (neg) {
00359 SetVar ic(home,IntSet::empty,
00360 IntSet(Set::Limits::min,Set::Limits::max));
00361 rel(home, iv, SRT_CMPL, ic);
00362 rel(home,ic,srt,s,b);
00363 } else {
00364 rel(home,iv,srt,s,b);
00365 }
00366 }
00367 case SetExpr::NT_INTER:
00368 {
00369 SetVarArgs bs(p+n);
00370 int i=0;
00371 post(home, SetExpr::NT_INTER, bs, i);
00372 SetVar br(home,IntSet::empty,
00373 IntSet(Set::Limits::min,Set::Limits::max));
00374 rel(home, SOT_INTER, bs, br);
00375 rel(home, br, srt, s, b);
00376 }
00377 break;
00378 case SetExpr::NT_UNION:
00379 {
00380 SetVarArgs bs(p+n);
00381 int i=0;
00382 post(home, SetExpr::NT_UNION, bs, i);
00383 SetVar br(home,IntSet::empty,
00384 IntSet(Set::Limits::min,Set::Limits::max));
00385 rel(home, SOT_UNION, bs, br);
00386 rel(home, br, srt, s, b);
00387 }
00388 break;
00389 case SetExpr::NT_DUNION:
00390 {
00391 SetVarArgs bs(p+n);
00392 int i=0;
00393 post(home, SetExpr::NT_DUNION, bs, i);
00394
00395 if (neg) {
00396 SetVar br(home,IntSet::empty,
00397 IntSet(Set::Limits::min,Set::Limits::max));
00398 rel(home, SOT_DUNION, bs, br);
00399 if (srt == SRT_CMPL)
00400 rel(home, br, SRT_EQ, s, b);
00401 else if (srt == SRT_EQ)
00402 rel(home, br, SRT_CMPL, s, b);
00403 else {
00404 SetVar bc(home,IntSet::empty,
00405 IntSet(Set::Limits::min,Set::Limits::max));
00406 rel(home, br, srt, bc);
00407 rel(home, bc, SRT_CMPL, s, b);
00408 }
00409 } else {
00410 SetVar br(home,IntSet::empty,
00411 IntSet(Set::Limits::min,Set::Limits::max));
00412 rel(home, SOT_DUNION, bs, br);
00413 rel(home, br, srt, s, b);
00414 }
00415 }
00416 break;
00417 default:
00418 GECODE_NEVER;
00419 }
00420 }
00421
00422 void
00423 NNF::post(Home home, NodeType t, SetVarArgs& b, int& i) const {
00424 if (this->t != t) {
00425 switch (this->t) {
00426 case SetExpr::NT_VAR:
00427 if (neg) {
00428 SetVar xc(home,IntSet::empty,
00429 IntSet(Set::Limits::min,Set::Limits::max));
00430 rel(home, xc, SRT_CMPL, u.a.x->x);
00431 b[i++]=xc;
00432 } else {
00433 b[i++]=u.a.x->x;
00434 }
00435 break;
00436 default:
00437 {
00438 SetVar s(home,IntSet::empty,
00439 IntSet(Set::Limits::min,Set::Limits::max));
00440 post(home,SRT_EQ,s);
00441 b[i++] = s;
00442 }
00443 break;
00444 }
00445 } else {
00446 u.b.l->post(home, t, b, i);
00447 u.b.r->post(home, t, b, i);
00448 }
00449 }
00450
00451 void
00452 NNF::post(Home home, SetRelType srt, const NNF* n) const {
00453 if (n->t == SetExpr::NT_VAR && !n->neg) {
00454 post(home,srt,n->u.a.x->x);
00455 } else if (t == SetExpr::NT_VAR && !neg) {
00456 SetRelType n_srt;
00457 switch (srt) {
00458 case SRT_SUB: n_srt = SRT_SUP; break;
00459 case SRT_SUP: n_srt = SRT_SUB; break;
00460 default: n_srt = srt;
00461 }
00462 n->post(home,n_srt,this);
00463 } else {
00464 SetVar nx(home,IntSet::empty,
00465 IntSet(Set::Limits::min,Set::Limits::max));
00466 n->post(home,SRT_EQ,nx);
00467 post(home,srt,nx);
00468 }
00469 }
00470
00471 void
00472 NNF::post(Home home, BoolVar b, bool t,
00473 SetRelType srt, const NNF* n) const {
00474 if (t) {
00475 if (n->t == SetExpr::NT_VAR && !n->neg) {
00476 post(home,srt,n->u.a.x->x,b);
00477 } else if (t == SetExpr::NT_VAR && !neg) {
00478 SetRelType n_srt;
00479 switch (srt) {
00480 case SRT_SUB: n_srt = SRT_SUP; break;
00481 case SRT_SUP: n_srt = SRT_SUB; break;
00482 default: n_srt = srt;
00483 }
00484 n->post(home,b,true,n_srt,this);
00485 } else {
00486 SetVar nx(home,IntSet::empty,
00487 IntSet(Set::Limits::min,Set::Limits::max));
00488 n->post(home,SRT_EQ,nx);
00489 post(home,srt,nx,b);
00490 }
00491 } else if (srt == SRT_EQ) {
00492 post(home,b,true,SRT_NQ,n);
00493 } else if (srt == SRT_NQ) {
00494 post(home,b,true,SRT_EQ,n);
00495 } else {
00496 BoolVar nb(home,0,1);
00497 rel(home,b,IRT_NQ,nb);
00498 post(home,nb,true,srt,n);
00499 }
00500 }
00501
00502 NNF*
00503 NNF::nnf(Region& r, Node* n, bool neg) {
00504 switch (n->t) {
00505 case SetExpr::NT_VAR:
00506 case SetExpr::NT_CONST:
00507 case SetExpr::NT_LEXP:
00508 {
00509 NNF* x = new (r) NNF;
00510 x->t = n->t; x->neg = neg; x->u.a.x = n;
00511 if (neg) {
00512 x->p = 0; x->n = 1;
00513 } else {
00514 x->p = 1; x->n = 0;
00515 }
00516 return x;
00517 }
00518 case SetExpr::NT_CMPL:
00519 return nnf(r,n->l,!neg);
00520 case SetExpr::NT_INTER:
00521 case SetExpr::NT_UNION:
00522 case SetExpr::NT_DUNION:
00523 {
00524 NodeType t; bool xneg;
00525 if (n->t == SetExpr::NT_DUNION) {
00526 t = n->t; xneg = neg; neg = false;
00527 } else {
00528 t = ((n->t == SetExpr::NT_INTER) == neg) ?
00529 SetExpr::NT_UNION : SetExpr::NT_INTER;
00530 xneg = false;
00531 }
00532 NNF* x = new (r) NNF;
00533 x->neg = xneg;
00534 x->t = t;
00535 x->u.b.l = nnf(r,n->l,neg);
00536 x->u.b.r = nnf(r,n->r,neg);
00537 int p_l, n_l;
00538 if ((x->u.b.l->t == t) || (x->u.b.l->t == SetExpr::NT_VAR)) {
00539 p_l=x->u.b.l->p; n_l=x->u.b.l->n;
00540 } else {
00541 p_l=1; n_l=0;
00542 }
00543 int p_r, n_r;
00544 if ((x->u.b.r->t == t) || (x->u.b.r->t == SetExpr::NT_VAR)) {
00545 p_r=x->u.b.r->p; n_r=x->u.b.r->n;
00546 } else {
00547 p_r=1; n_r=0;
00548 }
00549 x->p = p_l+p_r;
00550 x->n = n_l+n_r;
00551 return x;
00552 }
00553 default:
00554 GECODE_NEVER;
00555 }
00556 GECODE_NEVER;
00557 return NULL;
00558 }
00559 }
00560
00561 SetExpr::SetExpr(const SetVar& x) : n(new Node) {
00562 n->same = 1;
00563 n->t = NT_VAR;
00564 n->l = NULL;
00565 n->r = NULL;
00566 n->x = x;
00567 }
00568
00569 SetExpr::SetExpr(const IntSet& s) : n(new Node) {
00570 n->same = 1;
00571 n->t = NT_CONST;
00572 n->l = NULL;
00573 n->r = NULL;
00574 n->s = s;
00575 }
00576
00577 SetExpr::SetExpr(const LinIntExpr& e) : n(new Node) {
00578 n->same = 1;
00579 n->t = NT_LEXP;
00580 n->l = NULL;
00581 n->r = NULL;
00582 n->e = e;
00583 }
00584
00585 SetExpr::SetExpr(const SetExpr& l, NodeType t, const SetExpr& r)
00586 : n(new Node) {
00587 int ls = same(t,l.n->t) ? l.n->same : 1;
00588 int rs = same(t,r.n->t) ? r.n->same : 1;
00589 n->same = ls+rs;
00590 n->t = t;
00591 n->l = l.n;
00592 n->l->use++;
00593 n->r = r.n;
00594 n->r->use++;
00595 }
00596
00597 SetExpr::SetExpr(const SetExpr& l, NodeType t) {
00598 (void) t;
00599 assert(t == NT_CMPL);
00600 if (l.n->t == NT_CMPL) {
00601 n = l.n->l;
00602 n->use++;
00603 } else {
00604 n = new Node;
00605 n->same = 1;
00606 n->t = NT_CMPL;
00607 n->l = l.n;
00608 n->l->use++;
00609 n->r = NULL;
00610 }
00611 }
00612
00613 const SetExpr&
00614 SetExpr::operator =(const SetExpr& e) {
00615 if (this != &e) {
00616 if (n != NULL && n->decrement())
00617 delete n;
00618 n = e.n;
00619 n->use++;
00620 }
00621 return *this;
00622 }
00623
00624 SetExpr::~SetExpr(void) {
00625 if (n != NULL && n->decrement())
00626 delete n;
00627 }
00628
00629 SetExpr::SetExpr(const SetExpr& e) : n(e.n) {
00630 n->use++;
00631 }
00632
00633 SetVar
00634 SetExpr::post(Home home) const {
00635 Region r(home);
00636 SetVar s(home,IntSet::empty,
00637 IntSet(Set::Limits::min,Set::Limits::max));
00638 NNF::nnf(r,n,false)->post(home,SRT_EQ,s);
00639 return s;
00640 }
00641
00642 void
00643 SetExpr::post(Home home, SetRelType srt, const SetExpr& e) const {
00644 Region r(home);
00645 return NNF::nnf(r,n,false)->post(home,srt,NNF::nnf(r,e.n,false));
00646 }
00647 void
00648 SetExpr::post(Home home, BoolVar b, bool t,
00649 SetRelType srt, const SetExpr& e) const {
00650 Region r(home);
00651 return NNF::nnf(r,n,false)->post(home,b,t,srt,
00652 NNF::nnf(r,e.n,false));
00653 }
00654
00655 SetExpr
00656 operator &(const SetExpr& l, const SetExpr& r) {
00657 return SetExpr(l,SetExpr::NT_INTER,r);
00658 }
00659 SetExpr
00660 operator |(const SetExpr& l, const SetExpr& r) {
00661 return SetExpr(l,SetExpr::NT_UNION,r);
00662 }
00663 SetExpr
00664 operator +(const SetExpr& l, const SetExpr& r) {
00665 return SetExpr(l,SetExpr::NT_DUNION,r);
00666 }
00667 SetExpr
00668 operator -(const SetExpr& e) {
00669 return SetExpr(e,SetExpr::NT_CMPL);
00670 }
00671 SetExpr
00672 operator -(const SetExpr& l, const SetExpr& r) {
00673 return SetExpr(l,SetExpr::NT_INTER,-r);
00674 }
00675 SetExpr
00676 singleton(const LinIntExpr& e) {
00677 return SetExpr(e);
00678 }
00679
00680 SetExpr
00681 inter(const SetVarArgs& x) {
00682 if (x.size() == 0)
00683 return SetExpr(IntSet(Set::Limits::min,Set::Limits::max));
00684 SetExpr r(x[0]);
00685 for (int i=1; i<x.size(); i++)
00686 r = (r & x[i]);
00687 return r;
00688 }
00689 SetExpr
00690 setunion(const SetVarArgs& x) {
00691 if (x.size() == 0)
00692 return SetExpr(IntSet::empty);
00693 SetExpr r(x[0]);
00694 for (int i=1; i<x.size(); i++)
00695 r = (r | x[i]);
00696 return r;
00697 }
00698 SetExpr
00699 setdunion(const SetVarArgs& x) {
00700 if (x.size() == 0)
00701 return SetExpr(IntSet::empty);
00702 SetExpr r(x[0]);
00703 for (int i=1; i<x.size(); i++)
00704 r = (r + x[i]);
00705 return r;
00706 }
00707
00708 namespace MiniModel {
00710 class GECODE_MINIMODEL_EXPORT SetNonLinIntExpr : public NonLinIntExpr {
00711 public:
00713 enum SetNonLinIntExprType {
00714 SNLE_CARD,
00715 SNLE_MIN,
00716 SNLE_MAX
00717 } t;
00719 SetExpr e;
00721 SetNonLinIntExpr(const SetExpr& e0, SetNonLinIntExprType t0)
00722 : t(t0), e(e0) {}
00724 virtual IntVar post(Home home, IntVar* ret, IntConLevel) const {
00725 IntVar m = result(home,ret);
00726 switch (t) {
00727 case SNLE_CARD:
00728 cardinality(home, e.post(home), m);
00729 break;
00730 case SNLE_MIN:
00731 min(home, e.post(home), m);
00732 break;
00733 case SNLE_MAX:
00734 max(home, e.post(home), m);
00735 break;
00736 default:
00737 GECODE_NEVER;
00738 break;
00739 }
00740 return m;
00741 }
00742 virtual void post(Home home, IntRelType irt, int c,
00743 IntConLevel icl) const {
00744 if (t==SNLE_CARD && irt!=IRT_NQ) {
00745 switch (irt) {
00746 case IRT_LQ:
00747 cardinality(home, e.post(home),
00748 0U,
00749 static_cast<unsigned int>(c));
00750 break;
00751 case IRT_LE:
00752 cardinality(home, e.post(home),
00753 0U,
00754 static_cast<unsigned int>(c-1));
00755 break;
00756 case IRT_GQ:
00757 cardinality(home, e.post(home),
00758 static_cast<unsigned int>(c),
00759 Set::Limits::card);
00760 break;
00761 case IRT_GR:
00762 cardinality(home, e.post(home),
00763 static_cast<unsigned int>(c+1),
00764 Set::Limits::card);
00765 break;
00766 case IRT_EQ:
00767 cardinality(home, e.post(home),
00768 static_cast<unsigned int>(c),
00769 static_cast<unsigned int>(c));
00770 break;
00771 default:
00772 GECODE_NEVER;
00773 }
00774 } else if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) {
00775 c = (irt==IRT_GQ ? c : c+1);
00776 dom(home, e.post(home), SRT_SUB, c, Set::Limits::max);
00777 } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) {
00778 c = (irt==IRT_LQ ? c : c-1);
00779 dom(home, e.post(home), SRT_SUB, Set::Limits::min, c);
00780 } else {
00781 rel(home, post(home,NULL,icl), irt, c);
00782 }
00783 }
00784 virtual void post(Home home, IntRelType irt, int c,
00785 BoolVar b, IntConLevel icl) const {
00786 if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) {
00787 c = (irt==IRT_GQ ? c : c+1);
00788 dom(home, e.post(home), SRT_SUB, c, Set::Limits::max, b);
00789 } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) {
00790 c = (irt==IRT_LQ ? c : c-1);
00791 dom(home, e.post(home), SRT_SUB, Set::Limits::min, c, b);
00792 } else {
00793 rel(home, post(home,NULL,icl), irt, c, b);
00794 }
00795 }
00796 };
00797 }
00798
00799 LinIntExpr
00800 cardinality(const SetExpr& e) {
00801 return LinIntExpr(new MiniModel::SetNonLinIntExpr(e,
00802 MiniModel::SetNonLinIntExpr::SNLE_CARD));
00803 }
00804 LinIntExpr
00805 min(const SetExpr& e) {
00806 return LinIntExpr(new MiniModel::SetNonLinIntExpr(e,
00807 MiniModel::SetNonLinIntExpr::SNLE_MIN));
00808 }
00809 LinIntExpr
00810 max(const SetExpr& e) {
00811 return LinIntExpr(new MiniModel::SetNonLinIntExpr(e,
00812 MiniModel::SetNonLinIntExpr::SNLE_MAX));
00813 }
00814
00815
00816
00817
00818
00819 SetVar
00820 expr(Home home, const SetExpr& e) {
00821 if (!home.failed())
00822 return e.post(home);
00823 SetVar x(home,IntSet::empty,IntSet::empty);
00824 return x;
00825 }
00826
00827
00828 }
00829
00830 #endif
00831
00832