set-expr.cpp
Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 00002 /* 00003 * Main authors: 00004 * Guido Tack <tack@gecode.org> 00005 * Christian Schulte <schulte@gecode.org> 00006 * 00007 * Copyright: 00008 * Guido Tack, 2010 00009 * Christian Schulte, 2004 00010 * 00011 * Last modified: 00012 * $Date: 2010-07-14 20:32:01 +0200 (Wed, 14 Jul 2010) $ by $Author: schulte $ 00013 * $Revision: 11195 $ 00014 * 00015 * This file is part of Gecode, the generic constraint 00016 * development environment: 00017 * http://www.gecode.org 00018 * 00019 * Permission is hereby granted, free of charge, to any person obtaining 00020 * a copy of this software and associated documentation files (the 00021 * "Software"), to deal in the Software without restriction, including 00022 * without limitation the rights to use, copy, modify, merge, publish, 00023 * distribute, sublicense, and/or sell copies of the Software, and to 00024 * permit persons to whom the Software is furnished to do so, subject to 00025 * the following conditions: 00026 * 00027 * The above copyright notice and this permission notice shall be 00028 * included in all copies or substantial portions of the Software. 00029 * 00030 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 00031 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 00032 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 00033 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE 00034 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION 00035 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION 00036 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 00037 * 00038 */ 00039 00040 #include <gecode/minimodel.hh> 00041 00042 #ifdef GECODE_HAS_SET_VARS 00043 00044 namespace Gecode { 00045 00046 /* 00047 * Operations for nodes 00048 * 00049 */ 00050 bool 00051 SetExpr::Node::decrement(void) { 00052 if (--use == 0) { 00053 if ((l != NULL) && l->decrement()) 00054 delete l; 00055 if ((r != NULL) && r->decrement()) 00056 delete r; 00057 return true; 00058 } 00059 return false; 00060 } 00061 00062 00063 const SetExpr& 00064 SetExpr::operator =(const SetExpr& e) { 00065 if (this != &e) { 00066 if (n != NULL && n->decrement()) 00067 delete n; 00068 n = e.n; 00069 n->use++; 00070 } 00071 return *this; 00072 } 00073 00074 SetExpr::~SetExpr(void) { 00075 if (n != NULL && n->decrement()) 00076 delete n; 00077 } 00078 00079 /* 00080 * Operations for negation normalform 00081 * 00082 */ 00083 forceinline void 00084 SetExpr::NNF::operator delete(void*) {} 00085 00086 forceinline void 00087 SetExpr::NNF::operator delete(void*, Region&) {} 00088 00089 forceinline void* 00090 SetExpr::NNF::operator new(size_t s, Region& r) { 00091 return r.ralloc(s); 00092 } 00093 00094 void 00095 SetExpr::NNF::post(Home home, SetRelType srt, SetVar s) const { 00096 switch (t) { 00097 case NT_VAR: 00098 if (neg) { 00099 switch (srt) { 00100 case SRT_EQ: 00101 rel(home, u.a.x->x, SRT_CMPL, s); 00102 break; 00103 case SRT_CMPL: 00104 rel(home, u.a.x->x, SRT_EQ, s); 00105 break; 00106 default: 00107 SetVar bc(home,IntSet::empty, 00108 IntSet(Set::Limits::min,Set::Limits::max)); 00109 rel(home, s, SRT_CMPL, bc); 00110 rel(home, u.a.x->x, srt, bc); 00111 break; 00112 } 00113 } else 00114 rel(home, u.a.x->x, srt, s); 00115 break; 00116 case NT_CONST: 00117 { 00118 IntSet ss; 00119 if (neg) { 00120 IntSetRanges sr(u.a.x->s); 00121 Set::RangesCompl<IntSetRanges> src(sr); 00122 ss = IntSet(src); 00123 } else { 00124 ss = u.a.x->s; 00125 } 00126 switch (srt) { 00127 case SRT_SUB: srt = SRT_SUP; break; 00128 case SRT_SUP: srt = SRT_SUB; break; 00129 default: break; 00130 } 00131 dom(home, s, srt, ss); 00132 } 00133 break; 00134 case NT_LEXP: 00135 { 00136 IntVar iv = u.a.x->e.post(home,ICL_DEF); 00137 if (neg) { 00138 SetVar ic(home,IntSet::empty, 00139 IntSet(Set::Limits::min,Set::Limits::max)); 00140 rel(home, iv, SRT_CMPL, ic); 00141 rel(home,ic,srt,s); 00142 } else { 00143 rel(home,iv,srt,s); 00144 } 00145 } 00146 break; 00147 case NT_INTER: 00148 { 00149 SetVarArgs bs(p+n); 00150 int i=0; 00151 post(home, NT_INTER, bs, i); 00152 if (i == 2) { 00153 rel(home, bs[0], SOT_INTER, bs[1], srt, s); 00154 } else { 00155 if (srt == SRT_EQ) 00156 rel(home, SOT_INTER, bs, s); 00157 else { 00158 SetVar bc(home,IntSet::empty, 00159 IntSet(Set::Limits::min,Set::Limits::max)); 00160 rel(home, SOT_INTER, bs, bc); 00161 rel(home, bc, srt, s); 00162 } 00163 } 00164 } 00165 break; 00166 case NT_UNION: 00167 { 00168 SetVarArgs bs(p+n); 00169 int i=0; 00170 post(home, NT_UNION, bs, i); 00171 if (i == 2) { 00172 rel(home, bs[0], SOT_UNION, bs[1], srt, s); 00173 } else { 00174 if (srt == SRT_EQ) 00175 rel(home, SOT_UNION, bs, s); 00176 else { 00177 SetVar bc(home,IntSet::empty, 00178 IntSet(Set::Limits::min,Set::Limits::max)); 00179 rel(home, SOT_UNION, bs, bc); 00180 rel(home, bc, srt, s); 00181 } 00182 } 00183 } 00184 break; 00185 case NT_DUNION: 00186 { 00187 SetVarArgs bs(p+n); 00188 int i=0; 00189 post(home, NT_DUNION, bs, i); 00190 00191 if (i == 2) { 00192 if (neg) { 00193 if (srt == SRT_CMPL) { 00194 rel(home, bs[0], SOT_DUNION, bs[1], srt, s); 00195 } else { 00196 SetVar bc(home,IntSet::empty, 00197 IntSet(Set::Limits::min,Set::Limits::max)); 00198 rel(home,s,SRT_CMPL,bc); 00199 rel(home, bs[0], SOT_DUNION, bs[1], srt, bc); 00200 } 00201 } else { 00202 rel(home, bs[0], SOT_DUNION, bs[1], srt, s); 00203 } 00204 } else { 00205 if (neg) { 00206 if (srt == SRT_CMPL) { 00207 rel(home, SOT_DUNION, bs, s); 00208 } else { 00209 SetVar br(home,IntSet::empty, 00210 IntSet(Set::Limits::min,Set::Limits::max)); 00211 rel(home, SOT_DUNION, bs, br); 00212 if (srt == SRT_EQ) 00213 rel(home, br, SRT_CMPL, s); 00214 else { 00215 SetVar bc(home,IntSet::empty, 00216 IntSet(Set::Limits::min,Set::Limits::max)); 00217 rel(home, br, srt, bc); 00218 rel(home, bc, SRT_CMPL, s); 00219 } 00220 } 00221 } else { 00222 if (srt == SRT_EQ) 00223 rel(home, SOT_DUNION, bs, s); 00224 else { 00225 SetVar br(home,IntSet::empty, 00226 IntSet(Set::Limits::min,Set::Limits::max)); 00227 rel(home, SOT_DUNION, bs, br); 00228 rel(home, br, srt, s); 00229 } 00230 } 00231 } 00232 } 00233 break; 00234 default: 00235 GECODE_NEVER; 00236 } 00237 } 00238 00239 void 00240 SetExpr::NNF::post(Home home, SetRelType srt, SetVar s, BoolVar b) const { 00241 switch (t) { 00242 case NT_VAR: 00243 if (neg) { 00244 switch (srt) { 00245 case SRT_EQ: 00246 rel(home, u.a.x->x, SRT_CMPL, s, b); 00247 break; 00248 case SRT_CMPL: 00249 rel(home, u.a.x->x, SRT_EQ, s, b); 00250 break; 00251 default: 00252 SetVar bc(home,IntSet::empty, 00253 IntSet(Set::Limits::min,Set::Limits::max)); 00254 rel(home, s, SRT_CMPL, bc); 00255 rel(home, u.a.x->x, srt, bc, b); 00256 break; 00257 } 00258 } else 00259 rel(home, u.a.x->x, srt, s, b); 00260 break; 00261 case NT_CONST: 00262 { 00263 IntSet ss; 00264 if (neg) { 00265 IntSetRanges sr(u.a.x->s); 00266 Set::RangesCompl<IntSetRanges> src(sr); 00267 ss = IntSet(src); 00268 } else { 00269 ss = u.a.x->s; 00270 } 00271 dom(home, s, srt, ss, b); 00272 } 00273 break; 00274 case NT_LEXP: 00275 { 00276 IntVar iv = u.a.x->e.post(home,ICL_DEF); 00277 if (neg) { 00278 SetVar ic(home,IntSet::empty, 00279 IntSet(Set::Limits::min,Set::Limits::max)); 00280 rel(home, iv, SRT_CMPL, ic); 00281 rel(home,ic,srt,s,b); 00282 } else { 00283 rel(home,iv,srt,s,b); 00284 } 00285 } 00286 case NT_INTER: 00287 { 00288 SetVarArgs bs(p+n); 00289 int i=0; 00290 post(home, NT_INTER, bs, i); 00291 SetVar br(home,IntSet::empty, 00292 IntSet(Set::Limits::min,Set::Limits::max)); 00293 rel(home, SOT_INTER, bs, br); 00294 rel(home, br, srt, s, b); 00295 } 00296 break; 00297 case NT_UNION: 00298 { 00299 SetVarArgs bs(p+n); 00300 int i=0; 00301 post(home, NT_UNION, bs, i); 00302 SetVar br(home,IntSet::empty, 00303 IntSet(Set::Limits::min,Set::Limits::max)); 00304 rel(home, SOT_UNION, bs, br); 00305 rel(home, br, srt, s, b); 00306 } 00307 break; 00308 case NT_DUNION: 00309 { 00310 SetVarArgs bs(p+n); 00311 int i=0; 00312 post(home, NT_DUNION, bs, i); 00313 00314 if (neg) { 00315 SetVar br(home,IntSet::empty, 00316 IntSet(Set::Limits::min,Set::Limits::max)); 00317 rel(home, SOT_DUNION, bs, br); 00318 if (srt == SRT_CMPL) 00319 rel(home, br, SRT_EQ, s, b); 00320 else if (srt == SRT_EQ) 00321 rel(home, br, SRT_CMPL, s, b); 00322 else { 00323 SetVar bc(home,IntSet::empty, 00324 IntSet(Set::Limits::min,Set::Limits::max)); 00325 rel(home, br, srt, bc); 00326 rel(home, bc, SRT_CMPL, s, b); 00327 } 00328 } else { 00329 SetVar br(home,IntSet::empty, 00330 IntSet(Set::Limits::min,Set::Limits::max)); 00331 rel(home, SOT_DUNION, bs, br); 00332 rel(home, br, srt, s, b); 00333 } 00334 } 00335 break; 00336 default: 00337 GECODE_NEVER; 00338 } 00339 } 00340 00341 void 00342 SetExpr::NNF::post(Home home, NodeType t, 00343 SetVarArgs& b, int& i) const { 00344 if (this->t != t) { 00345 switch (this->t) { 00346 case NT_VAR: 00347 if (neg) { 00348 SetVar xc(home,IntSet::empty, 00349 IntSet(Set::Limits::min,Set::Limits::max)); 00350 rel(home, xc, SRT_CMPL, u.a.x->x); 00351 b[i++]=xc; 00352 } else { 00353 b[i++]=u.a.x->x; 00354 } 00355 break; 00356 default: 00357 { 00358 SetVar s(home,IntSet::empty, 00359 IntSet(Set::Limits::min,Set::Limits::max)); 00360 post(home,SRT_EQ,s); 00361 b[i++] = s; 00362 } 00363 break; 00364 } 00365 } else { 00366 u.b.l->post(home, t, b, i); 00367 u.b.r->post(home, t, b, i); 00368 } 00369 } 00370 00371 void 00372 SetExpr::NNF::post(Home home, SetRelType srt, const NNF* n) const { 00373 if (n->t == NT_VAR && !n->neg) { 00374 post(home,srt,n->u.a.x->x); 00375 } else if (t == NT_VAR && !neg) { 00376 SetRelType n_srt; 00377 switch (srt) { 00378 case SRT_SUB: n_srt = SRT_SUP; break; 00379 case SRT_SUP: n_srt = SRT_SUB; break; 00380 default: n_srt = srt; 00381 } 00382 n->post(home,n_srt,this); 00383 } else { 00384 SetVar nx(home,IntSet::empty, 00385 IntSet(Set::Limits::min,Set::Limits::max)); 00386 n->post(home,SRT_EQ,nx); 00387 post(home,srt,nx); 00388 } 00389 } 00390 00391 void 00392 SetExpr::NNF::post(Home home, BoolVar b, bool t, 00393 SetRelType srt, const NNF* n) const { 00394 if (t) { 00395 if (n->t == NT_VAR && !n->neg) { 00396 post(home,srt,n->u.a.x->x,b); 00397 } else if (t == NT_VAR && !neg) { 00398 SetRelType n_srt; 00399 switch (srt) { 00400 case SRT_SUB: n_srt = SRT_SUP; break; 00401 case SRT_SUP: n_srt = SRT_SUB; break; 00402 default: n_srt = srt; 00403 } 00404 n->post(home,b,true,n_srt,this); 00405 } else { 00406 SetVar nx(home,IntSet::empty, 00407 IntSet(Set::Limits::min,Set::Limits::max)); 00408 n->post(home,SRT_EQ,nx); 00409 post(home,srt,nx,b); 00410 } 00411 } else if (srt == SRT_EQ) { 00412 post(home,b,true,SRT_NQ,n); 00413 } else if (srt == SRT_NQ) { 00414 post(home,b,true,SRT_EQ,n); 00415 } else { 00416 BoolVar nb(home,0,1); 00417 rel(home,b,IRT_NQ,nb); 00418 post(home,nb,true,srt,n); 00419 } 00420 } 00421 00422 SetExpr::NNF* 00423 SetExpr::NNF::nnf(Region& r, Node* n, bool neg) { 00424 switch (n->t) { 00425 case NT_VAR: case NT_CONST: case NT_LEXP: 00426 { 00427 NNF* x = new (r) NNF; 00428 x->t = n->t; x->neg = neg; x->u.a.x = n; 00429 if (neg) { 00430 x->p = 0; x->n = 1; 00431 } else { 00432 x->p = 1; x->n = 0; 00433 } 00434 return x; 00435 } 00436 case NT_CMPL: 00437 return nnf(r,n->l,!neg); 00438 case NT_INTER: case NT_UNION: case NT_DUNION: 00439 { 00440 NodeType t; bool xneg; 00441 if (n->t == NT_DUNION) { 00442 t = n->t; xneg = neg; neg = false; 00443 } else { 00444 t = ((n->t == NT_INTER) == neg) ? NT_UNION : NT_INTER; 00445 xneg = false; 00446 } 00447 NNF* x = new (r) NNF; 00448 x->neg = xneg; 00449 x->t = t; 00450 x->u.b.l = nnf(r,n->l,neg); 00451 x->u.b.r = nnf(r,n->r,neg); 00452 int p_l, n_l; 00453 if ((x->u.b.l->t == t) || (x->u.b.l->t == NT_VAR)) { 00454 p_l=x->u.b.l->p; n_l=x->u.b.l->n; 00455 } else { 00456 p_l=1; n_l=0; 00457 } 00458 int p_r, n_r; 00459 if ((x->u.b.r->t == t) || (x->u.b.r->t == NT_VAR)) { 00460 p_r=x->u.b.r->p; n_r=x->u.b.r->n; 00461 } else { 00462 p_r=1; n_r=0; 00463 } 00464 x->p = p_l+p_r; 00465 x->n = n_l+n_r; 00466 return x; 00467 } 00468 default: 00469 GECODE_NEVER; 00470 } 00471 GECODE_NEVER; 00472 return NULL; 00473 } 00474 00475 00476 SetExpr 00477 operator &(const SetExpr& l, const SetExpr& r) { 00478 return SetExpr(l,SetExpr::NT_INTER,r); 00479 } 00480 SetExpr 00481 operator |(const SetExpr& l, const SetExpr& r) { 00482 return SetExpr(l,SetExpr::NT_UNION,r); 00483 } 00484 SetExpr 00485 operator +(const SetExpr& l, const SetExpr& r) { 00486 return SetExpr(l,SetExpr::NT_DUNION,r); 00487 } 00488 SetExpr 00489 operator -(const SetExpr& e) { 00490 return SetExpr(e,SetExpr::NT_CMPL); 00491 } 00492 SetExpr 00493 operator -(const SetExpr& l, const SetExpr& r) { 00494 return SetExpr(l,SetExpr::NT_INTER,-r); 00495 } 00496 SetExpr 00497 singleton(const LinExpr& e) { 00498 return SetExpr(e); 00499 } 00500 00501 SetExpr 00502 inter(const SetVarArgs& x) { 00503 if (x.size() == 0) 00504 return SetExpr(IntSet(Set::Limits::min,Set::Limits::max)); 00505 SetExpr r(x[0]); 00506 for (int i=1; i<x.size(); i++) 00507 r = (r & x[i]); 00508 return r; 00509 } 00510 SetExpr 00511 setunion(const SetVarArgs& x) { 00512 if (x.size() == 0) 00513 return SetExpr(IntSet::empty); 00514 SetExpr r(x[0]); 00515 for (int i=1; i<x.size(); i++) 00516 r = (r | x[i]); 00517 return r; 00518 } 00519 SetExpr 00520 setdunion(const SetVarArgs& x) { 00521 if (x.size() == 0) 00522 return SetExpr(IntSet::empty); 00523 SetExpr r(x[0]); 00524 for (int i=1; i<x.size(); i++) 00525 r = (r + x[i]); 00526 return r; 00527 } 00528 00529 namespace MiniModel { 00531 class GECODE_MINIMODEL_EXPORT SetNonLinExpr : public NonLinExpr { 00532 public: 00534 enum SetNonLinExprType { 00535 SNLE_CARD, 00536 SNLE_MIN, 00537 SNLE_MAX 00538 } t; 00540 SetExpr e; 00542 SetNonLinExpr(const SetExpr& e0, SetNonLinExprType t0) 00543 : t(t0), e(e0) {} 00545 virtual IntVar post(Home home, IntVar* ret, IntConLevel) const { 00546 IntVar m = result(home,ret); 00547 switch (t) { 00548 case SNLE_CARD: 00549 cardinality(home, e.post(home), m); 00550 break; 00551 case SNLE_MIN: 00552 min(home, e.post(home), m); 00553 break; 00554 case SNLE_MAX: 00555 max(home, e.post(home), m); 00556 break; 00557 default: 00558 GECODE_NEVER; 00559 break; 00560 } 00561 return m; 00562 } 00563 virtual void post(Home home, IntRelType irt, int c, 00564 IntConLevel icl) const { 00565 if (t==SNLE_CARD && irt!=IRT_NQ) { 00566 switch (irt) { 00567 case IRT_LQ: 00568 cardinality(home, e.post(home), 00569 0U, 00570 static_cast<unsigned int>(c)); 00571 break; 00572 case IRT_LE: 00573 cardinality(home, e.post(home), 00574 0U, 00575 static_cast<unsigned int>(c-1)); 00576 break; 00577 case IRT_GQ: 00578 cardinality(home, e.post(home), 00579 static_cast<unsigned int>(c), 00580 Set::Limits::card); 00581 break; 00582 case IRT_GR: 00583 cardinality(home, e.post(home), 00584 static_cast<unsigned int>(c+1), 00585 Set::Limits::card); 00586 break; 00587 case IRT_EQ: 00588 cardinality(home, e.post(home), 00589 static_cast<unsigned int>(c), 00590 static_cast<unsigned int>(c)); 00591 break; 00592 default: 00593 GECODE_NEVER; 00594 } 00595 } else if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) { 00596 c = (irt==IRT_GQ ? c : c+1); 00597 dom(home, e.post(home), SRT_SUB, c, Set::Limits::max); 00598 } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) { 00599 c = (irt==IRT_LQ ? c : c-1); 00600 dom(home, e.post(home), SRT_SUB, Set::Limits::min, c); 00601 } else { 00602 rel(home, post(home,NULL,icl), irt, c); 00603 } 00604 } 00605 virtual void post(Home home, IntRelType irt, int c, 00606 BoolVar b, IntConLevel icl) const { 00607 if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) { 00608 c = (irt==IRT_GQ ? c : c+1); 00609 dom(home, e.post(home), SRT_SUB, c, Set::Limits::max, b); 00610 } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) { 00611 c = (irt==IRT_LQ ? c : c-1); 00612 dom(home, e.post(home), SRT_SUB, Set::Limits::min, c, b); 00613 } else { 00614 rel(home, post(home,NULL,icl), irt, c, b); 00615 } 00616 } 00617 }; 00618 } 00619 00620 LinExpr 00621 cardinality(const SetExpr& e) { 00622 return LinExpr(new MiniModel::SetNonLinExpr(e, 00623 MiniModel::SetNonLinExpr::SNLE_CARD)); 00624 } 00625 LinExpr 00626 min(const SetExpr& e) { 00627 return LinExpr(new MiniModel::SetNonLinExpr(e, 00628 MiniModel::SetNonLinExpr::SNLE_MIN)); 00629 } 00630 LinExpr 00631 max(const SetExpr& e) { 00632 return LinExpr(new MiniModel::SetNonLinExpr(e, 00633 MiniModel::SetNonLinExpr::SNLE_MAX)); 00634 } 00635 00636 /* 00637 * Posting set expressions 00638 * 00639 */ 00640 SetVar 00641 expr(Home home, const SetExpr& e) { 00642 if (!home.failed()) 00643 return e.post(home); 00644 SetVar x(home,IntSet::empty,IntSet::empty); 00645 return x; 00646 } 00647 00648 } 00649 00650 #endif 00651 00652 // STATISTICS: minimodel-any