From: Aina Niemetz Date: Fri, 5 Mar 2021 14:09:06 +0000 (-0800) Subject: google test: Remove obsolete Expr test fixtures. (#6060) X-Git-Tag: cvc5-1.0.0~2147 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4a72fbf9c96d5dda96cc2b198a4ef2e7c23c7b44;p=cvc5.git google test: Remove obsolete Expr test fixtures. (#6060) --- diff --git a/test/unit/expr/attribute_black.cpp b/test/unit/expr/attribute_black.cpp index da15f6b63..1cf6bcfbe 100644 --- a/test/unit/expr/attribute_black.cpp +++ b/test/unit/expr/attribute_black.cpp @@ -21,7 +21,7 @@ #include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_value.h" -#include "test_expr.h" +#include "test_node.h" namespace CVC4 { @@ -30,7 +30,7 @@ using namespace smt; namespace test { -class TestExprBlackAttribute : public TestExprBlack +class TestExprBlackAttribute : public TestNode { protected: struct PrimitiveIntAttributeId diff --git a/test/unit/expr/attribute_white.cpp b/test/unit/expr/attribute_white.cpp index ab99b842f..60098b47f 100644 --- a/test/unit/expr/attribute_white.cpp +++ b/test/unit/expr/attribute_white.cpp @@ -25,7 +25,7 @@ #include "expr/node_value.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" -#include "test_expr.h" +#include "test_node.h" #include "theory/theory.h" #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" @@ -54,12 +54,12 @@ using TestFlag3 = Attribute; using TestFlag4 = Attribute; using TestFlag5 = Attribute; -class TestExprWhiteAttribute : public TestExprWhite +class TestExprWhiteAttribute : public TestNode { protected: void SetUp() override { - TestExprWhite::SetUp(); + TestNode::SetUp(); d_booleanType.reset(new TypeNode(d_nodeManager->booleanType())); } std::unique_ptr d_booleanType; diff --git a/test/unit/expr/kind_black.cpp b/test/unit/expr/kind_black.cpp index a5bba4d99..8cc732bd9 100644 --- a/test/unit/expr/kind_black.cpp +++ b/test/unit/expr/kind_black.cpp @@ -19,7 +19,7 @@ #include #include "expr/kind.h" -#include "test_expr.h" +#include "test.h" namespace CVC4 { @@ -27,16 +27,16 @@ using namespace kind; namespace test { -class TestExprBlackKind : public TestExprBlack +class TestExprBlackKind : public TestInternal { protected: void SetUp() override { - undefined = UNDEFINED_KIND; - null = NULL_EXPR; - last = LAST_KIND; - beyond = ((int32_t)LAST_KIND) + 1; - unknown = (Kind)beyond; + d_undefined = UNDEFINED_KIND; + d_null = NULL_EXPR; + d_last = LAST_KIND; + d_beyond = ((int32_t)LAST_KIND) + 1; + d_unknown = (Kind)d_beyond; } bool string_is_as_expected(Kind k, const char* s) @@ -48,38 +48,38 @@ class TestExprBlackKind : public TestExprBlack return act.str() == exp.str(); } - Kind undefined; - Kind unknown; - Kind null; - Kind last; - int32_t beyond; + Kind d_undefined; + Kind d_unknown; + Kind d_null; + Kind d_last; + int32_t d_beyond; }; TEST_F(TestExprBlackKind, equality) { - ASSERT_EQ(undefined, UNDEFINED_KIND); - ASSERT_EQ(last, LAST_KIND); + ASSERT_EQ(d_undefined, UNDEFINED_KIND); + ASSERT_EQ(d_last, LAST_KIND); } TEST_F(TestExprBlackKind, order) { - ASSERT_LT((int32_t)undefined, (int32_t)null); - ASSERT_LT((int32_t)null, (int32_t)last); - ASSERT_LT((int32_t)undefined, (int32_t)last); - ASSERT_LT((int32_t)last, (int32_t)unknown); + ASSERT_LT((int32_t)d_undefined, (int32_t)d_null); + ASSERT_LT((int32_t)d_null, (int32_t)d_last); + ASSERT_LT((int32_t)d_undefined, (int32_t)d_last); + ASSERT_LT((int32_t)d_last, (int32_t)d_unknown); } TEST_F(TestExprBlackKind, output) { - ASSERT_TRUE(string_is_as_expected(undefined, "UNDEFINED_KIND")); - ASSERT_TRUE(string_is_as_expected(null, "NULL")); - ASSERT_TRUE(string_is_as_expected(last, "LAST_KIND")); + ASSERT_TRUE(string_is_as_expected(d_undefined, "UNDEFINED_KIND")); + ASSERT_TRUE(string_is_as_expected(d_null, "NULL")); + ASSERT_TRUE(string_is_as_expected(d_last, "LAST_KIND")); } TEST_F(TestExprBlackKind, output_concat) { std::stringstream act, exp; - act << undefined << null << last << unknown; + act << d_undefined << d_null << d_last << d_unknown; exp << "UNDEFINED_KIND" << "NULL" << "LAST_KIND" diff --git a/test/unit/expr/kind_map_black.cpp b/test/unit/expr/kind_map_black.cpp index 83d0bb452..1d99d5780 100644 --- a/test/unit/expr/kind_map_black.cpp +++ b/test/unit/expr/kind_map_black.cpp @@ -19,7 +19,7 @@ #include #include "expr/kind_map.h" -#include "test_expr.h" +#include "test.h" namespace CVC4 { @@ -27,7 +27,7 @@ using namespace kind; namespace test { -class TestExprBlackKindMap : public TestExprBlack +class TestExprBlackKindMap : public TestInternal { }; diff --git a/test/unit/test_expr.h b/test/unit/test_expr.h deleted file mode 100644 index 8c81f5902..000000000 --- a/test/unit/test_expr.h +++ /dev/null @@ -1,58 +0,0 @@ -/********************* */ -/*! \file test_expr.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** 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 Common header for Expr unit tests. - **/ - -#ifndef CVC4__TEST__UNIT__TEST_EXPR_H -#define CVC4__TEST__UNIT__TEST_EXPR_H - -#include "expr/expr_manager.h" -#include "expr/node_manager.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "test.h" -#include "test_api.h" - -namespace CVC4 { -namespace test { - -class TestExprBlack : public TestApi -{ - protected: - void SetUp() override - { - d_exprManager = d_solver.getExprManager(); - d_nodeManager = NodeManager::fromExprManager(d_exprManager); - d_smtEngine = d_solver.getSmtEngine(); - d_scope.reset(new smt::SmtScope(d_smtEngine)); - } - std::unique_ptr d_scope; - ExprManager* d_exprManager; - NodeManager* d_nodeManager; - SmtEngine* d_smtEngine; -}; - -class TestExprWhite : public TestApi -{ - protected: - void SetUp() override - { - d_nodeManager.reset(new NodeManager(nullptr)); - d_scope.reset(new NodeManagerScope(d_nodeManager.get())); - } - std::unique_ptr d_nodeManager; - std::unique_ptr d_scope; -}; - -} // namespace test -} // namespace CVC4 -#endif diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index 0120dda76..b3b74cf90 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -21,17 +21,17 @@ #include "expr/dtype_cons.h" #include "expr/expr.h" #include "expr/type_node.h" -#include "test_expr.h" +#include "test_smt.h" namespace CVC4 { namespace test { -class TestUtilBlackDatatype : public TestExprBlack +class TestUtilBlackDatatype : public TestSmt { public: void SetUp() override { - TestExprBlack::SetUp(); + TestSmt::SetUp(); Debug.on("datatypes"); Debug.on("groundterms"); }