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, 2005
00008  *
00009  *  This file is part of Gecode, the generic constraint
00010  *  development environment:
00011  *     http://www.gecode.org
00012  *
00013  *  Permission is hereby granted, free of charge, to any person obtaining
00014  *  a copy of this software and associated documentation files (the
00015  *  "Software"), to deal in the Software without restriction, including
00016  *  without limitation the rights to use, copy, modify, merge, publish,
00017  *  distribute, sublicense, and/or sell copies of the Software, and to
00018  *  permit persons to whom the Software is furnished to do so, subject to
00019  *  the following conditions:
00020  *
00021  *  The above copyright notice and this permission notice shall be
00022  *  included in all copies or substantial portions of the Software.
00023  *
00024  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00025  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00026  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00027  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00028  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00029  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00030  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00031  *
00032  */
00033 
00034 #include "test/int.hh"
00035 
00036 #include <gecode/minimodel.hh>
00037 
00038 namespace Test { namespace Int {
00039 
00041    namespace Bool {
00042 
00043      inline int
00044      check(int x0, Gecode::BoolOpType op, int x1) {
00045        switch (op) {
00046        case Gecode::BOT_AND: return x0 & x1;
00047        case Gecode::BOT_OR:  return x0 | x1;
00048        case Gecode::BOT_IMP: return (!x0) | x1;
00049        case Gecode::BOT_EQV: return x0 == x1;
00050        case Gecode::BOT_XOR: return x0 != x1;
00051        default: GECODE_NEVER;
00052        }
00053        GECODE_NEVER;
00054        return 0;
00055      }
00056 
00062 
00063      class BinXYZ : public Test {
00064      protected:
00066        Gecode::BoolOpType op;
00067      public:
00069        BinXYZ(Gecode::BoolOpType op0)
00070          : Test("Bool::Bin::XYZ::"+str(op0),3,0,1), op(op0) {}
00072        virtual bool solution(const Assignment& x) const {
00073          return check(x[0],op,x[1]) == x[2];
00074        }
00076        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00077          using namespace Gecode;
00078          rel(home,
00079              channel(home,x[0]), op, channel(home,x[1]),
00080              channel(home,x[2]));
00081        }
00082      };
00083 
00085      class BinXXY : public Test {
00086      protected:
00088        Gecode::BoolOpType op;
00089      public:
00091        BinXXY(Gecode::BoolOpType op0)
00092          : Test("Bool::Bin::XXY::"+str(op0),2,0,1), op(op0) {}
00094        virtual bool solution(const Assignment& x) const {
00095          return check(x[0],op,x[0]) == x[1];
00096        }
00098        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00099          using namespace Gecode;
00100          BoolVar b = channel(home,x[0]);
00101          rel(home, b, op, b, channel(home,x[1]));
00102        }
00103      };
00104 
00106      class BinXYX : public Test {
00107      protected:
00109        Gecode::BoolOpType op;
00110      public:
00112        BinXYX(Gecode::BoolOpType op0)
00113          : Test("Bool::Bin::XYX::"+str(op0),2,0,1), op(op0) {}
00115        virtual bool solution(const Assignment& x) const {
00116          return check(x[0],op,x[1]) == x[0];
00117        }
00119        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00120          using namespace Gecode;
00121          BoolVar b = channel(home,x[0]);
00122          rel(home, b, op, channel(home,x[1]), b);
00123        }
00124      };
00125 
00127      class BinXYY : public Test {
00128      protected:
00130        Gecode::BoolOpType op;
00131      public:
00133        BinXYY(Gecode::BoolOpType op0)
00134          : Test("Bool::Bin::XYY::"+str(op0),2,0,1), op(op0) {}
00136        virtual bool solution(const Assignment& x) const {
00137          return check(x[0],op,x[1]) == x[1];
00138        }
00140        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00141          using namespace Gecode;
00142          BoolVar b = channel(home,x[1]);
00143          rel(home, channel(home,x[0]), op, b, b);
00144        }
00145      };
00146 
00148      class BinXXX : public Test {
00149      protected:
00151        Gecode::BoolOpType op;
00152      public:
00154        BinXXX(Gecode::BoolOpType op0)
00155          : Test("Bool::Bin::XXX::"+str(op0),1,0,1), op(op0) {}
00157        virtual bool solution(const Assignment& x) const {
00158          return check(x[0],op,x[0]) == x[0];
00159        }
00161        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00162          using namespace Gecode;
00163          BoolVar b = channel(home,x[0]);
00164          rel(home, b, op, b, b);
00165        }
00166      };
00167 
00169      class BinConstXY : public Test {
00170      protected:
00172        Gecode::BoolOpType op;
00174        int c;
00175      public:
00177        BinConstXY(Gecode::BoolOpType op0, int c0)
00178          : Test("Bool::Bin::XY::"+str(op0)+"::"+str(c0),2,0,1),
00179            op(op0), c(c0) {}
00181        virtual bool solution(const Assignment& x) const {
00182          return check(x[0],op,x[1]) == c;
00183        }
00185        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00186          using namespace Gecode;
00187          rel(home, channel(home,x[0]), op, channel(home,x[1]), c);
00188        }
00189      };
00190 
00192      class BinConstXX : public Test {
00193      protected:
00195        Gecode::BoolOpType op;
00197        int c;
00198      public:
00200        BinConstXX(Gecode::BoolOpType op0, int c0)
00201          : Test("Bool::Bin::XX::"+str(op0)+"::"+str(c0),1,0,1),
00202            op(op0), c(c0) {}
00204        virtual bool solution(const Assignment& x) const {
00205          return check(x[0],op,x[0]) == c;
00206        }
00208        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00209          using namespace Gecode;
00210          BoolVar b = channel(home,x[0]);
00211          rel(home, b, op, b, c);
00212        }
00213      };
00214 
00216      class Nary : public Test {
00217      protected:
00219        Gecode::BoolOpType op;
00220      public:
00222        Nary(Gecode::BoolOpType op0, int n)
00223          : Test("Bool::Nary::"+str(op0)+"::"+str(n),n+1,0,1), op(op0) {}
00225        virtual bool solution(const Assignment& x) const {
00226          int n = x.size()-1;
00227          int b = check(x[n-2],op,x[n-1]);
00228          for (int i=0; i<n-2; i++)
00229            b = check(x[i],op,b);
00230          return b == x[n];
00231        }
00233        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00234          using namespace Gecode;
00235          BoolVarArgs b(x.size()-1);
00236          for (int i=x.size()-1; i--; )
00237            b[i]=channel(home,x[i]);
00238          rel(home, op, b, channel(home,x[x.size()-1]));
00239        }
00240      };
00241 
00243      class NaryShared : public Test {
00244      protected:
00246        Gecode::BoolOpType op;
00247      public:
00249        NaryShared(Gecode::BoolOpType op0, int n)
00250          : Test("Bool::Nary::Shared::"+str(op0)+"::"+str(n),n,0,1),
00251            op(op0) {
00252          if ((op == Gecode::BOT_EQV) || (op == Gecode::BOT_XOR))
00253            testfix = false;
00254        }
00256        virtual bool solution(const Assignment& x) const {
00257          int n = x.size();
00258          int b = check(x[n-2],op,x[n-1]);
00259          for (int i=0; i<n-2; i++)
00260            b = check(x[i],op,b);
00261          return b == x[n-1];
00262        }
00264        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00265          using namespace Gecode;
00266          BoolVarArgs b(x.size());
00267          for (int i=x.size(); i--; )
00268            b[i]=channel(home,x[i]);
00269          rel(home, op, b, b[x.size()-1]);
00270        }
00271      };
00272 
00274      class NaryConst : public Test {
00275      protected:
00277        Gecode::BoolOpType op;
00279        int c;
00280      public:
00282        NaryConst(Gecode::BoolOpType op0, int n, int c0)
00283          : Test("Bool::Nary::"+str(op0)+"::"+str(n)+"::"+str(c0),n,0,1),
00284            op(op0), c(c0) {}
00286        virtual bool solution(const Assignment& x) const {
00287          int n = x.size();
00288          int b = check(x[n-2],op,x[n-1]);
00289          for (int i=0; i<n-2; i++)
00290            b = check(x[i],op,b);
00291          return b == c;
00292        }
00294        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00295          using namespace Gecode;
00296          BoolVarArgs b(x.size());
00297          for (int i=x.size(); i--; )
00298            b[i]=channel(home,x[i]);
00299          rel(home, op, b, c);
00300        }
00301      };
00302 
00303 
00305      class ClauseXYZ : public Test {
00306      protected:
00308        Gecode::BoolOpType op;
00309      public:
00311        ClauseXYZ(Gecode::BoolOpType op0, int n)
00312          : Test("Bool::Clause::XYZ::"+str(op0)+"::"+str(n),n+1,0,1), op(op0) {}
00314        virtual bool solution(const Assignment& x) const {
00315          int n = (x.size()-1) / 2;
00316          int b;
00317          if (n == 1) {
00318            b = check(x[0],op,!x[1]);
00319          } else {
00320            b = check(x[0],op,!x[n]);
00321            for (int i=1; i<n; i++)
00322              b = check(b,op,check(x[i],op,!x[n+i]));
00323          }
00324          return b == x[x.size()-1];
00325        }
00327        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00328          using namespace Gecode;
00329          int n = (x.size()-1) / 2;
00330          BoolVarArgs a(n), b(n);
00331          for (int i=n; i--; ) {
00332            a[i]=channel(home,x[i]);
00333            b[i]=channel(home,x[i+n]);
00334          }
00335          clause(home, op, a, b, channel(home,x[x.size()-1]));
00336        }
00337      };
00338 
00340      class ClauseXXYYX : public Test {
00341      protected:
00343        Gecode::BoolOpType op;
00344      public:
00346        ClauseXXYYX(Gecode::BoolOpType op0, int n)
00347          : Test("Bool::Clause::XXYYX::"+str(op0)+"::"+str(n),n,0,1),
00348            op(op0) {}
00350        virtual bool solution(const Assignment& x) const {
00351          int n = x.size() / 2;
00352          int b;
00353          if (n == 1) {
00354            b = check(x[0],op,!x[1]);
00355          } else {
00356            b = check(x[0],op,!x[n]);
00357            for (int i=1; i<n; i++)
00358              b = check(b,op,check(x[i],op,!x[n+i]));
00359          }
00360          return b == x[0];
00361        }
00363        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00364          using namespace Gecode;
00365          int n = x.size() / 2;
00366          BoolVarArgs a(2*n), b(2*n);
00367          for (int i=n; i--; ) {
00368            a[i]=a[i+n]=channel(home,x[i]);
00369            b[i]=b[i+n]=channel(home,x[i+n]);
00370          }
00371          clause(home, op, a, b, a[0]);
00372        }
00373      };
00374 
00376      class ClauseXXY : public Test {
00377      protected:
00379        Gecode::BoolOpType op;
00380      public:
00382        ClauseXXY(Gecode::BoolOpType op0, int n)
00383          : Test("Bool::Clause::XXY::"+str(op0)+"::"+str(n),n,0,1),
00384            op(op0) {}
00386        virtual bool solution(const Assignment& x) const {
00387          return (x[0] == 1) == (op == Gecode::BOT_OR);
00388        }
00390        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00391          using namespace Gecode;
00392          int n = x.size() / 2;
00393          BoolVarArgs a(2*n), b(2*n);
00394          for (int i=n; i--; ) {
00395            a[i]=b[i+n]=channel(home,x[i]);
00396            b[i]=a[i+n]=channel(home,x[i+n]);
00397          }
00398          clause(home, op, a, b, a[0]);
00399        }
00400      };
00401 
00403      class ClauseConst : public Test {
00404      protected:
00406        Gecode::BoolOpType op;
00408        int c;
00409      public:
00411        ClauseConst(Gecode::BoolOpType op0, int n, int c0)
00412          : Test("Bool::Clause::"+str(op0)+"::"+str(n)+"::"+str(c0),n,0,1),
00413            op(op0), c(c0) {}
00415        virtual bool solution(const Assignment& x) const {
00416          int n = x.size() / 2;
00417          int b;
00418          if (n == 1) {
00419            b = check(x[0],op,!x[1]);
00420          } else {
00421            b = check(x[0],op,!x[n]);
00422            for (int i=1; i<n; i++)
00423              b = check(b,op,check(x[i],op,!x[n+i]));
00424          }
00425          return b == c;
00426        }
00428        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00429          using namespace Gecode;
00430          int n = x.size() / 2;
00431          BoolVarArgs a(n), b(n);
00432          for (int i=n; i--; ) {
00433            a[i]=channel(home,x[i]);
00434            b[i]=channel(home,x[i+n]);
00435          }
00436          clause(home, op, a, b, c);
00437        }
00438      };
00439 
00441      class ITEInt : public Test {
00442      public:
00444        ITEInt(Gecode::IntPropLevel ipl)
00445          : Test("ITE::Int::"+str(ipl),4,-4,4,false,ipl) {}
00447        virtual bool solution(const Assignment& x) const {
00448          if ((x[0] < 0) || (x[0] > 1))
00449            return false;
00450          if (x[0] == 1)
00451            return x[1] == x[3];
00452          else
00453            return x[2] == x[3];
00454        }
00456        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00457          using namespace Gecode;
00458          if (Base::rand(2) != 0)
00459            ite(home,channel(home,x[0]),x[1],x[2],x[3]);
00460          else
00461            rel(home, ite(channel(home,x[0]),x[1],x[2]) == x[3]);
00462        }
00463      };
00464 
00466      class ITEBool : public Test {
00467      public:
00469        ITEBool(void)
00470          : Test("ITE::Bool",4,0,1,false) {}
00472        virtual bool solution(const Assignment& x) const {
00473          if (x[0] == 1)
00474            return x[1] == x[3];
00475          else
00476            return x[2] == x[3];
00477        }
00479        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00480          using namespace Gecode;
00481          ite(home,channel(home,x[0]),channel(home,x[1]),
00482              channel(home,x[2]),channel(home,x[3]));
00483        }
00484      };
00485 
00487      class Create {
00488      public:
00490        Create(void) {
00491          using namespace Gecode;
00492          for (BoolOpTypes bots; bots(); ++bots) {
00493            (void) new BinXYZ(bots.bot());
00494            (void) new BinXXY(bots.bot());
00495            (void) new BinXYX(bots.bot());
00496            (void) new BinXYY(bots.bot());
00497            (void) new BinXXX(bots.bot());
00498            (void) new BinConstXY(bots.bot(),0);
00499            (void) new BinConstXY(bots.bot(),1);
00500            (void) new BinConstXX(bots.bot(),0);
00501            (void) new BinConstXX(bots.bot(),1);
00502            (void) new Nary(bots.bot(),2);
00503            (void) new Nary(bots.bot(),6);
00504            (void) new Nary(bots.bot(),10);
00505            (void) new NaryShared(bots.bot(),2);
00506            (void) new NaryShared(bots.bot(),6);
00507            (void) new NaryShared(bots.bot(),10);
00508            (void) new NaryConst(bots.bot(),2,0);
00509            (void) new NaryConst(bots.bot(),6,0);
00510            (void) new NaryConst(bots.bot(),10,0);
00511            (void) new NaryConst(bots.bot(),2,1);
00512            (void) new NaryConst(bots.bot(),6,1);
00513            (void) new NaryConst(bots.bot(),10,1);
00514            if ((bots.bot() == BOT_AND) || (bots.bot() == BOT_OR)) {
00515              (void) new ClauseXYZ(bots.bot(),2);
00516              (void) new ClauseXYZ(bots.bot(),6);
00517              (void) new ClauseXYZ(bots.bot(),10);
00518              (void) new ClauseXXYYX(bots.bot(),2);
00519              (void) new ClauseXXYYX(bots.bot(),6);
00520              (void) new ClauseXXYYX(bots.bot(),10);
00521              (void) new ClauseXXY(bots.bot(),2);
00522              (void) new ClauseXXY(bots.bot(),6);
00523              (void) new ClauseXXY(bots.bot(),10);
00524              (void) new ClauseConst(bots.bot(),2,0);
00525              (void) new ClauseConst(bots.bot(),6,0);
00526              (void) new ClauseConst(bots.bot(),10,0);
00527              (void) new ClauseConst(bots.bot(),2,1);
00528              (void) new ClauseConst(bots.bot(),6,1);
00529              (void) new ClauseConst(bots.bot(),10,1);
00530            }
00531          }
00532        }
00533      };
00534 
00535      Create c;
00536      ITEInt itebnd(Gecode::IPL_BND);
00537      ITEInt itedom(Gecode::IPL_DOM);
00538      ITEBool itebool;
00539 
00541 
00542    }
00543 }}
00544 
00545 // STATISTICS: test-int
00546