From: Aina Niemetz Date: Tue, 9 Feb 2021 01:44:21 +0000 (-0800) Subject: google test: expr: Migrate type_node_white. (#5872) X-Git-Tag: cvc5-1.0.0~2304 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5baad1b32525ca623aaddfe557a3020edc4fe0b1;p=cvc5.git google test: expr: Migrate type_node_white. (#5872) --- diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index 18201b8a8..39545d056 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -25,4 +25,4 @@ 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_cxx_unit_test_white(type_node_white expr) +cvc4_add_unit_test_white(type_node_white expr) diff --git a/test/unit/expr/type_node_white.cpp b/test/unit/expr/type_node_white.cpp new file mode 100644 index 000000000..085b57642 --- /dev/null +++ b/test/unit/expr/type_node_white.cpp @@ -0,0 +1,99 @@ +/********************* */ +/*! \file type_node_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, 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 White box testing of TypeNode + ** + ** White box testing of TypeNode. + **/ + +#include +#include +#include + +#include "expr/expr.h" +#include "expr/expr_manager.h" +#include "expr/node_manager.h" +#include "expr/type_node.h" +#include "smt/smt_engine.h" +#include "test_node.h" + +namespace CVC4 { + +using namespace kind; +using namespace context; + +namespace test { + +class TestNodeWhiteTypeNode : public TestNodeWhite +{ + protected: + void SetUp() override + { + TestNodeWhite::SetUp(); + d_smt.reset(new SmtEngine(d_nodeManager.get())); + } + std::unique_ptr d_smt; +}; + +TEST_F(TestNodeWhiteTypeNode, sub_types) +{ + TypeNode realType = d_nodeManager->realType(); + TypeNode integerType = d_nodeManager->realType(); + TypeNode booleanType = d_nodeManager->booleanType(); + TypeNode arrayType = d_nodeManager->mkArrayType(realType, integerType); + TypeNode bvType = d_nodeManager->mkBitVectorType(32); + + Node x = d_nodeManager->mkBoundVar("x", realType); + Node xPos = d_nodeManager->mkNode(GT, x, d_nodeManager->mkConst(Rational(0))); + TypeNode funtype = d_nodeManager->mkFunctionType(integerType, booleanType); + Node lambda = d_nodeManager->mkVar("lambda", funtype); + std::vector formals; + formals.push_back(x); + d_smt->defineFunction(lambda, formals, xPos); + + ASSERT_FALSE(realType.isComparableTo(booleanType)); + ASSERT_TRUE(realType.isComparableTo(integerType)); + ASSERT_TRUE(realType.isComparableTo(realType)); + ASSERT_FALSE(realType.isComparableTo(arrayType)); + ASSERT_FALSE(realType.isComparableTo(bvType)); + + ASSERT_FALSE(booleanType.isComparableTo(integerType)); + ASSERT_FALSE(booleanType.isComparableTo(realType)); + ASSERT_TRUE(booleanType.isComparableTo(booleanType)); + ASSERT_FALSE(booleanType.isComparableTo(arrayType)); + ASSERT_FALSE(booleanType.isComparableTo(bvType)); + + ASSERT_TRUE(integerType.isComparableTo(realType)); + ASSERT_TRUE(integerType.isComparableTo(integerType)); + ASSERT_FALSE(integerType.isComparableTo(booleanType)); + ASSERT_FALSE(integerType.isComparableTo(arrayType)); + ASSERT_FALSE(integerType.isComparableTo(bvType)); + + ASSERT_FALSE(arrayType.isComparableTo(booleanType)); + ASSERT_FALSE(arrayType.isComparableTo(integerType)); + ASSERT_FALSE(arrayType.isComparableTo(realType)); + ASSERT_TRUE(arrayType.isComparableTo(arrayType)); + ASSERT_FALSE(arrayType.isComparableTo(bvType)); + + ASSERT_FALSE(bvType.isComparableTo(booleanType)); + ASSERT_FALSE(bvType.isComparableTo(integerType)); + ASSERT_FALSE(bvType.isComparableTo(realType)); + ASSERT_FALSE(bvType.isComparableTo(arrayType)); + ASSERT_TRUE(bvType.isComparableTo(bvType)); + + ASSERT_TRUE(realType.getBaseType() == realType); + ASSERT_TRUE(integerType.getBaseType() == realType); + ASSERT_TRUE(booleanType.getBaseType() == booleanType); + ASSERT_TRUE(arrayType.getBaseType() == arrayType); + ASSERT_TRUE(bvType.getBaseType() == bvType); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h deleted file mode 100644 index 042a7b1da..000000000 --- a/test/unit/expr/type_node_white.h +++ /dev/null @@ -1,109 +0,0 @@ -/********************* */ -/*! \file type_node_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 TypeNode - ** - ** White box testing of TypeNode. - **/ - -#include - -#include -#include -#include - -#include "expr/expr.h" -#include "expr/expr_manager.h" -#include "expr/node_manager.h" -#include "expr/type_node.h" -#include "smt/smt_engine.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace std; - -class TypeNodeWhite : public CxxTest::TestSuite { - ExprManager* d_em; - NodeManager* d_nm; - NodeManagerScope* d_scope; - SmtEngine* d_smt; - - public: - void setUp() override - { - d_em = new ExprManager(); - d_nm = d_em->getNodeManager(); - d_smt = new SmtEngine(d_nm); - d_scope = new NodeManagerScope(d_nm); - } - - void tearDown() override - { - delete d_scope; - delete d_smt; - delete d_em; - } - - void testSubtypes() { - TypeNode realType = d_nm->realType(); - TypeNode integerType = d_nm->realType(); - TypeNode booleanType = d_nm->booleanType(); - TypeNode arrayType = d_nm->mkArrayType(realType, integerType); - TypeNode bvType = d_nm->mkBitVectorType(32); - - Node x = d_nm->mkBoundVar("x", realType); - Node xPos = d_nm->mkNode(GT, x, d_nm->mkConst(Rational(0))); - TypeNode funtype = d_nm->mkFunctionType(integerType, booleanType); - Node lambda = d_nm->mkVar("lambda", funtype); - vector formals; - formals.push_back(x); - d_smt->defineFunction(lambda, formals, xPos); - - TS_ASSERT( not realType.isComparableTo(booleanType) ); - TS_ASSERT( realType.isComparableTo(integerType) ); - TS_ASSERT( realType.isComparableTo(realType) ); - TS_ASSERT( not realType.isComparableTo(arrayType) ); - TS_ASSERT( not realType.isComparableTo(bvType) ); - - TS_ASSERT( not booleanType.isComparableTo(integerType) ); - TS_ASSERT( not booleanType.isComparableTo(realType) ); - TS_ASSERT( booleanType.isComparableTo(booleanType) ); - TS_ASSERT( not booleanType.isComparableTo(arrayType) ); - TS_ASSERT( not booleanType.isComparableTo(bvType) ); - - TS_ASSERT( integerType.isComparableTo(realType) ); - TS_ASSERT( integerType.isComparableTo(integerType) ); - TS_ASSERT( not integerType.isComparableTo(booleanType) ); - TS_ASSERT( not integerType.isComparableTo(arrayType) ); - TS_ASSERT( not integerType.isComparableTo(bvType) ); - - TS_ASSERT( not arrayType.isComparableTo(booleanType) ); - TS_ASSERT( not arrayType.isComparableTo(integerType) ); - TS_ASSERT( not arrayType.isComparableTo(realType) ); - TS_ASSERT( arrayType.isComparableTo(arrayType) ); - TS_ASSERT( not arrayType.isComparableTo(bvType) ); - - TS_ASSERT( not bvType.isComparableTo(booleanType) ); - TS_ASSERT( not bvType.isComparableTo(integerType) ); - TS_ASSERT( not bvType.isComparableTo(realType) ); - TS_ASSERT( not bvType.isComparableTo(arrayType) ); - TS_ASSERT( bvType.isComparableTo(bvType) ); - - TS_ASSERT(realType.getBaseType() == realType); - TS_ASSERT(integerType.getBaseType() == realType); - TS_ASSERT(booleanType.getBaseType() == booleanType); - TS_ASSERT(arrayType.getBaseType() == arrayType); - TS_ASSERT(bvType.getBaseType() == bvType); - } - -};/* TypeNodeWhite */ -