Generated on Tue May 22 09:40:10 2018 for Gecode by doxygen 1.6.3

bool-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  *     Vincent Barichard <Vincent.Barichard@univ-angers.fr>
00007  *
00008  *  Copyright:
00009  *     Guido Tack, 2004
00010  *     Christian Schulte, 2004
00011  *     Vincent Barichard, 2012
00012  *
00013  *  This file is part of Gecode, the generic constraint
00014  *  development environment:
00015  *     http://www.gecode.org
00016  *
00017  *  Permission is hereby granted, free of charge, to any person obtaining
00018  *  a copy of this software and associated documentation files (the
00019  *  "Software"), to deal in the Software without restriction, including
00020  *  without limitation the rights to use, copy, modify, merge, publish,
00021  *  distribute, sublicense, and/or sell copies of the Software, and to
00022  *  permit persons to whom the Software is furnished to do so, subject to
00023  *  the following conditions:
00024  *
00025  *  The above copyright notice and this permission notice shall be
00026  *  included in all copies or substantial portions of the Software.
00027  *
00028  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00029  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00030  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00031  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00032  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00033  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00034  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
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    * Operations for nodes
00084    *
00085    */
00086   BoolExpr::Node::Node(void)
00087     : use(1), l(NULL), r(NULL), m(NULL) {}
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 != NULL) && l->decrement())
00106         delete l;
00107       if ((r != NULL) && 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    = NULL;
00124     n->r    = NULL;
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    = NULL;
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    = NULL;
00161     n->r    = NULL;
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     = NULL;
00171     n->r     = NULL;
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    = NULL;
00182     n->r    = NULL;
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    = NULL;
00191     n->r    = NULL;
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    = NULL;
00201     n->r    = NULL;
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       GECODE_MINIMODEL_EXPORT
00254       static NNF* nnf(Region& r, Node* n, bool neg);
00256       GECODE_MINIMODEL_EXPORT
00257       void post(Home home, NodeType t,
00258                 BoolVarArgs& bp, BoolVarArgs& bn,
00259                 int& ip, int& in,
00260                 IntPropLevel ipl) const;
00262       GECODE_MINIMODEL_EXPORT
00263       BoolVar expr(Home home, IntPropLevel ipl) const;
00265       GECODE_MINIMODEL_EXPORT
00266       void rel(Home home, IntPropLevel ipl) const;
00268       static void* operator new(size_t s, Region& r);
00270       static void operator delete(void*);
00272       static void operator delete(void*, Region&);
00273     };
00274 
00275     /*
00276      * Operations for negation normalform
00277      *
00278      */
00279     forceinline void
00280     NNF::operator delete(void*) {}
00281 
00282     forceinline void
00283     NNF::operator delete(void*, Region&) {}
00284 
00285     forceinline void*
00286     NNF::operator new(size_t s, Region& r) {
00287       return r.ralloc(s);
00288     }
00289 
00290     BoolVar
00291     NNF::expr(Home home, IntPropLevel ipl) const {
00292       if ((t == BoolExpr::NT_VAR) && !u.a.neg)
00293         return u.a.x->x;
00294       BoolVar b(home,0,1);
00295       switch (t) {
00296       case BoolExpr::NT_VAR:
00297         assert(u.a.neg);
00298         Gecode::rel(home, u.a.x->x, IRT_NQ, b);
00299         break;
00300       case BoolExpr::NT_RLIN:
00301         u.a.x->rl.post(home, b, !u.a.neg, ipl);
00302         break;
00303 #ifdef GECODE_HAS_FLOAT_VARS
00304       case BoolExpr::NT_RLINFLOAT:
00305         u.a.x->rfl.post(home, b, !u.a.neg);
00306         break;
00307 #endif
00308 #ifdef GECODE_HAS_SET_VARS
00309       case BoolExpr::NT_RSET:
00310         u.a.x->rs.post(home, b, !u.a.neg);
00311         break;
00312 #endif
00313       case BoolExpr::NT_MISC:
00314         u.a.x->m->post(home, b, u.a.neg, ipl);
00315         break;
00316       case BoolExpr::NT_AND:
00317         {
00318           BoolVarArgs bp(p), bn(n);
00319           int ip=0, in=0;
00320           post(home, BoolExpr::NT_AND, bp, bn, ip, in, ipl);
00321           clause(home, BOT_AND, bp, bn, b);
00322         }
00323         break;
00324       case BoolExpr::NT_OR:
00325         {
00326           BoolVarArgs bp(p), bn(n);
00327           int ip=0, in=0;
00328           post(home, BoolExpr::NT_OR, bp, bn, ip, in, ipl);
00329           clause(home, BOT_OR, bp, bn, b);
00330         }
00331         break;
00332       case BoolExpr::NT_EQV:
00333         {
00334           bool n = false;
00335           BoolVar l;
00336           if (u.b.l->t == BoolExpr::NT_VAR) {
00337             l = u.b.l->u.a.x->x;
00338             if (u.b.l->u.a.neg) n = !n;
00339           } else {
00340             l = u.b.l->expr(home,ipl);
00341           }
00342           BoolVar r;
00343           if (u.b.r->t == BoolExpr::NT_VAR) {
00344             r = u.b.r->u.a.x->x;
00345             if (u.b.r->u.a.neg) n = !n;
00346           } else {
00347             r = u.b.r->expr(home,ipl);
00348           }
00349           Gecode::rel(home, l, n ? BOT_XOR : BOT_EQV, r, b, ipl);
00350         }
00351         break;
00352       default:
00353         GECODE_NEVER;
00354       }
00355       return b;
00356     }
00357 
00358     void
00359     NNF::post(Home home, NodeType t,
00360               BoolVarArgs& bp, BoolVarArgs& bn,
00361               int& ip, int& in,
00362               IntPropLevel ipl) const {
00363       if (this->t != t) {
00364         switch (this->t) {
00365         case BoolExpr::NT_VAR:
00366           if (u.a.neg) {
00367             bn[in++]=u.a.x->x;
00368           } else {
00369             bp[ip++]=u.a.x->x;
00370           }
00371           break;
00372         case BoolExpr::NT_RLIN:
00373           {
00374             BoolVar b(home,0,1);
00375             u.a.x->rl.post(home, b, !u.a.neg, ipl);
00376             bp[ip++]=b;
00377           }
00378           break;
00379 #ifdef GECODE_HAS_FLOAT_VARS
00380         case BoolExpr::NT_RLINFLOAT:
00381           {
00382             BoolVar b(home,0,1);
00383             u.a.x->rfl.post(home, b, !u.a.neg);
00384             bp[ip++]=b;
00385           }
00386           break;
00387 #endif
00388 #ifdef GECODE_HAS_SET_VARS
00389         case BoolExpr::NT_RSET:
00390           {
00391             BoolVar b(home,0,1);
00392             u.a.x->rs.post(home, b, !u.a.neg);
00393             bp[ip++]=b;
00394           }
00395           break;
00396 #endif
00397         case BoolExpr::NT_MISC:
00398           {
00399             BoolVar b(home,0,1);
00400             u.a.x->m->post(home, b, u.a.neg, ipl);
00401             bp[ip++]=b;
00402           }
00403           break;
00404         default:
00405           bp[ip++] = expr(home, ipl);
00406           break;
00407         }
00408       } else {
00409         u.b.l->post(home, t, bp, bn, ip, in, ipl);
00410         u.b.r->post(home, t, bp, bn, ip, in, ipl);
00411       }
00412     }
00413 
00414     void
00415     NNF::rel(Home home, IntPropLevel ipl) const {
00416       switch (t) {
00417       case BoolExpr::NT_VAR:
00418         Gecode::rel(home, u.a.x->x, IRT_EQ, u.a.neg ? 0 : 1);
00419         break;
00420       case BoolExpr::NT_RLIN:
00421         u.a.x->rl.post(home, !u.a.neg, ipl);
00422         break;
00423 #ifdef GECODE_HAS_FLOAT_VARS
00424       case BoolExpr::NT_RLINFLOAT:
00425         u.a.x->rfl.post(home, !u.a.neg);
00426         break;
00427 #endif
00428 #ifdef GECODE_HAS_SET_VARS
00429       case BoolExpr::NT_RSET:
00430         u.a.x->rs.post(home, !u.a.neg);
00431         break;
00432 #endif
00433       case BoolExpr::NT_MISC:
00434         {
00435           BoolVar b(home,!u.a.neg,!u.a.neg);
00436           u.a.x->m->post(home, b, false, ipl);
00437         }
00438         break;
00439       case BoolExpr::NT_AND:
00440         u.b.l->rel(home, ipl);
00441         u.b.r->rel(home, ipl);
00442         break;
00443       case BoolExpr::NT_OR:
00444         {
00445           BoolVarArgs bp(p), bn(n);
00446           int ip=0, in=0;
00447           post(home, BoolExpr::NT_OR, bp, bn, ip, in, ipl);
00448           clause(home, BOT_OR, bp, bn, 1);
00449         }
00450         break;
00451       case BoolExpr::NT_EQV:
00452         if (u.b.l->t==BoolExpr::NT_VAR &&
00453             u.b.r->t==BoolExpr::NT_RLIN) {
00454           u.b.r->u.a.x->rl.post(home, u.b.l->u.a.x->x,
00455                                 u.b.l->u.a.neg==u.b.r->u.a.neg, ipl);
00456         } else if (u.b.r->t==BoolExpr::NT_VAR &&
00457                    u.b.l->t==BoolExpr::NT_RLIN) {
00458           u.b.l->u.a.x->rl.post(home, u.b.r->u.a.x->x,
00459                                 u.b.l->u.a.neg==u.b.r->u.a.neg, ipl);
00460         } else if (u.b.l->t==BoolExpr::NT_RLIN) {
00461           u.b.l->u.a.x->rl.post(home, u.b.r->expr(home,ipl),
00462                                 !u.b.l->u.a.neg,ipl);
00463         } else if (u.b.r->t==BoolExpr::NT_RLIN) {
00464           u.b.r->u.a.x->rl.post(home, u.b.l->expr(home,ipl),
00465                                 !u.b.r->u.a.neg,ipl);
00466 #ifdef GECODE_HAS_FLOAT_VARS
00467         } else if (u.b.l->t==BoolExpr::NT_VAR &&
00468                    u.b.r->t==BoolExpr::NT_RLINFLOAT) {
00469           u.b.r->u.a.x->rfl.post(home, u.b.l->u.a.x->x,
00470                                  u.b.l->u.a.neg==u.b.r->u.a.neg);
00471         } else if (u.b.r->t==BoolExpr::NT_VAR &&
00472                    u.b.l->t==BoolExpr::NT_RLINFLOAT) {
00473           u.b.l->u.a.x->rfl.post(home, u.b.r->u.a.x->x,
00474                                  u.b.l->u.a.neg==u.b.r->u.a.neg);
00475         } else if (u.b.l->t==BoolExpr::NT_RLINFLOAT) {
00476           u.b.l->u.a.x->rfl.post(home, u.b.r->expr(home,ipl),
00477                                  !u.b.l->u.a.neg);
00478         } else if (u.b.r->t==BoolExpr::NT_RLINFLOAT) {
00479           u.b.r->u.a.x->rfl.post(home, u.b.l->expr(home,ipl),
00480                                  !u.b.r->u.a.neg);
00481 #endif
00482 #ifdef GECODE_HAS_SET_VARS
00483         } else if (u.b.l->t==BoolExpr::NT_VAR &&
00484                    u.b.r->t==BoolExpr::NT_RSET) {
00485           u.b.r->u.a.x->rs.post(home, u.b.l->u.a.x->x,
00486                                 u.b.l->u.a.neg==u.b.r->u.a.neg);
00487         } else if (u.b.r->t==BoolExpr::NT_VAR &&
00488                    u.b.l->t==BoolExpr::NT_RSET) {
00489           u.b.l->u.a.x->rs.post(home, u.b.r->u.a.x->x,
00490                                 u.b.l->u.a.neg==u.b.r->u.a.neg);
00491         } else if (u.b.l->t==BoolExpr::NT_RSET) {
00492           u.b.l->u.a.x->rs.post(home, u.b.r->expr(home,ipl),
00493                                 !u.b.l->u.a.neg);
00494         } else if (u.b.r->t==BoolExpr::NT_RSET) {
00495           u.b.r->u.a.x->rs.post(home, u.b.l->expr(home,ipl),
00496                                 !u.b.r->u.a.neg);
00497 #endif
00498         } else {
00499           Gecode::rel(home, expr(home, ipl), IRT_EQ, 1);
00500         }
00501         break;
00502       default:
00503         GECODE_NEVER;
00504       }
00505     }
00506 
00507     NNF*
00508     NNF::nnf(Region& r, Node* n, bool neg) {
00509       switch (n->t) {
00510       case BoolExpr::NT_VAR:
00511       case BoolExpr::NT_RLIN:
00512       case BoolExpr::NT_MISC:
00513   #ifdef GECODE_HAS_FLOAT_VARS
00514       case BoolExpr::NT_RLINFLOAT:
00515   #endif
00516   #ifdef GECODE_HAS_SET_VARS
00517       case BoolExpr::NT_RSET:
00518   #endif
00519         {
00520           NNF* x = new (r) NNF;
00521           x->t = n->t; x->u.a.neg = neg; x->u.a.x = n;
00522           if (neg) {
00523             x->p = 0; x->n = 1;
00524           } else {
00525             x->p = 1; x->n = 0;
00526           }
00527           return x;
00528         }
00529       case BoolExpr::NT_NOT:
00530         return nnf(r,n->l,!neg);
00531       case BoolExpr::NT_AND: case BoolExpr::NT_OR:
00532         {
00533           NodeType t = ((n->t == BoolExpr::NT_AND) == neg) ?
00534             BoolExpr::NT_OR : BoolExpr::NT_AND;
00535           NNF* x = new (r) NNF;
00536           x->t = t;
00537           x->u.b.l = nnf(r,n->l,neg);
00538           x->u.b.r = nnf(r,n->r,neg);
00539           int p_l, n_l;
00540           if ((x->u.b.l->t == t) ||
00541               (x->u.b.l->t == BoolExpr::NT_VAR)) {
00542             p_l=x->u.b.l->p; n_l=x->u.b.l->n;
00543           } else {
00544             p_l=1; n_l=0;
00545           }
00546           int p_r, n_r;
00547           if ((x->u.b.r->t == t) ||
00548               (x->u.b.r->t == BoolExpr::NT_VAR)) {
00549             p_r=x->u.b.r->p; n_r=x->u.b.r->n;
00550           } else {
00551             p_r=1; n_r=0;
00552           }
00553           x->p = p_l+p_r;
00554           x->n = n_l+n_r;
00555           return x;
00556         }
00557       case BoolExpr::NT_EQV:
00558         {
00559           NNF* x = new (r) NNF;
00560           x->t = BoolExpr::NT_EQV;
00561           x->u.b.l = nnf(r,n->l,neg);
00562           x->u.b.r = nnf(r,n->r,false);
00563           x->p = 2; x->n = 0;
00564           return x;
00565         }
00566       default:
00567         GECODE_NEVER;
00568       }
00569       GECODE_NEVER;
00570       return NULL;
00571     }
00572   }
00573 
00574   BoolVar
00575   BoolExpr::expr(Home home, IntPropLevel ipl) const {
00576     Region r;
00577     return NNF::nnf(r,n,false)->expr(home,ipl);
00578   }
00579 
00580   void
00581   BoolExpr::rel(Home home, IntPropLevel ipl) const {
00582     Region r;
00583     return NNF::nnf(r,n,false)->rel(home,ipl);
00584   }
00585 
00586 
00587   BoolExpr
00588   operator &&(const BoolExpr& l, const BoolExpr& r) {
00589     return BoolExpr(l,BoolExpr::NT_AND,r);
00590   }
00591   BoolExpr
00592   operator ||(const BoolExpr& l, const BoolExpr& r) {
00593     return BoolExpr(l,BoolExpr::NT_OR,r);
00594   }
00595   BoolExpr
00596   operator ^(const BoolExpr& l, const BoolExpr& r) {
00597     return BoolExpr(BoolExpr(l,BoolExpr::NT_EQV,r),BoolExpr::NT_NOT);
00598   }
00599 
00600   BoolExpr
00601   operator !(const BoolExpr& e) {
00602     return BoolExpr(e,BoolExpr::NT_NOT);
00603   }
00604 
00605   BoolExpr
00606   operator !=(const BoolExpr& l, const BoolExpr& r) {
00607     return !BoolExpr(l, BoolExpr::NT_EQV, r);
00608   }
00609   BoolExpr
00610   operator ==(const BoolExpr& l, const BoolExpr& r) {
00611     return BoolExpr(l, BoolExpr::NT_EQV, r);
00612   }
00613   BoolExpr
00614   operator >>(const BoolExpr& l, const BoolExpr& r) {
00615     return BoolExpr(BoolExpr(l,BoolExpr::NT_NOT),
00616                     BoolExpr::NT_OR,r);
00617   }
00618   BoolExpr
00619   operator <<(const BoolExpr& l, const BoolExpr& r) {
00620     return BoolExpr(BoolExpr(r,BoolExpr::NT_NOT),
00621                     BoolExpr::NT_OR,l);
00622   }
00623   /*
00624    * Posting Boolean expressions and relations
00625    *
00626    */
00627   BoolVar
00628   expr(Home home, const BoolExpr& e, IntPropLevel ipl) {
00629     PostInfo pi(home);
00630     if (!home.failed())
00631       return e.expr(home,ipl);
00632     BoolVar x(home,0,1);
00633     return x;
00634   }
00635 
00636   void
00637   rel(Home home, const BoolExpr& e, IntPropLevel ipl) {
00638     GECODE_POST;
00639     if (home.failed()) return;
00640     e.rel(home,ipl);
00641   }
00642 
00643   /*
00644    * Boolean element constraints
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, IntPropLevel ipl);
00664   };
00665 
00666   BElementExpr::BElementExpr(const BoolVarArgs& b, const LinIntExpr& idx)
00667     : a(static_cast<BoolExpr*>(heap.ralloc(sizeof(BoolExpr)*b.size()))), n(b.size()), idx(idx) {
00668     for (int i=b.size(); i--;)
00669       new (&a[i]) BoolExpr(b[i]);
00670   }
00671 
00672   BElementExpr::~BElementExpr(void) {
00673     heap.free<BoolExpr>(a,n);
00674   }
00675 
00676   void
00677   BElementExpr::post(Home home, BoolVar b, bool neg, IntPropLevel ipl) {
00678     IntVar z = idx.post(home, ipl);
00679     if (z.assigned() && (z.val() >= 0) && (z.val() < n)) {
00680       BoolExpr be = neg ? (a[z.val()] == !b) : (a[z.val()] == b);
00681       be.rel(home,ipl);
00682     } else {
00683       BoolVarArgs x(n);
00684       for (int i=n; i--;)
00685         x[i] = a[i].expr(home,ipl);
00686       BoolVar res = neg ? (!b).expr(home,ipl) : b;
00687       element(home, x, z, res, ipl);
00688     }
00689   }
00690 
00691   BoolExpr
00692   element(const BoolVarArgs& b, const LinIntExpr& idx) {
00693     return BoolExpr(new BElementExpr(b,idx));
00694   }
00695 
00696 }
00697 
00698 // STATISTICS: minimodel-any