diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-31 15:23:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-31 22:23:17 +0000 |
commit | a1466978fbc328507406d4a121dab4d1a1047e1d (patch) | |
tree | 12b40f161bb4d7a6ee40c20c78a15d6cda3c1995 /test/unit | |
parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) |
Rename namespace CVC4 to CVC5. (#6249)
Diffstat (limited to 'test/unit')
87 files changed, 423 insertions, 424 deletions
diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp index ccc61c36a..97db622c6 100644 --- a/test/unit/api/datatype_api_black.cpp +++ b/test/unit/api/datatype_api_black.cpp @@ -16,7 +16,7 @@ #include "test_api.h" -namespace CVC4 { +namespace CVC5 { using namespace api; @@ -547,4 +547,4 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons) ASSERT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp index c816fa5a3..96ad29503 100644 --- a/test/unit/api/grammar_black.cpp +++ b/test/unit/api/grammar_black.cpp @@ -16,7 +16,7 @@ #include "test_api.h" -namespace CVC4 { +namespace CVC5 { using namespace api; @@ -122,4 +122,4 @@ TEST_F(TestApiBlackGrammar, addAnyVariable) ASSERT_THROW(g1.addAnyVariable(start), CVC4ApiException); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp index 46aa9799b..2333e5719 100644 --- a/test/unit/api/op_black.cpp +++ b/test/unit/api/op_black.cpp @@ -14,7 +14,7 @@ #include "test_api.h" -namespace CVC4 { +namespace CVC5 { using namespace api; @@ -178,4 +178,4 @@ TEST_F(TestApiBlackOp, opScopingToString) ASSERT_EQ(bitvector_repeat_ot.toString(), op_repr); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/api/op_white.cpp b/test/unit/api/op_white.cpp index a8509ee26..49a964e9e 100644 --- a/test/unit/api/op_white.cpp +++ b/test/unit/api/op_white.cpp @@ -14,7 +14,7 @@ #include "test_api.h" -namespace CVC4 { +namespace CVC5 { using namespace api; @@ -32,4 +32,4 @@ TEST_F(TestApiWhiteOp, opFromKind) ASSERT_EQ(plus, d_solver.mkOp(PLUS)); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp index a52eba2b7..f27b30431 100644 --- a/test/unit/api/result_black.cpp +++ b/test/unit/api/result_black.cpp @@ -14,7 +14,7 @@ #include "test_api.h" -namespace CVC4 { +namespace CVC5 { using namespace api; @@ -26,7 +26,7 @@ class TestApiBlackResult : public TestApi TEST_F(TestApiBlackResult, isNull) { - CVC4::api::Result res_null; + CVC5::api::Result res_null; ASSERT_TRUE(res_null.isNull()); ASSERT_FALSE(res_null.isSat()); ASSERT_FALSE(res_null.isUnsat()); @@ -37,7 +37,7 @@ TEST_F(TestApiBlackResult, isNull) Sort u_sort = d_solver.mkUninterpretedSort("u"); Term x = d_solver.mkVar(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x)); - CVC4::api::Result res = d_solver.checkSat(); + CVC5::api::Result res = d_solver.checkSat(); ASSERT_FALSE(res.isNull()); } @@ -46,9 +46,9 @@ TEST_F(TestApiBlackResult, eq) Sort u_sort = d_solver.mkUninterpretedSort("u"); Term x = d_solver.mkVar(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x)); - CVC4::api::Result res; - CVC4::api::Result res2 = d_solver.checkSat(); - CVC4::api::Result res3 = d_solver.checkSat(); + CVC5::api::Result res; + CVC5::api::Result res2 = d_solver.checkSat(); + CVC5::api::Result res3 = d_solver.checkSat(); res = res2; ASSERT_EQ(res, res2); ASSERT_EQ(res3, res2); @@ -59,7 +59,7 @@ TEST_F(TestApiBlackResult, isSat) Sort u_sort = d_solver.mkUninterpretedSort("u"); Term x = d_solver.mkVar(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x)); - CVC4::api::Result res = d_solver.checkSat(); + CVC5::api::Result res = d_solver.checkSat(); ASSERT_TRUE(res.isSat()); ASSERT_FALSE(res.isSatUnknown()); } @@ -69,7 +69,7 @@ TEST_F(TestApiBlackResult, isUnsat) Sort u_sort = d_solver.mkUninterpretedSort("u"); Term x = d_solver.mkVar(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x).notTerm()); - CVC4::api::Result res = d_solver.checkSat(); + CVC5::api::Result res = d_solver.checkSat(); ASSERT_TRUE(res.isUnsat()); ASSERT_FALSE(res.isSatUnknown()); } @@ -82,7 +82,7 @@ TEST_F(TestApiBlackResult, isSatUnknown) Sort int_sort = d_solver.getIntegerSort(); Term x = d_solver.mkVar(int_sort, "x"); d_solver.assertFormula(x.eqTerm(x).notTerm()); - CVC4::api::Result res = d_solver.checkSat(); + CVC5::api::Result res = d_solver.checkSat(); ASSERT_FALSE(res.isSat()); ASSERT_TRUE(res.isSatUnknown()); } @@ -96,10 +96,10 @@ TEST_F(TestApiBlackResult, isEntailed) Term a = x.eqTerm(y).notTerm(); Term b = x.eqTerm(y); d_solver.assertFormula(a); - CVC4::api::Result entailed = d_solver.checkEntailed(a); + CVC5::api::Result entailed = d_solver.checkEntailed(a); ASSERT_TRUE(entailed.isEntailed()); ASSERT_FALSE(entailed.isEntailmentUnknown()); - CVC4::api::Result not_entailed = d_solver.checkEntailed(b); + CVC5::api::Result not_entailed = d_solver.checkEntailed(b); ASSERT_TRUE(not_entailed.isNotEntailed()); ASSERT_FALSE(not_entailed.isEntailmentUnknown()); } @@ -112,10 +112,10 @@ TEST_F(TestApiBlackResult, isEntailmentUnknown) Sort int_sort = d_solver.getIntegerSort(); Term x = d_solver.mkVar(int_sort, "x"); d_solver.assertFormula(x.eqTerm(x).notTerm()); - CVC4::api::Result res = d_solver.checkEntailed(x.eqTerm(x)); + CVC5::api::Result res = d_solver.checkEntailed(x.eqTerm(x)); ASSERT_FALSE(res.isEntailed()); ASSERT_TRUE(res.isEntailmentUnknown()); ASSERT_EQ(res.getUnknownExplanation(), api::Result::UNKNOWN_REASON); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index ed7edf633..8f15e9017 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -16,7 +16,7 @@ #include "test_api.h" -namespace CVC4 { +namespace CVC5 { using namespace api; @@ -1422,7 +1422,7 @@ TEST_F(TestApiBlackSolver, getUnsatCore3) { d_solver.assertFormula(t); } - CVC4::api::Result res = d_solver.checkSat(); + CVC5::api::Result res = d_solver.checkSat(); ASSERT_TRUE(res.isUnsat()); } @@ -1533,7 +1533,7 @@ void checkSimpleSeparationConstraints(Solver* solver) solver->declareSeparationHeap(integer, integer); Term x = solver->mkConst(integer, "x"); Term p = solver->mkConst(integer, "p"); - Term heap = solver->mkTerm(CVC4::api::Kind::SEP_PTO, p, x); + Term heap = solver->mkTerm(CVC5::api::Kind::SEP_PTO, p, x); solver->assertFormula(heap); Term nil = solver->mkSepNil(integer); solver->assertFormula(nil.eqTerm(solver->mkReal(5))); @@ -2343,4 +2343,4 @@ TEST_F(TestApiBlackSolver, tupleProject) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/api/solver_white.cpp b/test/unit/api/solver_white.cpp index 84d68dbc6..66a6c70f1 100644 --- a/test/unit/api/solver_white.cpp +++ b/test/unit/api/solver_white.cpp @@ -17,7 +17,7 @@ #include "base/configuration.h" #include "test_api.h" -namespace CVC4 { +namespace CVC5 { using namespace api; @@ -54,4 +54,4 @@ TEST_F(TestApiWhiteSolver, getOp) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index 8e7eb00ec..f1ec0985a 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -16,7 +16,7 @@ #include "test_api.h" -namespace CVC4 { +namespace CVC5 { using namespace api; @@ -603,4 +603,4 @@ TEST_F(TestApiBlackSort, sortScopedToString) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index c087e2175..7ac1a881e 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -14,7 +14,7 @@ #include "test_api.h" -namespace CVC4 { +namespace CVC5 { using namespace api; @@ -848,4 +848,4 @@ TEST_F(TestApiBlackTerm, termScopedToString) ASSERT_EQ(x.toString(), "x"); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/api/term_white.cpp b/test/unit/api/term_white.cpp index 9906fd731..de8e94227 100644 --- a/test/unit/api/term_white.cpp +++ b/test/unit/api/term_white.cpp @@ -14,7 +14,7 @@ #include "test_api.h" -namespace CVC4 { +namespace CVC5 { using namespace api; @@ -81,4 +81,4 @@ TEST_F(TestApiWhiteTerm, getOp) ASSERT_EQ(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR)); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/base/map_util_black.cpp b/test/unit/base/map_util_black.cpp index 13e842653..76238ad04 100644 --- a/test/unit/base/map_util_black.cpp +++ b/test/unit/base/map_util_black.cpp @@ -27,7 +27,7 @@ #include "context/context.h" #include "test.h" -namespace CVC4 { +namespace CVC5 { using context::CDHashMap; using context::CDInsertHashMap; @@ -63,8 +63,8 @@ class TestBaseBlackMap : public TestInternal TEST_F(TestBaseBlackMap, map) { std::map<std::string, std::string> map = default_map(); - ASSERT_TRUE(CVC4::ContainsKey(map, "key")); - ASSERT_FALSE(CVC4::ContainsKey(map, "non key")); + ASSERT_TRUE(CVC5::ContainsKey(map, "key")); + ASSERT_FALSE(CVC5::ContainsKey(map, "non key")); ASSERT_EQ(FindOrNull(map, "non key"), nullptr); if (std::string* found_value = FindOrNull(map, "other")) @@ -78,8 +78,8 @@ TEST_F(TestBaseBlackMap, map) TEST_F(TestBaseBlackMap, constant_map) { const std::map<std::string, std::string> map = default_map(); - ASSERT_TRUE(CVC4::ContainsKey(map, "key")); - ASSERT_FALSE(CVC4::ContainsKey(map, "non key")); + ASSERT_TRUE(CVC5::ContainsKey(map, "key")); + ASSERT_FALSE(CVC5::ContainsKey(map, "non key")); if (const std::string* found_value = FindOrNull(map, "other")) { @@ -94,8 +94,8 @@ TEST_F(TestBaseBlackMap, unordered_map) { std::unordered_map<std::string, std::string> map(default_map().begin(), default_map().end()); - ASSERT_TRUE(CVC4::ContainsKey(map, "key")); - ASSERT_FALSE(CVC4::ContainsKey(map, "non key")); + ASSERT_TRUE(CVC5::ContainsKey(map, "key")); + ASSERT_FALSE(CVC5::ContainsKey(map, "non key")); ASSERT_EQ(FindOrNull(map, "non key"), nullptr); if (std::string* found_value = FindOrNull(map, "other")) @@ -110,8 +110,8 @@ TEST_F(TestBaseBlackMap, const_unordered_map) { const std::unordered_map<std::string, std::string> map(default_map().begin(), default_map().end()); - ASSERT_TRUE(CVC4::ContainsKey(map, "key")); - ASSERT_FALSE(CVC4::ContainsKey(map, "non key")); + ASSERT_TRUE(CVC5::ContainsKey(map, "key")); + ASSERT_FALSE(CVC5::ContainsKey(map, "non key")); if (const std::string* found_value = FindOrNull(map, "other")) { @@ -125,23 +125,23 @@ TEST_F(TestBaseBlackMap, const_unordered_map) TEST_F(TestBaseBlackMap, set) { std::set<std::string> set{"entry", "other"}; - ASSERT_TRUE(CVC4::ContainsKey(set, "entry")); - ASSERT_FALSE(CVC4::ContainsKey(set, "non member")); + ASSERT_TRUE(CVC5::ContainsKey(set, "entry")); + ASSERT_FALSE(CVC5::ContainsKey(set, "non member")); const std::set<std::string> const_set{"entry", "other"}; - ASSERT_TRUE(CVC4::ContainsKey(const_set, "entry")); - ASSERT_FALSE(CVC4::ContainsKey(const_set, "non member")); + ASSERT_TRUE(CVC5::ContainsKey(const_set, "entry")); + ASSERT_FALSE(CVC5::ContainsKey(const_set, "non member")); } TEST_F(TestBaseBlackMap, unordered_set) { std::unordered_set<std::string> set{"entry", "other"}; - ASSERT_TRUE(CVC4::ContainsKey(set, "entry")); - ASSERT_FALSE(CVC4::ContainsKey(set, "non member")); + ASSERT_TRUE(CVC5::ContainsKey(set, "entry")); + ASSERT_FALSE(CVC5::ContainsKey(set, "non member")); const std::unordered_set<std::string> const_set{"entry", "other"}; - ASSERT_TRUE(CVC4::ContainsKey(const_set, "entry")); - ASSERT_FALSE(CVC4::ContainsKey(const_set, "non member")); + ASSERT_TRUE(CVC5::ContainsKey(const_set, "entry")); + ASSERT_FALSE(CVC5::ContainsKey(const_set, "non member")); } TEST_F(TestBaseBlackMap, CDHashMap) @@ -150,8 +150,8 @@ TEST_F(TestBaseBlackMap, CDHashMap) CDHashMap<std::string, std::string> map(&context); insert_all(default_map(), &map); - ASSERT_TRUE(CVC4::ContainsKey(map, "key")); - ASSERT_FALSE(CVC4::ContainsKey(map, "non key")); + ASSERT_TRUE(CVC5::ContainsKey(map, "key")); + ASSERT_FALSE(CVC5::ContainsKey(map, "non key")); if (const std::string* found_value = FindOrNull(map, "other")) { @@ -168,8 +168,8 @@ TEST_F(TestBaseBlackMap, const_CDHashMap) insert_all(default_map(), &store); const auto& map = store; - ASSERT_TRUE(CVC4::ContainsKey(map, "key")); - ASSERT_FALSE(CVC4::ContainsKey(map, "non key")); + ASSERT_TRUE(CVC5::ContainsKey(map, "key")); + ASSERT_FALSE(CVC5::ContainsKey(map, "non key")); if (const std::string* found_value = FindOrNull(map, "other")) { @@ -185,8 +185,8 @@ TEST_F(TestBaseBlackMap, CDInsertHashMap) CDInsertHashMap<std::string, std::string> map(&context); insert_all(default_map(), &map); - ASSERT_TRUE(CVC4::ContainsKey(map, "key")); - ASSERT_FALSE(CVC4::ContainsKey(map, "non key")); + ASSERT_TRUE(CVC5::ContainsKey(map, "key")); + ASSERT_FALSE(CVC5::ContainsKey(map, "non key")); if (const std::string* found_value = FindOrNull(map, "other")) { @@ -203,8 +203,8 @@ TEST_F(TestBaseBlackMap, const_CDInsertHashMap) insert_all(default_map(), &store); const auto& map = store; - ASSERT_TRUE(CVC4::ContainsKey(map, "key")); - ASSERT_FALSE(CVC4::ContainsKey(map, "non key")); + ASSERT_TRUE(CVC5::ContainsKey(map, "key")); + ASSERT_FALSE(CVC5::ContainsKey(map, "non key")); if (const std::string* found_value = FindOrNull(map, "other")) { ASSERT_EQ(*found_value, "entry"); @@ -213,4 +213,4 @@ TEST_F(TestBaseBlackMap, const_CDInsertHashMap) ASSERT_EQ(FindOrDie(map, "other"), "entry"); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/context/cdhashmap_black.cpp b/test/unit/context/cdhashmap_black.cpp index a5788a585..51d76070a 100644 --- a/test/unit/context/cdhashmap_black.cpp +++ b/test/unit/context/cdhashmap_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::context::CDMap<>. + ** \brief Black box testing of CVC5::context::CDMap<>. ** - ** Black box testing of CVC4::context::CDMap<>. + ** Black box testing of CVC5::context::CDMap<>. **/ #include <map> @@ -21,11 +21,11 @@ #include "context/cdlist.h" #include "test_context.h" -namespace CVC4 { +namespace CVC5 { namespace test { -using CVC4::context::CDHashMap; -using CVC4::context::Context; +using CVC5::context::CDHashMap; +using CVC5::context::Context; class TestContextBlackCDHashMap : public TestContext { @@ -203,4 +203,4 @@ TEST_F(TestContextBlackCDHashMap, insert_at_context_level_zero) ASSERT_TRUE(elements_are(map, {{3, 4}, {23, 317}})); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/context/cdhashmap_white.cpp b/test/unit/context/cdhashmap_white.cpp index 91ddc726d..06bcd8d46 100644 --- a/test/unit/context/cdhashmap_white.cpp +++ b/test/unit/context/cdhashmap_white.cpp @@ -9,16 +9,16 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::context::CDMap<>. + ** \brief White box testing of CVC5::context::CDMap<>. ** - ** White box testing of CVC4::context::CDMap<>. + ** White box testing of CVC5::context::CDMap<>. **/ #include "base/check.h" #include "context/cdhashmap.h" #include "test_context.h" -namespace CVC4 { +namespace CVC5 { using namespace context; @@ -44,4 +44,4 @@ TEST_F(TestContextWhiteCDHashMap, unreachable_save_and_restore) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/context/cdlist_black.cpp b/test/unit/context/cdlist_black.cpp index 2339962ac..e903492ee 100644 --- a/test/unit/context/cdlist_black.cpp +++ b/test/unit/context/cdlist_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::context::CDList<>. + ** \brief Black box testing of CVC5::context::CDList<>. ** - ** Black box testing of CVC4::context::CDList<>. + ** Black box testing of CVC5::context::CDList<>. **/ #include <limits.h> @@ -24,7 +24,7 @@ #include "memory.h" #include "test_context.h" -namespace CVC4 { +namespace CVC5 { using namespace context; @@ -163,4 +163,4 @@ TEST_F(TestContextBlackCDList, pop_below_level_created) list.push_back(42); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/context/cdo_black.cpp b/test/unit/context/cdo_black.cpp index 16d7949e0..033e60f57 100644 --- a/test/unit/context/cdo_black.cpp +++ b/test/unit/context/cdo_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::context::CDO<>. + ** \brief Black box testing of CVC5::context::CDO<>. ** - ** Black box testing of CVC4::context::CDO<>. + ** Black box testing of CVC5::context::CDO<>. **/ #include <iostream> @@ -22,7 +22,7 @@ #include "context/cdo.h" #include "test_context.h" -namespace CVC4 { +namespace CVC5 { using namespace context; @@ -48,4 +48,4 @@ TEST_F(TestContextBlackCDO, cdo) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/context/context_black.cpp b/test/unit/context/context_black.cpp index 59b723055..7ec7ef6c8 100644 --- a/test/unit/context/context_black.cpp +++ b/test/unit/context/context_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::context::Context. + ** \brief Black box testing of CVC5::context::Context. ** - ** Black box testing of CVC4::context::Context. + ** Black box testing of CVC5::context::Context. **/ #include <iostream> @@ -22,7 +22,7 @@ #include "context/cdo.h" #include "test_context.h" -namespace CVC4 { +namespace CVC5 { using namespace context; @@ -241,4 +241,4 @@ TEST_F(TestContextBlack, top_scope_context_obj) #endif } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/context/context_mm_black.cpp b/test/unit/context/context_mm_black.cpp index b0259e71e..2dbec57b6 100644 --- a/test/unit/context/context_mm_black.cpp +++ b/test/unit/context/context_mm_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::context::ContextMemoryManager. + ** \brief Black box testing of CVC5::context::ContextMemoryManager. ** - ** Black box testing of CVC4::context::ContextMemoryManager. + ** Black box testing of CVC5::context::ContextMemoryManager. **/ #include <cstring> @@ -21,7 +21,7 @@ #include "context/context_mm.h" #include "test.h" -namespace CVC4 { +namespace CVC5 { using namespace context; @@ -104,4 +104,4 @@ TEST_F(TestContextBlackMM, push_pop) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/context/context_white.cpp b/test/unit/context/context_white.cpp index 9d8ff84c7..6ec7ea3a1 100644 --- a/test/unit/context/context_white.cpp +++ b/test/unit/context/context_white.cpp @@ -9,16 +9,16 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::context::Context. + ** \brief White box testing of CVC5::context::Context. ** - ** White box testing of CVC4::context::Context. + ** White box testing of CVC5::context::Context. **/ #include "base/check.h" #include "context/cdo.h" #include "test_context.h" -namespace CVC4 { +namespace CVC5 { using namespace context; @@ -180,4 +180,4 @@ TEST_F(TestContextWhite, simple) ASSERT_EQ(c.d_ppContextObjPrev, &s->d_pContextObjList); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp index c600e3477..0ee485fc2 100644 --- a/test/unit/main/interactive_shell_black.cpp +++ b/test/unit/main/interactive_shell_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::InteractiveShell. + ** \brief Black box testing of CVC5::InteractiveShell. ** - ** Black box testing of CVC4::InteractiveShell. + ** Black box testing of CVC5::InteractiveShell. **/ #include <sstream> @@ -27,7 +27,7 @@ #include "smt/command.h" #include "test.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestMainBlackInteractiveShell : public TestInternal @@ -41,7 +41,7 @@ class TestMainBlackInteractiveShell : public TestInternal d_options.set(options::in, d_sin.get()); d_options.set(options::out, d_sout.get()); d_options.set(options::inputLanguage, language::input::LANG_CVC4); - d_solver.reset(new CVC4::api::Solver(&d_options)); + d_solver.reset(new CVC5::api::Solver(&d_options)); d_symman.reset(new SymbolManager(d_solver.get())); } @@ -80,7 +80,7 @@ class TestMainBlackInteractiveShell : public TestInternal std::unique_ptr<std::stringstream> d_sin; std::unique_ptr<std::stringstream> d_sout; std::unique_ptr<SymbolManager> d_symman; - std::unique_ptr<CVC4::api::Solver> d_solver; + std::unique_ptr<CVC5::api::Solver> d_solver; Options d_options; }; @@ -133,4 +133,4 @@ TEST_F(TestMainBlackInteractiveShell, repeated_empty_lines) countCommands(shell, 0, 3); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/memory.h b/test/unit/memory.h index b54bcd451..1341274dd 100644 --- a/test/unit/memory.h +++ b/test/unit/memory.h @@ -15,7 +15,7 @@ ** ** Use it like this (for example): ** - ** CVC4::test::WithLimitedMemory wlm(amount); + ** CVC5::test::WithLimitedMemory wlm(amount); ** TS_ASSERT_THROWS( foo(), bad_alloc ); ** ** The WithLimitedMemory destructor will re-establish the previous limit. @@ -53,7 +53,7 @@ # endif #endif -namespace CVC4 { +namespace CVC5 { namespace test { #ifndef CVC4_MEMORY_LIMITING_DISABLED @@ -86,9 +86,8 @@ class WithLimitedMemory { }; /* class WithLimitedMemory */ #endif -} /* CVC4::test namespace */ -} /* CVC4 namespace */ - +} // namespace test +} // namespace CVC5 // Remove CVC4_MEMORY_LIMITING_DISABLED_REASON if it is defined. #ifdef CVC4_MEMORY_LIMITING_DISABLED_REASON diff --git a/test/unit/node/attribute_black.cpp b/test/unit/node/attribute_black.cpp index 487798e49..48f68159f 100644 --- a/test/unit/node/attribute_black.cpp +++ b/test/unit/node/attribute_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::Attribute. + ** \brief Black box testing of CVC5::Attribute. ** - ** Black box testing of CVC4::Attribute. + ** Black box testing of CVC5::Attribute. **/ #include <sstream> @@ -23,7 +23,7 @@ #include "expr/node_value.h" #include "test_node.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace smt; @@ -125,4 +125,4 @@ TEST_F(TestNodeBlackAttribute, bools) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp index fccb587db..75bc87893 100644 --- a/test/unit/node/attribute_white.cpp +++ b/test/unit/node/attribute_white.cpp @@ -30,7 +30,7 @@ #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace smt; @@ -445,4 +445,4 @@ TEST_F(TestNodeWhiteAttribute, attributes) ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr())); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/kind_black.cpp b/test/unit/node/kind_black.cpp index a33955152..9c497f026 100644 --- a/test/unit/node/kind_black.cpp +++ b/test/unit/node/kind_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::Kind. + ** \brief Black box testing of CVC5::Kind. ** - ** Black box testing of CVC4::Kind. + ** Black box testing of CVC5::Kind. **/ #include <iostream> @@ -21,7 +21,7 @@ #include "expr/kind.h" #include "test.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; @@ -87,4 +87,4 @@ TEST_F(TestNodeBlackKind, output_concat) ASSERT_EQ(act.str(), exp.str()); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/kind_map_black.cpp b/test/unit/node/kind_map_black.cpp index 8e1c45d79..85c8fb2cd 100644 --- a/test/unit/node/kind_map_black.cpp +++ b/test/unit/node/kind_map_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::KindMap + ** \brief Black box testing of CVC5::KindMap ** - ** Black box testing of CVC4::KindMap. + ** Black box testing of CVC5::KindMap. **/ #include <iostream> @@ -21,7 +21,7 @@ #include "expr/kind_map.h" #include "test.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; @@ -45,4 +45,4 @@ TEST_F(TestNodeBlackKindMap, simple) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp index bd243e0fd..47f66f0c3 100644 --- a/test/unit/node/node_algorithm_black.cpp +++ b/test/unit/node/node_algorithm_black.cpp @@ -25,7 +25,7 @@ #include "util/integer.h" #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { using namespace expr; using namespace kind; @@ -199,4 +199,4 @@ TEST_F(TestNodeBlackNodeAlgorithm, match) ASSERT_EQ(subs[x], a); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 3c1651155..7ae8a9434 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::Node. + ** \brief Black box testing of CVC5::Node. ** - ** Black box testing of CVC4::Node. + ** Black box testing of CVC5::Node. **/ #include <algorithm> @@ -30,7 +30,7 @@ #include "test_node.h" #include "theory/rewriter.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; @@ -784,4 +784,4 @@ TEST_F(TestNodeBlackNode, node_tnode_usage) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp index 7e38dd899..62410bcb7 100644 --- a/test/unit/node/node_builder_black.cpp +++ b/test/unit/node/node_builder_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::NodeBuilder. + ** \brief Black box testing of CVC5::NodeBuilder. ** - ** Black box testing of CVC4::NodeBuilder. + ** Black box testing of CVC5::NodeBuilder. **/ #include <limits.h> @@ -30,7 +30,7 @@ #define K 30u #define LARGE_K UINT_MAX / 40 -namespace CVC4 { +namespace CVC5 { using namespace kind; @@ -587,4 +587,4 @@ TEST_F(TestNodeBlackNodeBuilder, leftist_building) ASSERT_EQ(nexpected, n); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp index a2ede3ed0..7866d87bd 100644 --- a/test/unit/node/node_manager_black.cpp +++ b/test/unit/node/node_manager_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::NodeManager. + ** \brief Black box testing of CVC5::NodeManager. ** - ** Black box testing of CVC4::NodeManager. + ** Black box testing of CVC5::NodeManager. **/ #include <string> @@ -24,7 +24,7 @@ #include "util/integer.h" #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace expr; @@ -330,4 +330,4 @@ TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children) #endif } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp index daf211b78..588c39181 100644 --- a/test/unit/node/node_manager_white.cpp +++ b/test/unit/node/node_manager_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::NodeManager. + ** \brief White box testing of CVC5::NodeManager. ** - ** White box testing of CVC4::NodeManager. + ** White box testing of CVC5::NodeManager. **/ #include <string> @@ -21,9 +21,9 @@ #include "util/integer.h" #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { -using namespace CVC4::expr; +using namespace CVC5::expr; namespace test { @@ -81,4 +81,4 @@ TEST_F(TestNodeWhiteNodeManager, topological_sort) } } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/node_self_iterator_black.cpp b/test/unit/node/node_self_iterator_black.cpp index 34ab5f09b..0a0a877c3 100644 --- a/test/unit/node/node_self_iterator_black.cpp +++ b/test/unit/node/node_self_iterator_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::expr::NodeSelfIterator + ** \brief Black box testing of CVC5::expr::NodeSelfIterator ** - ** Black box testing of CVC4::expr::NodeSelfIterator + ** Black box testing of CVC5::expr::NodeSelfIterator **/ #include "expr/node.h" @@ -19,7 +19,7 @@ #include "expr/node_self_iterator.h" #include "test_node.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace expr; @@ -54,4 +54,4 @@ TEST_F(TestNodeBlackNodeSelfIterator, iteration) ASSERT_EQ(++i, x_and_y.end()); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/node_traversal_black.cpp b/test/unit/node/node_traversal_black.cpp index e443ff685..c54be86ac 100644 --- a/test/unit/node/node_traversal_black.cpp +++ b/test/unit/node/node_traversal_black.cpp @@ -26,7 +26,7 @@ #include "expr/node_value.h" #include "test_node.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; @@ -293,4 +293,4 @@ TEST_F(TestNodeBlackNodeTraversalPreorder, skip_if) ASSERT_EQ(actual, expected); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp index 651dd1990..d914c5dc2 100644 --- a/test/unit/node/node_white.cpp +++ b/test/unit/node/node_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::Node. + ** \brief White box testing of CVC5::Node. ** - ** White box testing of CVC4::Node. + ** White box testing of CVC5::Node. **/ #include <string> @@ -19,7 +19,7 @@ #include "base/check.h" #include "test_node.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace expr; @@ -79,4 +79,4 @@ TEST_F(TestNodeWhiteNode, iterators) ASSERT_EQ(v[2], y); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/symbol_table_black.cpp b/test/unit/node/symbol_table_black.cpp index c1865eaa9..27911c34b 100644 --- a/test/unit/node/symbol_table_black.cpp +++ b/test/unit/node/symbol_table_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::SymbolTable + ** \brief Black box testing of CVC5::SymbolTable ** - ** Black box testing of CVC4::SymbolTable. + ** Black box testing of CVC5::SymbolTable. **/ #include <sstream> @@ -24,7 +24,7 @@ #include "expr/symbol_table.h" #include "test_api.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace context; @@ -146,4 +146,4 @@ TEST_F(TestNodeBlackSymbolTable, bad_pop) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/type_cardinality_black.cpp b/test/unit/node/type_cardinality_black.cpp index 55936df0d..e2aeced08 100644 --- a/test/unit/node/type_cardinality_black.cpp +++ b/test/unit/node/type_cardinality_black.cpp @@ -21,7 +21,7 @@ #include "test_node.h" #include "util/cardinality.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; @@ -332,4 +332,4 @@ TEST_F(TestNodeBlackTypeCardinality, bitvectors) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp index f364e40fc..37d80a9fa 100644 --- a/test/unit/node/type_node_white.cpp +++ b/test/unit/node/type_node_white.cpp @@ -23,7 +23,7 @@ #include "smt/smt_engine.h" #include "test_node.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace context; @@ -94,4 +94,4 @@ TEST_F(TestNodeWhiteTypeNode, sub_types) ASSERT_TRUE(bvType.getBaseType() == bvType); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp index 87556d53d..827d7dd84 100644 --- a/test/unit/parser/parser_black.cpp +++ b/test/unit/parser/parser_black.cpp @@ -9,10 +9,10 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::parser::Parser for CVC and SMT-LIBv2 + ** \brief Black box testing of CVC5::parser::Parser for CVC and SMT-LIBv2 ** inputs. ** - ** Black box testing of CVC4::parser::Parser for CVC and SMT-LIbv2 inputs. + ** Black box testing of CVC5::parser::Parser for CVC and SMT-LIbv2 inputs. **/ #include <sstream> @@ -29,7 +29,7 @@ #include "smt/command.h" #include "test.h" -namespace CVC4 { +namespace CVC5 { using namespace parser; using namespace language::input; @@ -48,7 +48,7 @@ class TestParserBlackParser : public TestInternal TestInternal::SetUp(); d_options.set(options::parseOnly, true); d_symman.reset(nullptr); - d_solver.reset(new CVC4::api::Solver(&d_options)); + d_solver.reset(new CVC5::api::Solver(&d_options)); } void TearDown() override @@ -186,7 +186,7 @@ class TestParserBlackParser : public TestInternal Options d_options; InputLanguage d_lang; - std::unique_ptr<CVC4::api::Solver> d_solver; + std::unique_ptr<CVC5::api::Solver> d_solver; std::unique_ptr<SymbolManager> d_symman; }; @@ -392,4 +392,4 @@ TEST_F(TestParserBlackSmt2Parser, bad_exprs) #endif } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp index 08b16dd07..3ebd11b83 100644 --- a/test/unit/parser/parser_builder_black.cpp +++ b/test/unit/parser/parser_builder_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::parser::ParserBuilder. + ** \brief Black box testing of CVC5::parser::ParserBuilder. ** - ** Black box testing of CVC4::parser::ParserBuilder. + ** Black box testing of CVC5::parser::ParserBuilder. **/ #include <stdio.h> @@ -29,7 +29,7 @@ #include "parser/parser_builder.h" #include "test_api.h" -namespace CVC4 { +namespace CVC5 { using namespace parser; using namespace language::input; @@ -134,4 +134,4 @@ TEST_F(TestParseBlackParserBuilder, true_stream_input) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index 2bafd7f30..130d6b1cf 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -29,7 +29,7 @@ #include "theory/rewriter.h" #include "util/bitvector.h" -namespace CVC4 { +namespace CVC5 { using namespace preprocessing; using namespace preprocessing::passes; @@ -3099,4 +3099,4 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5b) ASSERT_EQ(BVGauss::getMinBwExpr(Rewriter::rewrite(plus7)), 17); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp index 279cca59a..cbd178576 100644 --- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp +++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp @@ -18,7 +18,7 @@ #include "smt/smt_engine.h" #include "test_smt.h" -namespace CVC4 { +namespace CVC5 { using namespace preprocessing::passes; @@ -47,4 +47,4 @@ TEST_F(TestPPWhiteForeignTheoryRewrite, simplify) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp index a84105b20..2f4d6fb38 100644 --- a/test/unit/printer/smt2_printer_black.cpp +++ b/test/unit/printer/smt2_printer_black.cpp @@ -23,7 +23,7 @@ #include "smt/smt_engine.h" #include "test_smt.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; @@ -59,4 +59,4 @@ TEST_F(TestPrinterBlackSmt2, regexp_loop) checkToString(n, "((_ re.loop 1 3) (str.to_re \"x\"))"); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp index ae41fd041..40f986d33 100644 --- a/test/unit/prop/cnf_stream_white.cpp +++ b/test/unit/prop/cnf_stream_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::prop::CnfStream. + ** \brief White box testing of CVC5::prop::CnfStream. ** - ** White box testing of CVC4::prop::CnfStream. + ** White box testing of CVC5::prop::CnfStream. **/ #include "base/check.h" @@ -28,7 +28,7 @@ #include "theory/theory.h" #include "theory/theory_engine.h" -namespace CVC4 { +namespace CVC5 { using namespace context; using namespace prop; @@ -113,7 +113,7 @@ class TestPropWhiteCnfStream : public TestSmt d_cnfContext.reset(new context::Context()); d_cnfRegistrar.reset(new prop::NullRegistrar); d_cnfStream.reset( - new CVC4::prop::CnfStream(d_satSolver.get(), + new CVC5::prop::CnfStream(d_satSolver.get(), d_cnfRegistrar.get(), d_cnfContext.get(), &d_smtEngine->getOutputManager(), @@ -271,4 +271,4 @@ TEST_F(TestPropWhiteCnfStream, ensure_literal) ASSERT_TRUE(d_cnfStream->hasLiteral(a_and_b)); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/test.h b/test/unit/test.h index e42b5e8c8..1c5614488 100644 --- a/test/unit/test.h +++ b/test/unit/test.h @@ -17,7 +17,7 @@ #include "gtest/gtest.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestInternal : public ::testing::Test @@ -25,5 +25,5 @@ class TestInternal : public ::testing::Test }; } // namespace test -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/test/unit/test_api.h b/test/unit/test_api.h index 4722b63ea..033136524 100644 --- a/test/unit/test_api.h +++ b/test/unit/test_api.h @@ -18,15 +18,15 @@ #include "api/cvc4cpp.h" #include "gtest/gtest.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestApi : public ::testing::Test { protected: - CVC4::api::Solver d_solver; + CVC5::api::Solver d_solver; }; } // namespace test -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/test/unit/test_context.h b/test/unit/test_context.h index ffb6d89be..024488fc4 100644 --- a/test/unit/test_context.h +++ b/test/unit/test_context.h @@ -18,16 +18,16 @@ #include "context/context.h" #include "test.h" -namespace CVC4 { +namespace CVC5 { 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; + void SetUp() override { d_context.reset(new CVC5::context::Context()); } + std::unique_ptr<CVC5::context::Context> d_context; }; } // namespace test -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/test/unit/test_node.h b/test/unit/test_node.h index cf343f006..1aefbae45 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -20,7 +20,7 @@ #include "smt/smt_engine_scope.h" #include "test.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestNode : public TestInternal @@ -45,5 +45,5 @@ class TestNode : public TestInternal }; } // namespace test -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index e55c00e65..a6097b56c 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -29,7 +29,7 @@ #include "util/resource_manager.h" #include "util/unsafe_interrupt_exception.h" -namespace CVC4 { +namespace CVC5 { namespace test { /* -------------------------------------------------------------------------- */ @@ -99,7 +99,7 @@ inline std::ostream& operator<<(std::ostream& out, OutputChannelCallType type) } } -class DummyOutputChannel : public CVC4::theory::OutputChannel +class DummyOutputChannel : public CVC5::theory::OutputChannel { public: DummyOutputChannel() {} @@ -249,5 +249,5 @@ class DummyTheory : public theory::Theory /* -------------------------------------------------------------------------- */ } // namespace test -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp index ff04adef1..54976c7d7 100644 --- a/test/unit/theory/evaluator_white.cpp +++ b/test/unit/theory/evaluator_white.cpp @@ -24,7 +24,7 @@ #include "theory/rewriter.h" #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; @@ -156,4 +156,4 @@ TEST_F(TestTheoryWhiteEvaluator, code) } } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/logic_info_white.cpp b/test/unit/theory/logic_info_white.cpp index 56dd062df..0c45cc4ed 100644 --- a/test/unit/theory/logic_info_white.cpp +++ b/test/unit/theory/logic_info_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Unit testing for CVC4::LogicInfo class + ** \brief Unit testing for CVC5::LogicInfo class ** - ** Unit testing for CVC4::LogicInfo class. + ** Unit testing for CVC5::LogicInfo class. **/ #include "base/configuration.h" @@ -19,7 +19,7 @@ #include "test.h" #include "theory/logic_info.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; @@ -544,33 +544,33 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) LogicInfo info; ASSERT_FALSE(info.isLocked()); - ASSERT_THROW(info.getLogicString(), CVC4::IllegalArgumentException); + ASSERT_THROW(info.getLogicString(), CVC5::IllegalArgumentException); ASSERT_THROW(info.isTheoryEnabled(THEORY_BUILTIN), - CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); ASSERT_THROW(info.isTheoryEnabled(THEORY_BOOL), - CVC4::IllegalArgumentException); - ASSERT_THROW(info.isTheoryEnabled(THEORY_UF), CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); + ASSERT_THROW(info.isTheoryEnabled(THEORY_UF), CVC5::IllegalArgumentException); ASSERT_THROW(info.isTheoryEnabled(THEORY_ARITH), - CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); ASSERT_THROW(info.isTheoryEnabled(THEORY_ARRAYS), - CVC4::IllegalArgumentException); - ASSERT_THROW(info.isTheoryEnabled(THEORY_BV), CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); + ASSERT_THROW(info.isTheoryEnabled(THEORY_BV), CVC5::IllegalArgumentException); ASSERT_THROW(info.isTheoryEnabled(THEORY_DATATYPES), - CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); ASSERT_THROW(info.isTheoryEnabled(THEORY_QUANTIFIERS), - CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_BUILTIN), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_BOOL), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_UF), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_ARITH), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_ARRAYS), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_BV), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_DATATYPES), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_QUANTIFIERS), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isQuantified(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.areIntegersUsed(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.areRealsUsed(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isLinear(), CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_BUILTIN), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_BOOL), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_UF), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_ARITH), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_ARRAYS), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_BV), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_DATATYPES), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_QUANTIFIERS), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isQuantified(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.areIntegersUsed(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.areRealsUsed(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isLinear(), CVC5::IllegalArgumentException); info.lock(); ASSERT_TRUE(info.isLocked()); @@ -598,17 +598,17 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) ASSERT_TRUE(info.areTranscendentalsUsed()); ASSERT_FALSE(info.isLinear()); - ASSERT_THROW(info.arithOnlyLinear(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.disableIntegers(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.disableQuantifiers(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.disableTheory(THEORY_BV), CVC4::IllegalArgumentException); + ASSERT_THROW(info.arithOnlyLinear(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.disableIntegers(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.disableQuantifiers(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.disableTheory(THEORY_BV), CVC5::IllegalArgumentException); ASSERT_THROW(info.disableTheory(THEORY_DATATYPES), - CVC4::IllegalArgumentException); - ASSERT_THROW(info.enableIntegers(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.disableReals(), CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); + ASSERT_THROW(info.enableIntegers(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.disableReals(), CVC5::IllegalArgumentException); ASSERT_THROW(info.disableTheory(THEORY_ARITH), - CVC4::IllegalArgumentException); - ASSERT_THROW(info.disableTheory(THEORY_UF), CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); + ASSERT_THROW(info.disableTheory(THEORY_UF), CVC5::IllegalArgumentException); info = info.getUnlockedCopy(); ASSERT_FALSE(info.isLocked()); info.disableTheory(THEORY_STRINGS); @@ -617,7 +617,7 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) info.arithOnlyLinear(); info.disableIntegers(); info.lock(); - if (CVC4::Configuration::isBuiltWithSymFPU()) + if (CVC5::Configuration::isBuiltWithSymFPU()) { ASSERT_EQ(info.getLogicString(), "SEP_AUFBVFPDTLRA"); } @@ -631,7 +631,7 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) info.disableQuantifiers(); info.disableTheory(THEORY_BAGS); info.lock(); - if (CVC4::Configuration::isBuiltWithSymFPU()) + if (CVC5::Configuration::isBuiltWithSymFPU()) { ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA"); } @@ -648,7 +648,7 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) info.enableIntegers(); info.disableReals(); info.lock(); - if (CVC4::Configuration::isBuiltWithSymFPU()) + if (CVC5::Configuration::isBuiltWithSymFPU()) { ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFFPLIA"); } @@ -1371,4 +1371,4 @@ TEST_F(TestTheoryWhiteLogicInfo, comparison) gt(ufHo, "QF_UF"); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp index 0b6bf6500..b87701534 100644 --- a/test/unit/theory/regexp_operation_black.cpp +++ b/test/unit/theory/regexp_operation_black.cpp @@ -27,7 +27,7 @@ #include "theory/strings/regexp_operation.h" #include "theory/strings/skolem_cache.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace theory; @@ -144,4 +144,4 @@ TEST_F(TestTheoryBlackRegexpOperation, star_wildcards) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index fd6e3f3c0..7a85ad13d 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -28,7 +28,7 @@ #include "theory/strings/strings_entail.h" #include "theory/strings/strings_rewriter.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace theory::quantifiers; @@ -85,10 +85,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_length_one) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); - Node aaad = d_nodeManager->mkConst(::CVC4::String("AAAD")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD")); + Node aaad = d_nodeManager->mkConst(::CVC5::String("AAAD")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node negOne = d_nodeManager->mkConst(Rational(-1)); @@ -149,8 +149,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption) Node zero = d_nodeManager->mkConst(Rational(0)); Node one = d_nodeManager->mkConst(Rational(1)); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); Node slen_y = d_nodeManager->mkNode(kind::STRING_LENGTH, y); Node x_plus_slen_y = d_nodeManager->mkNode(kind::PLUS, x, slen_y); @@ -223,10 +223,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); - Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); + Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD")); Node negone = d_nodeManager->mkConst(Rational(-1)); Node zero = d_nodeManager->mkConst(Rational(0)); Node one = d_nodeManager->mkConst(Rational(1)); @@ -364,8 +364,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_concat) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); Node zero = d_nodeManager->mkConst(Rational(0)); Node three = d_nodeManager->mkConst(Rational(3)); @@ -431,11 +431,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, length_preserve_rewrite) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); - Node f = d_nodeManager->mkConst(::CVC4::String("F")); - Node gh = d_nodeManager->mkConst(::CVC4::String("GH")); - Node ij = d_nodeManager->mkConst(::CVC4::String("IJ")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD")); + Node f = d_nodeManager->mkConst(::CVC5::String("F")); + Node gh = d_nodeManager->mkConst(::CVC5::String("GH")); + Node ij = d_nodeManager->mkConst(::CVC5::String("IJ")); Node i = d_nodeManager->mkVar("i", intType); Node s = d_nodeManager->mkVar("s", strType); @@ -467,12 +467,12 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); - Node aaad = d_nodeManager->mkConst(::CVC4::String("AAAD")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); - Node c = d_nodeManager->mkConst(::CVC4::String("C")); - Node ccc = d_nodeManager->mkConst(::CVC4::String("CCC")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD")); + Node aaad = d_nodeManager->mkConst(::CVC5::String("AAAD")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); + Node c = d_nodeManager->mkConst(::CVC5::String("C")); + Node ccc = d_nodeManager->mkConst(::CVC5::String("CCC")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node negOne = d_nodeManager->mkConst(Rational(-1)); @@ -577,12 +577,12 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node ab = d_nodeManager->mkConst(::CVC4::String("AB")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); - Node c = d_nodeManager->mkConst(::CVC4::String("C")); - Node d = d_nodeManager->mkConst(::CVC4::String("D")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node ab = d_nodeManager->mkConst(::CVC5::String("AB")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); + Node c = d_nodeManager->mkConst(::CVC5::String("C")); + Node d = d_nodeManager->mkConst(::CVC5::String("D")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node z = d_nodeManager->mkVar("z", strType); @@ -773,7 +773,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) d_nodeManager->mkConst(String("AZZZB")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("FOO")); + Node res = d_nodeManager->mkConst(::CVC5::String("FOO")); sameNormalForm(t, res); } @@ -790,7 +790,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) d_nodeManager->mkConst(String("ZAZZZBZZB")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZZB")); + Node res = d_nodeManager->mkConst(::CVC5::String("ZFOOZZB")); sameNormalForm(t, res); } @@ -807,7 +807,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) d_nodeManager->mkConst(String("ZAZZZBZAZB")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZAZB")); + Node res = d_nodeManager->mkConst(::CVC5::String("ZFOOZAZB")); sameNormalForm(t, res); } @@ -824,7 +824,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) d_nodeManager->mkConst(String("ZZZ")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("ZZZ")); + Node res = d_nodeManager->mkConst(::CVC5::String("ZZZ")); sameNormalForm(t, res); } @@ -841,7 +841,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) d_nodeManager->mkConst(String("ZZZ")), sigStar, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("FOOZZZ")); + Node res = d_nodeManager->mkConst(::CVC5::String("FOOZZZ")); sameNormalForm(t, res); } @@ -858,7 +858,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) d_nodeManager->mkConst(String("")), sigStar, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("FOO")); + Node res = d_nodeManager->mkConst(::CVC5::String("FOO")); sameNormalForm(t, res); } } @@ -893,7 +893,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) d_nodeManager->mkConst(String("AZZZB")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("FOO")); + Node res = d_nodeManager->mkConst(::CVC5::String("FOO")); sameNormalForm(t, res); } @@ -910,7 +910,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) d_nodeManager->mkConst(String("ZAZZZBZZB")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZZB")); + Node res = d_nodeManager->mkConst(::CVC5::String("ZFOOZZB")); sameNormalForm(t, res); } @@ -927,7 +927,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) d_nodeManager->mkConst(String("ZAZZZBZAZB")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZFOO")); + Node res = d_nodeManager->mkConst(::CVC5::String("ZFOOZFOO")); sameNormalForm(t, res); } @@ -944,7 +944,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) d_nodeManager->mkConst(String("ZZZ")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("ZZZ")); + Node res = d_nodeManager->mkConst(::CVC5::String("ZZZ")); sameNormalForm(t, res); } @@ -961,7 +961,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) d_nodeManager->mkConst(String("ZZZ")), sigStar, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("FOOFOOFOO")); + Node res = d_nodeManager->mkConst(::CVC5::String("FOOFOOFOO")); sameNormalForm(t, res); } @@ -978,7 +978,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) d_nodeManager->mkConst(String("")), sigStar, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("")); + Node res = d_nodeManager->mkConst(::CVC5::String("")); sameNormalForm(t, res); } } @@ -988,18 +988,18 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node ab = d_nodeManager->mkConst(::CVC4::String("AB")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); - Node c = d_nodeManager->mkConst(::CVC4::String("C")); - Node e = d_nodeManager->mkConst(::CVC4::String("E")); - Node h = d_nodeManager->mkConst(::CVC4::String("H")); - Node j = d_nodeManager->mkConst(::CVC4::String("J")); - Node p = d_nodeManager->mkConst(::CVC4::String("P")); - Node abc = d_nodeManager->mkConst(::CVC4::String("ABC")); - Node def = d_nodeManager->mkConst(::CVC4::String("DEF")); - Node ghi = d_nodeManager->mkConst(::CVC4::String("GHI")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node ab = d_nodeManager->mkConst(::CVC5::String("AB")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); + Node c = d_nodeManager->mkConst(::CVC5::String("C")); + Node e = d_nodeManager->mkConst(::CVC5::String("E")); + Node h = d_nodeManager->mkConst(::CVC5::String("H")); + Node j = d_nodeManager->mkConst(::CVC5::String("J")); + Node p = d_nodeManager->mkConst(::CVC5::String("P")); + Node abc = d_nodeManager->mkConst(::CVC5::String("ABC")); + Node def = d_nodeManager->mkConst(::CVC5::String("DEF")); + Node ghi = d_nodeManager->mkConst(::CVC5::String("GHI")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y); @@ -1356,9 +1356,9 @@ TEST_F(TestTheoryWhiteSequencesRewriter, infer_eqs_from_contains) { TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y); @@ -1400,8 +1400,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_prefix_suffix) { TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node xx = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x); @@ -1437,11 +1437,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext) TypeNode strType = d_nodeManager->stringType(); TypeNode intType = d_nodeManager->integerType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node aaa = d_nodeManager->mkConst(::CVC4::String("AAA")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); - Node ba = d_nodeManager->mkConst(::CVC4::String("BA")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node aaa = d_nodeManager->mkConst(::CVC5::String("AAA")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); + Node ba = d_nodeManager->mkConst(::CVC5::String("BA")); Node w = d_nodeManager->mkVar("w", strType); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); @@ -1726,14 +1726,14 @@ TEST_F(TestTheoryWhiteSequencesRewriter, strip_constant_endpoints) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node ab = d_nodeManager->mkConst(::CVC4::String("AB")); - Node abc = d_nodeManager->mkConst(::CVC4::String("ABC")); - Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); - Node bc = d_nodeManager->mkConst(::CVC4::String("BC")); - Node c = d_nodeManager->mkConst(::CVC4::String("C")); - Node cd = d_nodeManager->mkConst(::CVC4::String("CD")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node ab = d_nodeManager->mkConst(::CVC5::String("AB")); + Node abc = d_nodeManager->mkConst(::CVC5::String("ABC")); + Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD")); + Node bc = d_nodeManager->mkConst(::CVC5::String("BC")); + Node c = d_nodeManager->mkConst(::CVC5::String("C")); + Node cd = d_nodeManager->mkConst(::CVC5::String("CD")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node n = d_nodeManager->mkVar("n", intType); @@ -1833,7 +1833,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_membership) TypeNode strType = d_nodeManager->stringType(); std::vector<Node> vec_empty; - Node abc = d_nodeManager->mkConst(::CVC4::String("ABC")); + Node abc = d_nodeManager->mkConst(::CVC5::String("ABC")); Node re_abc = d_nodeManager->mkNode(kind::STRING_TO_REGEXP, abc); Node x = d_nodeManager->mkVar("x", strType); @@ -1908,4 +1908,4 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_regexp_concat) } } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/strings_rewriter_white.cpp b/test/unit/theory/strings_rewriter_white.cpp index 93aa1667a..94bf8b581 100644 --- a/test/unit/theory/strings_rewriter_white.cpp +++ b/test/unit/theory/strings_rewriter_white.cpp @@ -24,7 +24,7 @@ #include "theory/rewriter.h" #include "theory/strings/strings_rewriter.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace theory; @@ -41,8 +41,8 @@ TEST_F(TestTheoryWhiteStringsRewriter, rewrite_leq) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node bc = d_nodeManager->mkConst(::CVC4::String("BC")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node bc = d_nodeManager->mkConst(::CVC5::String("BC")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); @@ -61,4 +61,4 @@ TEST_F(TestTheoryWhiteStringsRewriter, rewrite_leq) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index d0ed5718e..ac992f5c9 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -24,7 +24,7 @@ #include "theory/theory_engine.h" #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace theory::arith; @@ -122,4 +122,4 @@ TEST_F(TestTheoryWhiteArith, int_normal_form) ASSERT_EQ(Rewriter::rewrite(Rewriter::rewrite(t)), Rewriter::rewrite(t)); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index ce6dbc79a..09f5c2ae9 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -18,7 +18,7 @@ #include "theory/bags/normal_form.h" #include "theory/strings/type_enumerator.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace kind; @@ -40,7 +40,7 @@ class TestTheoryWhiteBagsNormalForm : public TestSmt std::vector<Node> getNStrings(size_t n) { std::vector<Node> elements(n); - CVC4::theory::strings::StringEnumerator enumerator( + CVC5::theory::strings::StringEnumerator enumerator( d_nodeManager->stringType()); for (size_t i = 0; i < n; i++) @@ -586,4 +586,4 @@ TEST_F(TestTheoryWhiteBagsNormalForm, to_set) ASSERT_EQ(output3, NormalForm::evaluate(input3)); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 987f21fb5..a1cc2761a 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -17,7 +17,7 @@ #include "theory/bags/bags_rewriter.h" #include "theory/strings/type_enumerator.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace kind; @@ -688,4 +688,4 @@ TEST_F(TestTheoryWhiteBagsRewriter, to_set) && response.d_status == REWRITE_AGAIN_FULL); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index 0922a22a4..830169c8b 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -17,7 +17,7 @@ #include "theory/bags/theory_bags_type_rules.h" #include "theory/strings/type_enumerator.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace kind; @@ -33,7 +33,7 @@ class TestTheoryWhiteBagsTypeRule : public TestSmt std::vector<Node> getNStrings(size_t n) { std::vector<Node> elements(n); - CVC4::theory::strings::StringEnumerator enumerator( + CVC5::theory::strings::StringEnumerator enumerator( d_nodeManager->stringType()); for (size_t i = 0; i < n; i++) @@ -110,4 +110,4 @@ TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator) ASSERT_TRUE(d_nodeManager->mkNode(BAG_TO_SET, bag).getType().isSet()); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp index 096013110..ddd43a063 100644 --- a/test/unit/theory/theory_black.cpp +++ b/test/unit/theory/theory_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::theory + ** \brief Black box testing of CVC5::theory ** - ** Black box testing of CVC4::theory + ** Black box testing of CVC5::theory **/ #include <sstream> @@ -23,7 +23,7 @@ #include "test_smt.h" #include "theory/rewriter.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace context; @@ -129,4 +129,4 @@ TEST_F(TestTheoryBlack, array_const) ASSERT_TRUE(arr2.isConst()); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index 7888ba52b..247f5428f 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -22,7 +22,7 @@ #include "theory/bv/int_blaster.h" #include "util/bitvector.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace theory; @@ -44,4 +44,4 @@ class TestTheoryWhiteBvIntblaster : public TestSmtNoFinishInit Node d_one; }; } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_bv_rewriter_white.cpp b/test/unit/theory/theory_bv_rewriter_white.cpp index 556785680..c7262117c 100644 --- a/test/unit/theory/theory_bv_rewriter_white.cpp +++ b/test/unit/theory/theory_bv_rewriter_white.cpp @@ -23,7 +23,7 @@ #include "theory/rewriter.h" #include "util/bitvector.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace theory; @@ -81,4 +81,4 @@ TEST_F(TestTheoryWhiteBvRewriter, rewrite_bv_ite) ASSERT_EQ(nr, Rewriter::rewrite(nr)); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index 1447670f3..020c7d0a5 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -25,7 +25,7 @@ #include "theory/theory.h" #include "theory/theory_engine.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace theory::bv; @@ -93,4 +93,4 @@ TEST_F(TestTheoryWhiteBv, mkUmulo) } } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp index e0040e3d3..ff2f3a836 100644 --- a/test/unit/theory/theory_engine_white.cpp +++ b/test/unit/theory/theory_engine_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::theory::Theory. + ** \brief White box testing of CVC5::theory::Theory. ** - ** White box testing of CVC4::theory::Theory. This test creates + ** White box testing of CVC5::theory::Theory. This test creates ** "fake" theory interfaces and injects them into TheoryEngine, so we ** can test TheoryEngine's behavior without relying on independent ** theory behavior. This is done in TheoryEngineWhite::setUp() by @@ -33,7 +33,7 @@ #include "util/integer.h" #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace expr; @@ -183,4 +183,4 @@ TEST_F(TestTheoryWhiteEngine, rewrite_rules) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index 81556d33a..fc20d6d73 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -15,7 +15,7 @@ #include "smt/optimization_solver.h" #include "test_smt.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace smt; @@ -136,4 +136,4 @@ TEST_F(TestTheoryWhiteIntOpt, result) std::cout << "Result is :" << r << std::endl; } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp index 942986a7e..715eea5f9 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp @@ -24,7 +24,7 @@ #include "theory/rewriter.h" #include "util/bitvector.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace theory::bv; @@ -452,4 +452,4 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvEqual) ASSERT_EQ(norm_axax[1], a); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index 7b6a73d2c..4ad3f04ef 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -20,7 +20,7 @@ #include "theory/quantifiers/bv_inverter_utils.h" #include "util/result.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace theory; @@ -1611,4 +1611,4 @@ TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sext_sgt_false) runTestSext(false, BITVECTOR_SGT); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_sets_type_enumerator_white.cpp b/test/unit/theory/theory_sets_type_enumerator_white.cpp index fdf8e3a5e..adee0c266 100644 --- a/test/unit/theory/theory_sets_type_enumerator_white.cpp +++ b/test/unit/theory/theory_sets_type_enumerator_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::theory::sets::SetsTypeEnumerator + ** \brief White box testing of CVC5::theory::sets::SetsTypeEnumerator ** - ** White box testing of CVC4::theory::sets::SetsTypeEnumerator. (These tests + ** White box testing of CVC5::theory::sets::SetsTypeEnumerator. (These tests ** depends on the ordering that the SetsTypeEnumerator use, so it's a *white-box ** test.) @@ -21,7 +21,7 @@ #include "test_smt.h" #include "theory/sets/theory_sets_type_enumerator.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace kind; @@ -152,4 +152,4 @@ TEST_F(TestTheoryWhiteSetsTypeEnumerator, bv) ASSERT_TRUE(setEnumerator.isFinished()); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp index b6bda5564..22b0a09d6 100644 --- a/test/unit/theory/theory_sets_type_rules_white.cpp +++ b/test/unit/theory/theory_sets_type_rules_white.cpp @@ -16,9 +16,9 @@ #include "test_api.h" #include "test_node.h" -namespace CVC4 { +namespace CVC5 { -using namespace CVC4::api; +using namespace CVC5::api; namespace test { @@ -83,4 +83,4 @@ TEST_F(TestTheoryWhiteSetsTypeRuleInternal, singleton_node) ASSERT_TRUE(n.isConst()); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp index 64ebe2b97..06a86b844 100644 --- a/test/unit/theory/theory_strings_skolem_cache_black.cpp +++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp @@ -20,7 +20,7 @@ #include "util/rational.h" #include "util/string.h" -namespace CVC4 { +namespace CVC5 { using namespace theory::strings; @@ -59,4 +59,4 @@ TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached) } } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_strings_word_white.cpp b/test/unit/theory/theory_strings_word_white.cpp index 5e5c57053..03b9ed4c2 100644 --- a/test/unit/theory/theory_strings_word_white.cpp +++ b/test/unit/theory/theory_strings_word_white.cpp @@ -20,7 +20,7 @@ #include "test_node.h" #include "theory/strings/word.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace theory::strings; @@ -121,4 +121,4 @@ TEST_F(TestTheoryWhiteStringsWord, strings) ASSERT_TRUE(Word::roverlap(aaaaa, aa) == 2); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp index 048fac5ac..41abdd6d1 100644 --- a/test/unit/theory/theory_white.cpp +++ b/test/unit/theory/theory_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::theory::Theory. + ** \brief Black box testing of CVC5::theory::Theory. ** - ** Black box testing of CVC4::theory::Theory. + ** Black box testing of CVC5::theory::Theory. **/ #include <memory> @@ -24,7 +24,7 @@ #include "theory/theory_engine.h" #include "util/resource_manager.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace expr; @@ -109,4 +109,4 @@ TEST_F(TestTheoryWhite, outputChannel) d_outputChannel.d_callHistory.clear(); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp index 538a608e8..2e018f9cf 100644 --- a/test/unit/theory/type_enumerator_white.cpp +++ b/test/unit/theory/type_enumerator_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::theory::TypeEnumerator + ** \brief White box testing of CVC5::theory::TypeEnumerator ** - ** White box testing of CVC4::theory::TypeEnumerator. (These tests depends + ** White box testing of CVC5::theory::TypeEnumerator. (These tests depends ** on the ordering that the TypeEnumerators use, so it's a white-box test.) **/ @@ -25,7 +25,7 @@ #include "test_smt.h" #include "theory/type_enumerator.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace kind; @@ -332,4 +332,4 @@ TEST_F(TestTheoryWhiteTypeEnumerator, bv) ASSERT_THROW(*++te, NoMoreValuesException); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index 540fca6f2..5be00263d 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -9,15 +9,15 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::ArrayStoreAll + ** \brief Black box testing of CVC5::ArrayStoreAll ** - ** Black box testing of CVC4::ArrayStoreAll. + ** Black box testing of CVC5::ArrayStoreAll. **/ #include "expr/array_store_all.h" #include "test_smt.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilWhiteArrayStoreAll : public TestSmt @@ -75,4 +75,4 @@ TEST_F(TestUtilWhiteArrayStoreAll, const_error) IllegalArgumentException); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/assert_white.cpp b/test/unit/util/assert_white.cpp index 0f1d5786e..a64bf275d 100644 --- a/test/unit/util/assert_white.cpp +++ b/test/unit/util/assert_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::Configuration. + ** \brief White box testing of CVC5::Configuration. ** - ** White box testing of CVC4::Configuration. + ** White box testing of CVC5::Configuration. **/ #include <cstring> @@ -20,7 +20,7 @@ #include "base/check.h" #include "test.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilWhite : public TestInternal @@ -86,4 +86,4 @@ TEST_F(TestUtilWhite, CheckArgument) ASSERT_THROW(CheckArgument(false, "x"), IllegalArgumentException); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/binary_heap_black.cpp b/test/unit/util/binary_heap_black.cpp index b35b8fa21..0b52b6d14 100644 --- a/test/unit/util/binary_heap_black.cpp +++ b/test/unit/util/binary_heap_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::BinaryHeap + ** \brief Black box testing of CVC5::BinaryHeap ** - ** Black box testing of CVC4::BinaryHeap. + ** Black box testing of CVC5::BinaryHeap. **/ #include <iostream> @@ -20,7 +20,7 @@ #include "test.h" #include "util/bin_heap.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilBlackBinaryHeap : public TestInternal @@ -230,4 +230,4 @@ TEST_F(TestUtilBlackBinaryHeap, large_heap) ASSERT_TRUE(heap.empty()); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/bitvector_black.cpp b/test/unit/util/bitvector_black.cpp index 3de70cfec..b26d8a1c6 100644 --- a/test/unit/util/bitvector_black.cpp +++ b/test/unit/util/bitvector_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::BitVector + ** \brief Black box testing of CVC5::BitVector ** - ** Black box testing of CVC4::BitVector. + ** Black box testing of CVC5::BitVector. **/ #include <sstream> @@ -19,7 +19,7 @@ #include "test.h" #include "util/bitvector.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilBlackBitVector : public TestInternal @@ -203,4 +203,4 @@ TEST_F(TestUtilBlackBitVector, static_helpers) ASSERT_EQ(BitVector::mkMaxSigned(4).toSignedInteger(), Integer(7)); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp index ef5ddadd6..cce2518c4 100644 --- a/test/unit/util/boolean_simplification_black.cpp +++ b/test/unit/util/boolean_simplification_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::BooleanSimplification + ** \brief Black box testing of CVC5::BooleanSimplification ** - ** Black box testing of CVC4::BooleanSimplification. + ** Black box testing of CVC5::BooleanSimplification. **/ #include <algorithm> @@ -26,7 +26,7 @@ #include "smt_util/boolean_simplification.h" #include "test_node.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilBlackBooleanSimplification : public TestNode @@ -248,4 +248,4 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyConflict) #endif } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/cardinality_black.cpp b/test/unit/util/cardinality_black.cpp index 9f5552037..b4b6ab6a5 100644 --- a/test/unit/util/cardinality_black.cpp +++ b/test/unit/util/cardinality_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Public-box testing of CVC4::Cardinality + ** \brief Public-box testing of CVC5::Cardinality ** - ** Public-box testing of CVC4::Cardinality. + ** Public-box testing of CVC5::Cardinality. **/ #include <sstream> @@ -22,7 +22,7 @@ #include "util/cardinality.h" #include "util/integer.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilBlackCardinality : public TestInternal @@ -270,4 +270,4 @@ TEST_F(TestUtilBlackCardinality, cardinalities) ASSERT_EQ((z ^ z).getBethNumber(), 3); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/check_white.cpp b/test/unit/util/check_white.cpp index 5ee0f42c4..4985bced3 100644 --- a/test/unit/util/check_white.cpp +++ b/test/unit/util/check_white.cpp @@ -20,7 +20,7 @@ #include "base/check.h" #include "test.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilWhiteCheck : public TestInternal @@ -63,4 +63,4 @@ TEST_F(TestUtilWhiteCheck, expect_abort) ASSERT_DEATH(AlwaysAssert(false), "false"); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/configuration_black.cpp b/test/unit/util/configuration_black.cpp index 44ae8c04b..a7c5c2703 100644 --- a/test/unit/util/configuration_black.cpp +++ b/test/unit/util/configuration_black.cpp @@ -9,15 +9,15 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::Configuration. + ** \brief Black box testing of CVC5::Configuration. ** - ** Black box testing of CVC4::Configuration. + ** Black box testing of CVC5::Configuration. **/ #include "base/configuration.h" #include "test.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilBlackConfiguration : public TestInternal @@ -96,4 +96,4 @@ TEST_F(TestUtilBlackConfiguration, about) Configuration::about(); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index ef24d870d..b486d91e9 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::DType + ** \brief Black box testing of CVC5::DType ** - ** Black box testing of CVC4::DType. + ** Black box testing of CVC5::DType. **/ #include <sstream> @@ -21,7 +21,7 @@ #include "expr/type_node.h" #include "test_smt.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilBlackDatatype : public TestSmt @@ -495,4 +495,4 @@ TEST_F(TestUtilBlackDatatype, parametric_DType) ASSERT_EQ(TypeNode::leastCommonTypeNode(pairIntInt, pairIntInt), pairIntInt); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/exception_black.cpp b/test/unit/util/exception_black.cpp index d6ac7af67..7216c0b8c 100644 --- a/test/unit/util/exception_black.cpp +++ b/test/unit/util/exception_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::Exception. + ** \brief Black box testing of CVC5::Exception. ** - ** Black box testing of CVC4::Exception. + ** Black box testing of CVC5::Exception. **/ #include <iostream> @@ -20,14 +20,14 @@ #include "base/exception.h" #include "test.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilBlackException : public TestInternal { }; -// CVC4::Exception is a simple class, just test it all at once. +// CVC5::Exception is a simple class, just test it all at once. TEST_F(TestUtilBlackException, exceptions) { Exception e1; @@ -52,4 +52,4 @@ TEST_F(TestUtilBlackException, exceptions) ASSERT_EQ(s3.str(), std::string("three of 'em!")); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/floatingpoint_black.cpp b/test/unit/util/floatingpoint_black.cpp index fd27268d1..391c656f3 100644 --- a/test/unit/util/floatingpoint_black.cpp +++ b/test/unit/util/floatingpoint_black.cpp @@ -9,15 +9,15 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::FloatingPoint. + ** \brief Black box testing of CVC5::FloatingPoint. ** - ** Black box testing of CVC4::FloatingPoint. + ** Black box testing of CVC5::FloatingPoint. **/ #include "test.h" #include "util/floatingpoint.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilBlackFloatingPoint : public TestInternal @@ -136,4 +136,4 @@ TEST_F(TestUtilBlackFloatingPoint, makeMaxNormal) ASSERT_TRUE(mfp128.isNormal()); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/integer_black.cpp b/test/unit/util/integer_black.cpp index 29b971160..fc92fa0d2 100644 --- a/test/unit/util/integer_black.cpp +++ b/test/unit/util/integer_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::Integer. + ** \brief Black box testing of CVC5::Integer. ** - ** Black box testing of CVC4::Integer. + ** Black box testing of CVC5::Integer. **/ #include <limits> @@ -21,7 +21,7 @@ #include "test.h" #include "util/integer.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilBlackInteger : public TestInternal @@ -564,4 +564,4 @@ TEST_F(TestUtilBlackInteger, modInverse) } } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/integer_white.cpp b/test/unit/util/integer_white.cpp index 16e606d87..3b5363dda 100644 --- a/test/unit/util/integer_white.cpp +++ b/test/unit/util/integer_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::Integer. + ** \brief White box testing of CVC5::Integer. ** - ** White box testing of CVC4::Integer. + ** White box testing of CVC5::Integer. **/ #include <sstream> @@ -19,7 +19,7 @@ #include "test.h" #include "util/integer.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilWhiteInteger : public TestInternal @@ -53,4 +53,4 @@ TEST_F(TestUtilWhiteInteger, construction) ASSERT_EQ(Integer(u), Integer(u)); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp index 48b1d4087..f5c973849 100644 --- a/test/unit/util/output_black.cpp +++ b/test/unit/util/output_black.cpp @@ -20,7 +20,7 @@ #include "base/output.h" #include "test.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilBlackOutput : public TestInternal @@ -241,4 +241,4 @@ TEST_F(TestUtilBlackOutput, simple_print) #endif /* CVC4_MUZZLE */ } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/rational_black.cpp b/test/unit/util/rational_black.cpp index d3eaaf61e..e6dee5d55 100644 --- a/test/unit/util/rational_black.cpp +++ b/test/unit/util/rational_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::Rational. + ** \brief Black box testing of CVC5::Rational. ** - ** Black box testing of CVC4::Rational. + ** Black box testing of CVC5::Rational. **/ #include <sstream> @@ -19,7 +19,7 @@ #include "test.h" #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilBlackRational : public TestInternal @@ -44,4 +44,4 @@ TEST_F(TestUtilBlackRational, fromDecimal) ASSERT_THROW(Rational::fromDecimal("Hello, world!");, std::invalid_argument); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/rational_white.cpp b/test/unit/util/rational_white.cpp index df2dd1b17..542a43990 100644 --- a/test/unit/util/rational_white.cpp +++ b/test/unit/util/rational_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::Rational. + ** \brief White box testing of CVC5::Rational. ** - ** White box testing of CVC4::Rational. + ** White box testing of CVC5::Rational. **/ #include <sstream> @@ -19,7 +19,7 @@ #include "test.h" #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilWhiteRational : public TestInternal @@ -416,4 +416,4 @@ TEST_F(TestUtilWhiteRational, constructrion) ASSERT_EQ(Rational(u), Rational(u)); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/real_algebraic_number_black.cpp b/test/unit/util/real_algebraic_number_black.cpp index 97bbb438c..4300b709c 100644 --- a/test/unit/util/real_algebraic_number_black.cpp +++ b/test/unit/util/real_algebraic_number_black.cpp @@ -9,15 +9,15 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::RealAlgebraicNumber. + ** \brief Black box testing of CVC5::RealAlgebraicNumber. ** - ** Black box testing of CVC4::RealAlgebraicNumber. + ** Black box testing of CVC5::RealAlgebraicNumber. **/ #include "test.h" #include "util/real_algebraic_number.h" -namespace CVC4 { +namespace CVC5 { namespace test { #ifndef CVC4_POLY_IMP @@ -81,4 +81,4 @@ TEST_F(TestUtilBlackRealAlgebraicNumber, arithmetic) ASSERT_EQ(msqrt2 * sqrt2, RealAlgebraicNumber(Integer(-2))); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp index 71cde7e5a..f8a14d9b2 100644 --- a/test/unit/util/stats_black.cpp +++ b/test/unit/util/stats_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::Stat and associated classes + ** \brief Black box testing of CVC5::Stat and associated classes ** - ** Black box testing of CVC4::Stat and associated classes. + ** Black box testing of CVC5::Stat and associated classes. **/ #include <fcntl.h> @@ -27,7 +27,7 @@ #include "util/stats_histogram.h" #include "util/stats_timer.h" -namespace CVC4 { +namespace CVC5 { namespace test { class TestUtilBlackStats : public TestInternal @@ -49,7 +49,7 @@ TEST_F(TestUtilBlackStats, stats) BackedStat<void*> backedAddr("backedDouble", (void*)0xDEADBEEF); IntegralHistogramStat<std::int64_t> histIntStat("hist-int"); histIntStat << 15 << 16 << 15 << 14 << 16; - IntegralHistogramStat<CVC4::PfRule> histPfRuleStat("hist-pfrule"); + IntegralHistogramStat<CVC5::PfRule> histPfRuleStat("hist-pfrule"); histPfRuleStat << PfRule::ASSUME << PfRule::SCOPE << PfRule::ASSUME; // A statistic with no safe_print support @@ -161,4 +161,4 @@ TEST_F(TestUtilBlackStats, stats) #endif } } // namespace test -} // namespace CVC4 +} // namespace CVC5 |