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