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