test/unit/theory/type_enumerator_white.h

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