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 forceinline void*
00049 BoolExpr::Node::operator new(size_t size) {
00050 return heap.ralloc(size);
00051 }
00052
00053 forceinline void
00054 BoolExpr::Node::operator delete(void* p, size_t) {
00055 heap.rfree(p);
00056 }
00057
00058 forceinline
00059 BoolExpr::Node::Node(void) : use(1) {}
00060
00061 bool
00062 BoolExpr::Node::decrement(void) {
00063 if (--use == 0) {
00064 if ((l != NULL) && l->decrement())
00065 delete l;
00066 if ((r != NULL) && r->decrement())
00067 delete r;
00068 return true;
00069 }
00070 return false;
00071 }
00072
00073 BoolExpr::BoolExpr(const BoolVar& x) : n(new Node) {
00074 n->same = 1;
00075 n->t = NT_VAR;
00076 n->l = NULL;
00077 n->r = NULL;
00078 n->x = x;
00079 }
00080
00081 BoolExpr::BoolExpr(const BoolExpr& l, NodeType t, const BoolExpr& r)
00082 : n(new Node) {
00083 unsigned int ls = ((l.n->t == t) || (l.n->t == NT_VAR)) ? l.n->same : 1;
00084 unsigned int rs = ((r.n->t == t) || (r.n->t == NT_VAR)) ? r.n->same : 1;
00085 n->same = ls+rs;
00086 n->t = t;
00087 n->l = l.n;
00088 n->l->use++;
00089 n->r = r.n;
00090 n->r->use++;
00091 }
00092
00093 BoolExpr::BoolExpr(const BoolExpr& l, NodeType t) {
00094 (void) t;
00095 assert(t == NT_NOT);
00096 if (l.n->t == NT_NOT) {
00097 n = l.n->l;
00098 n->use++;
00099 } else {
00100 n = new Node;
00101 n->same = 1;
00102 n->t = NT_NOT;
00103 n->l = l.n;
00104 n->l->use++;
00105 n->r = NULL;
00106 }
00107 }
00108
00109 BoolExpr::BoolExpr(const LinRel<IntVar>& rl)
00110 : n(new Node) {
00111 n->same = 1;
00112 n->t = NT_RLIN_INT;
00113 n->l = NULL;
00114 n->r = NULL;
00115 n->rl_int = rl;
00116 }
00117
00118 BoolExpr::BoolExpr(const LinRel<BoolVar>& rl)
00119 : n(new Node) {
00120 n->same = 1;
00121 n->t = NT_RLIN_BOOL;
00122 n->l = NULL;
00123 n->r = NULL;
00124 n->rl_bool = rl;
00125 }
00126
00127 const BoolExpr&
00128 BoolExpr::operator =(const BoolExpr& e) {
00129 if (this != &e) {
00130 if (n->decrement())
00131 delete n;
00132 n = e.n;
00133 n->use++;
00134 }
00135 return *this;
00136 }
00137
00138 BoolExpr::~BoolExpr(void) {
00139 if (n->decrement())
00140 delete n;
00141 }
00142
00143
00144
00145
00146
00147 forceinline void
00148 BoolExpr::NNF::operator delete(void*) {}
00149
00150 forceinline void
00151 BoolExpr::NNF::operator delete(void*, Region&) {}
00152
00153 forceinline void*
00154 BoolExpr::NNF::operator new(size_t s, Region& r) {
00155 return r.ralloc(s);
00156 }
00157
00158 BoolVar
00159 BoolExpr::NNF::post(Home home, IntConLevel icl) const {
00160 if ((t == NT_VAR) && !u.a.neg)
00161 return u.a.x->x;
00162 BoolVar b(home,0,1);
00163 switch (t) {
00164 case NT_VAR:
00165 assert(u.a.neg);
00166 rel(home, u.a.x->x, IRT_NQ, b);
00167 break;
00168 case NT_RLIN_INT:
00169 u.a.x->rl_int.post(home, b, !u.a.neg, icl);
00170 break;
00171 case NT_RLIN_BOOL:
00172 u.a.x->rl_bool.post(home, b, !u.a.neg, icl);
00173 break;
00174 case NT_AND:
00175 {
00176 BoolVarArgs bp(p), bn(n);
00177 int ip=0, in=0;
00178 post(home, NT_AND, bp, bn, ip, in, icl);
00179 clause(home, BOT_AND, bp, bn, b);
00180 }
00181 break;
00182 case NT_OR:
00183 {
00184 BoolVarArgs bp(p), bn(n);
00185 int ip=0, in=0;
00186 post(home, NT_OR, bp, bn, ip, in, icl);
00187 clause(home, BOT_OR, bp, bn, b);
00188 }
00189 break;
00190 case NT_EQV:
00191 {
00192 bool n = false;
00193 BoolVar l;
00194 if (u.b.l->t == NT_VAR) {
00195 l = u.b.l->u.a.x->x;
00196 if (u.b.l->u.a.neg) n = !n;
00197 } else {
00198 l = u.b.l->post(home,icl);
00199 }
00200 BoolVar r;
00201 if (u.b.r->t == NT_VAR) {
00202 r = u.b.r->u.a.x->x;
00203 if (u.b.r->u.a.neg) n = !n;
00204 } else {
00205 r = u.b.r->post(home,icl);
00206 }
00207 rel(home, l, n ? BOT_XOR : BOT_EQV, r, b, icl);
00208 }
00209 break;
00210 default:
00211 GECODE_NEVER;
00212 }
00213 return b;
00214 }
00215
00216 void
00217 BoolExpr::NNF::post(Home home, NodeType t,
00218 BoolVarArgs& bp, BoolVarArgs& bn,
00219 int& ip, int& in,
00220 IntConLevel icl) const {
00221 if (this->t != t) {
00222 switch (this->t) {
00223 case NT_VAR:
00224 if (u.a.neg) {
00225 bn[in++]=u.a.x->x;
00226 } else {
00227 bp[ip++]=u.a.x->x;
00228 }
00229 break;
00230 case NT_RLIN_INT:
00231 {
00232 BoolVar b(home,0,1);
00233 u.a.x->rl_int.post(home, b, !u.a.neg, icl);
00234 bp[ip++]=b;
00235 }
00236 break;
00237 case NT_RLIN_BOOL:
00238 {
00239 BoolVar b(home,0,1);
00240 u.a.x->rl_bool.post(home, b, !u.a.neg, icl);
00241 bp[ip++]=b;
00242 }
00243 break;
00244 default:
00245 bp[ip++] = post(home, icl);
00246 break;
00247 }
00248 } else {
00249 u.b.l->post(home, t, bp, bn, ip, in, icl);
00250 u.b.r->post(home, t, bp, bn, ip, in, icl);
00251 }
00252 }
00253
00254 void
00255 BoolExpr::NNF::post(Home home, bool b, IntConLevel icl) const {
00256 if (b) {
00257 switch (t) {
00258 case NT_VAR:
00259 rel(home, u.a.x->x, IRT_EQ, u.a.neg ? 0 : 1);
00260 break;
00261 case NT_RLIN_INT:
00262 u.a.x->rl_int.post(home, !u.a.neg, icl);
00263 break;
00264 case NT_RLIN_BOOL:
00265 u.a.x->rl_bool.post(home, !u.a.neg, icl);
00266 break;
00267 case NT_AND:
00268 u.b.l->post(home, true, icl);
00269 u.b.r->post(home, true, icl);
00270 break;
00271 case NT_OR:
00272 {
00273 BoolVarArgs bp(p), bn(n);
00274 int ip=0, in=0;
00275 post(home, NT_OR, bp, bn, ip, in, icl);
00276 clause(home, BOT_OR, bp, bn, 1);
00277 }
00278 break;
00279 case NT_EQV:
00280 rel(home, post(home, icl), IRT_EQ, 1);
00281 break;
00282 default:
00283 GECODE_NEVER;
00284 }
00285 } else {
00286 switch (t) {
00287 case NT_VAR:
00288 rel(home, u.a.x->x, IRT_EQ, u.a.neg ? 1 : 0);
00289 break;
00290 case NT_RLIN_INT:
00291 u.a.x->rl_int.post(home, u.a.neg, icl);
00292 break;
00293 case NT_RLIN_BOOL:
00294 u.a.x->rl_bool.post(home, u.a.neg, icl);
00295 break;
00296 case NT_AND:
00297 {
00298 BoolVarArgs bp(p), bn(n);
00299 int ip=0, in=0;
00300 post(home, NT_AND, bp, bn, ip, in, icl);
00301 clause(home, BOT_AND, bp, bn, 0);
00302 }
00303 break;
00304 case NT_OR:
00305 u.b.l->post(home, false, icl);
00306 u.b.r->post(home, false, icl);
00307 break;
00308 case NT_EQV:
00309 rel(home, post(home, icl), IRT_EQ, 0);
00310 break;
00311 default:
00312 GECODE_NEVER;
00313 }
00314 }
00315 }
00316
00317 BoolExpr::NNF*
00318 BoolExpr::NNF::nnf(Region& r, Node* n, bool neg) {
00319 switch (n->t) {
00320 case NT_VAR: case NT_RLIN_INT: case NT_RLIN_BOOL:
00321 {
00322 NNF* x = new (r) NNF;
00323 x->t = n->t; x->u.a.neg = neg; x->u.a.x = n;
00324 if (neg) {
00325 x->p = 0; x->n = 1;
00326 } else {
00327 x->p = 1; x->n = 0;
00328 }
00329 return x;
00330 }
00331 case NT_NOT:
00332 return nnf(r,n->l,!neg);
00333 case NT_AND: case NT_OR:
00334 {
00335 NodeType t = ((n->t == NT_AND) == neg) ? NT_OR : NT_AND;
00336 NNF* x = new (r) NNF;
00337 x->t = t;
00338 x->u.b.l = nnf(r,n->l,neg);
00339 x->u.b.r = nnf(r,n->r,neg);
00340 unsigned int p_l, n_l;
00341 if ((x->u.b.l->t == t) || (x->u.b.l->t == NT_VAR)) {
00342 p_l=x->u.b.l->p; n_l=x->u.b.l->n;
00343 } else {
00344 p_l=1; n_l=0;
00345 }
00346 unsigned int p_r, n_r;
00347 if ((x->u.b.r->t == t) || (x->u.b.r->t == NT_VAR)) {
00348 p_r=x->u.b.r->p; n_r=x->u.b.r->n;
00349 } else {
00350 p_r=1; n_r=0;
00351 }
00352 x->p = p_l+p_r;
00353 x->n = n_l+n_r;
00354 return x;
00355 }
00356 case NT_EQV:
00357 {
00358 NNF* x = new (r) NNF;
00359 x->t = NT_EQV;
00360 x->u.b.l = nnf(r,n->l,neg);
00361 x->u.b.r = nnf(r,n->r,false);
00362 x->p = 2; x->n = 0;
00363 return x;
00364 }
00365 default:
00366 GECODE_NEVER;
00367 }
00368 GECODE_NEVER;
00369 return NULL;
00370 }
00371
00372 }
00373
00374