Generated on Fri May 13 2011 22:41:21 for Gecode by doxygen 1.7.1

bool-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, 2004
00009  *     Christian Schulte, 2004
00010  *
00011  *  Last modified:
00012  *     $Date: 2011-01-21 16:01:14 +0100 (Fri, 21 Jan 2011) $ by $Author: schulte $
00013  *     $Revision: 11553 $
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 namespace Gecode {
00043 
00044   /*
00045    * Operations for nodes
00046    *
00047    */
00048   bool
00049   BoolExpr::Node::decrement(void) {
00050     if (--use == 0) {
00051       if ((l != NULL) && l->decrement())
00052         delete l;
00053       if ((r != NULL) && r->decrement())
00054         delete r;
00055       return true;
00056     }
00057     return false;
00058   }
00059 
00060 
00061   BoolExpr::BoolExpr(const BoolVar& x) : n(new Node) {
00062     n->same = 1;
00063     n->t    = NT_VAR;
00064     n->l    = NULL;
00065     n->r    = NULL;
00066     n->x    = x;
00067     n->m    = NULL;
00068   }
00069 
00070   BoolExpr::BoolExpr(const BoolExpr& l, NodeType t, const BoolExpr& r)
00071     : n(new Node) {
00072     int ls = ((l.n->t == t) || (l.n->t == NT_VAR)) ? l.n->same : 1;
00073     int rs = ((r.n->t == t) || (r.n->t == NT_VAR)) ? r.n->same : 1;
00074     n->same = ls+rs;
00075     n->t    = t;
00076     n->l    = l.n;
00077     n->l->use++;
00078     n->r    = r.n;
00079     n->r->use++;
00080     n->m    = NULL;
00081   }
00082 
00083   BoolExpr::BoolExpr(const BoolExpr& l, NodeType t) {
00084     (void) t;
00085     assert(t == NT_NOT);
00086     if (l.n->t == NT_NOT) {
00087       n = l.n->l;
00088       n->use++;
00089     } else {
00090       n = new Node;
00091       n->same = 1;
00092       n->t    = NT_NOT;
00093       n->l    = l.n;
00094       n->l->use++;
00095       n->r    = NULL;
00096       n->m    = NULL;
00097     }
00098   }
00099 
00100   BoolExpr::BoolExpr(const LinRel& rl)
00101     : n(new Node) {
00102     n->same = 1;
00103     n->t    = NT_RLIN;
00104     n->l    = NULL;
00105     n->r    = NULL;
00106     n->rl   = rl;
00107     n->m    = NULL;
00108   }
00109 
00110 #ifdef GECODE_HAS_SET_VARS
00111   BoolExpr::BoolExpr(const SetRel& rs)
00112     : n(new Node) {
00113     n->same = 1;
00114     n->t    = NT_RSET;
00115     n->l    = NULL;
00116     n->r    = NULL;
00117     n->rs   = rs;
00118     n->m    = NULL;
00119   }
00120 
00121   BoolExpr::BoolExpr(const SetCmpRel& rs)
00122     : n(new Node) {
00123     n->same = 1;
00124     n->t    = NT_RSET;
00125     n->l    = NULL;
00126     n->r    = NULL;
00127     n->rs   = rs;
00128     n->m    = NULL;
00129   }
00130 #endif
00131 
00132   BoolExpr::BoolExpr(BoolExpr::MiscExpr* m)
00133     : n(new Node) {
00134     n->same = 1;
00135     n->t    = NT_MISC;
00136     n->l    = NULL;
00137     n->r    = NULL;
00138     n->m    = m;
00139   }
00140 
00141   const BoolExpr&
00142   BoolExpr::operator =(const BoolExpr& e) {
00143     if (this != &e) {
00144       if (n->decrement())
00145         delete n;
00146       n = e.n;
00147       n->use++;
00148     }
00149     return *this;
00150   }
00151 
00152   BoolExpr::MiscExpr::~MiscExpr(void) {}
00153 
00154   BoolExpr::~BoolExpr(void) {
00155     if (n->decrement())
00156       delete n;
00157   }
00158 
00159   /*
00160    * Operations for negation normalform
00161    *
00162    */
00163   forceinline void
00164   BoolExpr::NNF::operator delete(void*) {}
00165 
00166   forceinline void
00167   BoolExpr::NNF::operator delete(void*, Region&) {}
00168 
00169   forceinline void*
00170   BoolExpr::NNF::operator new(size_t s, Region& r) {
00171     return r.ralloc(s);
00172   }
00173 
00174   BoolVar
00175   BoolExpr::NNF::expr(Home home, IntConLevel icl) const {
00176     if ((t == NT_VAR) && !u.a.neg)
00177       return u.a.x->x;
00178     BoolVar b(home,0,1);
00179     switch (t) {
00180     case NT_VAR:
00181       assert(u.a.neg);
00182       Gecode::rel(home, u.a.x->x, IRT_NQ, b);
00183       break;
00184     case NT_RLIN:
00185       u.a.x->rl.post(home, b, !u.a.neg, icl);
00186       break;
00187 #ifdef GECODE_HAS_SET_VARS
00188     case NT_RSET:
00189       u.a.x->rs.post(home, b, !u.a.neg);
00190       break;
00191 #endif
00192     case NT_MISC:
00193       u.a.x->m->post(home, b, !u.a.neg, icl);
00194       break;
00195     case NT_AND:
00196       {
00197         BoolVarArgs bp(p), bn(n);
00198         int ip=0, in=0;
00199         post(home, NT_AND, bp, bn, ip, in, icl);
00200         clause(home, BOT_AND, bp, bn, b);
00201       }
00202       break;
00203     case NT_OR:
00204       {
00205         BoolVarArgs bp(p), bn(n);
00206         int ip=0, in=0;
00207         post(home, NT_OR, bp, bn, ip, in, icl);
00208         clause(home, BOT_OR, bp, bn, b);
00209       }
00210       break;
00211     case NT_EQV:
00212       {
00213         bool n = false;
00214         BoolVar l;
00215         if (u.b.l->t == NT_VAR) {
00216           l = u.b.l->u.a.x->x;
00217           if (u.b.l->u.a.neg) n = !n;
00218         } else {
00219           l = u.b.l->expr(home,icl);
00220         }
00221         BoolVar r;
00222         if (u.b.r->t == NT_VAR) {
00223           r = u.b.r->u.a.x->x;
00224           if (u.b.r->u.a.neg) n = !n;
00225         } else {
00226           r = u.b.r->expr(home,icl);
00227         }
00228         Gecode::rel(home, l, n ? BOT_XOR : BOT_EQV, r, b, icl);
00229       }
00230       break;
00231     default:
00232       GECODE_NEVER;
00233     }
00234     return b;
00235   }
00236 
00237   void
00238   BoolExpr::NNF::post(Home home, NodeType t,
00239                       BoolVarArgs& bp, BoolVarArgs& bn,
00240                       int& ip, int& in,
00241                       IntConLevel icl) const {
00242     if (this->t != t) {
00243       switch (this->t) {
00244       case NT_VAR:
00245         if (u.a.neg) {
00246           bn[in++]=u.a.x->x;
00247         } else {
00248           bp[ip++]=u.a.x->x;
00249         }
00250         break;
00251       case NT_RLIN:
00252         {
00253           BoolVar b(home,0,1);
00254           u.a.x->rl.post(home, b, !u.a.neg, icl);
00255           bp[ip++]=b;
00256         }
00257         break;
00258 #ifdef GECODE_HAS_SET_VARS
00259       case NT_RSET:
00260         {
00261           BoolVar b(home,0,1);
00262           u.a.x->rs.post(home, b, !u.a.neg);
00263           bp[ip++]=b;
00264         }
00265         break;
00266 #endif
00267       case NT_MISC:
00268         {
00269           BoolVar b(home,0,1);
00270           u.a.x->m->post(home, b, !u.a.neg, icl);
00271           bp[ip++]=b;
00272         }
00273         break;      
00274       default:
00275         bp[ip++] = expr(home, icl);
00276         break;
00277       }
00278     } else {
00279       u.b.l->post(home, t, bp, bn, ip, in, icl);
00280       u.b.r->post(home, t, bp, bn, ip, in, icl);
00281     }
00282   }
00283 
00284   void
00285   BoolExpr::NNF::rel(Home home, IntConLevel icl) const {
00286     switch (t) {
00287     case NT_VAR:
00288       Gecode::rel(home, u.a.x->x, IRT_EQ, u.a.neg ? 0 : 1);
00289       break;
00290     case NT_RLIN:
00291       u.a.x->rl.post(home, !u.a.neg, icl);
00292       break;
00293 #ifdef GECODE_HAS_SET_VARS
00294     case NT_RSET:
00295       u.a.x->rs.post(home, !u.a.neg);
00296       break;
00297 #endif
00298     case NT_MISC:
00299       {
00300         BoolVar b(home,!u.a.neg,!u.a.neg);
00301         u.a.x->m->post(home, b, false, icl);
00302       }
00303       break;
00304     case NT_AND:
00305       u.b.l->rel(home, icl);
00306       u.b.r->rel(home, icl);
00307       break;
00308     case NT_OR:
00309       {
00310         BoolVarArgs bp(p), bn(n);
00311         int ip=0, in=0;
00312         post(home, NT_OR, bp, bn, ip, in, icl);
00313         clause(home, BOT_OR, bp, bn, 1);
00314       }
00315       break;
00316     case NT_EQV:
00317       if (u.b.l->t==NT_VAR && u.b.r->t==NT_RLIN) {
00318         u.b.r->u.a.x->rl.post(home, u.b.l->u.a.x->x,
00319                               u.b.l->u.a.neg==u.b.r->u.a.neg, icl);
00320       } else if (u.b.r->t==NT_VAR && u.b.l->t==NT_RLIN) {
00321         u.b.l->u.a.x->rl.post(home, u.b.r->u.a.x->x,
00322                               u.b.l->u.a.neg==u.b.r->u.a.neg, icl);
00323       } else if (u.b.l->t==NT_RLIN) {
00324         u.b.l->u.a.x->rl.post(home, u.b.r->expr(home,icl),
00325                               !u.b.l->u.a.neg,icl);
00326       } else if (u.b.r->t==NT_RLIN) {
00327         u.b.r->u.a.x->rl.post(home, u.b.l->expr(home,icl),
00328                               !u.b.r->u.a.neg,icl);
00329 #ifdef GECODE_HAS_SET_VARS
00330       } else if (u.b.l->t==NT_VAR && u.b.r->t==NT_RSET) {
00331         u.b.r->u.a.x->rs.post(home, u.b.l->u.a.x->x,
00332                               u.b.l->u.a.neg==u.b.r->u.a.neg);
00333       } else if (u.b.r->t==NT_VAR && u.b.l->t==NT_RSET) {
00334         u.b.l->u.a.x->rs.post(home, u.b.r->u.a.x->x,
00335                               u.b.l->u.a.neg==u.b.r->u.a.neg);
00336       } else if (u.b.l->t==NT_RSET) {
00337         u.b.l->u.a.x->rs.post(home, u.b.r->expr(home,icl),
00338                               !u.b.l->u.a.neg);
00339       } else if (u.b.r->t==NT_RSET) {
00340         u.b.r->u.a.x->rs.post(home, u.b.l->expr(home,icl),
00341                               !u.b.r->u.a.neg);
00342 #endif
00343       } else {
00344         Gecode::rel(home, expr(home, icl), IRT_EQ, 1);
00345       }
00346       break;
00347     default:
00348       GECODE_NEVER;
00349     }
00350   }
00351 
00352   BoolExpr::NNF*
00353   BoolExpr::NNF::nnf(Region& r, Node* n, bool neg) {
00354     switch (n->t) {
00355     case NT_VAR: case NT_RLIN: case NT_MISC:
00356 #ifdef GECODE_HAS_SET_VARS
00357     case NT_RSET:
00358 #endif
00359       {
00360         NNF* x = new (r) NNF;
00361         x->t = n->t; x->u.a.neg = neg; x->u.a.x = n;
00362         if (neg) {
00363           x->p = 0; x->n = 1;
00364         } else {
00365           x->p = 1; x->n = 0;
00366         }
00367         return x;
00368       }
00369     case NT_NOT:
00370       return nnf(r,n->l,!neg);
00371     case NT_AND: case NT_OR:
00372       {
00373         NodeType t = ((n->t == NT_AND) == neg) ? NT_OR : NT_AND;
00374         NNF* x = new (r) NNF;
00375         x->t = t;
00376         x->u.b.l = nnf(r,n->l,neg);
00377         x->u.b.r = nnf(r,n->r,neg);
00378         int p_l, n_l;
00379         if ((x->u.b.l->t == t) || (x->u.b.l->t == NT_VAR)) {
00380           p_l=x->u.b.l->p; n_l=x->u.b.l->n;
00381         } else {
00382           p_l=1; n_l=0;
00383         }
00384         int p_r, n_r;
00385         if ((x->u.b.r->t == t) || (x->u.b.r->t == NT_VAR)) {
00386           p_r=x->u.b.r->p; n_r=x->u.b.r->n;
00387         } else {
00388           p_r=1; n_r=0;
00389         }
00390         x->p = p_l+p_r;
00391         x->n = n_l+n_r;
00392         return x;
00393       }
00394     case NT_EQV:
00395       {
00396         NNF* x = new (r) NNF;
00397         x->t = NT_EQV;
00398         x->u.b.l = nnf(r,n->l,neg);
00399         x->u.b.r = nnf(r,n->r,false);
00400         x->p = 2; x->n = 0;
00401         return x;
00402       }
00403     default:
00404       GECODE_NEVER;
00405     }
00406     GECODE_NEVER;
00407     return NULL;
00408   }
00409 
00410 
00411   BoolExpr
00412   operator &&(const BoolExpr& l, const BoolExpr& r) {
00413     return BoolExpr(l,BoolExpr::NT_AND,r);
00414   }
00415   BoolExpr
00416   operator ||(const BoolExpr& l, const BoolExpr& r) {
00417     return BoolExpr(l,BoolExpr::NT_OR,r);
00418   }
00419   BoolExpr
00420   operator ^(const BoolExpr& l, const BoolExpr& r) {
00421     return BoolExpr(BoolExpr(l,BoolExpr::NT_EQV,r),BoolExpr::NT_NOT);
00422   }
00423 
00424   BoolExpr
00425   operator !(const BoolExpr& e) {
00426     return BoolExpr(e,BoolExpr::NT_NOT);
00427   }
00428 
00429   BoolExpr
00430   operator !=(const BoolExpr& l, const BoolExpr& r) {
00431     return !BoolExpr(l, BoolExpr::NT_EQV, r);
00432   }
00433   BoolExpr
00434   operator ==(const BoolExpr& l, const BoolExpr& r) {
00435     return BoolExpr(l, BoolExpr::NT_EQV, r);
00436   }
00437   BoolExpr
00438   operator >>(const BoolExpr& l, const BoolExpr& r) {
00439     return BoolExpr(BoolExpr(l,BoolExpr::NT_NOT),
00440                     BoolExpr::NT_OR,r);
00441   }
00442   BoolExpr
00443   operator <<(const BoolExpr& l, const BoolExpr& r) {
00444     return BoolExpr(BoolExpr(r,BoolExpr::NT_NOT),
00445                     BoolExpr::NT_OR,l);
00446   }
00447   /*
00448    * Posting Boolean expressions and relations
00449    *
00450    */
00451   BoolVar
00452   expr(Home home, const BoolExpr& e, IntConLevel icl) {
00453     if (!home.failed())
00454       return e.expr(home,icl);
00455     BoolVar x(home,0,1);
00456     return x;
00457   }
00458 
00459   void
00460   rel(Home home, const BoolExpr& e, IntConLevel icl) {
00461     if (home.failed()) return;
00462     e.rel(home,icl);
00463   }
00464 
00465   /*
00466    * Boolean element constraints
00467    *
00468    */
00469   
00471   class BElementExpr : public BoolExpr::MiscExpr {
00472   public:
00474     BoolExpr* a;
00476     int n;
00478     LinExpr idx;
00480     BElementExpr(int size);
00482     virtual ~BElementExpr(void);
00484     virtual void post(Space& home, BoolVar b, bool neg, IntConLevel icl);
00485   };
00486 
00487   BElementExpr::BElementExpr(int size)
00488     : a(heap.alloc<BoolExpr>(size)), n(size) {}
00489 
00490   BElementExpr::~BElementExpr(void) {
00491     heap.free<BoolExpr>(a,n);
00492   }
00493   
00494   void
00495   BElementExpr::post(Space& home, BoolVar b, bool pos, IntConLevel icl) {
00496     IntVar z = idx.post(home, icl);
00497     if (z.assigned() && z.val() >= 0 && z.val() < n) {
00498       BoolExpr be = pos ? (a[z.val()] == b) : (a[z.val()] == !b);
00499       be.rel(home,icl);
00500     } else {
00501       BoolVarArgs x(n);
00502       for (int i=n; i--;)
00503         x[i] = a[i].expr(home,icl);
00504       BoolVar res = pos ? b : (!b).expr(home,icl);
00505       element(home, x, z, res, icl);
00506     }
00507   }
00508 
00509   BoolExpr
00510   element(const BoolVarArgs& b, const LinExpr& idx) {
00511     BElementExpr* be = new BElementExpr(b.size());
00512     for (int i=b.size(); i--;)
00513       new (&be->a[i]) BoolExpr(b[i]);
00514     be->idx = idx;
00515     return BoolExpr(be);
00516   }
00517 
00518 }
00519 
00520 // STATISTICS: minimodel-any