Generated on Fri Oct 19 11:25:14 2018 for Gecode by doxygen 1.6.3

set-expr.cpp

Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
00002 /*
00003  *  Main authors:
00004  *     Guido Tack <tack@gecode.org>
00005  *     Christian Schulte <schulte@gecode.org>
00006  *
00007  *  Copyright:
00008  *     Guido Tack, 2010
00009  *     Christian Schulte, 2004
00010  *
00011  *  This file is part of Gecode, the generic constraint
00012  *  development environment:
00013  *     http://www.gecode.org
00014  *
00015  *  Permission is hereby granted, free of charge, to any person obtaining
00016  *  a copy of this software and associated documentation files (the
00017  *  "Software"), to deal in the Software without restriction, including
00018  *  without limitation the rights to use, copy, modify, merge, publish,
00019  *  distribute, sublicense, and/or sell copies of the Software, and to
00020  *  permit persons to whom the Software is furnished to do so, subject to
00021  *  the following conditions:
00022  *
00023  *  The above copyright notice and this permission notice shall be
00024  *  included in all copies or substantial portions of the Software.
00025  *
00026  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00027  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00028  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00029  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00030  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00031  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00032  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
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    * Operations for nodes
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      * Operations for negation normalform
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         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 NULL;
00573     }
00574   }
00575 
00576   SetExpr::SetExpr(const SetVar& x) : n(new Node) {
00577     n->same = 1;
00578     n->t    = NT_VAR;
00579     n->l    = NULL;
00580     n->r    = NULL;
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    = NULL;
00588     n->r    = NULL;
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    = NULL;
00596     n->r    = NULL;
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    = NULL;
00625     }
00626   }
00627 
00628   const SetExpr&
00629   SetExpr::operator =(const SetExpr& e) {
00630     if (this != &e) {
00631       if (n != NULL && 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 != NULL && 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, IntPropLevel) const {
00740         IntVar m = result(home,ret);
00741         switch (t) {
00742         case SNLE_CARD:
00743           cardinality(home, e.post(home), m);
00744           break;
00745         case SNLE_MIN:
00746           min(home, e.post(home), m);
00747           break;
00748         case SNLE_MAX:
00749           max(home, e.post(home), m);
00750           break;
00751         default:
00752           GECODE_NEVER;
00753           break;
00754         }
00755         return m;
00756       }
00757       virtual void post(Home home, IntRelType irt, int c,
00758                         IntPropLevel ipl) const {
00759         if (t==SNLE_CARD && irt!=IRT_NQ) {
00760           switch (irt) {
00761           case IRT_LQ:
00762             cardinality(home, e.post(home),
00763                         0U,
00764                         static_cast<unsigned int>(c));
00765             break;
00766           case IRT_LE:
00767             cardinality(home, e.post(home),
00768                         0U,
00769                         static_cast<unsigned int>(c-1));
00770             break;
00771           case IRT_GQ:
00772             cardinality(home, e.post(home),
00773                         static_cast<unsigned int>(c),
00774                         Set::Limits::card);
00775             break;
00776           case IRT_GR:
00777             cardinality(home, e.post(home),
00778                         static_cast<unsigned int>(c+1),
00779                         Set::Limits::card);
00780             break;
00781           case IRT_EQ:
00782             cardinality(home, e.post(home),
00783                         static_cast<unsigned int>(c),
00784                         static_cast<unsigned int>(c));
00785             break;
00786           default:
00787             GECODE_NEVER;
00788           }
00789         } else if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) {
00790           c = (irt==IRT_GQ ? c : c+1);
00791           dom(home, e.post(home), SRT_SUB, c, Set::Limits::max);
00792         } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) {
00793           c = (irt==IRT_LQ ? c : c-1);
00794           dom(home, e.post(home), SRT_SUB, Set::Limits::min, c);
00795         } else {
00796           rel(home, post(home,NULL,ipl), irt, c);
00797         }
00798       }
00799       virtual void post(Home home, IntRelType irt, int c,
00800                         BoolVar b, IntPropLevel ipl) const {
00801         if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) {
00802           c = (irt==IRT_GQ ? c : c+1);
00803           dom(home, e.post(home), SRT_SUB, c, Set::Limits::max, b);
00804         } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) {
00805           c = (irt==IRT_LQ ? c : c-1);
00806           dom(home, e.post(home), SRT_SUB, Set::Limits::min, c, b);
00807         } else {
00808           rel(home, post(home,NULL,ipl), irt, c, b);
00809         }
00810       }
00811     };
00812   }
00813 
00814   LinIntExpr
00815   cardinality(const SetExpr& e) {
00816     return LinIntExpr(new MiniModel::SetNonLinIntExpr(e,
00817       MiniModel::SetNonLinIntExpr::SNLE_CARD));
00818   }
00819   LinIntExpr
00820   min(const SetExpr& e) {
00821     return LinIntExpr(new MiniModel::SetNonLinIntExpr(e,
00822       MiniModel::SetNonLinIntExpr::SNLE_MIN));
00823   }
00824   LinIntExpr
00825   max(const SetExpr& e) {
00826     return LinIntExpr(new MiniModel::SetNonLinIntExpr(e,
00827       MiniModel::SetNonLinIntExpr::SNLE_MAX));
00828   }
00829 
00830   /*
00831    * Posting set expressions
00832    *
00833    */
00834   SetVar
00835   expr(Home home, const SetExpr& e) {
00836     PostInfo pi(home);
00837     if (!home.failed())
00838       return e.post(home);
00839     SetVar x(home,IntSet::empty,IntSet::empty);
00840     return x;
00841   }
00842 
00843 
00844 }
00845 
00846 #endif
00847 
00848 // STATISTICS: minimodel-any