From: Aina Niemetz Date: Thu, 3 Dec 2020 19:29:58 +0000 (-0800) Subject: google test: Add fixture for context tests. (#5590) X-Git-Tag: cvc5-1.0.0~2510 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8e1dc557383f754e33399b6b0f783e7048732df0;p=cvc5.git 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 9b171cf2c..fad525655 100644 --- 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 7e599b135..c87406a87 100644 --- 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 83ac768f1..ca64a322f 100644 --- 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 05427c01d..bb60ab7ac 100644 --- 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 8627f6033..f616a1a30 100644 --- 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 db3474af2..c8c98818f 100644 --- 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 1664ae70d..1f7f0ec1c 100644 --- 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 83e48f8ab..3e830c1fa 100644 --- 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 index 000000000..6d5420d56 --- /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 d_context; +}; + +} // namespace test +} // namespace CVC4 +#endif