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  *  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 "test/int.hh"
00039 
00040 #include <gecode/minimodel.hh>
00041 
00042 namespace Test { namespace Int {
00043 
00045    namespace Bool {
00046 
00047      inline int
00048      check(int x0, Gecode::BoolOpType op, int x1) {
00049        switch (op) {
00050        case Gecode::BOT_AND: return x0 & x1;
00051        case Gecode::BOT_OR:  return x0 | x1;
00052        case Gecode::BOT_IMP: return !x0 | x1;
00053        case Gecode::BOT_EQV: return x0 == x1;
00054        case Gecode::BOT_XOR: return x0 != x1;
00055        default: GECODE_NEVER;
00056        }
00057        GECODE_NEVER;
00058        return 0;
00059      }
00060 
00066 
00067      class BinXYZ : public Test {
00068      protected:
00070        Gecode::BoolOpType op;
00071      public:
00073        BinXYZ(Gecode::BoolOpType op0)
00074          : Test("Bool::Bin::XYZ::"+str(op0),3,0,1), op(op0) {}
00076        virtual bool solution(const Assignment& x) const {
00077          return check(x[0],op,x[1]) == x[2];
00078        }
00080        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00081          using namespace Gecode;
00082          rel(home,
00083              channel(home,x[0]), op, channel(home,x[1]),
00084              channel(home,x[2]));
00085        }
00086      };
00087 
00089      class BinXXY : public Test {
00090      protected:
00092        Gecode::BoolOpType op;
00093      public:
00095        BinXXY(Gecode::BoolOpType op0)
00096          : Test("Bool::Bin::XXY::"+str(op0),2,0,1), op(op0) {}
00098        virtual bool solution(const Assignment& x) const {
00099          return check(x[0],op,x[0]) == x[1];
00100        }
00102        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00103          using namespace Gecode;
00104          BoolVar b = channel(home,x[0]);
00105          rel(home, b, op, b, channel(home,x[1]));
00106        }
00107      };
00108 
00110      class BinXYX : public Test {
00111      protected:
00113        Gecode::BoolOpType op;
00114      public:
00116        BinXYX(Gecode::BoolOpType op0)
00117          : Test("Bool::Bin::XYX::"+str(op0),2,0,1), op(op0) {}
00119        virtual bool solution(const Assignment& x) const {
00120          return check(x[0],op,x[1]) == x[0];
00121        }
00123        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00124          using namespace Gecode;
00125          BoolVar b = channel(home,x[0]);
00126          rel(home, b, op, channel(home,x[1]), b);
00127        }
00128      };
00129 
00131      class BinXYY : public Test {
00132      protected:
00134        Gecode::BoolOpType op;
00135      public:
00137        BinXYY(Gecode::BoolOpType op0)
00138          : Test("Bool::Bin::XYY::"+str(op0),2,0,1), op(op0) {}
00140        virtual bool solution(const Assignment& x) const {
00141          return check(x[0],op,x[1]) == x[1];
00142        }
00144        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00145          using namespace Gecode;
00146          BoolVar b = channel(home,x[1]);
00147          rel(home, channel(home,x[0]), op, b, b);
00148        }
00149      };
00150 
00152      class BinXXX : public Test {
00153      protected:
00155        Gecode::BoolOpType op;
00156      public:
00158        BinXXX(Gecode::BoolOpType op0)
00159          : Test("Bool::Bin::XXX::"+str(op0),1,0,1), op(op0) {}
00161        virtual bool solution(const Assignment& x) const {
00162          return check(x[0],op,x[0]) == x[0];
00163        }
00165        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00166          using namespace Gecode;
00167          BoolVar b = channel(home,x[0]);
00168          rel(home, b, op, b, b);
00169        }
00170      };
00171 
00173      class BinConstXY : public Test {
00174      protected:
00176        Gecode::BoolOpType op;
00178        int c;
00179      public:
00181        BinConstXY(Gecode::BoolOpType op0, int c0)
00182          : Test("Bool::Bin::XY::"+str(op0)+"::"+str(c0),2,0,1),
00183            op(op0), c(c0) {}
00185        virtual bool solution(const Assignment& x) const {
00186          return check(x[0],op,x[1]) == c;
00187        }
00189        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00190          using namespace Gecode;
00191          rel(home, channel(home,x[0]), op, channel(home,x[1]), c);
00192        }
00193      };
00194 
00196      class BinConstXX : public Test {
00197      protected:
00199        Gecode::BoolOpType op;
00201        int c;
00202      public:
00204        BinConstXX(Gecode::BoolOpType op0, int c0)
00205          : Test("Bool::Bin::XX::"+str(op0)+"::"+str(c0),1,0,1),
00206            op(op0), c(c0) {}
00208        virtual bool solution(const Assignment& x) const {
00209          return check(x[0],op,x[0]) == c;
00210        }
00212        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00213          using namespace Gecode;
00214          BoolVar b = channel(home,x[0]);
00215          rel(home, b, op, b, c);
00216        }
00217      };
00218 
00220      class Nary : public Test {
00221      protected:
00223        Gecode::BoolOpType op;
00224      public:
00226        Nary(Gecode::BoolOpType op0, int n)
00227          : Test("Bool::Nary::"+str(op0)+"::"+str(n),n+1,0,1), op(op0) {}
00229        virtual bool solution(const Assignment& x) const {
00230          int n = x.size()-1;
00231          int b = check(x[n-2],op,x[n-1]);
00232          for (int i=0; i<n-2; i++)
00233            b = check(x[i],op,b);
00234          return b == x[n];
00235        }
00237        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00238          using namespace Gecode;
00239          BoolVarArgs b(x.size()-1);
00240          for (int i=x.size()-1; i--; )
00241            b[i]=channel(home,x[i]);
00242          rel(home, op, b, channel(home,x[x.size()-1]));
00243        }
00244      };
00245 
00247      class NaryShared : public Test {
00248      protected:
00250        Gecode::BoolOpType op;
00251      public:
00253        NaryShared(Gecode::BoolOpType op0, int n)
00254          : Test("Bool::Nary::Shared::"+str(op0)+"::"+str(n),n,0,1),
00255            op(op0) {
00256          if ((op == Gecode::BOT_EQV) || (op == Gecode::BOT_XOR))
00257            testfix = false;
00258        }
00260        virtual bool solution(const Assignment& x) const {
00261          int n = x.size();
00262          int b = check(x[n-2],op,x[n-1]);
00263          for (int i=0; i<n-2; i++)
00264            b = check(x[i],op,b);
00265          return b == x[n-1];
00266        }
00268        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00269          using namespace Gecode;
00270          BoolVarArgs b(x.size());
00271          for (int i=x.size(); i--; )
00272            b[i]=channel(home,x[i]);
00273          rel(home, op, b, b[x.size()-1]);
00274        }
00275      };
00276 
00278      class NaryConst : public Test {
00279      protected:
00281        Gecode::BoolOpType op;
00283        int c;
00284      public:
00286        NaryConst(Gecode::BoolOpType op0, int n, int c0)
00287          : Test("Bool::Nary::"+str(op0)+"::"+str(n)+"::"+str(c0),n,0,1),
00288            op(op0), c(c0) {}
00290        virtual bool solution(const Assignment& x) const {
00291          int n = x.size();
00292          int b = check(x[n-2],op,x[n-1]);
00293          for (int i=0; i<n-2; i++)
00294            b = check(x[i],op,b);
00295          return b == c;
00296        }
00298        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00299          using namespace Gecode;
00300          BoolVarArgs b(x.size());
00301          for (int i=x.size(); i--; )
00302            b[i]=channel(home,x[i]);
00303          rel(home, op, b, c);
00304        }
00305      };
00306 
00307 
00309      class ClauseXYZ : public Test {
00310      protected:
00312        Gecode::BoolOpType op;
00313      public:
00315        ClauseXYZ(Gecode::BoolOpType op0, int n)
00316          : Test("Bool::Clause::XYZ::"+str(op0)+"::"+str(n),n+1,0,1), op(op0) {}
00318        virtual bool solution(const Assignment& x) const {
00319          int n = (x.size()-1) / 2;
00320          int b;
00321          if (n == 1) {
00322            b = check(x[0],op,!x[1]);
00323          } else {
00324            b = check(x[0],op,!x[n]);
00325            for (int i=1; i<n; i++)
00326              b = check(b,op,check(x[i],op,!x[n+i]));
00327          }
00328          return b == x[x.size()-1];
00329        }
00331        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00332          using namespace Gecode;
00333          int n = (x.size()-1) / 2;
00334          BoolVarArgs a(n), b(n);
00335          for (int i=n; i--; ) {
00336            a[i]=channel(home,x[i]);
00337            b[i]=channel(home,x[i+n]);
00338          }
00339          clause(home, op, a, b, channel(home,x[x.size()-1]));
00340        }
00341      };
00342 
00344      class ClauseXXYYX : public Test {
00345      protected:
00347        Gecode::BoolOpType op;
00348      public:
00350        ClauseXXYYX(Gecode::BoolOpType op0, int n)
00351          : Test("Bool::Clause::XXYYX::"+str(op0)+"::"+str(n),n,0,1),
00352            op(op0) {}
00354        virtual bool solution(const Assignment& x) const {
00355          int n = x.size() / 2;
00356          int b;
00357          if (n == 1) {
00358            b = check(x[0],op,!x[1]);
00359          } else {
00360            b = check(x[0],op,!x[n]);
00361            for (int i=1; i<n; i++)
00362              b = check(b,op,check(x[i],op,!x[n+i]));
00363          }
00364          return b == x[0];
00365        }
00367        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00368          using namespace Gecode;
00369          int n = x.size() / 2;
00370          BoolVarArgs a(2*n), b(2*n);
00371          for (int i=n; i--; ) {
00372            a[i]=a[i+n]=channel(home,x[i]);
00373            b[i]=b[i+n]=channel(home,x[i+n]);
00374          }
00375          clause(home, op, a, b, a[0]);
00376        }
00377      };
00378 
00380      class ClauseXXY : public Test {
00381      protected:
00383        Gecode::BoolOpType op;
00384      public:
00386        ClauseXXY(Gecode::BoolOpType op0, int n)
00387          : Test("Bool::Clause::XXY::"+str(op0)+"::"+str(n),n,0,1),
00388            op(op0) {}
00390        virtual bool solution(const Assignment& x) const {
00391          return (x[0] == 1) == (op == Gecode::BOT_OR);
00392        }
00394        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00395          using namespace Gecode;
00396          int n = x.size() / 2;
00397          BoolVarArgs a(2*n), b(2*n);
00398          for (int i=n; i--; ) {
00399            a[i]=b[i+n]=channel(home,x[i]);
00400            b[i]=a[i+n]=channel(home,x[i+n]);
00401          }
00402          clause(home, op, a, b, a[0]);
00403        }
00404      };
00405 
00407      class ClauseConst : public Test {
00408      protected:
00410        Gecode::BoolOpType op;
00412        int c;
00413      public:
00415        ClauseConst(Gecode::BoolOpType op0, int n, int c0)
00416          : Test("Bool::Clause::"+str(op0)+"::"+str(n)+"::"+str(c0),n,0,1),
00417            op(op0), c(c0) {}
00419        virtual bool solution(const Assignment& x) const {
00420          int n = x.size() / 2;
00421          int b;
00422          if (n == 1) {
00423            b = check(x[0],op,!x[1]);
00424          } else {
00425            b = check(x[0],op,!x[n]);
00426            for (int i=1; i<n; i++)
00427              b = check(b,op,check(x[i],op,!x[n+i]));
00428          }
00429          return b == c;
00430        }
00432        virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
00433          using namespace Gecode;
00434          int n = x.size() / 2;
00435          BoolVarArgs a(n), b(n);
00436          for (int i=n; i--; ) {
00437            a[i]=channel(home,x[i]);
00438            b[i]=channel(home,x[i+n]);
00439          }
00440          clause(home, op, a, b, c);
00441        }
00442      };
00443 
00445      class Create {
00446      public:
00448        Create(void) {
00449          using namespace Gecode;
00450          for (BoolOpTypes bots; bots(); ++bots) {
00451            (void) new BinXYZ(bots.bot());
00452            (void) new BinXXY(bots.bot());
00453            (void) new BinXYX(bots.bot());
00454            (void) new BinXYY(bots.bot());
00455            (void) new BinXXX(bots.bot());
00456            (void) new BinConstXY(bots.bot(),0);
00457            (void) new BinConstXY(bots.bot(),1);
00458            (void) new BinConstXX(bots.bot(),0);
00459            (void) new BinConstXX(bots.bot(),1);
00460            (void) new Nary(bots.bot(),2);
00461            (void) new Nary(bots.bot(),6);
00462            (void) new Nary(bots.bot(),10);
00463            (void) new NaryShared(bots.bot(),2);
00464            (void) new NaryShared(bots.bot(),6);
00465            (void) new NaryShared(bots.bot(),10);
00466            (void) new NaryConst(bots.bot(),2,0);
00467            (void) new NaryConst(bots.bot(),6,0);
00468            (void) new NaryConst(bots.bot(),10,0);
00469            (void) new NaryConst(bots.bot(),2,1);
00470            (void) new NaryConst(bots.bot(),6,1);
00471            (void) new NaryConst(bots.bot(),10,1);
00472            if ((bots.bot() == BOT_AND) || (bots.bot() == BOT_OR)) {
00473              (void) new ClauseXYZ(bots.bot(),2);
00474              (void) new ClauseXYZ(bots.bot(),6);
00475              (void) new ClauseXYZ(bots.bot(),10);
00476              (void) new ClauseXXYYX(bots.bot(),2);
00477              (void) new ClauseXXYYX(bots.bot(),6);
00478              (void) new ClauseXXYYX(bots.bot(),10);
00479              (void) new ClauseXXY(bots.bot(),2);
00480              (void) new ClauseXXY(bots.bot(),6);
00481              (void) new ClauseXXY(bots.bot(),10);
00482              (void) new ClauseConst(bots.bot(),2,0);
00483              (void) new ClauseConst(bots.bot(),6,0);
00484              (void) new ClauseConst(bots.bot(),10,0);
00485              (void) new ClauseConst(bots.bot(),2,1);
00486              (void) new ClauseConst(bots.bot(),6,1);
00487              (void) new ClauseConst(bots.bot(),10,1);
00488            }
00489          }
00490        }
00491      };
00492 
00493      Create c;
00495 
00496    }
00497 }}
00498 
00499 // STATISTICS: test-int
00500