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