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