bool.cpp

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