Generated on Tue Jul 27 2010 21:59:17 for Gecode by doxygen 1.7.1

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  *  Last modified:
00012  *     $Date: 2010-07-14 20:32:01 +0200 (Wed, 14 Jul 2010) $ by $Author: schulte $
00013  *     $Revision: 11195 $
00014  *
00015  *  This file is part of Gecode, the generic constraint
00016  *  development environment:
00017  *     http://www.gecode.org
00018  *
00019  *  Permission is hereby granted, free of charge, to any person obtaining
00020  *  a copy of this software and associated documentation files (the
00021  *  "Software"), to deal in the Software without restriction, including
00022  *  without limitation the rights to use, copy, modify, merge, publish,
00023  *  distribute, sublicense, and/or sell copies of the Software, and to
00024  *  permit persons to whom the Software is furnished to do so, subject to
00025  *  the following conditions:
00026  *
00027  *  The above copyright notice and this permission notice shall be
00028  *  included in all copies or substantial portions of the Software.
00029  *
00030  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00031  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00032  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00033  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00034  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00035  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00036  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00037  *
00038  */
00039 
00040 #include <gecode/minimodel.hh>
00041 
00042 #ifdef GECODE_HAS_SET_VARS
00043 
00044 namespace Gecode {
00045 
00046   /*
00047    * Operations for nodes
00048    *
00049    */
00050   bool
00051   SetExpr::Node::decrement(void) {
00052     if (--use == 0) {
00053       if ((l != NULL) && l->decrement())
00054         delete l;
00055       if ((r != NULL) && r->decrement())
00056         delete r;
00057       return true;
00058     }
00059     return false;
00060   }
00061 
00062 
00063   const SetExpr&
00064   SetExpr::operator =(const SetExpr& e) {
00065     if (this != &e) {
00066       if (n != NULL && n->decrement())
00067         delete n;
00068       n = e.n;
00069       n->use++;
00070     }
00071     return *this;
00072   }
00073 
00074   SetExpr::~SetExpr(void) {
00075     if (n != NULL && n->decrement())
00076       delete n;
00077   }
00078 
00079   /*
00080    * Operations for negation normalform
00081    *
00082    */
00083   forceinline void
00084   SetExpr::NNF::operator delete(void*) {}
00085 
00086   forceinline void
00087   SetExpr::NNF::operator delete(void*, Region&) {}
00088 
00089   forceinline void*
00090   SetExpr::NNF::operator new(size_t s, Region& r) {
00091     return r.ralloc(s);
00092   }
00093 
00094   void
00095   SetExpr::NNF::post(Home home, SetRelType srt, SetVar s) const {
00096     switch (t) {
00097     case NT_VAR:
00098       if (neg) {
00099         switch (srt) {
00100         case SRT_EQ:
00101           rel(home, u.a.x->x, SRT_CMPL, s);
00102           break;
00103         case SRT_CMPL:
00104           rel(home, u.a.x->x, SRT_EQ, s);
00105           break;
00106         default:
00107           SetVar bc(home,IntSet::empty,
00108                     IntSet(Set::Limits::min,Set::Limits::max));
00109           rel(home, s, SRT_CMPL, bc);
00110           rel(home, u.a.x->x, srt, bc);
00111           break;
00112         }
00113       } else
00114         rel(home, u.a.x->x, srt, s);
00115       break;
00116     case NT_CONST:
00117       {
00118         IntSet ss;
00119         if (neg) {
00120           IntSetRanges sr(u.a.x->s);
00121           Set::RangesCompl<IntSetRanges> src(sr);
00122           ss = IntSet(src);
00123         } else {
00124           ss = u.a.x->s;
00125         }
00126         switch (srt) {
00127         case SRT_SUB: srt = SRT_SUP; break;
00128         case SRT_SUP: srt = SRT_SUB; break;
00129         default: break;
00130         }
00131         dom(home, s, srt, ss);
00132       }
00133       break;
00134     case NT_LEXP:
00135       {
00136         IntVar iv = u.a.x->e.post(home,ICL_DEF);
00137         if (neg) {
00138           SetVar ic(home,IntSet::empty,
00139                     IntSet(Set::Limits::min,Set::Limits::max));
00140           rel(home, iv, SRT_CMPL, ic);
00141           rel(home,ic,srt,s);
00142         } else {
00143           rel(home,iv,srt,s);
00144         }
00145       }
00146       break;
00147     case NT_INTER:
00148       {
00149         SetVarArgs bs(p+n);
00150         int i=0;
00151         post(home, NT_INTER, bs, i);
00152         if (i == 2) {
00153           rel(home, bs[0], SOT_INTER, bs[1], srt, s);
00154         } else {
00155           if (srt == SRT_EQ)
00156             rel(home, SOT_INTER, bs, s);
00157           else {
00158             SetVar bc(home,IntSet::empty,
00159                       IntSet(Set::Limits::min,Set::Limits::max));
00160             rel(home, SOT_INTER, bs, bc);
00161             rel(home, bc, srt, s);
00162           }
00163         }
00164       }
00165       break;
00166     case NT_UNION:
00167       {
00168         SetVarArgs bs(p+n);
00169         int i=0;
00170         post(home, NT_UNION, bs, i);
00171         if (i == 2) {
00172           rel(home, bs[0], SOT_UNION, bs[1], srt, s);
00173         } else {
00174           if (srt == SRT_EQ)
00175             rel(home, SOT_UNION, bs, s);
00176           else {
00177             SetVar bc(home,IntSet::empty,
00178                       IntSet(Set::Limits::min,Set::Limits::max));
00179             rel(home, SOT_UNION, bs, bc);
00180             rel(home, bc, srt, s);
00181           }
00182         }
00183       }
00184       break;
00185     case NT_DUNION:
00186       {
00187         SetVarArgs bs(p+n);
00188         int i=0;
00189         post(home, NT_DUNION, bs, i);
00190 
00191         if (i == 2) {
00192           if (neg) {
00193             if (srt == SRT_CMPL) {
00194               rel(home, bs[0], SOT_DUNION, bs[1], srt, s);
00195             } else {
00196               SetVar bc(home,IntSet::empty,
00197                 IntSet(Set::Limits::min,Set::Limits::max));
00198               rel(home,s,SRT_CMPL,bc);
00199               rel(home, bs[0], SOT_DUNION, bs[1], srt, bc);
00200             }
00201           } else {
00202             rel(home, bs[0], SOT_DUNION, bs[1], srt, s);
00203           }
00204         } else {
00205           if (neg) {
00206             if (srt == SRT_CMPL) {
00207               rel(home, SOT_DUNION, bs, s);
00208             } else {
00209               SetVar br(home,IntSet::empty,
00210                         IntSet(Set::Limits::min,Set::Limits::max));
00211               rel(home, SOT_DUNION, bs, br);
00212               if (srt == SRT_EQ)
00213                 rel(home, br, SRT_CMPL, s);
00214               else {
00215                 SetVar bc(home,IntSet::empty,
00216                           IntSet(Set::Limits::min,Set::Limits::max));
00217                 rel(home, br, srt, bc);
00218                 rel(home, bc, SRT_CMPL, s);
00219               }
00220             }
00221           } else {
00222             if (srt == SRT_EQ)
00223               rel(home, SOT_DUNION, bs, s);
00224             else {
00225               SetVar br(home,IntSet::empty,
00226                         IntSet(Set::Limits::min,Set::Limits::max));
00227               rel(home, SOT_DUNION, bs, br);
00228               rel(home, br, srt, s);
00229             }
00230           }
00231         }
00232       }
00233       break;
00234     default:
00235       GECODE_NEVER;
00236     }
00237   }
00238 
00239   void
00240   SetExpr::NNF::post(Home home, SetRelType srt, SetVar s, BoolVar b) const {
00241     switch (t) {
00242     case NT_VAR:
00243       if (neg) {
00244         switch (srt) {
00245         case SRT_EQ:
00246           rel(home, u.a.x->x, SRT_CMPL, s, b);
00247           break;
00248         case SRT_CMPL:
00249           rel(home, u.a.x->x, SRT_EQ, s, b);
00250           break;
00251         default:
00252           SetVar bc(home,IntSet::empty,
00253                     IntSet(Set::Limits::min,Set::Limits::max));
00254           rel(home, s, SRT_CMPL, bc);
00255           rel(home, u.a.x->x, srt, bc, b);
00256           break;
00257         }
00258       } else
00259         rel(home, u.a.x->x, srt, s, b);
00260       break;
00261     case NT_CONST:
00262       {
00263         IntSet ss;
00264         if (neg) {
00265           IntSetRanges sr(u.a.x->s);
00266           Set::RangesCompl<IntSetRanges> src(sr);
00267           ss = IntSet(src);
00268         } else {
00269           ss = u.a.x->s;
00270         }
00271         dom(home, s, srt, ss, b);
00272       }
00273       break;
00274     case NT_LEXP:
00275       {
00276         IntVar iv = u.a.x->e.post(home,ICL_DEF);
00277         if (neg) {
00278           SetVar ic(home,IntSet::empty,
00279                     IntSet(Set::Limits::min,Set::Limits::max));
00280           rel(home, iv, SRT_CMPL, ic);
00281           rel(home,ic,srt,s,b);
00282         } else {
00283           rel(home,iv,srt,s,b);
00284         }
00285       }
00286     case NT_INTER:
00287       {
00288         SetVarArgs bs(p+n);
00289         int i=0;
00290         post(home, NT_INTER, bs, i);
00291         SetVar br(home,IntSet::empty,
00292                   IntSet(Set::Limits::min,Set::Limits::max));
00293         rel(home, SOT_INTER, bs, br);
00294         rel(home, br, srt, s, b);
00295       }
00296       break;
00297     case NT_UNION:
00298       {
00299         SetVarArgs bs(p+n);
00300         int i=0;
00301         post(home, NT_UNION, bs, i);
00302         SetVar br(home,IntSet::empty,
00303                   IntSet(Set::Limits::min,Set::Limits::max));
00304         rel(home, SOT_UNION, bs, br);
00305         rel(home, br, srt, s, b);
00306       }
00307       break;
00308     case NT_DUNION:
00309       {
00310         SetVarArgs bs(p+n);
00311         int i=0;
00312         post(home, NT_DUNION, bs, i);
00313 
00314         if (neg) {
00315           SetVar br(home,IntSet::empty,
00316                     IntSet(Set::Limits::min,Set::Limits::max));
00317           rel(home, SOT_DUNION, bs, br);
00318           if (srt == SRT_CMPL)
00319             rel(home, br, SRT_EQ, s, b);
00320           else if (srt == SRT_EQ)
00321             rel(home, br, SRT_CMPL, s, b);
00322           else {
00323             SetVar bc(home,IntSet::empty,
00324                       IntSet(Set::Limits::min,Set::Limits::max));
00325             rel(home, br, srt, bc);
00326             rel(home, bc, SRT_CMPL, s, b);
00327           }
00328         } else {
00329           SetVar br(home,IntSet::empty,
00330                     IntSet(Set::Limits::min,Set::Limits::max));
00331           rel(home, SOT_DUNION, bs, br);
00332           rel(home, br, srt, s, b);
00333         }
00334       }
00335       break;
00336     default:
00337       GECODE_NEVER;
00338     }
00339   }
00340 
00341   void
00342   SetExpr::NNF::post(Home home, NodeType t,
00343                      SetVarArgs& b, int& i) const {
00344     if (this->t != t) {
00345       switch (this->t) {
00346       case NT_VAR:
00347         if (neg) {
00348           SetVar xc(home,IntSet::empty,
00349                     IntSet(Set::Limits::min,Set::Limits::max));
00350           rel(home, xc, SRT_CMPL, u.a.x->x);
00351           b[i++]=xc;
00352         } else {
00353           b[i++]=u.a.x->x;
00354         }
00355         break;
00356       default:
00357         {
00358           SetVar s(home,IntSet::empty,
00359                    IntSet(Set::Limits::min,Set::Limits::max));
00360           post(home,SRT_EQ,s);
00361           b[i++] = s;
00362         }
00363         break;
00364       }
00365     } else {
00366       u.b.l->post(home, t, b, i);
00367       u.b.r->post(home, t, b, i);
00368     }
00369   }
00370 
00371   void
00372   SetExpr::NNF::post(Home home, SetRelType srt, const NNF* n) const {
00373     if (n->t == NT_VAR && !n->neg) {
00374       post(home,srt,n->u.a.x->x);
00375     } else if (t == NT_VAR && !neg) {
00376       SetRelType n_srt;
00377       switch (srt) {
00378       case SRT_SUB: n_srt = SRT_SUP; break;
00379       case SRT_SUP: n_srt = SRT_SUB; break;
00380       default: n_srt = srt;
00381       }
00382       n->post(home,n_srt,this);
00383     } else {
00384       SetVar nx(home,IntSet::empty,
00385                 IntSet(Set::Limits::min,Set::Limits::max));
00386       n->post(home,SRT_EQ,nx);
00387       post(home,srt,nx);
00388     }
00389   }
00390 
00391   void
00392   SetExpr::NNF::post(Home home, BoolVar b, bool t,
00393                      SetRelType srt, const NNF* n) const {
00394     if (t) {
00395       if (n->t == NT_VAR && !n->neg) {
00396         post(home,srt,n->u.a.x->x,b);
00397       } else if (t == NT_VAR && !neg) {
00398         SetRelType n_srt;
00399         switch (srt) {
00400         case SRT_SUB: n_srt = SRT_SUP; break;
00401         case SRT_SUP: n_srt = SRT_SUB; break;
00402         default: n_srt = srt;
00403         }
00404         n->post(home,b,true,n_srt,this);
00405       } else {
00406         SetVar nx(home,IntSet::empty,
00407                   IntSet(Set::Limits::min,Set::Limits::max));
00408         n->post(home,SRT_EQ,nx);
00409         post(home,srt,nx,b);
00410       }
00411     } else if (srt == SRT_EQ) {
00412       post(home,b,true,SRT_NQ,n);
00413     } else if (srt == SRT_NQ) {
00414       post(home,b,true,SRT_EQ,n);
00415     } else {
00416       BoolVar nb(home,0,1);
00417       rel(home,b,IRT_NQ,nb);
00418       post(home,nb,true,srt,n);
00419     }
00420   }
00421 
00422   SetExpr::NNF*
00423   SetExpr::NNF::nnf(Region& r, Node* n, bool neg) {
00424     switch (n->t) {
00425     case NT_VAR: case NT_CONST: case NT_LEXP:
00426       {
00427         NNF* x = new (r) NNF;
00428         x->t = n->t; x->neg = neg; x->u.a.x = n;
00429         if (neg) {
00430           x->p = 0; x->n = 1;
00431         } else {
00432           x->p = 1; x->n = 0;
00433         }
00434         return x;
00435       }
00436     case NT_CMPL:
00437       return nnf(r,n->l,!neg);
00438     case NT_INTER: case NT_UNION: case NT_DUNION:
00439       {
00440         NodeType t; bool xneg;
00441         if (n->t == NT_DUNION) {
00442           t = n->t; xneg = neg; neg = false;
00443         } else {
00444           t = ((n->t == NT_INTER) == neg) ? NT_UNION : NT_INTER;
00445           xneg = false;
00446         }
00447         NNF* x = new (r) NNF;
00448         x->neg = xneg;
00449         x->t = t;
00450         x->u.b.l = nnf(r,n->l,neg);
00451         x->u.b.r = nnf(r,n->r,neg);
00452         int p_l, n_l;
00453         if ((x->u.b.l->t == t) || (x->u.b.l->t == NT_VAR)) {
00454           p_l=x->u.b.l->p; n_l=x->u.b.l->n;
00455         } else {
00456           p_l=1; n_l=0;
00457         }
00458         int p_r, n_r;
00459         if ((x->u.b.r->t == t) || (x->u.b.r->t == NT_VAR)) {
00460           p_r=x->u.b.r->p; n_r=x->u.b.r->n;
00461         } else {
00462           p_r=1; n_r=0;
00463         }
00464         x->p = p_l+p_r;
00465         x->n = n_l+n_r;
00466         return x;
00467       }
00468     default:
00469       GECODE_NEVER;
00470     }
00471     GECODE_NEVER;
00472     return NULL;
00473   }
00474 
00475 
00476   SetExpr
00477   operator &(const SetExpr& l, const SetExpr& r) {
00478     return SetExpr(l,SetExpr::NT_INTER,r);
00479   }
00480   SetExpr
00481   operator |(const SetExpr& l, const SetExpr& r) {
00482     return SetExpr(l,SetExpr::NT_UNION,r);
00483   }
00484   SetExpr
00485   operator +(const SetExpr& l, const SetExpr& r) {
00486     return SetExpr(l,SetExpr::NT_DUNION,r);
00487   }
00488   SetExpr
00489   operator -(const SetExpr& e) {
00490     return SetExpr(e,SetExpr::NT_CMPL);
00491   }
00492   SetExpr
00493   operator -(const SetExpr& l, const SetExpr& r) {
00494     return SetExpr(l,SetExpr::NT_INTER,-r);
00495   }
00496   SetExpr
00497   singleton(const LinExpr& e) {
00498     return SetExpr(e);
00499   }
00500 
00501   SetExpr
00502   inter(const SetVarArgs& x) {
00503     if (x.size() == 0)
00504       return SetExpr(IntSet(Set::Limits::min,Set::Limits::max));
00505     SetExpr r(x[0]);
00506     for (int i=1; i<x.size(); i++)
00507       r = (r & x[i]);
00508     return r;
00509   }
00510   SetExpr
00511   setunion(const SetVarArgs& x) {
00512     if (x.size() == 0)
00513       return SetExpr(IntSet::empty);
00514     SetExpr r(x[0]);
00515     for (int i=1; i<x.size(); i++)
00516       r = (r | x[i]);
00517     return r;    
00518   }
00519   SetExpr
00520   setdunion(const SetVarArgs& x) {
00521     if (x.size() == 0)
00522       return SetExpr(IntSet::empty);
00523     SetExpr r(x[0]);
00524     for (int i=1; i<x.size(); i++)
00525       r = (r + x[i]);
00526     return r;    
00527   }
00528 
00529   namespace MiniModel {
00531     class GECODE_MINIMODEL_EXPORT SetNonLinExpr : public NonLinExpr {
00532     public:
00534       enum SetNonLinExprType {
00535         SNLE_CARD, 
00536         SNLE_MIN,  
00537         SNLE_MAX   
00538       } t;
00540       SetExpr e;
00542       SetNonLinExpr(const SetExpr& e0, SetNonLinExprType t0)
00543         : t(t0), e(e0) {}
00545       virtual IntVar post(Home home, IntVar* ret, IntConLevel) const {
00546         IntVar m = result(home,ret);
00547         switch (t) {
00548         case SNLE_CARD:
00549           cardinality(home, e.post(home), m);
00550           break;
00551         case SNLE_MIN:
00552           min(home, e.post(home), m);
00553           break;
00554         case SNLE_MAX:
00555           max(home, e.post(home), m);
00556           break;
00557         default:
00558           GECODE_NEVER;
00559           break;
00560         }
00561         return m;
00562       }
00563       virtual void post(Home home, IntRelType irt, int c,
00564                         IntConLevel icl) const {
00565         if (t==SNLE_CARD && irt!=IRT_NQ) {
00566           switch (irt) {
00567           case IRT_LQ:
00568             cardinality(home, e.post(home), 
00569                         0U, 
00570                         static_cast<unsigned int>(c));
00571             break;
00572           case IRT_LE:
00573             cardinality(home, e.post(home), 
00574                         0U, 
00575                         static_cast<unsigned int>(c-1));
00576             break;
00577           case IRT_GQ:
00578             cardinality(home, e.post(home), 
00579                         static_cast<unsigned int>(c), 
00580                         Set::Limits::card);
00581             break;
00582           case IRT_GR:
00583             cardinality(home, e.post(home), 
00584                         static_cast<unsigned int>(c+1), 
00585                         Set::Limits::card);
00586             break;
00587           case IRT_EQ:
00588             cardinality(home, e.post(home), 
00589                         static_cast<unsigned int>(c),
00590                         static_cast<unsigned int>(c));
00591             break;
00592           default:
00593             GECODE_NEVER;
00594           }
00595         } else if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) {
00596           c = (irt==IRT_GQ ? c : c+1);
00597           dom(home, e.post(home), SRT_SUB, c, Set::Limits::max);
00598         } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) {
00599           c = (irt==IRT_LQ ? c : c-1);
00600           dom(home, e.post(home), SRT_SUB, Set::Limits::min, c);
00601         } else {
00602           rel(home, post(home,NULL,icl), irt, c);
00603         }
00604       }
00605       virtual void post(Home home, IntRelType irt, int c,
00606                         BoolVar b, IntConLevel icl) const {
00607         if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) {
00608           c = (irt==IRT_GQ ? c : c+1);
00609           dom(home, e.post(home), SRT_SUB, c, Set::Limits::max, b);
00610         } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) {
00611           c = (irt==IRT_LQ ? c : c-1);
00612           dom(home, e.post(home), SRT_SUB, Set::Limits::min, c, b);
00613         } else {
00614           rel(home, post(home,NULL,icl), irt, c, b);
00615         }
00616       }
00617     };
00618   }
00619 
00620   LinExpr
00621   cardinality(const SetExpr& e) {
00622     return LinExpr(new MiniModel::SetNonLinExpr(e,
00623       MiniModel::SetNonLinExpr::SNLE_CARD));
00624   }
00625   LinExpr
00626   min(const SetExpr& e) {
00627     return LinExpr(new MiniModel::SetNonLinExpr(e,
00628       MiniModel::SetNonLinExpr::SNLE_MIN));
00629   }
00630   LinExpr
00631   max(const SetExpr& e) {
00632     return LinExpr(new MiniModel::SetNonLinExpr(e,
00633       MiniModel::SetNonLinExpr::SNLE_MAX));
00634   }
00635 
00636   /*
00637    * Posting set expressions
00638    *
00639    */
00640   SetVar
00641   expr(Home home, const SetExpr& e) {
00642     if (!home.failed())
00643       return e.post(home);
00644     SetVar x(home,IntSet::empty,IntSet::empty);
00645     return x;
00646   }
00647 
00648 }
00649 
00650 #endif
00651 
00652 // STATISTICS: minimodel-any