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