Generated on Mon May 10 06:46:33 2010 for Gecode by doxygen 1.6.3

bool.cpp

Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
00002 /*
00003  *  Main authors:
00004  *     Christian Schulte <schulte@gecode.org>
00005  *
00006  *  Copyright:
00007  *     Christian Schulte, 2002
00008  *
00009  *  Last modified:
00010  *     $Date: 2010-03-03 17:40:32 +0100 (Wed, 03 Mar 2010) $ by $Author: schulte $
00011  *     $Revision: 10365 $
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/int/bool.hh>
00039 #include <gecode/int/rel.hh>
00040 
00041 namespace Gecode {
00042 
00043   namespace {
00044 
00045     forceinline void
00046     post_and(Home home, BoolVar x0, BoolVar x1, BoolVar x2) {
00047       using namespace Int;
00048       NegBoolView n0(x0); NegBoolView n1(x1); NegBoolView n2(x2);
00049       GECODE_ES_FAIL((Bool::Or<NegBoolView,NegBoolView,NegBoolView>
00050                            ::post(home,n0,n1,n2)));
00051     }
00052     forceinline void
00053     post_or(Home home, BoolVar x0, BoolVar x1, BoolVar x2) {
00054       using namespace Int;
00055       GECODE_ES_FAIL((Bool::Or<BoolView,BoolView,BoolView>
00056                            ::post(home,x0,x1,x2)));
00057     }
00058     forceinline void
00059     post_imp(Home home, BoolVar x0, BoolVar x1, BoolVar x2) {
00060       using namespace Int;
00061       NegBoolView n0(x0);
00062       GECODE_ES_FAIL((Bool::Or<NegBoolView,BoolView,BoolView>
00063                            ::post(home,n0,x1,x2)));
00064     }
00065     forceinline void
00066     post_eqv(Home home, BoolVar x0, BoolVar x1, BoolVar x2) {
00067       using namespace Int;
00068       GECODE_ES_FAIL((Bool::Eqv<BoolView,BoolView,BoolView>
00069                            ::post(home,x0,x1,x2)));
00070     }
00071     forceinline void
00072     post_xor(Home home, BoolVar x0, BoolVar x1, BoolVar x2) {
00073       using namespace Int;
00074       NegBoolView n2(x2);
00075       GECODE_ES_FAIL((Bool::Eqv<BoolView,BoolView,NegBoolView>
00076                            ::post(home,x0,x1,n2)));
00077     }
00078 
00079   }
00080 
00081   void
00082   rel(Home home, BoolVar x0, IntRelType r, BoolVar x1, IntConLevel) {
00083     using namespace Int;
00084     if (home.failed()) return;
00085     switch (r) {
00086     case IRT_EQ:
00087       GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>
00088                            ::post(home,x0,x1)));
00089       break;
00090     case IRT_NQ:
00091       {
00092         NegBoolView n1(x1);
00093         GECODE_ES_FAIL((Bool::Eq<BoolView,NegBoolView>
00094                              ::post(home,x0,n1)));
00095       }
00096       break;
00097     case IRT_GQ:
00098       GECODE_ES_FAIL(Bool::Lq<BoolView>::post(home,x1,x0));
00099       break;
00100     case IRT_LQ:
00101       GECODE_ES_FAIL(Bool::Lq<BoolView>::post(home,x0,x1));
00102       break;
00103     case IRT_GR:
00104       GECODE_ES_FAIL(Bool::Le<BoolView>::post(home,x1,x0));
00105       break;
00106     case IRT_LE:
00107       GECODE_ES_FAIL(Bool::Le<BoolView>::post(home,x0,x1));
00108       break;
00109     default:
00110       throw UnknownRelation("Int::rel");
00111     }
00112   }
00113 
00114   void
00115   rel(Home home, BoolVar x0, IntRelType r, int n, IntConLevel) {
00116     using namespace Int;
00117     if (home.failed()) return;
00118     BoolView x(x0);
00119     if (n == 0) {
00120       switch (r) {
00121       case IRT_LQ:
00122       case IRT_EQ:
00123         GECODE_ME_FAIL(x.zero(home)); break;
00124       case IRT_NQ:
00125       case IRT_GR:
00126         GECODE_ME_FAIL(x.one(home)); break;
00127       case IRT_LE:
00128         home.fail(); break;
00129       case IRT_GQ:
00130         break;
00131       default:
00132         throw UnknownRelation("Int::rel");
00133       }
00134     } else if (n == 1) {
00135       switch (r) {
00136       case IRT_GQ:
00137       case IRT_EQ:
00138         GECODE_ME_FAIL(x.one(home)); break;
00139       case IRT_NQ:
00140       case IRT_LE:
00141         GECODE_ME_FAIL(x.zero(home)); break;
00142       case IRT_GR:
00143         home.fail(); break;
00144       case IRT_LQ:
00145         break;
00146       default:
00147         throw UnknownRelation("Int::rel");
00148       }
00149     } else {
00150       throw NotZeroOne("Int::rel");
00151     }
00152   }
00153 
00154   void
00155   rel(Home home, BoolVar x0, IntRelType r, BoolVar x1, BoolVar b,
00156       IntConLevel) {
00157     using namespace Int;
00158     if (home.failed()) return;
00159     switch (r) {
00160     case IRT_EQ:
00161       GECODE_ES_FAIL((Bool::Eqv<BoolView,BoolView,BoolView>
00162                            ::post(home,x0,x1,b)));
00163       break;
00164     case IRT_NQ:
00165       {
00166         NegBoolView n(b);
00167         GECODE_ES_FAIL((Bool::Eqv<BoolView,BoolView,NegBoolView>
00168                              ::post(home,x0,x1,n)));
00169       }
00170       break;
00171     case IRT_GQ:
00172       std::swap(x0,x1);
00173     case IRT_LQ:
00174       {
00175         NegBoolView n0(x0);
00176         GECODE_ES_FAIL((Bool::Or<NegBoolView,BoolView,BoolView>
00177                              ::post(home,n0,x1,b)));
00178       }
00179       break;
00180     case IRT_GR:
00181       std::swap(x0,x1);
00182     case IRT_LE:
00183       {
00184         NegBoolView n1(x1), n(b);
00185         GECODE_ES_FAIL((Bool::Or<BoolView,NegBoolView,NegBoolView>
00186                              ::post(home,x0,n1,n)));
00187       }
00188       break;
00189     default:
00190       throw UnknownRelation("Int::rel");
00191     }
00192   }
00193 
00194   void
00195   rel(Home home, BoolVar x0, IntRelType r, int n, BoolVar b,
00196       IntConLevel) {
00197     using namespace Int;
00198     if (home.failed()) return;
00199     BoolView x(x0);
00200     BoolView y(b);
00201     if (n == 0) {
00202       switch (r) {
00203       case IRT_LQ:
00204       case IRT_EQ:
00205         {
00206           NegBoolView z(y);
00207           GECODE_ES_FAIL((Bool::Eq<BoolView,NegBoolView>
00208                                ::post(home,x,z)));
00209         }
00210         break;
00211       case IRT_NQ:
00212       case IRT_GR:
00213         GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>
00214                              ::post(home,x,y)));
00215         break;
00216       case IRT_LE:
00217         GECODE_ME_FAIL(y.zero(home));
00218         break;
00219       case IRT_GQ:
00220         GECODE_ME_FAIL(y.one(home));
00221         break;
00222       default:
00223         throw UnknownRelation("Int::rel");
00224       }
00225     } else if (n == 1) {
00226       switch (r) {
00227       case IRT_GQ:
00228       case IRT_EQ:
00229         GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>
00230                              ::post(home,x,y)));
00231         break;
00232       case IRT_NQ:
00233       case IRT_LE:
00234         {
00235           NegBoolView z(y);
00236           GECODE_ES_FAIL((Bool::Eq<BoolView,NegBoolView>
00237                                ::post(home,x,z)));
00238         }
00239         break;
00240       case IRT_GR:
00241         GECODE_ME_FAIL(y.zero(home));
00242         break;
00243       case IRT_LQ:
00244         GECODE_ME_FAIL(y.one(home));
00245         break;
00246       default:
00247         throw UnknownRelation("Int::rel");
00248       }
00249     } else {
00250       throw NotZeroOne("Int::rel");
00251     }
00252   }
00253 
00254   void
00255   rel(Home home, const BoolVarArgs& x, IntRelType r, BoolVar y,
00256       IntConLevel) {
00257     using namespace Int;
00258     if (home.failed()) return;
00259     switch (r) {
00260     case IRT_EQ:
00261       for (int i=x.size(); i--; ) {
00262         GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>
00263                              ::post(home,x[i],y)));
00264       }
00265       break;
00266     case IRT_NQ:
00267       {
00268         NegBoolView n(y);
00269         for (int i=x.size(); i--; ) {
00270           GECODE_ES_FAIL((Bool::Eq<BoolView,NegBoolView>
00271                                ::post(home,x[i],n)));
00272         }
00273       }
00274       break;
00275     case IRT_GQ:
00276       for (int i=x.size(); i--; ) {
00277         GECODE_ES_FAIL(Bool::Lq<BoolView>::post(home,y,x[i]));
00278       }
00279       break;
00280     case IRT_LQ:
00281       for (int i=x.size(); i--; ) {
00282         GECODE_ES_FAIL(Bool::Lq<BoolView>::post(home,x[i],y));
00283       }
00284       break;
00285     case IRT_GR:
00286       for (int i=x.size(); i--; ) {
00287         GECODE_ES_FAIL(Bool::Le<BoolView>::post(home,y,x[i]));
00288       }
00289       break;
00290     case IRT_LE:
00291       for (int i=x.size(); i--; ) {
00292         GECODE_ES_FAIL(Bool::Le<BoolView>::post(home,x[i],y));
00293       }
00294       break;
00295     default:
00296       throw UnknownRelation("Int::rel");
00297     }
00298   }
00299 
00300   void
00301   rel(Home home, const BoolVarArgs& x, IntRelType r, int n,
00302       IntConLevel) {
00303     using namespace Int;
00304     if (home.failed()) return;
00305     if (n == 0) {
00306       switch (r) {
00307       case IRT_LQ:
00308       case IRT_EQ:
00309         for (int i=x.size(); i--; ) {
00310           BoolView xi(x[i]); GECODE_ME_FAIL(xi.zero(home));
00311         }
00312         break;
00313       case IRT_NQ:
00314       case IRT_GR:
00315         for (int i=x.size(); i--; ) {
00316           BoolView xi(x[i]); GECODE_ME_FAIL(xi.one(home));
00317         }
00318         break;
00319       case IRT_LE:
00320         home.fail(); break;
00321       case IRT_GQ:
00322         break;
00323       default:
00324         throw UnknownRelation("Int::rel");
00325       }
00326     } else if (n == 1) {
00327       switch (r) {
00328       case IRT_GQ:
00329       case IRT_EQ:
00330         for (int i=x.size(); i--; ) {
00331           BoolView xi(x[i]); GECODE_ME_FAIL(xi.one(home));
00332         }
00333         break;
00334       case IRT_NQ:
00335       case IRT_LE:
00336         for (int i=x.size(); i--; ) {
00337           BoolView xi(x[i]); GECODE_ME_FAIL(xi.zero(home));
00338         }
00339         break;
00340       case IRT_GR:
00341         home.fail(); break;
00342       case IRT_LQ:
00343         break;
00344       default:
00345         throw UnknownRelation("Int::rel");
00346       }
00347     } else {
00348       throw NotZeroOne("Int::rel");
00349     }
00350   }
00351 
00352   void
00353   rel(Home home, const BoolVarArgs& x, IntRelType r, IntConLevel) {
00354     using namespace Int;
00355     if (home.failed() || (x.size() < 2)) return;
00356     switch (r) {
00357     case IRT_EQ:
00358       for (int i=x.size()-1; i--; )
00359         GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>
00360                              ::post(home,x[i],x[i+1])));
00361       break;
00362     case IRT_NQ:
00363       if (x.size() == 2) {
00364         NegBoolView n(x[1]);
00365         GECODE_ES_FAIL((Bool::Eq<BoolView,NegBoolView>
00366                              ::post(home,x[0],n)));
00367       } else {
00368         home.fail();
00369       }
00370       break;
00371     case IRT_LE:
00372       if (x.size() == 2) {
00373         GECODE_ES_FAIL(Bool::Le<BoolView>::post(home,x[0],x[1]));
00374       } else {
00375         home.fail();
00376       }
00377       break;
00378     case IRT_LQ:
00379       for (int i=x.size()-1; i--; )
00380         GECODE_ES_FAIL(Bool::Lq<BoolView>::post(home,x[i],x[i+1]));
00381       break;
00382     case IRT_GR:
00383       if (x.size() == 2) {
00384         GECODE_ES_FAIL(Bool::Le<BoolView>::post(home,x[1],x[0]));
00385       } else {
00386         home.fail();
00387       }
00388       break;
00389     case IRT_GQ:
00390       for (int i=x.size()-1; i--; )
00391         GECODE_ES_FAIL(Bool::Lq<BoolView>::post(home,x[i+1],x[i]));
00392       break;
00393     default:
00394       throw UnknownRelation("Int::rel");
00395     }
00396   }
00397 
00398   void
00399   rel(Home home, const BoolVarArgs& x, IntRelType r, const BoolVarArgs& y,
00400       IntConLevel) {
00401     using namespace Int;
00402     if (x.size() != y.size())
00403       throw ArgumentSizeMismatch("Int::rel");
00404     if (home.failed()) return;
00405 
00406     switch (r) {
00407     case IRT_GR:
00408       {
00409         ViewArray<BoolView> xv(home,x), yv(home,y);
00410         GECODE_ES_FAIL(Rel::Lex<BoolView>::post(home,yv,xv,true));
00411       }
00412       break;
00413     case IRT_LE:
00414       {
00415         ViewArray<BoolView> xv(home,x), yv(home,y);
00416         GECODE_ES_FAIL(Rel::Lex<BoolView>::post(home,xv,yv,true));
00417       }
00418       break;
00419     case IRT_GQ:
00420       {
00421         ViewArray<BoolView> xv(home,x), yv(home,y);
00422         GECODE_ES_FAIL(Rel::Lex<BoolView>::post(home,yv,xv,false));
00423       }
00424       break;
00425     case IRT_LQ:
00426       {
00427         ViewArray<BoolView> xv(home,x), yv(home,y);
00428         GECODE_ES_FAIL(Rel::Lex<BoolView>::post(home,xv,yv,false));
00429       }
00430       break;
00431     case IRT_EQ:
00432       for (int i=x.size(); i--; ) {
00433         GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>
00434                              ::post(home,x[i],y[i])));
00435       }
00436       break;
00437     case IRT_NQ:
00438       {
00439         ViewArray<BoolView> b(home,x.size());
00440         for (int i=x.size(); i--; ) {
00441           BoolVar bi(home,0,1); b[i]=bi;
00442           NegBoolView n(b[i]);
00443           GECODE_ES_FAIL((Bool::Eqv<BoolView,BoolView,NegBoolView>
00444                                ::post(home,x[i],y[i],n)));
00445         }
00446         GECODE_ES_FAIL(Bool::NaryOrTrue<BoolView>::post(home,b));
00447       }
00448       break;
00449     default:
00450       throw UnknownRelation("Int::rel");
00451     }
00452   }
00453 
00454   void
00455   rel(Home home, BoolVar x0, BoolOpType o, BoolVar x1, BoolVar x2,
00456       IntConLevel) {
00457     using namespace Int;
00458     if (home.failed()) return;
00459     switch (o) {
00460     case BOT_AND: post_and(home,x0,x1,x2); break;
00461     case BOT_OR:  post_or(home,x0,x1,x2); break;
00462     case BOT_IMP: post_imp(home,x0,x1,x2); break;
00463     case BOT_EQV: post_eqv(home,x0,x1,x2); break;
00464     case BOT_XOR: post_xor(home,x0,x1,x2); break;
00465     default: throw UnknownOperation("Int::rel");
00466     }
00467   }
00468 
00469   void
00470   rel(Home home, BoolVar x0, BoolOpType o, BoolVar x1, int n,
00471       IntConLevel) {
00472     using namespace Int;
00473     if (home.failed()) return;
00474     if (n == 0) {
00475       switch (o) {
00476       case BOT_AND:
00477         {
00478           NegBoolView n0(x0); NegBoolView n1(x1);
00479           GECODE_ES_FAIL((Bool::BinOrTrue<NegBoolView,NegBoolView>
00480                                ::post(home,n0,n1)));
00481         }
00482         break;
00483       case BOT_OR:
00484         {
00485           BoolView b0(x0); BoolView b1(x1);
00486           GECODE_ME_FAIL(b0.zero(home));
00487           GECODE_ME_FAIL(b1.zero(home));
00488         }
00489         break;
00490       case BOT_IMP:
00491         {
00492           BoolView b0(x0); BoolView b1(x1);
00493           GECODE_ME_FAIL(b0.one(home));
00494           GECODE_ME_FAIL(b1.zero(home));
00495         }
00496         break;
00497       case BOT_EQV:
00498         {
00499           NegBoolView n0(x0);
00500           GECODE_ES_FAIL((Bool::Eq<NegBoolView,BoolView>
00501                                ::post(home,n0,x1)));
00502         }
00503         break;
00504       case BOT_XOR:
00505         GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>
00506                              ::post(home,x0,x1)));
00507         break;
00508       default:
00509         throw UnknownOperation("Int::rel");
00510       }
00511     } else if (n == 1) {
00512       switch (o) {
00513       case BOT_AND:
00514         {
00515           BoolView b0(x0); BoolView b1(x1);
00516           GECODE_ME_FAIL(b0.one(home));
00517           GECODE_ME_FAIL(b1.one(home));
00518         }
00519         break;
00520       case BOT_OR:
00521         GECODE_ES_FAIL((Bool::BinOrTrue<BoolView,BoolView>
00522                              ::post(home,x0,x1)));
00523         break;
00524       case BOT_IMP:
00525         {
00526           NegBoolView n0(x0);
00527           GECODE_ES_FAIL((Bool::BinOrTrue<NegBoolView,BoolView>
00528                                ::post(home,n0,x1)));
00529         }
00530         break;
00531       case BOT_EQV:
00532         GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>
00533                              ::post(home,x0,x1)));
00534         break;
00535       case BOT_XOR:
00536         {
00537           NegBoolView n0(x0);
00538           GECODE_ES_FAIL((Bool::Eq<NegBoolView,BoolView>
00539                                ::post(home,n0,x1)));
00540         }
00541         break;
00542       default:
00543         throw UnknownOperation("Int::rel");
00544       }
00545     } else {
00546       throw NotZeroOne("Int::rel");
00547     }
00548   }
00549 
00550   void
00551   rel(Home home, BoolOpType o, const BoolVarArgs& x, BoolVar y,
00552       IntConLevel) {
00553     using namespace Int;
00554     if (home.failed()) return;
00555     int m = x.size();
00556     Region r(home);
00557     switch (o) {
00558     case BOT_AND:
00559       {
00560         ViewArray<NegBoolView> b(home,m);
00561         for (int i=m; i--; ) {
00562           NegBoolView nb(x[i]); b[i]=nb;
00563         }
00564         NegBoolView ny(y);
00565         b.unique(home);
00566         GECODE_ES_FAIL((Bool::NaryOr<NegBoolView,NegBoolView>
00567                              ::post(home,b,ny)));
00568       }
00569       break;
00570     case BOT_OR:
00571       {
00572         ViewArray<BoolView> b(home,x);
00573         b.unique(home);
00574         GECODE_ES_FAIL((Bool::NaryOr<BoolView,BoolView>::post(home,b,y)));
00575       }
00576       break;
00577     case BOT_IMP:
00578       if (m < 2) {
00579         throw TooFewArguments("Int::rel");
00580       } else {
00581         BoolVar* z = r.alloc<BoolVar>(m);
00582         z[0]=x[0]; z[m-1]=y;
00583         for (int i=1; i<m-1; i++)
00584           z[i].init(home,0,1);
00585         for (int i=1; i<m; i++)
00586           post_imp(home,z[i-1],x[i],z[i]);
00587       }
00588       break;
00589     case BOT_EQV:
00590       if (m < 2) {
00591         throw TooFewArguments("Int::rel");
00592       } else {
00593         BoolVar* z = r.alloc<BoolVar>(m);
00594         z[0]=x[0]; z[m-1]=y;
00595         for (int i=1; i<m-1; i++)
00596           z[i].init(home,0,1);
00597         for (int i=1; i<m; i++)
00598           post_eqv(home,z[i-1],x[i],z[i]);
00599       }
00600       break;
00601     case BOT_XOR:
00602       if (m < 2) {
00603         throw TooFewArguments("Int::rel");
00604       } else {
00605         BoolVar* z = r.alloc<BoolVar>(m);
00606         z[0]=x[0]; z[m-1]=y;
00607         for (int i=1; i<m-1; i++)
00608           z[i].init(home,0,1);
00609         for (int i=1; i<m; i++)
00610           post_xor(home,z[i-1],x[i],z[i]);
00611       }
00612       break;
00613     default:
00614       throw UnknownOperation("Int::rel");
00615     }
00616   }
00617 
00618   void
00619   rel(Home home, BoolOpType o, const BoolVarArgs& x, int n,
00620       IntConLevel) {
00621     using namespace Int;
00622     if ((n < 0) || (n > 1))
00623       throw NotZeroOne("Int::rel");
00624     if (home.failed()) return;
00625     int m = x.size();
00626     Region r(home);
00627     switch (o) {
00628     case BOT_AND:
00629       if (n == 0) {
00630         ViewArray<NegBoolView> b(home,m);
00631         for (int i=m; i--; ) {
00632           NegBoolView nb(x[i]); b[i]=nb;
00633         }
00634         b.unique(home);
00635         GECODE_ES_FAIL(Bool::NaryOrTrue<NegBoolView>::post(home,b));
00636       } else {
00637         for (int i=m; i--; ) {
00638           BoolView b(x[i]); GECODE_ME_FAIL(b.one(home));
00639         }
00640       }
00641       break;
00642     case BOT_OR:
00643       if (n == 0) {
00644         for (int i=m; i--; ) {
00645           BoolView b(x[i]); GECODE_ME_FAIL(b.zero(home));
00646         }
00647       } else {
00648         ViewArray<BoolView> b(home,x);
00649         b.unique(home);
00650         GECODE_ES_FAIL(Bool::NaryOrTrue<BoolView>::post(home,b));
00651       }
00652       break;
00653     case BOT_IMP:
00654       if (m < 2) {
00655         throw TooFewArguments("Int::rel");
00656       } else {
00657         BoolVar* z = r.alloc<BoolVar>(m);
00658         z[0]=x[0]; z[m-1].init(home,n,n);;
00659         for (int i=1; i<m-1; i++)
00660           z[i].init(home,0,1);
00661         for (int i=1; i<m; i++)
00662           post_imp(home,z[i-1],x[i],z[i]);
00663       }
00664       break;
00665     case BOT_EQV:
00666       if (m < 2) {
00667         throw TooFewArguments("Int::rel");
00668       } else {
00669         BoolVar* z = r.alloc<BoolVar>(m);
00670         z[0]=x[0]; z[m-1].init(home,n,n);
00671         for (int i=1; i<m-1; i++)
00672           z[i].init(home,0,1);
00673         for (int i=1; i<m; i++)
00674           post_eqv(home,z[i-1],x[i],z[i]);
00675       }
00676       break;
00677     case BOT_XOR:
00678       if (m < 2) {
00679         throw TooFewArguments("Int::rel");
00680       } else {
00681         BoolVar* z = r.alloc<BoolVar>(m);
00682         z[0]=x[0]; z[m-1].init(home,n,n);
00683         for (int i=1; i<m-1; i++)
00684           z[i].init(home,0,1);
00685         for (int i=1; i<m; i++)
00686           post_xor(home,z[i-1],x[i],z[i]);
00687       }
00688       break;
00689     default:
00690       throw UnknownOperation("Int::rel");
00691     }
00692   }
00693 
00694   void
00695   clause(Home home, BoolOpType o, const BoolVarArgs& x, const BoolVarArgs& y,
00696          int n, IntConLevel) {
00697     using namespace Int;
00698     if ((n < 0) || (n > 1))
00699       throw NotZeroOne("Int::rel");
00700     if (home.failed()) return;
00701     switch (o) {
00702     case BOT_AND:
00703       if (n == 0) {
00704         ViewArray<NegBoolView> xv(home,x.size());
00705         for (int i=x.size(); i--; ) {
00706           NegBoolView n(x[i]); xv[i]=n;
00707         }
00708         ViewArray<BoolView> yv(home,y);
00709         xv.unique(home); yv.unique(home);
00710         GECODE_ES_FAIL((Bool::ClauseTrue<NegBoolView,BoolView>
00711                              ::post(home,xv,yv)));
00712       } else {
00713         for (int i=x.size(); i--; ) {
00714           BoolView b(x[i]); GECODE_ME_FAIL(b.one(home));
00715         }
00716         for (int i=y.size(); i--; ) {
00717           BoolView b(y[i]); GECODE_ME_FAIL(b.zero(home));
00718         }
00719       }
00720       break;
00721     case BOT_OR:
00722       if (n == 0) {
00723         for (int i=x.size(); i--; ) {
00724           BoolView b(x[i]); GECODE_ME_FAIL(b.zero(home));
00725         }
00726         for (int i=y.size(); i--; ) {
00727           BoolView b(y[i]); GECODE_ME_FAIL(b.one(home));
00728         }
00729       } else {
00730         ViewArray<BoolView> xv(home,x);
00731         ViewArray<NegBoolView> yv(home,y.size());
00732         for (int i=y.size(); i--; ) {
00733           NegBoolView n(y[i]); yv[i]=n;
00734         }
00735         xv.unique(home); yv.unique(home);
00736         GECODE_ES_FAIL((Bool::ClauseTrue<BoolView,NegBoolView>
00737                              ::post(home,xv,yv)));
00738       }
00739       break;
00740     default:
00741       throw IllegalOperation("Int::clause");
00742     }
00743   }
00744 
00745   void
00746   clause(Home home, BoolOpType o, const BoolVarArgs& x, const BoolVarArgs& y,
00747          BoolVar z, IntConLevel) {
00748     using namespace Int;
00749     if (home.failed()) return;
00750     switch (o) {
00751     case BOT_AND:
00752       {
00753         ViewArray<NegBoolView> xv(home,x.size());
00754         for (int i=x.size(); i--; ) {
00755           NegBoolView n(x[i]); xv[i]=n;
00756         }
00757         ViewArray<BoolView> yv(home,y);
00758         xv.unique(home); yv.unique(home);
00759         NegBoolView nz(z);
00760         GECODE_ES_FAIL((Bool::Clause<NegBoolView,BoolView>
00761                              ::post(home,xv,yv,nz)));
00762       }
00763       break;
00764     case BOT_OR:
00765       {
00766         ViewArray<BoolView> xv(home,x);
00767         ViewArray<NegBoolView> yv(home,y.size());
00768         for (int i=y.size(); i--; ) {
00769           NegBoolView n(y[i]); yv[i]=n;
00770         }
00771         xv.unique(home); yv.unique(home);
00772         GECODE_ES_FAIL((Bool::Clause<BoolView,NegBoolView>
00773                              ::post(home,xv,yv,z)));
00774       }
00775       break;
00776     default:
00777       throw IllegalOperation("Int::clause");
00778     }
00779   }
00780 
00781 }
00782 
00783 // STATISTICS: int-post