test/unit/theory/type_enumerator_white.h

   1 /*********************                                                        */
   2 /*! \file type_enumerator_white.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief White box testing of CVC4::theory::TypeEnumerator
  13  **
  14  ** White box testing of CVC4::theory::TypeEnumerator.  (These tests depends
  15  ** on the ordering that the TypeEnumerators use, so it's a white-box test.)
  16  **/
  17
  18 #include <cxxtest/TestSuite.h>
  19
  20 #include "expr/node_manager.h"
  21 #include "expr/expr_manager.h"
  22 #include "expr/type_node.h"
  23 #include "expr/kind.h"
  24 #include "theory/type_enumerator.h"
  25 #include "util/language.h"
  26 #include "util/array_store_all.h"
  27
  28 using namespace CVC4;
  29 using namespace CVC4::theory;
  30 using namespace CVC4::kind;
  31
  32 using namespace std;
  33
  34 class TypeEnumeratorWhite : public CxxTest::TestSuite {
  35   ExprManager* d_em;
  36   NodeManager* d_nm;
  37   NodeManagerScope* d_scope;
  38
  39 public:
  40
  41   void setUp() {
  42     d_em = new ExprManager();
  43     d_nm = NodeManager::fromExprManager(d_em);
  44     d_scope = new NodeManagerScope(d_nm);
  45   }
  46
  47   void tearDown() {
  48     delete d_scope;
  49     delete d_em;
  50   }
  51
  52   void testBooleans() {
  53     TypeEnumerator te(d_nm->booleanType());
  54     TS_ASSERT( ! te.isFinished() );
  55     TS_ASSERT_EQUALS(*te, d_nm->mkConst(false));
  56     TS_ASSERT( ! te.isFinished() );
  57     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(true));
  58     TS_ASSERT( ! te.isFinished() );
  59     TS_ASSERT_THROWS(*++te, NoMoreValuesException);
  60     TS_ASSERT( te.isFinished() );
  61     TS_ASSERT_THROWS(*++te, NoMoreValuesException);
  62     TS_ASSERT( te.isFinished() );
  63     TS_ASSERT_THROWS(*++te, NoMoreValuesException);
  64     TS_ASSERT( te.isFinished() );
  65   }
  66
  67   void testUF() {
  68     TypeNode sortn = d_nm->mkSort("T");
  69     Type sort = sortn.toType();
  70     TypeNode sortn2 = d_nm->mkSort("U");
  71     Type sort2 = sortn2.toType();
  72     TypeEnumerator te(sortn);
  73     TS_ASSERT_EQUALS(*te, d_nm->mkConst(UninterpretedConstant(sort, 0)));
  74     for(size_t i = 1; i < 100; ++i) {
  75       TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort, i)));
  76       TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort2, i)));
  77       TS_ASSERT_EQUALS(*++te, d_nm->mkConst(UninterpretedConstant(sort, i)));
  78       TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort, i + 2)));
  79     }
  80   }
  81
  82   void testArith() {
  83     TypeEnumerator te(d_nm->integerType());
  84     TS_ASSERT( ! te.isFinished() );
  85     TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0)));
  86     for(int i = 1; i <= 100; ++i) {
  87       TS_ASSERT( ! te.isFinished() );
  88       TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(i)));
  89       TS_ASSERT( ! te.isFinished() );
  90       TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-i)));
  91     }
  92     TS_ASSERT( ! te.isFinished() );
  93
  94     te = TypeEnumerator(d_nm->realType());
  95     TS_ASSERT( ! te.isFinished() );
  96     TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0, 1)));
  97     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 1)));
  98     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 1)));
  99     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 1)));
 100     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 1)));
 101     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 2)));
 102     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 2)));
 103     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 1)));
 104     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 1)));
 105     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 3)));
 106     TS_ASSERT( ! te.isFinished() );
 107     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 3)));
 108     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(4, 1)));
 109     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-4, 1)));
 110     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 2)));
 111     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 2)));
 112     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 3)));
 113     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 3)));
 114     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 4)));
 115     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 4)));
 116     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 1)));
 117     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 1)));
 118     TS_ASSERT( ! te.isFinished() );
 119     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 5)));
 120     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 5)));
 121     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(6, 1)));
 122     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-6, 1)));
 123     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 2)));
 124     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 2)));
 125     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(4, 3)));
 126     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-4, 3)));
 127     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 4)));
 128     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 4)));
 129     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 5)));
 130     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 5)));
 131     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 6)));
 132     TS_ASSERT( ! te.isFinished() );
 133     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 6)));
 134     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(7, 1)));
 135     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-7, 1)));
 136     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 3)));
 137     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 3)));
 138     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 5)));
 139     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 5)));
 140     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 7)));
 141     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 7)));
 142     TS_ASSERT( ! te.isFinished() );
 143
 144     // subrange bounded only below
 145     te = TypeEnumerator(d_nm->mkSubrangeType(SubrangeBounds(SubrangeBound(Integer(0)), SubrangeBound())));
 146     TS_ASSERT( ! te.isFinished() );
 147     TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0)));
 148     for(int i = 1; i <= 100; ++i) {
 149       TS_ASSERT( ! (++te).isFinished() );
 150       TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(i)));
 151     }
 152     TS_ASSERT( ! te.isFinished() );
 153
 154     // subrange bounded only above
 155     te = TypeEnumerator(d_nm->mkSubrangeType(SubrangeBounds(SubrangeBound(), SubrangeBound(Integer(-5)))));
 156     TS_ASSERT( ! te.isFinished() );
 157     TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(-5)));
 158     for(int i = 1; i <= 100; ++i) {
 159       TS_ASSERT( ! (++te).isFinished() );
 160       TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(-5 - i)));
 161     }
 162     TS_ASSERT( ! te.isFinished() );
 163
 164     // finite subrange
 165     te = TypeEnumerator(d_nm->mkSubrangeType(SubrangeBounds(SubrangeBound(Integer(-10)), SubrangeBound(Integer(15)))));
 166     TS_ASSERT( ! te.isFinished() );
 167     TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(-10)));
 168     for(int i = -9; i <= 15; ++i) {
 169       TS_ASSERT( ! (++te).isFinished() );
 170       TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(i)));
 171     }
 172     TS_ASSERT( (++te).isFinished() );
 173     TS_ASSERT_THROWS(*te, NoMoreValuesException);
 174 std::cout<<"here\n";
 175     TS_ASSERT_THROWS(*++te, NoMoreValuesException);
 176   }
 177
 178   void testDatatypesFinite() {
 179     Datatype dt("Colors");
 180     dt.addConstructor(DatatypeConstructor("red"));
 181     dt.addConstructor(DatatypeConstructor("orange"));
 182     dt.addConstructor(DatatypeConstructor("yellow"));
 183     dt.addConstructor(DatatypeConstructor("green"));
 184     dt.addConstructor(DatatypeConstructor("blue"));
 185     dt.addConstructor(DatatypeConstructor("violet"));
 186     TypeNode datatype = TypeNode::fromType(d_em->mkDatatypeType(dt));
 187     TypeEnumerator te(datatype);
 188     TS_ASSERT_EQUALS(*te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("red")));
 189     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("orange")));
 190     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("yellow")));
 191     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("green")));
 192     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("blue")));
 193     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("violet")));
 194     TS_ASSERT_THROWS(*++te, NoMoreValuesException);
 195     TS_ASSERT_THROWS(*++te, NoMoreValuesException);
 196     TS_ASSERT_THROWS(*++te, NoMoreValuesException);
 197   }
 198
 199   void testDatatypesInfinite1() {
 200     Datatype colors("Colors");
 201     colors.addConstructor(DatatypeConstructor("red"));
 202     colors.addConstructor(DatatypeConstructor("orange"));
 203     colors.addConstructor(DatatypeConstructor("yellow"));
 204     colors.addConstructor(DatatypeConstructor("green"));
 205     colors.addConstructor(DatatypeConstructor("blue"));
 206     colors.addConstructor(DatatypeConstructor("violet"));
 207     TypeNode colorsType = TypeNode::fromType(d_em->mkDatatypeType(colors));
 208     Datatype listColors("ListColors");
 209     DatatypeConstructor consC("cons");
 210     consC.addArg("car", colorsType.toType());
 211     consC.addArg("cdr", DatatypeSelfType());
 212     listColors.addConstructor(consC);
 213     listColors.addConstructor(DatatypeConstructor("nil"));
 214     TypeNode listColorsType = TypeNode::fromType(d_em->mkDatatypeType(listColors));
 215
 216     TypeEnumerator te(listColorsType);
 217     TS_ASSERT( ! te.isFinished() );
 218     Node cons = Node::fromExpr(DatatypeType(listColorsType.toType()).getDatatype().getConstructor("cons"));
 219     Node nil = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(listColorsType.toType()).getDatatype().getConstructor("nil"));
 220     Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("red"));
 221     Node orange = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("orange"));
 222     Node yellow = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("yellow"));
 223     TS_ASSERT_EQUALS(*te, nil);
 224     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil));
 225     TS_ASSERT( ! te.isFinished() );
 226     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
 227                             d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)));
 228     TS_ASSERT( ! te.isFinished() );
 229     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil));
 230     TS_ASSERT( ! te.isFinished() );
 231     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
 232                             d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
 233                             d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))));
 234     TS_ASSERT( ! te.isFinished() );
 235     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange,
 236                             d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)));
 237     TS_ASSERT( ! te.isFinished() );
 238     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, yellow, nil));
 239     TS_ASSERT( ! te.isFinished() );
 240     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
 241                             d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil)));
 242     TS_ASSERT( ! te.isFinished() );
 243   }
 244
 245   void NOTYETtestDatatypesInfinite2() {
 246     //TypeNode datatype;
 247     //TypeEnumerator te(datatype);
 248     //TS_ASSERT( ! te.isFinished() );
 249     TS_FAIL("unimplemented");
 250   }
 251
 252   void testArraysInfinite() {
 253     TypeEnumerator te(d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType()));
 254     hash_set<Node, NodeHashFunction> elts;
 255     for(size_t i = 0; i < 1000; ++i) {
 256       TS_ASSERT( ! te.isFinished() );
 257       Node elt = *te++;
 258       // ensure no duplicates
 259       TS_ASSERT( elts.find(elt) == elts.end() );
 260       elts.insert(elt);
 261     }
 262     TS_ASSERT( ! te.isFinished() );
 263
 264     // ensure that certain items were found
 265     ArrayType arrayType(d_em->mkArrayType(d_em->integerType(), d_em->integerType()));
 266     Node zeroes = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(0))));
 267     Node ones = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(1))));
 268     Node twos = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(2))));
 269     Node threes = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(3))));
 270     Node fours = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(4))));
 271     Node tens = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(10))));
 272
 273     Node zero = d_nm->mkConst(Rational(0));
 274     Node one = d_nm->mkConst(Rational(1));
 275     Node two = d_nm->mkConst(Rational(2));
 276     Node three = d_nm->mkConst(Rational(3));
 277     Node four = d_nm->mkConst(Rational(4));
 278     Node five = d_nm->mkConst(Rational(5));
 279     Node eleven = d_nm->mkConst(Rational(11));
 280
 281     // FIXME: the arrays enumerator isn't currently a fair enumerator,
 282     // so these will fail; disable them for now
 283     //TS_ASSERT( elts.find( d_nm->mkNode(STORE, ones, zero, zero) ) != elts.end() );
 284     //TS_ASSERT( elts.find( d_nm->mkNode(STORE, tens, four, five) ) != elts.end() );
 285     //TS_ASSERT( elts.find( d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, fours, eleven, two), two, one), zero, two) ) != elts.end() );
 286     //TS_ASSERT( elts.find( threes ) != elts.end() );
 287     //TS_ASSERT( elts.find( d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, twos, three, zero), two, zero), one, zero), zero, zero) ) != elts.end() );
 288   }
 289
 290   void testBV() {
 291     TypeEnumerator te(d_nm->mkBitVectorType(3));
 292     TS_ASSERT_EQUALS(*te, d_nm->mkConst(BitVector(3u, 0u)));
 293     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 1u)));
 294     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 2u)));
 295     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 3u)));
 296     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 4u)));
 297     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 5u)));
 298     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 6u)));
 299     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 7u)));
 300     TS_ASSERT_THROWS(*++te, NoMoreValuesException);
 301     TS_ASSERT_THROWS(*++te, NoMoreValuesException);
 302     TS_ASSERT_THROWS(*++te, NoMoreValuesException);
 303   }
 304
 305 };/* class TypeEnumeratorWhite */