Generated on Tue Jul 27 2010 21:59:17 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: 2010-07-16 10:51:05 +0200 (Fri, 16 Jul 2010) $ by $Author: tack $
00013  *     $Revision: 11208 $
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   const BoolExpr&
00062   BoolExpr::operator =(const BoolExpr& e) {
00063     if (this != &e) {
00064       if (n->decrement())
00065         delete n;
00066       n = e.n;
00067       n->use++;
00068     }
00069     return *this;
00070   }
00071 
00072   BoolExpr::~BoolExpr(void) {
00073     if (n->decrement())
00074       delete n;
00075   }
00076 
00077   /*
00078    * Operations for negation normalform
00079    *
00080    */
00081   forceinline void
00082   BoolExpr::NNF::operator delete(void*) {}
00083 
00084   forceinline void
00085   BoolExpr::NNF::operator delete(void*, Region&) {}
00086 
00087   forceinline void*
00088   BoolExpr::NNF::operator new(size_t s, Region& r) {
00089     return r.ralloc(s);
00090   }
00091 
00092   BoolVar
00093   BoolExpr::NNF::expr(Home home, IntConLevel icl) const {
00094     if ((t == NT_VAR) && !u.a.neg)
00095       return u.a.x->x;
00096     BoolVar b(home,0,1);
00097     switch (t) {
00098     case NT_VAR:
00099       assert(u.a.neg);
00100       Gecode::rel(home, u.a.x->x, IRT_NQ, b);
00101       break;
00102     case NT_RLIN:
00103       u.a.x->rl.post(home, b, !u.a.neg, icl);
00104       break;
00105 #ifdef GECODE_HAS_SET_VARS
00106     case NT_RSET:
00107       u.a.x->rs.post(home, b, !u.a.neg);
00108       break;
00109 #endif
00110     case NT_AND:
00111       {
00112         BoolVarArgs bp(p), bn(n);
00113         int ip=0, in=0;
00114         post(home, NT_AND, bp, bn, ip, in, icl);
00115         clause(home, BOT_AND, bp, bn, b);
00116       }
00117       break;
00118     case NT_OR:
00119       {
00120         BoolVarArgs bp(p), bn(n);
00121         int ip=0, in=0;
00122         post(home, NT_OR, bp, bn, ip, in, icl);
00123         clause(home, BOT_OR, bp, bn, b);
00124       }
00125       break;
00126     case NT_EQV:
00127       {
00128         bool n = false;
00129         BoolVar l;
00130         if (u.b.l->t == NT_VAR) {
00131           l = u.b.l->u.a.x->x;
00132           if (u.b.l->u.a.neg) n = !n;
00133         } else {
00134           l = u.b.l->expr(home,icl);
00135         }
00136         BoolVar r;
00137         if (u.b.r->t == NT_VAR) {
00138           r = u.b.r->u.a.x->x;
00139           if (u.b.r->u.a.neg) n = !n;
00140         } else {
00141           r = u.b.r->expr(home,icl);
00142         }
00143         Gecode::rel(home, l, n ? BOT_XOR : BOT_EQV, r, b, icl);
00144       }
00145       break;
00146     default:
00147       GECODE_NEVER;
00148     }
00149     return b;
00150   }
00151 
00152   void
00153   BoolExpr::NNF::post(Home home, NodeType t,
00154                       BoolVarArgs& bp, BoolVarArgs& bn,
00155                       int& ip, int& in,
00156                       IntConLevel icl) const {
00157     if (this->t != t) {
00158       switch (this->t) {
00159       case NT_VAR:
00160         if (u.a.neg) {
00161           bn[in++]=u.a.x->x;
00162         } else {
00163           bp[ip++]=u.a.x->x;
00164         }
00165         break;
00166       case NT_RLIN:
00167         {
00168           BoolVar b(home,0,1);
00169           u.a.x->rl.post(home, b, !u.a.neg, icl);
00170           bp[ip++]=b;
00171         }
00172         break;
00173 #ifdef GECODE_HAS_SET_VARS
00174       case NT_RSET:
00175         {
00176           BoolVar b(home,0,1);
00177           u.a.x->rs.post(home, b, !u.a.neg);
00178           bp[ip++]=b;
00179         }
00180         break;
00181 #endif
00182       default:
00183         bp[ip++] = expr(home, icl);
00184         break;
00185       }
00186     } else {
00187       u.b.l->post(home, t, bp, bn, ip, in, icl);
00188       u.b.r->post(home, t, bp, bn, ip, in, icl);
00189     }
00190   }
00191 
00192   void
00193   BoolExpr::NNF::rel(Home home, IntConLevel icl) const {
00194     switch (t) {
00195     case NT_VAR:
00196       Gecode::rel(home, u.a.x->x, IRT_EQ, u.a.neg ? 0 : 1);
00197       break;
00198     case NT_RLIN:
00199       u.a.x->rl.post(home, !u.a.neg, icl);
00200       break;
00201 #ifdef GECODE_HAS_SET_VARS
00202     case NT_RSET:
00203       u.a.x->rs.post(home, !u.a.neg);
00204       break;
00205 #endif
00206     case NT_AND:
00207       u.b.l->rel(home, icl);
00208       u.b.r->rel(home, icl);
00209       break;
00210     case NT_OR:
00211       {
00212         BoolVarArgs bp(p), bn(n);
00213         int ip=0, in=0;
00214         post(home, NT_OR, bp, bn, ip, in, icl);
00215         clause(home, BOT_OR, bp, bn, 1);
00216       }
00217       break;
00218     case NT_EQV:
00219       if (u.b.l->t==NT_VAR && u.b.r->t==NT_RLIN) {
00220         u.b.r->u.a.x->rl.post(home, u.b.l->u.a.x->x,
00221                               u.b.l->u.a.neg==u.b.r->u.a.neg, icl);
00222       } else if (u.b.r->t==NT_VAR && u.b.l->t==NT_RLIN) {
00223         u.b.l->u.a.x->rl.post(home, u.b.r->u.a.x->x,
00224                               u.b.l->u.a.neg==u.b.r->u.a.neg, icl);
00225       } else if (u.b.l->t==NT_RLIN) {
00226         u.b.l->u.a.x->rl.post(home, u.b.r->expr(home,icl),
00227                               !u.b.l->u.a.neg,icl);
00228       } else if (u.b.r->t==NT_RLIN) {
00229         u.b.r->u.a.x->rl.post(home, u.b.l->expr(home,icl),
00230                               !u.b.r->u.a.neg,icl);
00231 #ifdef GECODE_HAS_SET_VARS
00232       } else if (u.b.l->t==NT_VAR && u.b.r->t==NT_RSET) {
00233         u.b.r->u.a.x->rs.post(home, u.b.l->u.a.x->x,
00234                               u.b.l->u.a.neg==u.b.r->u.a.neg);
00235       } else if (u.b.r->t==NT_VAR && u.b.l->t==NT_RSET) {
00236         u.b.l->u.a.x->rs.post(home, u.b.r->u.a.x->x,
00237                               u.b.l->u.a.neg==u.b.r->u.a.neg);
00238       } else if (u.b.l->t==NT_RSET) {
00239         u.b.l->u.a.x->rs.post(home, u.b.r->expr(home,icl),
00240                               !u.b.l->u.a.neg);
00241       } else if (u.b.r->t==NT_RSET) {
00242         u.b.r->u.a.x->rs.post(home, u.b.l->expr(home,icl),
00243                               !u.b.r->u.a.neg);
00244 #endif
00245       } else {
00246         Gecode::rel(home, expr(home, icl), IRT_EQ, 1);
00247       }
00248       break;
00249     default:
00250       GECODE_NEVER;
00251     }
00252   }
00253 
00254   BoolExpr::NNF*
00255   BoolExpr::NNF::nnf(Region& r, Node* n, bool neg) {
00256     switch (n->t) {
00257     case NT_VAR: case NT_RLIN:
00258 #ifdef GECODE_HAS_SET_VARS
00259     case NT_RSET:
00260 #endif
00261       {
00262         NNF* x = new (r) NNF;
00263         x->t = n->t; x->u.a.neg = neg; x->u.a.x = n;
00264         if (neg) {
00265           x->p = 0; x->n = 1;
00266         } else {
00267           x->p = 1; x->n = 0;
00268         }
00269         return x;
00270       }
00271     case NT_NOT:
00272       return nnf(r,n->l,!neg);
00273     case NT_AND: case NT_OR:
00274       {
00275         NodeType t = ((n->t == NT_AND) == neg) ? NT_OR : NT_AND;
00276         NNF* x = new (r) NNF;
00277         x->t = t;
00278         x->u.b.l = nnf(r,n->l,neg);
00279         x->u.b.r = nnf(r,n->r,neg);
00280         int p_l, n_l;
00281         if ((x->u.b.l->t == t) || (x->u.b.l->t == NT_VAR)) {
00282           p_l=x->u.b.l->p; n_l=x->u.b.l->n;
00283         } else {
00284           p_l=1; n_l=0;
00285         }
00286         int p_r, n_r;
00287         if ((x->u.b.r->t == t) || (x->u.b.r->t == NT_VAR)) {
00288           p_r=x->u.b.r->p; n_r=x->u.b.r->n;
00289         } else {
00290           p_r=1; n_r=0;
00291         }
00292         x->p = p_l+p_r;
00293         x->n = n_l+n_r;
00294         return x;
00295       }
00296     case NT_EQV:
00297       {
00298         NNF* x = new (r) NNF;
00299         x->t = NT_EQV;
00300         x->u.b.l = nnf(r,n->l,neg);
00301         x->u.b.r = nnf(r,n->r,false);
00302         x->p = 2; x->n = 0;
00303         return x;
00304       }
00305     default:
00306       GECODE_NEVER;
00307     }
00308     GECODE_NEVER;
00309     return NULL;
00310   }
00311 
00312 
00313   BoolExpr
00314   operator &&(const BoolExpr& l, const BoolExpr& r) {
00315     return BoolExpr(l,BoolExpr::NT_AND,r);
00316   }
00317   BoolExpr
00318   operator ||(const BoolExpr& l, const BoolExpr& r) {
00319     return BoolExpr(l,BoolExpr::NT_OR,r);
00320   }
00321   BoolExpr
00322   operator ^(const BoolExpr& l, const BoolExpr& r) {
00323     return BoolExpr(BoolExpr(l,BoolExpr::NT_EQV,r),BoolExpr::NT_NOT);
00324   }
00325 
00326   BoolExpr
00327   operator !(const BoolExpr& e) {
00328     return BoolExpr(e,BoolExpr::NT_NOT);
00329   }
00330 
00331   BoolExpr
00332   operator !=(const BoolExpr& l, const BoolExpr& r) {
00333     return !BoolExpr(l, BoolExpr::NT_EQV, r);
00334   }
00335   BoolExpr
00336   operator ==(const BoolExpr& l, const BoolExpr& r) {
00337     return BoolExpr(l, BoolExpr::NT_EQV, r);
00338   }
00339   BoolExpr
00340   operator >>(const BoolExpr& l, const BoolExpr& r) {
00341     return BoolExpr(BoolExpr(l,BoolExpr::NT_NOT),
00342                     BoolExpr::NT_OR,r);
00343   }
00344   BoolExpr
00345   operator <<(const BoolExpr& l, const BoolExpr& r) {
00346     return BoolExpr(BoolExpr(r,BoolExpr::NT_NOT),
00347                     BoolExpr::NT_OR,l);
00348   }
00349 
00350   /*
00351    * Posting Boolean expressions and relations
00352    *
00353    */
00354   BoolVar
00355   expr(Home home, const BoolExpr& e, IntConLevel icl) {
00356     if (!home.failed())
00357       return e.expr(home,icl);
00358     BoolVar x(home,0,1);
00359     return x;
00360   }
00361 
00362   void
00363   rel(Home home, const BoolExpr& e, IntConLevel icl) {
00364     if (home.failed()) return;
00365     e.rel(home,icl);
00366   }
00367 
00368 }
00369 
00370 // STATISTICS: minimodel-any