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
00039
00040 #include <gecode/minimodel.hh>
00041
00042 namespace Gecode {
00043
00044
00045
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
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
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
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