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