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