From: Aina Niemetz Date: Tue, 9 Feb 2021 17:47:53 +0000 (-0800) Subject: google test: expr: Migrate type_cardinality_black. (#5871) X-Git-Tag: cvc5-1.0.0~2301 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ac7e08a787592830db232a62c11b0cb5bcdd5edb;p=cvc5.git google test: expr: Migrate type_cardinality_black. (#5871) --- diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index f4af29bdc..81ce20ed3 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -24,5 +24,5 @@ cvc4_add_unit_test_black(node_self_iterator_black expr) cvc4_add_unit_test_black(node_traversal_black expr) cvc4_add_unit_test_white(node_white expr) cvc4_add_unit_test_black(symbol_table_black expr) -cvc4_add_cxx_unit_test_black(type_cardinality_public expr) +cvc4_add_unit_test_black(type_cardinality_black expr) cvc4_add_unit_test_white(type_node_white expr) diff --git a/test/unit/expr/type_cardinality_black.cpp b/test/unit/expr/type_cardinality_black.cpp new file mode 100644 index 000000000..8473ab5da --- /dev/null +++ b/test/unit/expr/type_cardinality_black.cpp @@ -0,0 +1,302 @@ +/********************* */ +/*! \file type_cardinality_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters, Andrew Reynolds + ** 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 Public box testing of Type::getCardinality() for various Types + ** + ** Public box testing of Type::getCardinality() for various Types. + **/ + +#include + +#include "expr/expr_manager.h" +#include "expr/kind.h" +#include "expr/node_manager.h" +#include "expr/type.h" +#include "test_api.h" +#include "util/cardinality.h" + +namespace CVC4 { + +using namespace kind; + +namespace test { + +class TestTypeCardinalityBlack : public TestApi +{ + protected: + void SetUp() override + { + TestApi::SetUp(); + d_em = d_solver.getExprManager(); + d_nm = d_solver.getNodeManager(); + } + ExprManager* d_em; + NodeManager* d_nm; +}; + +TEST_F(TestTypeCardinalityBlack, basics) +{ + ASSERT_EQ(d_em->booleanType().getCardinality().compare(2), + Cardinality::EQUAL); + ASSERT_EQ(d_em->integerType().getCardinality().compare(Cardinality::INTEGERS), + Cardinality::EQUAL); + ASSERT_EQ(d_em->realType().getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); +} + +TEST_F(TestTypeCardinalityBlack, arrays) +{ + Type intToInt = d_em->mkArrayType(d_em->integerType(), d_em->integerType()); + Type realToReal = d_em->mkArrayType(d_em->realType(), d_em->realType()); + Type realToInt = d_em->mkArrayType(d_em->realType(), d_em->integerType()); + Type intToReal = d_em->mkArrayType(d_em->integerType(), d_em->realType()); + Type intToBool = d_em->mkArrayType(d_em->integerType(), d_em->booleanType()); + Type realToBool = d_em->mkArrayType(d_em->realType(), d_em->booleanType()); + Type boolToReal = d_em->mkArrayType(d_em->booleanType(), d_em->realType()); + Type boolToInt = d_em->mkArrayType(d_em->booleanType(), d_em->integerType()); + Type boolToBool = d_em->mkArrayType(d_em->booleanType(), d_em->booleanType()); + + ASSERT_EQ(intToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(realToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(intToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(intToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(realToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(boolToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(boolToInt.getCardinality().compare(Cardinality::INTEGERS), + Cardinality::EQUAL); + ASSERT_EQ(boolToBool.getCardinality().compare(4), Cardinality::EQUAL); +} + +TEST_F(TestTypeCardinalityBlack, unary_functions) +{ + Type intToInt = + d_em->mkFunctionType(d_em->integerType(), d_em->integerType()); + Type realToReal = d_em->mkFunctionType(d_em->realType(), d_em->realType()); + Type realToInt = d_em->mkFunctionType(d_em->realType(), d_em->integerType()); + Type intToReal = d_em->mkFunctionType(d_em->integerType(), d_em->realType()); + Type intToBool = + d_em->mkFunctionType(d_em->integerType(), d_em->booleanType()); + Type realToBool = d_em->mkFunctionType(d_em->realType(), d_em->booleanType()); + Type boolToReal = d_em->mkFunctionType(d_em->booleanType(), d_em->realType()); + Type boolToInt = + d_em->mkFunctionType(d_em->booleanType(), d_em->integerType()); + Type boolToBool = + d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType()); + + ASSERT_EQ(intToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(realToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(intToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(intToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(realToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(boolToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(boolToInt.getCardinality().compare(Cardinality::INTEGERS), + Cardinality::EQUAL); + ASSERT_EQ(boolToBool.getCardinality().compare(4), Cardinality::EQUAL); +} + +TEST_F(TestTypeCardinalityBlack, binary_functions) +{ + std::vector boolbool; + boolbool.push_back(d_em->booleanType()); + boolbool.push_back(d_em->booleanType()); + std::vector boolint; + boolint.push_back(d_em->booleanType()); + boolint.push_back(d_em->integerType()); + std::vector intbool; + intbool.push_back(d_em->integerType()); + intbool.push_back(d_em->booleanType()); + std::vector intint; + intint.push_back(d_em->integerType()); + intint.push_back(d_em->integerType()); + std::vector intreal; + intreal.push_back(d_em->integerType()); + intreal.push_back(d_em->realType()); + std::vector realint; + realint.push_back(d_em->realType()); + realint.push_back(d_em->integerType()); + std::vector realreal; + realreal.push_back(d_em->realType()); + realreal.push_back(d_em->realType()); + std::vector realbool; + realbool.push_back(d_em->realType()); + realbool.push_back(d_em->booleanType()); + std::vector boolreal; + boolreal.push_back(d_em->booleanType()); + boolreal.push_back(d_em->realType()); + + Type boolboolToBool = d_em->mkFunctionType(boolbool, d_em->booleanType()); + Type boolboolToInt = d_em->mkFunctionType(boolbool, d_em->integerType()); + Type boolboolToReal = d_em->mkFunctionType(boolbool, d_em->realType()); + + Type boolintToBool = d_em->mkFunctionType(boolint, d_em->booleanType()); + Type boolintToInt = d_em->mkFunctionType(boolint, d_em->integerType()); + Type boolintToReal = d_em->mkFunctionType(boolint, d_em->realType()); + + Type intboolToBool = d_em->mkFunctionType(intbool, d_em->booleanType()); + Type intboolToInt = d_em->mkFunctionType(intbool, d_em->integerType()); + Type intboolToReal = d_em->mkFunctionType(intbool, d_em->realType()); + + Type intintToBool = d_em->mkFunctionType(intint, d_em->booleanType()); + Type intintToInt = d_em->mkFunctionType(intint, d_em->integerType()); + Type intintToReal = d_em->mkFunctionType(intint, d_em->realType()); + + Type intrealToBool = d_em->mkFunctionType(intreal, d_em->booleanType()); + Type intrealToInt = d_em->mkFunctionType(intreal, d_em->integerType()); + Type intrealToReal = d_em->mkFunctionType(intreal, d_em->realType()); + + Type realintToBool = d_em->mkFunctionType(realint, d_em->booleanType()); + Type realintToInt = d_em->mkFunctionType(realint, d_em->integerType()); + Type realintToReal = d_em->mkFunctionType(realint, d_em->realType()); + + Type realrealToBool = d_em->mkFunctionType(realreal, d_em->booleanType()); + Type realrealToInt = d_em->mkFunctionType(realreal, d_em->integerType()); + Type realrealToReal = d_em->mkFunctionType(realreal, d_em->realType()); + + Type realboolToBool = d_em->mkFunctionType(realbool, d_em->booleanType()); + Type realboolToInt = d_em->mkFunctionType(realbool, d_em->integerType()); + Type realboolToReal = d_em->mkFunctionType(realbool, d_em->realType()); + + Type boolrealToBool = d_em->mkFunctionType(boolreal, d_em->booleanType()); + Type boolrealToInt = d_em->mkFunctionType(boolreal, d_em->integerType()); + Type boolrealToReal = d_em->mkFunctionType(boolreal, d_em->realType()); + + ASSERT_EQ(boolboolToBool.getCardinality().compare(16), Cardinality::EQUAL); + ASSERT_EQ(boolboolToInt.getCardinality().compare(Cardinality::INTEGERS), + Cardinality::EQUAL); + ASSERT_EQ(boolboolToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + + ASSERT_EQ(boolintToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(boolintToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(boolintToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + + ASSERT_EQ(intboolToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(intboolToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(intboolToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + + ASSERT_EQ(intintToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(intintToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(intintToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + + ASSERT_EQ(intrealToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(intrealToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(intrealToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + + ASSERT_EQ(realintToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realintToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realintToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + + ASSERT_EQ(realrealToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realrealToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realrealToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + + ASSERT_EQ(realboolToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realboolToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realboolToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + + ASSERT_EQ(boolrealToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(boolrealToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(boolrealToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); +} + +TEST_F(TestTypeCardinalityBlack, ternary_functions) +{ + std::vector boolbool; + boolbool.push_back(d_nm->booleanType()); + boolbool.push_back(d_nm->booleanType()); + std::vector boolboolbool = boolbool; + boolboolbool.push_back(d_nm->booleanType()); + + TypeNode boolboolTuple = d_nm->mkTupleType(boolbool); + TypeNode boolboolboolTuple = d_nm->mkTupleType(boolboolbool); + + TypeNode boolboolboolToBool = + d_nm->mkFunctionType(boolboolbool, d_nm->booleanType()); + TypeNode boolboolToBoolbool = d_nm->mkFunctionType(boolbool, boolboolTuple); + TypeNode boolToBoolboolbool = + d_nm->mkFunctionType(d_nm->booleanType(), boolboolboolTuple); + + ASSERT_EQ(boolboolboolToBool.getCardinality().compare(/* 2 ^ 8 */ 1 << 8), + Cardinality::EQUAL); + ASSERT_EQ( + boolboolToBoolbool.getCardinality().compare(/* 4 ^ 4 */ 4 * 4 * 4 * 4), + Cardinality::EQUAL); + ASSERT_EQ(boolToBoolboolbool.getCardinality().compare(/* 8 ^ 2 */ 8 * 8), + Cardinality::EQUAL); +} + +TEST_F(TestTypeCardinalityBlack, undefined_sorts) +{ + Type foo = d_em->mkSort("foo", NodeManager::SORT_FLAG_NONE); + // We've currently assigned them a specific Beth number, which + // isn't really correct, but... + ASSERT_FALSE(foo.getCardinality().isFinite()); +} + +TEST_F(TestTypeCardinalityBlack, bitvectors) +{ + ASSERT_EQ(d_em->mkBitVectorType(0).getCardinality().compare(0), + Cardinality::EQUAL); + Cardinality lastCard = 0; + for (unsigned i = 1; i <= 65; ++i) + { + Cardinality card = Cardinality(2) ^ i; + Cardinality typeCard = d_em->mkBitVectorType(i).getCardinality(); + ASSERT_TRUE(typeCard.compare(lastCard) == Cardinality::GREATER + || (typeCard.isLargeFinite() && lastCard.isLargeFinite())); + ASSERT_TRUE(typeCard.compare(card) == Cardinality::EQUAL + || typeCard.isLargeFinite()); + lastCard = typeCard; + } +} + +} // namespace test +} // namespace CVC4 diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h deleted file mode 100644 index 40a8b58dc..000000000 --- a/test/unit/expr/type_cardinality_public.h +++ /dev/null @@ -1,243 +0,0 @@ -/********************* */ -/*! \file type_cardinality_public.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Andrew Reynolds - ** 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 Public box testing of Type::getCardinality() for various Types - ** - ** Public box testing of Type::getCardinality() for various Types. - **/ - -#include - -#include -#include -#include - -#include "api/cvc4cpp.h" -#include "expr/expr_manager.h" -#include "expr/kind.h" -#include "expr/node_manager.h" -#include "expr/type.h" -#include "util/cardinality.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace std; - -class TypeCardinalityPublic : public CxxTest::TestSuite { - public: - void setUp() override - { - d_slv = new api::Solver(); - d_em = d_slv->getExprManager(); - d_nm = d_slv->getNodeManager(); - } - - void tearDown() override { delete d_slv; } - - void testTheBasics() - { - TS_ASSERT(d_em->booleanType().getCardinality().compare(2) - == Cardinality::EQUAL); - TS_ASSERT( - d_em->integerType().getCardinality().compare(Cardinality::INTEGERS) - == Cardinality::EQUAL); - TS_ASSERT(d_em->realType().getCardinality().compare(Cardinality::REALS) - == Cardinality::EQUAL); - } - - void testArrays() { - Type intToInt = d_em->mkArrayType(d_em->integerType(), d_em->integerType()); - Type realToReal = d_em->mkArrayType(d_em->realType(), d_em->realType()); - Type realToInt = d_em->mkArrayType(d_em->realType(), d_em->integerType()); - Type intToReal = d_em->mkArrayType(d_em->integerType(), d_em->realType()); - Type intToBool = d_em->mkArrayType(d_em->integerType(), d_em->booleanType()); - Type realToBool = d_em->mkArrayType(d_em->realType(), d_em->booleanType()); - Type boolToReal = d_em->mkArrayType(d_em->booleanType(), d_em->realType()); - Type boolToInt = d_em->mkArrayType(d_em->booleanType(), d_em->integerType()); - Type boolToBool = d_em->mkArrayType(d_em->booleanType(), d_em->booleanType()); - - TS_ASSERT( intToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( realToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( realToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( intToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( intToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( realToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( boolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( boolToInt.getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL ); - TS_ASSERT( boolToBool.getCardinality().compare(4) == Cardinality::EQUAL ); - } - - void testUnaryFunctions() { - Type intToInt = d_em->mkFunctionType(d_em->integerType(), d_em->integerType()); - Type realToReal = d_em->mkFunctionType(d_em->realType(), d_em->realType()); - Type realToInt = d_em->mkFunctionType(d_em->realType(), d_em->integerType()); - Type intToReal = d_em->mkFunctionType(d_em->integerType(), d_em->realType()); - Type intToBool = d_em->mkFunctionType(d_em->integerType(), d_em->booleanType()); - Type realToBool = d_em->mkFunctionType(d_em->realType(), d_em->booleanType()); - Type boolToReal = d_em->mkFunctionType(d_em->booleanType(), d_em->realType()); - Type boolToInt = d_em->mkFunctionType(d_em->booleanType(), d_em->integerType()); - Type boolToBool = d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType()); - - TS_ASSERT( intToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( realToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( realToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( intToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( intToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( realToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( boolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( boolToInt.getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL ); - TS_ASSERT( boolToBool.getCardinality().compare(4) == Cardinality::EQUAL ); - } - - void testBinaryFunctions() { - vector boolbool; boolbool.push_back(d_em->booleanType()); boolbool.push_back(d_em->booleanType()); - vector boolint; boolint.push_back(d_em->booleanType()); boolint.push_back(d_em->integerType()); - vector intbool; intbool.push_back(d_em->integerType()); intbool.push_back(d_em->booleanType()); - vector intint; intint.push_back(d_em->integerType()); intint.push_back(d_em->integerType()); - vector intreal; intreal.push_back(d_em->integerType()); intreal.push_back(d_em->realType()); - vector realint; realint.push_back(d_em->realType()); realint.push_back(d_em->integerType()); - vector realreal; realreal.push_back(d_em->realType()); realreal.push_back(d_em->realType()); - vector realbool; realbool.push_back(d_em->realType()); realbool.push_back(d_em->booleanType()); - vector boolreal; boolreal.push_back(d_em->booleanType()); boolreal.push_back(d_em->realType()); - - Type boolboolToBool = d_em->mkFunctionType(boolbool, d_em->booleanType()); - Type boolboolToInt = d_em->mkFunctionType(boolbool, d_em->integerType()); - Type boolboolToReal = d_em->mkFunctionType(boolbool, d_em->realType()); - - Type boolintToBool = d_em->mkFunctionType(boolint, d_em->booleanType()); - Type boolintToInt = d_em->mkFunctionType(boolint, d_em->integerType()); - Type boolintToReal = d_em->mkFunctionType(boolint, d_em->realType()); - - Type intboolToBool = d_em->mkFunctionType(intbool, d_em->booleanType()); - Type intboolToInt = d_em->mkFunctionType(intbool, d_em->integerType()); - Type intboolToReal = d_em->mkFunctionType(intbool, d_em->realType()); - - Type intintToBool = d_em->mkFunctionType(intint, d_em->booleanType()); - Type intintToInt = d_em->mkFunctionType(intint, d_em->integerType()); - Type intintToReal = d_em->mkFunctionType(intint, d_em->realType()); - - Type intrealToBool = d_em->mkFunctionType(intreal, d_em->booleanType()); - Type intrealToInt = d_em->mkFunctionType(intreal, d_em->integerType()); - Type intrealToReal = d_em->mkFunctionType(intreal, d_em->realType()); - - Type realintToBool = d_em->mkFunctionType(realint, d_em->booleanType()); - Type realintToInt = d_em->mkFunctionType(realint, d_em->integerType()); - Type realintToReal = d_em->mkFunctionType(realint, d_em->realType()); - - Type realrealToBool = d_em->mkFunctionType(realreal, d_em->booleanType()); - Type realrealToInt = d_em->mkFunctionType(realreal, d_em->integerType()); - Type realrealToReal = d_em->mkFunctionType(realreal, d_em->realType()); - - Type realboolToBool = d_em->mkFunctionType(realbool, d_em->booleanType()); - Type realboolToInt = d_em->mkFunctionType(realbool, d_em->integerType()); - Type realboolToReal = d_em->mkFunctionType(realbool, d_em->realType()); - - Type boolrealToBool = d_em->mkFunctionType(boolreal, d_em->booleanType()); - Type boolrealToInt = d_em->mkFunctionType(boolreal, d_em->integerType()); - Type boolrealToReal = d_em->mkFunctionType(boolreal, d_em->realType()); - - TS_ASSERT( boolboolToBool.getCardinality().compare(16) == Cardinality::EQUAL ); - TS_ASSERT( boolboolToInt.getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL ); - TS_ASSERT( boolboolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - - TS_ASSERT( boolintToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( boolintToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( boolintToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - - TS_ASSERT( intboolToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( intboolToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( intboolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - - TS_ASSERT( intintToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( intintToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( intintToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - - TS_ASSERT( intrealToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( intrealToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( intrealToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - - TS_ASSERT( realintToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( realintToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( realintToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - - TS_ASSERT( realrealToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( realrealToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( realrealToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - - TS_ASSERT( realboolToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( realboolToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( realboolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - - TS_ASSERT( boolrealToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( boolrealToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( boolrealToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - } - - void testTernaryFunctions() { - vector boolbool; - boolbool.push_back(d_nm->booleanType()); - boolbool.push_back(d_nm->booleanType()); - vector boolboolbool = boolbool; - boolboolbool.push_back(d_nm->booleanType()); - - TypeNode boolboolTuple = d_nm->mkTupleType(boolbool); - TypeNode boolboolboolTuple = d_nm->mkTupleType(boolboolbool); - - TypeNode boolboolboolToBool = - d_nm->mkFunctionType(boolboolbool, d_nm->booleanType()); - TypeNode boolboolToBoolbool = d_nm->mkFunctionType(boolbool, boolboolTuple); - TypeNode boolToBoolboolbool = - d_nm->mkFunctionType(d_nm->booleanType(), boolboolboolTuple); - - TS_ASSERT( boolboolboolToBool.getCardinality().compare(/* 2 ^ 8 */ 1 << 8) == Cardinality::EQUAL ); - TS_ASSERT( boolboolToBoolbool.getCardinality().compare(/* 4 ^ 4 */ 4 * 4 * 4 * 4) == Cardinality::EQUAL ); - TS_ASSERT( boolToBoolboolbool.getCardinality().compare(/* 8 ^ 2 */ 8 * 8) == Cardinality::EQUAL ); - } - - void testUndefinedSorts() { - Type foo = d_em->mkSort("foo", NodeManager::SORT_FLAG_NONE); - // We've currently assigned them a specific Beth number, which - // isn't really correct, but... - TS_ASSERT( !foo.getCardinality().isFinite() ); - } - - void testBitvectors() { - //Debug.on("bvcard"); - TS_ASSERT( d_em->mkBitVectorType(0).getCardinality().compare(0) == Cardinality::EQUAL ); - Cardinality lastCard = 0; - for(unsigned i = 1; i <= 65; ++i) { - try { - Cardinality card = Cardinality(2) ^ i; - Cardinality typeCard = d_em->mkBitVectorType(i).getCardinality(); - TS_ASSERT( typeCard.compare(lastCard) == Cardinality::GREATER || - (typeCard.isLargeFinite() && lastCard.isLargeFinite()) ); - if( typeCard.compare(card) != Cardinality::EQUAL ) { - if( typeCard.isLargeFinite() ) { - cout << "test hit large finite card at bitvector(" << i << ")" << endl; - } else { - stringstream ss; - ss << "test failed for bitvector(" << i << ")"; - TS_FAIL(ss.str().c_str()); - } - } - lastCard = typeCard; - } catch(Exception& e) { - cout << endl << e << endl; - throw; - } - } - } - - private: - api::Solver* d_slv; - ExprManager* d_em; - NodeManager* d_nm; -};/* TypeCardinalityPublic */