00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038 #include <gecode/minimodel.hh>
00039
00040 namespace Gecode {
00041
00043 class BoolExpr::Node {
00044 public:
00046 unsigned int use;
00048 int same;
00050 NodeType t;
00052 Node *l, *r;
00054 BoolVar x;
00056 LinIntRel rl;
00057 #ifdef GECODE_HAS_FLOAT_VARS
00058
00059 LinFloatRel rfl;
00060 #endif
00061 #ifdef GECODE_HAS_SET_VARS
00062
00063 SetRel rs;
00064 #endif
00065
00066 Misc* m;
00067
00069 Node(void);
00071 ~Node(void);
00073 GECODE_MINIMODEL_EXPORT
00074 bool decrement(void);
00076 static void* operator new(size_t size);
00078 static void operator delete(void* p, size_t size);
00079 };
00080
00081
00082
00083
00084
00085
00086 BoolExpr::Node::Node(void)
00087 : use(1), l(NULL), r(NULL), m(NULL) {}
00088
00089 BoolExpr::Node::~Node(void) {
00090 delete m;
00091 }
00092
00093 void*
00094 BoolExpr::Node::operator new(size_t size) {
00095 return heap.ralloc(size);
00096 }
00097 void
00098 BoolExpr::Node::operator delete(void* p, size_t) {
00099 heap.rfree(p);
00100 }
00101
00102 bool
00103 BoolExpr::Node::decrement(void) {
00104 if (--use == 0) {
00105 if ((l != NULL) && l->decrement())
00106 delete l;
00107 if ((r != NULL) && r->decrement())
00108 delete r;
00109 return true;
00110 }
00111 return false;
00112 }
00113
00114 BoolExpr::BoolExpr(void) : n(new Node) {}
00115
00116 BoolExpr::BoolExpr(const BoolExpr& e) : n(e.n) {
00117 n->use++;
00118 }
00119
00120 BoolExpr::BoolExpr(const BoolVar& x) : n(new Node) {
00121 n->same = 1;
00122 n->t = NT_VAR;
00123 n->l = NULL;
00124 n->r = NULL;
00125 n->x = x;
00126 }
00127
00128 BoolExpr::BoolExpr(const BoolExpr& l, NodeType t, const BoolExpr& r)
00129 : n(new Node) {
00130 int ls = ((l.n->t == t) || (l.n->t == NT_VAR)) ? l.n->same : 1;
00131 int rs = ((r.n->t == t) || (r.n->t == NT_VAR)) ? r.n->same : 1;
00132 n->same = ls+rs;
00133 n->t = t;
00134 n->l = l.n;
00135 n->l->use++;
00136 n->r = r.n;
00137 n->r->use++;
00138 }
00139
00140 BoolExpr::BoolExpr(const BoolExpr& l, NodeType t) {
00141 (void) t;
00142 assert(t == NT_NOT);
00143 if (l.n->t == NT_NOT) {
00144 n = l.n->l;
00145 n->use++;
00146 } else {
00147 n = new Node;
00148 n->same = 1;
00149 n->t = NT_NOT;
00150 n->l = l.n;
00151 n->l->use++;
00152 n->r = NULL;
00153 }
00154 }
00155
00156 BoolExpr::BoolExpr(const LinIntRel& rl)
00157 : n(new Node) {
00158 n->same = 1;
00159 n->t = NT_RLIN;
00160 n->l = NULL;
00161 n->r = NULL;
00162 n->rl = rl;
00163 }
00164
00165 #ifdef GECODE_HAS_FLOAT_VARS
00166 BoolExpr::BoolExpr(const LinFloatRel& rfl)
00167 : n(new Node) {
00168 n->same = 1;
00169 n->t = NT_RLINFLOAT;
00170 n->l = NULL;
00171 n->r = NULL;
00172 n->rfl = rfl;
00173 }
00174 #endif
00175
00176 #ifdef GECODE_HAS_SET_VARS
00177 BoolExpr::BoolExpr(const SetRel& rs)
00178 : n(new Node) {
00179 n->same = 1;
00180 n->t = NT_RSET;
00181 n->l = NULL;
00182 n->r = NULL;
00183 n->rs = rs;
00184 }
00185
00186 BoolExpr::BoolExpr(const SetCmpRel& rs)
00187 : n(new Node) {
00188 n->same = 1;
00189 n->t = NT_RSET;
00190 n->l = NULL;
00191 n->r = NULL;
00192 n->rs = rs;
00193 }
00194 #endif
00195
00196 BoolExpr::BoolExpr(BoolExpr::Misc* m)
00197 : n(new Node) {
00198 n->same = 1;
00199 n->t = NT_MISC;
00200 n->l = NULL;
00201 n->r = NULL;
00202 n->m = m;
00203 }
00204
00205 const BoolExpr&
00206 BoolExpr::operator =(const BoolExpr& e) {
00207 if (this != &e) {
00208 if (n->decrement())
00209 delete n;
00210 n = e.n;
00211 n->use++;
00212 }
00213 return *this;
00214 }
00215
00216 BoolExpr::Misc::~Misc(void) {}
00217
00218 BoolExpr::~BoolExpr(void) {
00219 if (n->decrement())
00220 delete n;
00221 }
00222
00223 namespace {
00225 class NNF {
00226 public:
00227 typedef BoolExpr::NodeType NodeType;
00228 typedef BoolExpr::Node Node;
00230 NodeType t;
00232 int p;
00234 int n;
00236 union {
00238 struct {
00240 NNF* l;
00242 NNF* r;
00243 } b;
00245 struct {
00247 bool neg;
00249 Node* x;
00250 } a;
00251 } u;
00253 GECODE_MINIMODEL_EXPORT
00254 static NNF* nnf(Region& r, Node* n, bool neg);
00256 GECODE_MINIMODEL_EXPORT
00257 void post(Home home, NodeType t,
00258 BoolVarArgs& bp, BoolVarArgs& bn,
00259 int& ip, int& in,
00260 IntPropLevel ipl) const;
00262 GECODE_MINIMODEL_EXPORT
00263 BoolVar expr(Home home, IntPropLevel ipl) const;
00265 GECODE_MINIMODEL_EXPORT
00266 void rel(Home home, IntPropLevel ipl) const;
00268 static void* operator new(size_t s, Region& r);
00270 static void operator delete(void*);
00272 static void operator delete(void*, Region&);
00273 };
00274
00275
00276
00277
00278
00279 forceinline void
00280 NNF::operator delete(void*) {}
00281
00282 forceinline void
00283 NNF::operator delete(void*, Region&) {}
00284
00285 forceinline void*
00286 NNF::operator new(size_t s, Region& r) {
00287 return r.ralloc(s);
00288 }
00289
00290 BoolVar
00291 NNF::expr(Home home, IntPropLevel ipl) const {
00292 if ((t == BoolExpr::NT_VAR) && !u.a.neg)
00293 return u.a.x->x;
00294 BoolVar b(home,0,1);
00295 switch (t) {
00296 case BoolExpr::NT_VAR:
00297 assert(u.a.neg);
00298 Gecode::rel(home, u.a.x->x, IRT_NQ, b);
00299 break;
00300 case BoolExpr::NT_RLIN:
00301 u.a.x->rl.post(home, b, !u.a.neg, ipl);
00302 break;
00303 #ifdef GECODE_HAS_FLOAT_VARS
00304 case BoolExpr::NT_RLINFLOAT:
00305 u.a.x->rfl.post(home, b, !u.a.neg);
00306 break;
00307 #endif
00308 #ifdef GECODE_HAS_SET_VARS
00309 case BoolExpr::NT_RSET:
00310 u.a.x->rs.post(home, b, !u.a.neg);
00311 break;
00312 #endif
00313 case BoolExpr::NT_MISC:
00314 u.a.x->m->post(home, b, u.a.neg, ipl);
00315 break;
00316 case BoolExpr::NT_AND:
00317 {
00318 BoolVarArgs bp(p), bn(n);
00319 int ip=0, in=0;
00320 post(home, BoolExpr::NT_AND, bp, bn, ip, in, ipl);
00321 clause(home, BOT_AND, bp, bn, b);
00322 }
00323 break;
00324 case BoolExpr::NT_OR:
00325 {
00326 BoolVarArgs bp(p), bn(n);
00327 int ip=0, in=0;
00328 post(home, BoolExpr::NT_OR, bp, bn, ip, in, ipl);
00329 clause(home, BOT_OR, bp, bn, b);
00330 }
00331 break;
00332 case BoolExpr::NT_EQV:
00333 {
00334 bool n = false;
00335 BoolVar l;
00336 if (u.b.l->t == BoolExpr::NT_VAR) {
00337 l = u.b.l->u.a.x->x;
00338 if (u.b.l->u.a.neg) n = !n;
00339 } else {
00340 l = u.b.l->expr(home,ipl);
00341 }
00342 BoolVar r;
00343 if (u.b.r->t == BoolExpr::NT_VAR) {
00344 r = u.b.r->u.a.x->x;
00345 if (u.b.r->u.a.neg) n = !n;
00346 } else {
00347 r = u.b.r->expr(home,ipl);
00348 }
00349 Gecode::rel(home, l, n ? BOT_XOR : BOT_EQV, r, b, ipl);
00350 }
00351 break;
00352 default:
00353 GECODE_NEVER;
00354 }
00355 return b;
00356 }
00357
00358 void
00359 NNF::post(Home home, NodeType t,
00360 BoolVarArgs& bp, BoolVarArgs& bn,
00361 int& ip, int& in,
00362 IntPropLevel ipl) const {
00363 if (this->t != t) {
00364 switch (this->t) {
00365 case BoolExpr::NT_VAR:
00366 if (u.a.neg) {
00367 bn[in++]=u.a.x->x;
00368 } else {
00369 bp[ip++]=u.a.x->x;
00370 }
00371 break;
00372 case BoolExpr::NT_RLIN:
00373 {
00374 BoolVar b(home,0,1);
00375 u.a.x->rl.post(home, b, !u.a.neg, ipl);
00376 bp[ip++]=b;
00377 }
00378 break;
00379 #ifdef GECODE_HAS_FLOAT_VARS
00380 case BoolExpr::NT_RLINFLOAT:
00381 {
00382 BoolVar b(home,0,1);
00383 u.a.x->rfl.post(home, b, !u.a.neg);
00384 bp[ip++]=b;
00385 }
00386 break;
00387 #endif
00388 #ifdef GECODE_HAS_SET_VARS
00389 case BoolExpr::NT_RSET:
00390 {
00391 BoolVar b(home,0,1);
00392 u.a.x->rs.post(home, b, !u.a.neg);
00393 bp[ip++]=b;
00394 }
00395 break;
00396 #endif
00397 case BoolExpr::NT_MISC:
00398 {
00399 BoolVar b(home,0,1);
00400 u.a.x->m->post(home, b, u.a.neg, ipl);
00401 bp[ip++]=b;
00402 }
00403 break;
00404 default:
00405 bp[ip++] = expr(home, ipl);
00406 break;
00407 }
00408 } else {
00409 u.b.l->post(home, t, bp, bn, ip, in, ipl);
00410 u.b.r->post(home, t, bp, bn, ip, in, ipl);
00411 }
00412 }
00413
00414 void
00415 NNF::rel(Home home, IntPropLevel ipl) const {
00416 switch (t) {
00417 case BoolExpr::NT_VAR:
00418 Gecode::rel(home, u.a.x->x, IRT_EQ, u.a.neg ? 0 : 1);
00419 break;
00420 case BoolExpr::NT_RLIN:
00421 u.a.x->rl.post(home, !u.a.neg, ipl);
00422 break;
00423 #ifdef GECODE_HAS_FLOAT_VARS
00424 case BoolExpr::NT_RLINFLOAT:
00425 u.a.x->rfl.post(home, !u.a.neg);
00426 break;
00427 #endif
00428 #ifdef GECODE_HAS_SET_VARS
00429 case BoolExpr::NT_RSET:
00430 u.a.x->rs.post(home, !u.a.neg);
00431 break;
00432 #endif
00433 case BoolExpr::NT_MISC:
00434 {
00435 BoolVar b(home,!u.a.neg,!u.a.neg);
00436 u.a.x->m->post(home, b, false, ipl);
00437 }
00438 break;
00439 case BoolExpr::NT_AND:
00440 u.b.l->rel(home, ipl);
00441 u.b.r->rel(home, ipl);
00442 break;
00443 case BoolExpr::NT_OR:
00444 {
00445 BoolVarArgs bp(p), bn(n);
00446 int ip=0, in=0;
00447 post(home, BoolExpr::NT_OR, bp, bn, ip, in, ipl);
00448 clause(home, BOT_OR, bp, bn, 1);
00449 }
00450 break;
00451 case BoolExpr::NT_EQV:
00452 if (u.b.l->t==BoolExpr::NT_VAR &&
00453 u.b.r->t==BoolExpr::NT_RLIN) {
00454 u.b.r->u.a.x->rl.post(home, u.b.l->u.a.x->x,
00455 u.b.l->u.a.neg==u.b.r->u.a.neg, ipl);
00456 } else if (u.b.r->t==BoolExpr::NT_VAR &&
00457 u.b.l->t==BoolExpr::NT_RLIN) {
00458 u.b.l->u.a.x->rl.post(home, u.b.r->u.a.x->x,
00459 u.b.l->u.a.neg==u.b.r->u.a.neg, ipl);
00460 } else if (u.b.l->t==BoolExpr::NT_RLIN) {
00461 u.b.l->u.a.x->rl.post(home, u.b.r->expr(home,ipl),
00462 !u.b.l->u.a.neg,ipl);
00463 } else if (u.b.r->t==BoolExpr::NT_RLIN) {
00464 u.b.r->u.a.x->rl.post(home, u.b.l->expr(home,ipl),
00465 !u.b.r->u.a.neg,ipl);
00466 #ifdef GECODE_HAS_FLOAT_VARS
00467 } else if (u.b.l->t==BoolExpr::NT_VAR &&
00468 u.b.r->t==BoolExpr::NT_RLINFLOAT) {
00469 u.b.r->u.a.x->rfl.post(home, u.b.l->u.a.x->x,
00470 u.b.l->u.a.neg==u.b.r->u.a.neg);
00471 } else if (u.b.r->t==BoolExpr::NT_VAR &&
00472 u.b.l->t==BoolExpr::NT_RLINFLOAT) {
00473 u.b.l->u.a.x->rfl.post(home, u.b.r->u.a.x->x,
00474 u.b.l->u.a.neg==u.b.r->u.a.neg);
00475 } else if (u.b.l->t==BoolExpr::NT_RLINFLOAT) {
00476 u.b.l->u.a.x->rfl.post(home, u.b.r->expr(home,ipl),
00477 !u.b.l->u.a.neg);
00478 } else if (u.b.r->t==BoolExpr::NT_RLINFLOAT) {
00479 u.b.r->u.a.x->rfl.post(home, u.b.l->expr(home,ipl),
00480 !u.b.r->u.a.neg);
00481 #endif
00482 #ifdef GECODE_HAS_SET_VARS
00483 } else if (u.b.l->t==BoolExpr::NT_VAR &&
00484 u.b.r->t==BoolExpr::NT_RSET) {
00485 u.b.r->u.a.x->rs.post(home, u.b.l->u.a.x->x,
00486 u.b.l->u.a.neg==u.b.r->u.a.neg);
00487 } else if (u.b.r->t==BoolExpr::NT_VAR &&
00488 u.b.l->t==BoolExpr::NT_RSET) {
00489 u.b.l->u.a.x->rs.post(home, u.b.r->u.a.x->x,
00490 u.b.l->u.a.neg==u.b.r->u.a.neg);
00491 } else if (u.b.l->t==BoolExpr::NT_RSET) {
00492 u.b.l->u.a.x->rs.post(home, u.b.r->expr(home,ipl),
00493 !u.b.l->u.a.neg);
00494 } else if (u.b.r->t==BoolExpr::NT_RSET) {
00495 u.b.r->u.a.x->rs.post(home, u.b.l->expr(home,ipl),
00496 !u.b.r->u.a.neg);
00497 #endif
00498 } else {
00499 Gecode::rel(home, expr(home, ipl), IRT_EQ, 1);
00500 }
00501 break;
00502 default:
00503 GECODE_NEVER;
00504 }
00505 }
00506
00507 NNF*
00508 NNF::nnf(Region& r, Node* n, bool neg) {
00509 switch (n->t) {
00510 case BoolExpr::NT_VAR:
00511 case BoolExpr::NT_RLIN:
00512 case BoolExpr::NT_MISC:
00513 #ifdef GECODE_HAS_FLOAT_VARS
00514 case BoolExpr::NT_RLINFLOAT:
00515 #endif
00516 #ifdef GECODE_HAS_SET_VARS
00517 case BoolExpr::NT_RSET:
00518 #endif
00519 {
00520 NNF* x = new (r) NNF;
00521 x->t = n->t; x->u.a.neg = neg; x->u.a.x = n;
00522 if (neg) {
00523 x->p = 0; x->n = 1;
00524 } else {
00525 x->p = 1; x->n = 0;
00526 }
00527 return x;
00528 }
00529 case BoolExpr::NT_NOT:
00530 return nnf(r,n->l,!neg);
00531 case BoolExpr::NT_AND: case BoolExpr::NT_OR:
00532 {
00533 NodeType t = ((n->t == BoolExpr::NT_AND) == neg) ?
00534 BoolExpr::NT_OR : BoolExpr::NT_AND;
00535 NNF* x = new (r) NNF;
00536 x->t = t;
00537 x->u.b.l = nnf(r,n->l,neg);
00538 x->u.b.r = nnf(r,n->r,neg);
00539 int p_l, n_l;
00540 if ((x->u.b.l->t == t) ||
00541 (x->u.b.l->t == BoolExpr::NT_VAR)) {
00542 p_l=x->u.b.l->p; n_l=x->u.b.l->n;
00543 } else {
00544 p_l=1; n_l=0;
00545 }
00546 int p_r, n_r;
00547 if ((x->u.b.r->t == t) ||
00548 (x->u.b.r->t == BoolExpr::NT_VAR)) {
00549 p_r=x->u.b.r->p; n_r=x->u.b.r->n;
00550 } else {
00551 p_r=1; n_r=0;
00552 }
00553 x->p = p_l+p_r;
00554 x->n = n_l+n_r;
00555 return x;
00556 }
00557 case BoolExpr::NT_EQV:
00558 {
00559 NNF* x = new (r) NNF;
00560 x->t = BoolExpr::NT_EQV;
00561 x->u.b.l = nnf(r,n->l,neg);
00562 x->u.b.r = nnf(r,n->r,false);
00563 x->p = 2; x->n = 0;
00564 return x;
00565 }
00566 default:
00567 GECODE_NEVER;
00568 }
00569 GECODE_NEVER;
00570 return NULL;
00571 }
00572 }
00573
00574 BoolVar
00575 BoolExpr::expr(Home home, IntPropLevel ipl) const {
00576 Region r;
00577 return NNF::nnf(r,n,false)->expr(home,ipl);
00578 }
00579
00580 void
00581 BoolExpr::rel(Home home, IntPropLevel ipl) const {
00582 Region r;
00583 return NNF::nnf(r,n,false)->rel(home,ipl);
00584 }
00585
00586
00587 BoolExpr
00588 operator &&(const BoolExpr& l, const BoolExpr& r) {
00589 return BoolExpr(l,BoolExpr::NT_AND,r);
00590 }
00591 BoolExpr
00592 operator ||(const BoolExpr& l, const BoolExpr& r) {
00593 return BoolExpr(l,BoolExpr::NT_OR,r);
00594 }
00595 BoolExpr
00596 operator ^(const BoolExpr& l, const BoolExpr& r) {
00597 return BoolExpr(BoolExpr(l,BoolExpr::NT_EQV,r),BoolExpr::NT_NOT);
00598 }
00599
00600 BoolExpr
00601 operator !(const BoolExpr& e) {
00602 return BoolExpr(e,BoolExpr::NT_NOT);
00603 }
00604
00605 BoolExpr
00606 operator !=(const BoolExpr& l, const BoolExpr& r) {
00607 return !BoolExpr(l, BoolExpr::NT_EQV, r);
00608 }
00609 BoolExpr
00610 operator ==(const BoolExpr& l, const BoolExpr& r) {
00611 return BoolExpr(l, BoolExpr::NT_EQV, r);
00612 }
00613 BoolExpr
00614 operator >>(const BoolExpr& l, const BoolExpr& r) {
00615 return BoolExpr(BoolExpr(l,BoolExpr::NT_NOT),
00616 BoolExpr::NT_OR,r);
00617 }
00618 BoolExpr
00619 operator <<(const BoolExpr& l, const BoolExpr& r) {
00620 return BoolExpr(BoolExpr(r,BoolExpr::NT_NOT),
00621 BoolExpr::NT_OR,l);
00622 }
00623
00624
00625
00626
00627 BoolVar
00628 expr(Home home, const BoolExpr& e, IntPropLevel ipl) {
00629 PostInfo pi(home);
00630 if (!home.failed())
00631 return e.expr(home,ipl);
00632 BoolVar x(home,0,1);
00633 return x;
00634 }
00635
00636 void
00637 rel(Home home, const BoolExpr& e, IntPropLevel ipl) {
00638 GECODE_POST;
00639 if (home.failed()) return;
00640 e.rel(home,ipl);
00641 }
00642
00643
00644
00645
00646
00647
00649 class BElementExpr : public BoolExpr::Misc {
00650 protected:
00652 BoolExpr* a;
00654 int n;
00656 LinIntExpr idx;
00657 public:
00659 BElementExpr(const BoolVarArgs& b, const LinIntExpr& idx);
00661 virtual ~BElementExpr(void);
00663 virtual void post(Home home, BoolVar b, bool neg, IntPropLevel ipl);
00664 };
00665
00666 BElementExpr::BElementExpr(const BoolVarArgs& b, const LinIntExpr& idx)
00667 : a(static_cast<BoolExpr*>(heap.ralloc(sizeof(BoolExpr)*b.size()))), n(b.size()), idx(idx) {
00668 for (int i=b.size(); i--;)
00669 new (&a[i]) BoolExpr(b[i]);
00670 }
00671
00672 BElementExpr::~BElementExpr(void) {
00673 heap.free<BoolExpr>(a,n);
00674 }
00675
00676 void
00677 BElementExpr::post(Home home, BoolVar b, bool neg, IntPropLevel ipl) {
00678 IntVar z = idx.post(home, ipl);
00679 if (z.assigned() && (z.val() >= 0) && (z.val() < n)) {
00680 BoolExpr be = neg ? (a[z.val()] == !b) : (a[z.val()] == b);
00681 be.rel(home,ipl);
00682 } else {
00683 BoolVarArgs x(n);
00684 for (int i=n; i--;)
00685 x[i] = a[i].expr(home,ipl);
00686 BoolVar res = neg ? (!b).expr(home,ipl) : b;
00687 element(home, x, z, res, ipl);
00688 }
00689 }
00690
00691 BoolExpr
00692 element(const BoolVarArgs& b, const LinIntExpr& idx) {
00693 return BoolExpr(new BElementExpr(b,idx));
00694 }
00695
00696 }
00697
00698