google test: Remove obsolete Expr test fixtures. (#6060)

6 files changed, 32 insertions, 90 deletions

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<Test3, bool>;
 using TestFlag4 = Attribute<Test4, bool>;
 using TestFlag5 = Attribute<Test5, bool>;
 
-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<TypeNode> 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 <string>
 
 #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 <string>
 
 #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<smt::SmtScope> 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<NodeManager> d_nodeManager;
-  std::unique_ptr<NodeManagerScope> 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");
   }