From: Aina Niemetz Date: Fri, 26 Feb 2021 23:16:57 +0000 (-0800) Subject: google test: theory: Migrate type_enumerator_white. (#6007) X-Git-Tag: cvc5-1.0.0~2197 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=21b3b7d708ce85c23c8d7a337d334b0989723595;p=cvc5.git google test: theory: Migrate type_enumerator_white. (#6007) --- diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 90155518e..32219e232 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -28,4 +28,4 @@ cvc4_add_unit_test_white(theory_sets_type_rules_white theory) cvc4_add_cxx_unit_test_white(theory_strings_skolem_cache_black theory) cvc4_add_cxx_unit_test_white(theory_strings_word_white theory) cvc4_add_cxx_unit_test_white(theory_white theory) -cvc4_add_cxx_unit_test_white(type_enumerator_white theory) +cvc4_add_unit_test_white(type_enumerator_white theory) diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp new file mode 100644 index 000000000..0693d7d35 --- /dev/null +++ b/test/unit/theory/type_enumerator_white.cpp @@ -0,0 +1,335 @@ +/********************* */ +/*! \file type_enumerator_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Andrew Reynolds, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief White box testing of CVC4::theory::TypeEnumerator + ** + ** White box testing of CVC4::theory::TypeEnumerator. (These tests depends + ** on the ordering that the TypeEnumerators use, so it's a white-box test.) + **/ + +#include + +#include "expr/array_store_all.h" +#include "expr/dtype.h" +#include "expr/kind.h" +#include "expr/type_node.h" +#include "options/language.h" +#include "test_smt.h" +#include "theory/type_enumerator.h" + +namespace CVC4 { + +using namespace theory; +using namespace kind; + +namespace test { + +class TestTheoryWhiteTypeEnumerator : public TestSmt +{ +}; + +TEST_F(TestTheoryWhiteTypeEnumerator, booleans) +{ + TypeEnumerator te(d_nodeManager->booleanType()); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*te, d_nodeManager->mkConst(false)); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*++te, d_nodeManager->mkConst(true)); + ASSERT_FALSE(te.isFinished()); + ASSERT_THROW(*++te, NoMoreValuesException); + ASSERT_TRUE(te.isFinished()); + ASSERT_THROW(*++te, NoMoreValuesException); + ASSERT_TRUE(te.isFinished()); + ASSERT_THROW(*++te, NoMoreValuesException); + ASSERT_TRUE(te.isFinished()); +} + +TEST_F(TestTheoryWhiteTypeEnumerator, uf) +{ + TypeNode sort = d_nodeManager->mkSort("T"); + TypeNode sort2 = d_nodeManager->mkSort("U"); + TypeEnumerator te(sort); + ASSERT_EQ(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, 0))); + for (size_t i = 1; i < 100; ++i) + { + ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i))); + ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort2, i))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(UninterpretedConstant(sort, i))); + ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i + 2))); + } +} + +TEST_F(TestTheoryWhiteTypeEnumerator, arith) +{ + TypeEnumerator te(d_nodeManager->integerType()); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*te, d_nodeManager->mkConst(Rational(0))); + for (int i = 1; i <= 100; ++i) + { + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(i))); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-i))); + } + ASSERT_FALSE(te.isFinished()); + + te = TypeEnumerator(d_nodeManager->realType()); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*te, d_nodeManager->mkConst(Rational(0, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 3))); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(4, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-4, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 4))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 4))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 1))); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(6, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-6, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(4, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-4, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 4))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 4))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 6))); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 6))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(7, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-7, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 7))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 7))); + ASSERT_FALSE(te.isFinished()); +} + +TEST_F(TestTheoryWhiteTypeEnumerator, dtypes_finite) +{ + DType dt("Colors"); + dt.addConstructor(std::make_shared("red")); + dt.addConstructor(std::make_shared("orange")); + dt.addConstructor(std::make_shared("yellow")); + dt.addConstructor(std::make_shared("green")); + dt.addConstructor(std::make_shared("blue")); + dt.addConstructor(std::make_shared("violet")); + TypeNode datatype = d_nodeManager->mkDatatypeType(dt); + const std::vector >& dtcons = + datatype.getDType().getConstructors(); + TypeEnumerator te(datatype); + ASSERT_EQ( + *te, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor())); + ASSERT_EQ( + *++te, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor())); + ASSERT_EQ( + *++te, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor())); + ASSERT_EQ( + *++te, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[3]->getConstructor())); + ASSERT_EQ( + *++te, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[4]->getConstructor())); + ASSERT_EQ( + *++te, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[5]->getConstructor())); + ASSERT_THROW(*++te, NoMoreValuesException); + ASSERT_THROW(*++te, NoMoreValuesException); + ASSERT_THROW(*++te, NoMoreValuesException); +} + +TEST_F(TestTheoryWhiteTypeEnumerator, dtypes_infinite) +{ + DType colors("Colors"); + colors.addConstructor(std::make_shared("red")); + colors.addConstructor(std::make_shared("orange")); + colors.addConstructor(std::make_shared("yellow")); + colors.addConstructor(std::make_shared("green")); + colors.addConstructor(std::make_shared("blue")); + colors.addConstructor(std::make_shared("violet")); + TypeNode colorsType = d_nodeManager->mkDatatypeType(colors); + const std::vector >& ctCons = + colorsType.getDType().getConstructors(); + DType listColors("ListColors"); + std::shared_ptr consC = + std::make_shared("cons"); + consC->addArg("car", colorsType); + consC->addArgSelf("cdr"); + listColors.addConstructor(consC); + listColors.addConstructor(std::make_shared("nil")); + TypeNode listColorsType = d_nodeManager->mkDatatypeType(listColors); + const std::vector >& lctCons = + listColorsType.getDType().getConstructors(); + + TypeEnumerator te(listColorsType); + ASSERT_FALSE(te.isFinished()); + Node cons = lctCons[0]->getConstructor(); + Node nil = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, lctCons[1]->getConstructor()); + Node red = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, ctCons[0]->getConstructor()); + Node orange = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, ctCons[1]->getConstructor()); + Node yellow = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, ctCons[2]->getConstructor()); + ASSERT_EQ(*te, nil); + ASSERT_EQ(*++te, d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*++te, + d_nodeManager->mkNode( + APPLY_CONSTRUCTOR, + cons, + red, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*++te, d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil)); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*++te, + d_nodeManager->mkNode( + APPLY_CONSTRUCTOR, + cons, + red, + d_nodeManager->mkNode( + APPLY_CONSTRUCTOR, + cons, + red, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*++te, + d_nodeManager->mkNode( + APPLY_CONSTRUCTOR, + cons, + orange, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*++te, d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, yellow, nil)); + ASSERT_FALSE(te.isFinished()); + ASSERT_EQ(*++te, + d_nodeManager->mkNode( + APPLY_CONSTRUCTOR, + cons, + red, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil))); + ASSERT_FALSE(te.isFinished()); +} + +TEST_F(TestTheoryWhiteTypeEnumerator, arrays_infinite) +{ + TypeEnumerator te(d_nodeManager->mkArrayType(d_nodeManager->integerType(), + d_nodeManager->integerType())); + std::unordered_set elts; + for (uint32_t i = 0; i < 1000; ++i) + { + ASSERT_FALSE(te.isFinished()); + Node elt = *te++; + // ensure no duplicates + ASSERT_TRUE(elts.find(elt) == elts.end()); + elts.insert(elt); + } + ASSERT_FALSE(te.isFinished()); + + // ensure that certain items were found + TypeNode arrayType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), + d_nodeManager->integerType()); + Node zeroes = d_nodeManager->mkConst( + ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(0)))); + Node ones = d_nodeManager->mkConst( + ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(1)))); + Node twos = d_nodeManager->mkConst( + ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(2)))); + Node threes = d_nodeManager->mkConst( + ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(3)))); + Node fours = d_nodeManager->mkConst( + ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(4)))); + Node tens = d_nodeManager->mkConst( + ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(10)))); + + Node zero = d_nodeManager->mkConst(Rational(0)); + Node one = d_nodeManager->mkConst(Rational(1)); + Node two = d_nodeManager->mkConst(Rational(2)); + Node three = d_nodeManager->mkConst(Rational(3)); + Node four = d_nodeManager->mkConst(Rational(4)); + Node five = d_nodeManager->mkConst(Rational(5)); + Node eleven = d_nodeManager->mkConst(Rational(11)); + + ASSERT_EQ(elts.find(d_nodeManager->mkNode(STORE, ones, zero, zero)), + elts.end()); + + // the arrays enumerator is currently not a fair enumerator -- when it is, + // these should be flipped + ASSERT_EQ(elts.find(d_nodeManager->mkNode(STORE, tens, four, five)), + elts.end()); + ASSERT_EQ(elts.find(d_nodeManager->mkNode( + STORE, + d_nodeManager->mkNode( + STORE, + d_nodeManager->mkNode(STORE, fours, eleven, two), + two, + one), + zero, + two)), + elts.end()); + ASSERT_EQ(elts.find(threes), elts.end()); + ASSERT_EQ(elts.find(d_nodeManager->mkNode( + STORE, + d_nodeManager->mkNode( + STORE, + d_nodeManager->mkNode( + STORE, + d_nodeManager->mkNode(STORE, twos, three, zero), + two, + zero), + one, + zero), + zero, + zero)), + elts.end()); +} + +TEST_F(TestTheoryWhiteTypeEnumerator, bv) +{ + TypeEnumerator te(d_nodeManager->mkBitVectorType(3)); + ASSERT_EQ(*te, d_nodeManager->mkConst(BitVector(3u, 0u))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 1u))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 2u))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 3u))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 4u))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 5u))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 6u))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 7u))); + ASSERT_THROW(*++te, NoMoreValuesException); + ASSERT_THROW(*++te, NoMoreValuesException); + ASSERT_THROW(*++te, NoMoreValuesException); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h deleted file mode 100644 index 24bf9922e..000000000 --- a/test/unit/theory/type_enumerator_white.h +++ /dev/null @@ -1,304 +0,0 @@ -/********************* */ -/*! \file type_enumerator_white.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief White box testing of CVC4::theory::TypeEnumerator - ** - ** White box testing of CVC4::theory::TypeEnumerator. (These tests depends - ** on the ordering that the TypeEnumerators use, so it's a white-box test.) - **/ - -#include - -#include - -#include "expr/array_store_all.h" -#include "expr/dtype.h" -#include "expr/expr_manager.h" -#include "expr/kind.h" -#include "expr/node_manager.h" -#include "expr/type_node.h" -#include "options/language.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/type_enumerator.h" - -using namespace CVC4; -using namespace CVC4::smt; -using namespace CVC4::theory; -using namespace CVC4::kind; - -using namespace std; - -class TypeEnumeratorWhite : public CxxTest::TestSuite { - public: - void setUp() override - { - d_em = new ExprManager(); - d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_nm); - d_scope = new SmtScope(d_smt); - d_smt->finishInit(); - } - - void tearDown() override - { - delete d_scope; - delete d_smt; - delete d_em; - } - - void testBooleans() { - TypeEnumerator te(d_nm->booleanType()); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*te, d_nm->mkConst(false)); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(true)); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_THROWS(*++te, NoMoreValuesException&); - TS_ASSERT( te.isFinished() ); - TS_ASSERT_THROWS(*++te, NoMoreValuesException&); - TS_ASSERT( te.isFinished() ); - TS_ASSERT_THROWS(*++te, NoMoreValuesException&); - TS_ASSERT( te.isFinished() ); - } - - void testUF() { - TypeNode sort = d_nm->mkSort("T"); - TypeNode sort2 = d_nm->mkSort("U"); - TypeEnumerator te(sort); - TS_ASSERT_EQUALS(*te, d_nm->mkConst(UninterpretedConstant(sort, 0))); - for(size_t i = 1; i < 100; ++i) { - TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort, i))); - TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort2, i))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(UninterpretedConstant(sort, i))); - TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort, i + 2))); - } - } - - void testArith() { - TypeEnumerator te(d_nm->integerType()); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0))); - for(int i = 1; i <= 100; ++i) { - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(i))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-i))); - } - TS_ASSERT( ! te.isFinished() ); - - te = TypeEnumerator(d_nm->realType()); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 2))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 2))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 3))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 3))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(4, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-4, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 2))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 2))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 3))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 3))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 4))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 4))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 1))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 5))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 5))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(6, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-6, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 2))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 2))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(4, 3))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-4, 3))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 4))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 4))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 5))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 5))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 6))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 6))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(7, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-7, 1))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 3))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 3))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 5))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 5))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 7))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 7))); - TS_ASSERT( ! te.isFinished() ); - } - - void testDTypesFinite() - { - DType dt("Colors"); - dt.addConstructor(std::make_shared("red")); - dt.addConstructor(std::make_shared("orange")); - dt.addConstructor(std::make_shared("yellow")); - dt.addConstructor(std::make_shared("green")); - dt.addConstructor(std::make_shared("blue")); - dt.addConstructor(std::make_shared("violet")); - TypeNode datatype = d_nm->mkDatatypeType(dt); - const std::vector >& dtcons = - datatype.getDType().getConstructors(); - TypeEnumerator te(datatype); - TS_ASSERT_EQUALS( - *te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor())); - TS_ASSERT_EQUALS( - *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor())); - TS_ASSERT_EQUALS( - *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor())); - TS_ASSERT_EQUALS( - *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[3]->getConstructor())); - TS_ASSERT_EQUALS( - *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[4]->getConstructor())); - TS_ASSERT_EQUALS( - *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[5]->getConstructor())); - TS_ASSERT_THROWS(*++te, NoMoreValuesException&); - TS_ASSERT_THROWS(*++te, NoMoreValuesException&); - TS_ASSERT_THROWS(*++te, NoMoreValuesException&); - } - - void testDTypesInfinite1() - { - DType colors("Colors"); - colors.addConstructor(std::make_shared("red")); - colors.addConstructor(std::make_shared("orange")); - colors.addConstructor(std::make_shared("yellow")); - colors.addConstructor(std::make_shared("green")); - colors.addConstructor(std::make_shared("blue")); - colors.addConstructor(std::make_shared("violet")); - TypeNode colorsType = d_nm->mkDatatypeType(colors); - const std::vector >& ctCons = - colorsType.getDType().getConstructors(); - DType listColors("ListColors"); - std::shared_ptr consC = - std::make_shared("cons"); - consC->addArg("car", colorsType); - consC->addArgSelf("cdr"); - listColors.addConstructor(consC); - listColors.addConstructor(std::make_shared("nil")); - TypeNode listColorsType = d_nm->mkDatatypeType(listColors); - const std::vector >& lctCons = - listColorsType.getDType().getConstructors(); - - TypeEnumerator te(listColorsType); - TS_ASSERT( ! te.isFinished() ); - Node cons = lctCons[0]->getConstructor(); - Node nil = d_nm->mkNode(APPLY_CONSTRUCTOR, lctCons[1]->getConstructor()); - Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[0]->getConstructor()); - Node orange = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[1]->getConstructor()); - Node yellow = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[2]->getConstructor()); - TS_ASSERT_EQUALS(*te, nil); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil)); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, yellow, nil)); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil))); - TS_ASSERT( ! te.isFinished() ); - } - - void NOTYETtestDTypesInfinite2() - { - //TypeNode datatype; - //TypeEnumerator te(datatype); - //TS_ASSERT( ! te.isFinished() ); - TS_FAIL("unimplemented"); - } - - void testArraysInfinite() { - TypeEnumerator te(d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType())); - unordered_set elts; - for(size_t i = 0; i < 1000; ++i) { - TS_ASSERT( ! te.isFinished() ); - Node elt = *te++; - // ensure no duplicates - TS_ASSERT( elts.find(elt) == elts.end() ); - elts.insert(elt); - } - TS_ASSERT( ! te.isFinished() ); - - // ensure that certain items were found - TypeNode arrayType = - d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType()); - Node zeroes = - d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(0)))); - Node ones = - d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(1)))); - Node twos = - d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(2)))); - Node threes = - d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(3)))); - Node fours = - d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(4)))); - Node tens = - d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(10)))); - - Node zero = d_nm->mkConst(Rational(0)); - Node one = d_nm->mkConst(Rational(1)); - Node two = d_nm->mkConst(Rational(2)); - Node three = d_nm->mkConst(Rational(3)); - Node four = d_nm->mkConst(Rational(4)); - Node five = d_nm->mkConst(Rational(5)); - Node eleven = d_nm->mkConst(Rational(11)); - - // FIXME: the arrays enumerator isn't currently a fair enumerator, - // so these will fail; disable them for now - //TS_ASSERT( elts.find( d_nm->mkNode(STORE, ones, zero, zero) ) != elts.end() ); - //TS_ASSERT( elts.find( d_nm->mkNode(STORE, tens, four, five) ) != elts.end() ); - //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() ); - //TS_ASSERT( elts.find( threes ) != elts.end() ); - //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() ); - } - - void testBV() { - TypeEnumerator te(d_nm->mkBitVectorType(3)); - TS_ASSERT_EQUALS(*te, d_nm->mkConst(BitVector(3u, 0u))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 1u))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 2u))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 3u))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 4u))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 5u))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 6u))); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 7u))); - TS_ASSERT_THROWS(*++te, NoMoreValuesException&); - TS_ASSERT_THROWS(*++te, NoMoreValuesException&); - TS_ASSERT_THROWS(*++te, NoMoreValuesException&); - } - - private: - ExprManager* d_em; - SmtEngine* d_smt; - NodeManager* d_nm; - SmtScope* d_scope; -};/* class TypeEnumeratorWhite */