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(nullptr), r(nullptr), m(nullptr) {}
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 != nullptr) && l->decrement())
00106 delete l;
00107 if ((r != nullptr) && 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 = nullptr;
00124 n->r = nullptr;
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 = nullptr;
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 = nullptr;
00161 n->r = nullptr;
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 = nullptr;
00171 n->r = nullptr;
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 = nullptr;
00182 n->r = nullptr;
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 = nullptr;
00191 n->r = nullptr;
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 = nullptr;
00201 n->r = nullptr;
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 static NNF* nnf(Region& r, Node* n, bool neg);
00255 GECODE_MINIMODEL_EXPORT
00256 void post(Home home, NodeType t,
00257 BoolVarArgs& bp, BoolVarArgs& bn,
00258 int& ip, int& in,
00259 const IntPropLevels& ipls) const;
00261 GECODE_MINIMODEL_EXPORT
00262 BoolVar expr(Home home, const IntPropLevels& ipls) const;
00264 GECODE_MINIMODEL_EXPORT
00265 void rel(Home home, const IntPropLevels& ipls) const;
00267 static void* operator new(size_t s, Region& r);
00269 static void operator delete(void*);
00271 static void operator delete(void*, Region&);
00272 };
00273
00274
00275
00276
00277
00278 forceinline void
00279 NNF::operator delete(void*) {}
00280
00281 forceinline void
00282 NNF::operator delete(void*, Region&) {}
00283
00284 forceinline void*
00285 NNF::operator new(size_t s, Region& r) {
00286 return r.ralloc(s);
00287 }
00288
00289 BoolVar
00290 NNF::expr(Home home, const IntPropLevels& ipls) const {
00291 if ((t == BoolExpr::NT_VAR) && !u.a.neg)
00292 return u.a.x->x;
00293 BoolVar b(home,0,1);
00294 switch (t) {
00295 case BoolExpr::NT_VAR:
00296 assert(u.a.neg);
00297 Gecode::rel(home, u.a.x->x, IRT_NQ, b);
00298 break;
00299 case BoolExpr::NT_RLIN:
00300 u.a.x->rl.post(home, b, !u.a.neg, ipls);
00301 break;
00302 #ifdef GECODE_HAS_FLOAT_VARS
00303 case BoolExpr::NT_RLINFLOAT:
00304 u.a.x->rfl.post(home, b, !u.a.neg);
00305 break;
00306 #endif
00307 #ifdef GECODE_HAS_SET_VARS
00308 case BoolExpr::NT_RSET:
00309 u.a.x->rs.post(home, b, !u.a.neg);
00310 break;
00311 #endif
00312 case BoolExpr::NT_MISC:
00313 u.a.x->m->post(home, b, u.a.neg, ipls);
00314 break;
00315 case BoolExpr::NT_AND:
00316 {
00317 BoolVarArgs bp(p), bn(n);
00318 int ip=0, in=0;
00319 post(home, BoolExpr::NT_AND, bp, bn, ip, in, ipls);
00320 clause(home, BOT_AND, bp, bn, b);
00321 }
00322 break;
00323 case BoolExpr::NT_OR:
00324 {
00325 BoolVarArgs bp(p), bn(n);
00326 int ip=0, in=0;
00327 post(home, BoolExpr::NT_OR, bp, bn, ip, in, ipls);
00328 clause(home, BOT_OR, bp, bn, b);
00329 }
00330 break;
00331 case BoolExpr::NT_EQV:
00332 {
00333 bool n = false;
00334 BoolVar l;
00335 if (u.b.l->t == BoolExpr::NT_VAR) {
00336 l = u.b.l->u.a.x->x;
00337 if (u.b.l->u.a.neg) n = !n;
00338 } else {
00339 l = u.b.l->expr(home,ipls);
00340 }
00341 BoolVar r;
00342 if (u.b.r->t == BoolExpr::NT_VAR) {
00343 r = u.b.r->u.a.x->x;
00344 if (u.b.r->u.a.neg) n = !n;
00345 } else {
00346 r = u.b.r->expr(home,ipls);
00347 }
00348 Gecode::rel(home, l, n ? BOT_XOR : BOT_EQV, r, b);
00349 }
00350 break;
00351 default:
00352 GECODE_NEVER;
00353 }
00354 return b;
00355 }
00356
00357 void
00358 NNF::post(Home home, NodeType t,
00359 BoolVarArgs& bp, BoolVarArgs& bn,
00360 int& ip, int& in,
00361 const IntPropLevels& ipls) const {
00362 if (this->t != t) {
00363 switch (this->t) {
00364 case BoolExpr::NT_VAR:
00365 if (u.a.neg) {
00366 bn[in++]=u.a.x->x;
00367 } else {
00368 bp[ip++]=u.a.x->x;
00369 }
00370 break;
00371 case BoolExpr::NT_RLIN:
00372 {
00373 BoolVar b(home,0,1);
00374 u.a.x->rl.post(home, b, !u.a.neg, ipls);
00375 bp[ip++]=b;
00376 }
00377 break;
00378 #ifdef GECODE_HAS_FLOAT_VARS
00379 case BoolExpr::NT_RLINFLOAT:
00380 {
00381 BoolVar b(home,0,1);
00382 u.a.x->rfl.post(home, b, !u.a.neg);
00383 bp[ip++]=b;
00384 }
00385 break;
00386 #endif
00387 #ifdef GECODE_HAS_SET_VARS
00388 case BoolExpr::NT_RSET:
00389 {
00390 BoolVar b(home,0,1);
00391 u.a.x->rs.post(home, b, !u.a.neg);
00392 bp[ip++]=b;
00393 }
00394 break;
00395 #endif
00396 case BoolExpr::NT_MISC:
00397 {
00398 BoolVar b(home,0,1);
00399 u.a.x->m->post(home, b, u.a.neg, ipls);
00400 bp[ip++]=b;
00401 }
00402 break;
00403 default:
00404 bp[ip++] = expr(home, ipls);
00405 break;
00406 }
00407 } else {
00408 u.b.l->post(home, t, bp, bn, ip, in, ipls);
00409 u.b.r->post(home, t, bp, bn, ip, in, ipls);
00410 }
00411 }
00412
00413 void
00414 NNF::rel(Home home, const IntPropLevels& ipls) const {
00415 switch (t) {
00416 case BoolExpr::NT_VAR:
00417 Gecode::rel(home, u.a.x->x, IRT_EQ, u.a.neg ? 0 : 1);
00418 break;
00419 case BoolExpr::NT_RLIN:
00420 u.a.x->rl.post(home, !u.a.neg, ipls);
00421 break;
00422 #ifdef GECODE_HAS_FLOAT_VARS
00423 case BoolExpr::NT_RLINFLOAT:
00424 u.a.x->rfl.post(home, !u.a.neg);
00425 break;
00426 #endif
00427 #ifdef GECODE_HAS_SET_VARS
00428 case BoolExpr::NT_RSET:
00429 u.a.x->rs.post(home, !u.a.neg);
00430 break;
00431 #endif
00432 case BoolExpr::NT_MISC:
00433 {
00434 BoolVar b(home,!u.a.neg,!u.a.neg);
00435 u.a.x->m->post(home, b, false, ipls);
00436 }
00437 break;
00438 case BoolExpr::NT_AND:
00439 u.b.l->rel(home, ipls);
00440 u.b.r->rel(home, ipls);
00441 break;
00442 case BoolExpr::NT_OR:
00443 {
00444 BoolVarArgs bp(p), bn(n);
00445 int ip=0, in=0;
00446 post(home, BoolExpr::NT_OR, bp, bn, ip, in, ipls);
00447 clause(home, BOT_OR, bp, bn, 1);
00448 }
00449 break;
00450 case BoolExpr::NT_EQV:
00451 if (u.b.l->t==BoolExpr::NT_VAR &&
00452 u.b.r->t==BoolExpr::NT_RLIN) {
00453 u.b.r->u.a.x->rl.post(home, u.b.l->u.a.x->x,
00454 u.b.l->u.a.neg==u.b.r->u.a.neg, ipls);
00455 } else if (u.b.r->t==BoolExpr::NT_VAR &&
00456 u.b.l->t==BoolExpr::NT_RLIN) {
00457 u.b.l->u.a.x->rl.post(home, u.b.r->u.a.x->x,
00458 u.b.l->u.a.neg==u.b.r->u.a.neg, ipls);
00459 } else if (u.b.l->t==BoolExpr::NT_RLIN) {
00460 u.b.l->u.a.x->rl.post(home, u.b.r->expr(home,ipls),
00461 !u.b.l->u.a.neg,ipls);
00462 } else if (u.b.r->t==BoolExpr::NT_RLIN) {
00463 u.b.r->u.a.x->rl.post(home, u.b.l->expr(home,ipls),
00464 !u.b.r->u.a.neg,ipls);
00465 #ifdef GECODE_HAS_FLOAT_VARS
00466 } else if (u.b.l->t==BoolExpr::NT_VAR &&
00467 u.b.r->t==BoolExpr::NT_RLINFLOAT) {
00468 u.b.r->u.a.x->rfl.post(home, u.b.l->u.a.x->x,
00469 u.b.l->u.a.neg==u.b.r->u.a.neg);
00470 } else if (u.b.r->t==BoolExpr::NT_VAR &&
00471 u.b.l->t==BoolExpr::NT_RLINFLOAT) {
00472 u.b.l->u.a.x->rfl.post(home, u.b.r->u.a.x->x,
00473 u.b.l->u.a.neg==u.b.r->u.a.neg);
00474 } else if (u.b.l->t==BoolExpr::NT_RLINFLOAT) {
00475 u.b.l->u.a.x->rfl.post(home, u.b.r->expr(home,ipls),
00476 !u.b.l->u.a.neg);
00477 } else if (u.b.r->t==BoolExpr::NT_RLINFLOAT) {
00478 u.b.r->u.a.x->rfl.post(home, u.b.l->expr(home,ipls),
00479 !u.b.r->u.a.neg);
00480 #endif
00481 #ifdef GECODE_HAS_SET_VARS
00482 } else if (u.b.l->t==BoolExpr::NT_VAR &&
00483 u.b.r->t==BoolExpr::NT_RSET) {
00484 u.b.r->u.a.x->rs.post(home, u.b.l->u.a.x->x,
00485 u.b.l->u.a.neg==u.b.r->u.a.neg);
00486 } else if (u.b.r->t==BoolExpr::NT_VAR &&
00487 u.b.l->t==BoolExpr::NT_RSET) {
00488 u.b.l->u.a.x->rs.post(home, u.b.r->u.a.x->x,
00489 u.b.l->u.a.neg==u.b.r->u.a.neg);
00490 } else if (u.b.l->t==BoolExpr::NT_RSET) {
00491 u.b.l->u.a.x->rs.post(home, u.b.r->expr(home,ipls),
00492 !u.b.l->u.a.neg);
00493 } else if (u.b.r->t==BoolExpr::NT_RSET) {
00494 u.b.r->u.a.x->rs.post(home, u.b.l->expr(home,ipls),
00495 !u.b.r->u.a.neg);
00496 #endif
00497 } else {
00498 Gecode::rel(home, expr(home, ipls), IRT_EQ, 1);
00499 }
00500 break;
00501 default:
00502 GECODE_NEVER;
00503 }
00504 }
00505
00506 NNF*
00507 NNF::nnf(Region& r, Node* n, bool neg) {
00508 switch (n->t) {
00509 case BoolExpr::NT_VAR:
00510 case BoolExpr::NT_RLIN:
00511 case BoolExpr::NT_MISC:
00512 #ifdef GECODE_HAS_FLOAT_VARS
00513 case BoolExpr::NT_RLINFLOAT:
00514 #endif
00515 #ifdef GECODE_HAS_SET_VARS
00516 case BoolExpr::NT_RSET:
00517 #endif
00518 {
00519 NNF* x = new (r) NNF;
00520 x->t = n->t; x->u.a.neg = neg; x->u.a.x = n;
00521 if (neg) {
00522 x->p = 0; x->n = 1;
00523 } else {
00524 x->p = 1; x->n = 0;
00525 }
00526 return x;
00527 }
00528 case BoolExpr::NT_NOT:
00529 return nnf(r,n->l,!neg);
00530 case BoolExpr::NT_AND: case BoolExpr::NT_OR:
00531 {
00532 NodeType t = ((n->t == BoolExpr::NT_AND) == neg) ?
00533 BoolExpr::NT_OR : BoolExpr::NT_AND;
00534 NNF* x = new (r) NNF;
00535 x->t = t;
00536 x->u.b.l = nnf(r,n->l,neg);
00537 x->u.b.r = nnf(r,n->r,neg);
00538 int p_l, n_l;
00539 if ((x->u.b.l->t == t) ||
00540 (x->u.b.l->t == BoolExpr::NT_VAR)) {
00541 p_l=x->u.b.l->p; n_l=x->u.b.l->n;
00542 } else {
00543 p_l=1; n_l=0;
00544 }
00545 int p_r, n_r;
00546 if ((x->u.b.r->t == t) ||
00547 (x->u.b.r->t == BoolExpr::NT_VAR)) {
00548 p_r=x->u.b.r->p; n_r=x->u.b.r->n;
00549 } else {
00550 p_r=1; n_r=0;
00551 }
00552 x->p = p_l+p_r;
00553 x->n = n_l+n_r;
00554 return x;
00555 }
00556 case BoolExpr::NT_EQV:
00557 {
00558 NNF* x = new (r) NNF;
00559 x->t = BoolExpr::NT_EQV;
00560 x->u.b.l = nnf(r,n->l,neg);
00561 x->u.b.r = nnf(r,n->r,false);
00562 x->p = 2; x->n = 0;
00563 return x;
00564 }
00565 default:
00566 GECODE_NEVER;
00567 }
00568 GECODE_NEVER;
00569 return nullptr;
00570 }
00571 }
00572
00573 BoolVar
00574 BoolExpr::expr(Home home, const IntPropLevels& ipls) const {
00575 Region r;
00576 return NNF::nnf(r,n,false)->expr(home,ipls);
00577 }
00578
00579 void
00580 BoolExpr::rel(Home home, const IntPropLevels& ipls) const {
00581 Region r;
00582 return NNF::nnf(r,n,false)->rel(home,ipls);
00583 }
00584
00585
00586 BoolExpr
00587 operator &&(const BoolExpr& l, const BoolExpr& r) {
00588 return BoolExpr(l,BoolExpr::NT_AND,r);
00589 }
00590 BoolExpr
00591 operator ||(const BoolExpr& l, const BoolExpr& r) {
00592 return BoolExpr(l,BoolExpr::NT_OR,r);
00593 }
00594 BoolExpr
00595 operator ^(const BoolExpr& l, const BoolExpr& r) {
00596 return BoolExpr(BoolExpr(l,BoolExpr::NT_EQV,r),BoolExpr::NT_NOT);
00597 }
00598
00599 BoolExpr
00600 operator !(const BoolExpr& e) {
00601 return BoolExpr(e,BoolExpr::NT_NOT);
00602 }
00603
00604 BoolExpr
00605 operator !=(const BoolExpr& l, const BoolExpr& r) {
00606 return !BoolExpr(l, BoolExpr::NT_EQV, r);
00607 }
00608 BoolExpr
00609 operator ==(const BoolExpr& l, const BoolExpr& r) {
00610 return BoolExpr(l, BoolExpr::NT_EQV, r);
00611 }
00612 BoolExpr
00613 operator >>(const BoolExpr& l, const BoolExpr& r) {
00614 return BoolExpr(BoolExpr(l,BoolExpr::NT_NOT),
00615 BoolExpr::NT_OR,r);
00616 }
00617 BoolExpr
00618 operator <<(const BoolExpr& l, const BoolExpr& r) {
00619 return BoolExpr(BoolExpr(r,BoolExpr::NT_NOT),
00620 BoolExpr::NT_OR,l);
00621 }
00622
00623
00624
00625
00626
00627
00628 BoolVar
00629 expr(Home home, const BoolExpr& e, const IntPropLevels& ipls) {
00630 PostInfo pi(home);
00631 if (!home.failed())
00632 return e.expr(home,ipls);
00633 BoolVar x(home,0,1);
00634 return x;
00635 }
00636
00637 void
00638 rel(Home home, const BoolExpr& e, const IntPropLevels& ipls) {
00639 GECODE_POST;
00640 e.rel(home,ipls);
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,
00664 const IntPropLevels& ipls);
00665 };
00666
00667 BElementExpr::BElementExpr(const BoolVarArgs& b, const LinIntExpr& idx)
00668 : a(static_cast<BoolExpr*>(heap.ralloc(sizeof(BoolExpr)*b.size()))), n(b.size()), idx(idx) {
00669 for (int i=b.size(); i--;)
00670 new (&a[i]) BoolExpr(b[i]);
00671 }
00672
00673 BElementExpr::~BElementExpr(void) {
00674 heap.free<BoolExpr>(a,n);
00675 }
00676
00677 void
00678 BElementExpr::post(Home home, BoolVar b, bool neg,
00679 const IntPropLevels& ipls) {
00680 IntVar z = idx.post(home, ipls);
00681 if (z.assigned() && (z.val() >= 0) && (z.val() < n)) {
00682 BoolExpr be = neg ? (a[z.val()] == !b) : (a[z.val()] == b);
00683 be.rel(home,ipls);
00684 } else {
00685 BoolVarArgs x(n);
00686 for (int i=n; i--;)
00687 x[i] = a[i].expr(home,ipls);
00688 BoolVar res = neg ? (!b).expr(home,ipls) : b;
00689 element(home, x, z, res, ipls.element());
00690 }
00691 }
00692
00693 BoolExpr
00694 element(const BoolVarArgs& b, const LinIntExpr& idx) {
00695 return BoolExpr(new BElementExpr(b,idx));
00696 }
00697
00698 }
00699
00700