Generated on Mon May 10 06:46:43 2010 for Gecode by doxygen 1.6.3

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-02-03 11:13:34 +0100 (Wed, 03 Feb 2010) $ by $Author: schulte $
00013  *     $Revision: 10262 $
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::post(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       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     case NT_AND:
00106       {
00107         BoolVarArgs bp(p), bn(n);
00108         int ip=0, in=0;
00109         post(home, NT_AND, bp, bn, ip, in, icl);
00110         clause(home, BOT_AND, bp, bn, b);
00111       }
00112       break;
00113     case NT_OR:
00114       {
00115         BoolVarArgs bp(p), bn(n);
00116         int ip=0, in=0;
00117         post(home, NT_OR, bp, bn, ip, in, icl);
00118         clause(home, BOT_OR, bp, bn, b);
00119       }
00120       break;
00121     case NT_EQV:
00122       {
00123         bool n = false;
00124         BoolVar l;
00125         if (u.b.l->t == NT_VAR) {
00126           l = u.b.l->u.a.x->x;
00127           if (u.b.l->u.a.neg) n = !n;
00128         } else {
00129           l = u.b.l->post(home,icl);
00130         }
00131         BoolVar r;
00132         if (u.b.r->t == NT_VAR) {
00133           r = u.b.r->u.a.x->x;
00134           if (u.b.r->u.a.neg) n = !n;
00135         } else {
00136           r = u.b.r->post(home,icl);
00137         }
00138         rel(home, l, n ? BOT_XOR : BOT_EQV, r, b, icl);
00139       }
00140       break;
00141     default:
00142       GECODE_NEVER;
00143     }
00144     return b;
00145   }
00146 
00147   void
00148   BoolExpr::NNF::post(Home home, NodeType t,
00149                       BoolVarArgs& bp, BoolVarArgs& bn,
00150                       int& ip, int& in,
00151                       IntConLevel icl) const {
00152     if (this->t != t) {
00153       switch (this->t) {
00154       case NT_VAR:
00155         if (u.a.neg) {
00156           bn[in++]=u.a.x->x;
00157         } else {
00158           bp[ip++]=u.a.x->x;
00159         }
00160         break;
00161       case NT_RLIN:
00162         {
00163           BoolVar b(home,0,1);
00164           u.a.x->rl.post(home, b, !u.a.neg, icl);
00165           bp[ip++]=b;
00166         }
00167         break;
00168       default:
00169         bp[ip++] = post(home, icl);
00170         break;
00171       }
00172     } else {
00173       u.b.l->post(home, t, bp, bn, ip, in, icl);
00174       u.b.r->post(home, t, bp, bn, ip, in, icl);
00175     }
00176   }
00177 
00178   void
00179   BoolExpr::NNF::post(Home home, bool b, IntConLevel icl) const {
00180     if (b) {
00181       switch (t) {
00182       case NT_VAR:
00183         rel(home, u.a.x->x, IRT_EQ, u.a.neg ? 0 : 1);
00184         break;
00185       case NT_RLIN:
00186         u.a.x->rl.post(home, !u.a.neg, icl);
00187         break;
00188       case NT_AND:
00189         u.b.l->post(home, true, icl);
00190         u.b.r->post(home, true, icl);
00191         break;
00192       case NT_OR:
00193         {
00194           BoolVarArgs bp(p), bn(n);
00195           int ip=0, in=0;
00196           post(home, NT_OR, bp, bn, ip, in, icl);
00197           clause(home, BOT_OR, bp, bn, 1);
00198         }
00199         break;
00200       case NT_EQV:
00201         rel(home, post(home, icl), IRT_EQ, 1);
00202         break;
00203       default:
00204         GECODE_NEVER;
00205       }
00206     } else {
00207       switch (t) {
00208       case NT_VAR:
00209         rel(home, u.a.x->x, IRT_EQ, u.a.neg ? 1 : 0);
00210         break;
00211       case NT_RLIN:
00212         u.a.x->rl.post(home, u.a.neg, icl);
00213         break;
00214       case NT_AND:
00215         {
00216           BoolVarArgs bp(p), bn(n);
00217           int ip=0, in=0;
00218           post(home, NT_AND, bp, bn, ip, in, icl);
00219           clause(home, BOT_AND, bp, bn, 0);
00220         }
00221         break;
00222       case NT_OR:
00223         u.b.l->post(home, false, icl);
00224         u.b.r->post(home, false, icl);
00225         break;
00226       case NT_EQV:
00227         rel(home, post(home, icl), IRT_EQ, 0);
00228         break;
00229       default:
00230         GECODE_NEVER;
00231       }
00232     }
00233   }
00234 
00235   BoolExpr::NNF*
00236   BoolExpr::NNF::nnf(Region& r, Node* n, bool neg) {
00237     switch (n->t) {
00238     case NT_VAR: case NT_RLIN:
00239       {
00240         NNF* x = new (r) NNF;
00241         x->t = n->t; x->u.a.neg = neg; x->u.a.x = n;
00242         if (neg) {
00243           x->p = 0; x->n = 1;
00244         } else {
00245           x->p = 1; x->n = 0;
00246         }
00247         return x;
00248       }
00249     case NT_NOT:
00250       return nnf(r,n->l,!neg);
00251     case NT_AND: case NT_OR:
00252       {
00253         NodeType t = ((n->t == NT_AND) == neg) ? NT_OR : NT_AND;
00254         NNF* x = new (r) NNF;
00255         x->t = t;
00256         x->u.b.l = nnf(r,n->l,neg);
00257         x->u.b.r = nnf(r,n->r,neg);
00258         unsigned int p_l, n_l;
00259         if ((x->u.b.l->t == t) || (x->u.b.l->t == NT_VAR)) {
00260           p_l=x->u.b.l->p; n_l=x->u.b.l->n;
00261         } else {
00262           p_l=1; n_l=0;
00263         }
00264         unsigned int p_r, n_r;
00265         if ((x->u.b.r->t == t) || (x->u.b.r->t == NT_VAR)) {
00266           p_r=x->u.b.r->p; n_r=x->u.b.r->n;
00267         } else {
00268           p_r=1; n_r=0;
00269         }
00270         x->p = p_l+p_r;
00271         x->n = n_l+n_r;
00272         return x;
00273       }
00274     case NT_EQV:
00275       {
00276         NNF* x = new (r) NNF;
00277         x->t = NT_EQV;
00278         x->u.b.l = nnf(r,n->l,neg);
00279         x->u.b.r = nnf(r,n->r,false);
00280         x->p = 2; x->n = 0;
00281         return x;
00282       }
00283     default:
00284       GECODE_NEVER;
00285     }
00286     GECODE_NEVER;
00287     return NULL;
00288   }
00289 
00290 
00291   BoolExpr
00292   operator &&(const BoolExpr& l, const BoolExpr& r) {
00293     return BoolExpr(l,BoolExpr::NT_AND,r);
00294   }
00295   BoolExpr
00296   operator ||(const BoolExpr& l, const BoolExpr& r) {
00297     return BoolExpr(l,BoolExpr::NT_OR,r);
00298   }
00299   BoolExpr
00300   operator ^(const BoolExpr& l, const BoolExpr& r) {
00301     return BoolExpr(BoolExpr(l,BoolExpr::NT_EQV,r),BoolExpr::NT_NOT);
00302   }
00303 
00304   BoolExpr
00305   operator ~(const LinRel& rl) {
00306     return BoolExpr(rl);
00307   }
00308   BoolExpr
00309   operator !(const BoolExpr& e) {
00310     return BoolExpr(e,BoolExpr::NT_NOT);
00311   }
00312 
00313   BoolExpr
00314   eqv(const BoolExpr& l, const BoolExpr& r) {
00315     return BoolExpr(l, BoolExpr::NT_EQV, r);
00316   }
00317   BoolExpr
00318   imp(const BoolExpr& l, const BoolExpr& r) {
00319     return BoolExpr(BoolExpr(l,BoolExpr::NT_NOT),
00320                     BoolExpr::NT_OR,r);
00321   }
00322 
00323   /*
00324    * Posting Boolean expressions
00325    *
00326    */
00327   BoolVar
00328   post(Home home, const BoolExpr& e, IntConLevel icl) {
00329     if (!home.failed())
00330       return e.post(home,icl);
00331     BoolVar x(home,0,1);
00332     return x;
00333   }
00334 
00335 }
00336 
00337 // STATISTICS: minimodel-any