google test: Add fixture for context tests. (#5590)

Context test PRs will be updated to use this after this is merged to
master.

diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp
index 9b171cf2c9dfb724ceffc2104ca562562291694a..fad525655fd7756d8cdb80c0dc7abc51383965e6 100644 (file)
--- a/test/unit/api/datatype_api_black.cpp
+++ b/test/unit/api/datatype_api_black.cpp
@@ -16,7 +16,11 @@
 
 #include "test_api.h"
 
-using namespace CVC4::api;
+namespace CVC4 {
+
+using namespace api;
+
+namespace test {
 
 class TestApiDatatypeBlack : public TestApi
 {
@@ -542,3 +546,5 @@ TEST_F(TestApiDatatypeBlack, datatypeSpecializedCons)
   // error to get the specialized constructor term for Int
   EXPECT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException);
 }
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp
index 7e599b135e505ac6a58b0aa2c304a64a120fffb0..c87406a87768574c24cf861a9b7c46abebc33b2b 100644 (file)
--- a/test/unit/api/grammar_black.cpp
+++ b/test/unit/api/grammar_black.cpp
@@ -16,7 +16,11 @@
 
 #include "test_api.h"
 
-using namespace CVC4::api;
+namespace CVC4 {
+
+using namespace api;
+
+namespace test {
 
 class TestApiGrammarBlack : public TestApi
 {
@@ -115,3 +119,5 @@ TEST_F(TestApiGrammarBlack, addAnyVariable)
 
   ASSERT_THROW(g1.addAnyVariable(start), CVC4ApiException);
 }
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp
index 83ac768f1d6e8b0fdf2ff6f362c9fd77eb7b27fe..ca64a322fc0890582f37eb2f834d5d74d602c091 100644 (file)
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/op_black.cpp
@@ -14,7 +14,11 @@
 
 #include "test_api.h"
 
-using namespace CVC4::api;
+namespace CVC4 {
+
+using namespace api;
+
+namespace test {
 
 class TestApiOpBlack : public TestApi
 {
@@ -178,3 +182,5 @@ TEST_F(TestApiOpBlack, opScopingToString)
   Solver solver2;
   EXPECT_EQ(bitvector_repeat_ot.toString(), op_repr);
 }
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp
index 05427c01d2c22e3ef61c6e77b2330d3f7b7d435d..bb60ab7ac10c0279978b811f45689f3c47884456 100644 (file)
--- a/test/unit/api/result_black.cpp
+++ b/test/unit/api/result_black.cpp
@@ -14,7 +14,11 @@
 
 #include "test_api.h"
 
-using namespace CVC4::api;
+namespace CVC4 {
+
+using namespace api;
+
+namespace test {
 
 class TestApiResultBlack : public TestApi
 {
@@ -22,7 +26,7 @@ class TestApiResultBlack : public TestApi
 
 TEST_F(TestApiResultBlack, isNull)
 {
-  Result res_null;
+  CVC4::api::Result res_null;
   ASSERT_TRUE(res_null.isNull());
   ASSERT_FALSE(res_null.isSat());
   ASSERT_FALSE(res_null.isUnsat());
@@ -33,7 +37,7 @@ TEST_F(TestApiResultBlack, isNull)
   Sort u_sort = d_solver.mkUninterpretedSort("u");
   Term x = d_solver.mkVar(u_sort, "x");
   d_solver.assertFormula(x.eqTerm(x));
-  Result res = d_solver.checkSat();
+  CVC4::api::Result res = d_solver.checkSat();
   ASSERT_FALSE(res.isNull());
 }
 
@@ -42,9 +46,9 @@ TEST_F(TestApiResultBlack, eq)
   Sort u_sort = d_solver.mkUninterpretedSort("u");
   Term x = d_solver.mkVar(u_sort, "x");
   d_solver.assertFormula(x.eqTerm(x));
-  Result res;
-  Result res2 = d_solver.checkSat();
-  Result res3 = d_solver.checkSat();
+  CVC4::api::Result res;
+  CVC4::api::Result res2 = d_solver.checkSat();
+  CVC4::api::Result res3 = d_solver.checkSat();
   res = res2;
   EXPECT_EQ(res, res2);
   EXPECT_EQ(res3, res2);
@@ -55,7 +59,7 @@ TEST_F(TestApiResultBlack, isSat)
   Sort u_sort = d_solver.mkUninterpretedSort("u");
   Term x = d_solver.mkVar(u_sort, "x");
   d_solver.assertFormula(x.eqTerm(x));
-  Result res = d_solver.checkSat();
+  CVC4::api::Result res = d_solver.checkSat();
   ASSERT_TRUE(res.isSat());
   ASSERT_FALSE(res.isSatUnknown());
 }
@@ -65,7 +69,7 @@ TEST_F(TestApiResultBlack, isUnsat)
   Sort u_sort = d_solver.mkUninterpretedSort("u");
   Term x = d_solver.mkVar(u_sort, "x");
   d_solver.assertFormula(x.eqTerm(x).notTerm());
-  Result res = d_solver.checkSat();
+  CVC4::api::Result res = d_solver.checkSat();
   ASSERT_TRUE(res.isUnsat());
   ASSERT_FALSE(res.isSatUnknown());
 }
@@ -78,7 +82,7 @@ TEST_F(TestApiResultBlack, isSatUnknown)
   Sort int_sort = d_solver.getIntegerSort();
   Term x = d_solver.mkVar(int_sort, "x");
   d_solver.assertFormula(x.eqTerm(x).notTerm());
-  Result res = d_solver.checkSat();
+  CVC4::api::Result res = d_solver.checkSat();
   ASSERT_FALSE(res.isSat());
   ASSERT_TRUE(res.isSatUnknown());
 }
@@ -92,10 +96,10 @@ TEST_F(TestApiResultBlack, isEntailed)
   Term a = x.eqTerm(y).notTerm();
   Term b = x.eqTerm(y);
   d_solver.assertFormula(a);
-  Result entailed = d_solver.checkEntailed(a);
+  CVC4::api::Result entailed = d_solver.checkEntailed(a);
   ASSERT_TRUE(entailed.isEntailed());
   ASSERT_FALSE(entailed.isEntailmentUnknown());
-  Result not_entailed = d_solver.checkEntailed(b);
+  CVC4::api::Result not_entailed = d_solver.checkEntailed(b);
   ASSERT_TRUE(not_entailed.isNotEntailed());
   ASSERT_FALSE(not_entailed.isEntailmentUnknown());
 }
@@ -108,8 +112,10 @@ TEST_F(TestApiResultBlack, isEntailmentUnknown)
   Sort int_sort = d_solver.getIntegerSort();
   Term x = d_solver.mkVar(int_sort, "x");
   d_solver.assertFormula(x.eqTerm(x).notTerm());
-  Result res = d_solver.checkEntailed(x.eqTerm(x));
+  CVC4::api::Result res = d_solver.checkEntailed(x.eqTerm(x));
   ASSERT_FALSE(res.isEntailed());
   ASSERT_TRUE(res.isEntailmentUnknown());
   EXPECT_EQ(res.getUnknownExplanation(), "UNKNOWN_REASON");
 }
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index 8627f6033c9a39d185fcceb796789ed33b4c53c8..f616a1a300674addd0b32714bcae958cae08603d 100644 (file)
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -14,7 +14,11 @@
 
 #include "test_api.h"
 
-using namespace CVC4::api;
+namespace CVC4 {
+
+using namespace api;
+
+namespace test {
 
 class TestApiTermBlack : public TestApi
 {
@@ -766,3 +770,5 @@ TEST_F(TestApiTermBlack, termScopedToString)
   Solver solver2;
   EXPECT_EQ(x.toString(), "x");
 }
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/base/map_util_black.cpp b/test/unit/base/map_util_black.cpp
index db3474af2fc38c269dda50e94ff7a3df5d40e8d2..c8c98818f75073d5395f758c1966f28ac9474c66 100644 (file)
--- a/test/unit/base/map_util_black.cpp
+++ b/test/unit/base/map_util_black.cpp
@@ -27,12 +27,13 @@
 #include "context/context.h"
 #include "test.h"
 
-using CVC4::ContainsKey;
-using CVC4::FindOrDie;
-using CVC4::FindOrNull;
-using CVC4::context::CDHashMap;
-using CVC4::context::CDInsertHashMap;
-using CVC4::context::Context;
+namespace CVC4 {
+
+using context::CDHashMap;
+using context::CDInsertHashMap;
+using context::Context;
+
+namespace test {
 
 class TestMapBlack : public TestInternal
 {
@@ -211,3 +212,5 @@ TEST_F(TestMapBlack, const_CDInsertHashMap)
   EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
   EXPECT_EQ(FindOrDie(map, "other"), "entry");
 }
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/test.h b/test/unit/test.h
index 1664ae70dd295467a9ef86d2148416bb6d267e52..1f7f0ec1cc5d60f2c2652c32c01d65a058d63b07 100644 (file)
--- a/test/unit/test.h
+++ b/test/unit/test.h
@@ -17,8 +17,13 @@
 
 #include "gtest/gtest.h"
 
+namespace CVC4 {
+namespace test {
+
 class TestInternal : public ::testing::Test
 {
 };
 
+}  // namespace test
+}  // namespace CVC4
 #endif

diff --git a/test/unit/test_api.h b/test/unit/test_api.h
index 83e48f8abcfadb3600f0dfb54eda7476a55f96e9..3e830c1fae03bd27df824cd5547d4f7d179dc255 100644 (file)
--- a/test/unit/test_api.h
+++ b/test/unit/test_api.h
@@ -18,10 +18,15 @@
 #include "api/cvc4cpp.h"
 #include "gtest/gtest.h"
 
+namespace CVC4 {
+namespace test {
+
 class TestApi : public ::testing::Test
 {
  protected:
   CVC4::api::Solver d_solver;
 };
 
+}  // namespace test
+}  // namespace CVC4
 #endif

diff --git a/test/unit/test_context.h b/test/unit/test_context.h
new file mode 100644 (file)
index 0000000..6d5420d
--- /dev/null
+++ b/test/unit/test_context.h
@@ -0,0 +1,33 @@
+/*********************                                                        */
+/*! \file test_context.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 Header for context unit tests.
+ **/
+
+#ifndef CVC4__TEST__UNIT__TEST_CONTEXT_H
+#define CVC4__TEST__UNIT__TEST_CONTEXT_H
+
+#include "context/context.h"
+#include "test.h"
+
+namespace CVC4 {
+namespace test {
+
+class TestContext : public TestInternal
+{
+ protected:
+  void SetUp() override { d_context.reset(new CVC4::context::Context()); }
+  std::unique_ptr<CVC4::context::Context> d_context;
+};
+
+}  // namespace test
+}  // namespace CVC4
+#endif