diff options
Diffstat (limited to 'test/unit/api')
-rw-r--r-- | test/unit/api/datatype_api_black.cpp | 4 | ||||
-rw-r--r-- | test/unit/api/grammar_black.cpp | 4 | ||||
-rw-r--r-- | test/unit/api/op_black.cpp | 4 | ||||
-rw-r--r-- | test/unit/api/op_white.cpp | 4 | ||||
-rw-r--r-- | test/unit/api/result_black.cpp | 26 | ||||
-rw-r--r-- | test/unit/api/solver_black.cpp | 8 | ||||
-rw-r--r-- | test/unit/api/solver_white.cpp | 4 | ||||
-rw-r--r-- | test/unit/api/sort_black.cpp | 4 | ||||
-rw-r--r-- | test/unit/api/term_black.cpp | 4 | ||||
-rw-r--r-- | test/unit/api/term_white.cpp | 4 |
10 files changed, 33 insertions, 33 deletions
diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp index 97db622c6..190816921 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 CVC5 { +namespace cvc5 { using namespace api; @@ -547,4 +547,4 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons) ASSERT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException); } } // namespace test -} // namespace CVC5 +} // namespace cvc5 diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp index 96ad29503..9c1f750b8 100644 --- a/test/unit/api/grammar_black.cpp +++ b/test/unit/api/grammar_black.cpp @@ -16,7 +16,7 @@ #include "test_api.h" -namespace CVC5 { +namespace cvc5 { using namespace api; @@ -122,4 +122,4 @@ TEST_F(TestApiBlackGrammar, addAnyVariable) ASSERT_THROW(g1.addAnyVariable(start), CVC4ApiException); } } // namespace test -} // namespace CVC5 +} // namespace cvc5 diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp index 2333e5719..0e6626ec5 100644 --- a/test/unit/api/op_black.cpp +++ b/test/unit/api/op_black.cpp @@ -14,7 +14,7 @@ #include "test_api.h" -namespace CVC5 { +namespace cvc5 { using namespace api; @@ -178,4 +178,4 @@ TEST_F(TestApiBlackOp, opScopingToString) ASSERT_EQ(bitvector_repeat_ot.toString(), op_repr); } } // namespace test -} // namespace CVC5 +} // namespace cvc5 diff --git a/test/unit/api/op_white.cpp b/test/unit/api/op_white.cpp index 49a964e9e..909aafcbb 100644 --- a/test/unit/api/op_white.cpp +++ b/test/unit/api/op_white.cpp @@ -14,7 +14,7 @@ #include "test_api.h" -namespace CVC5 { +namespace cvc5 { using namespace api; @@ -32,4 +32,4 @@ TEST_F(TestApiWhiteOp, opFromKind) ASSERT_EQ(plus, d_solver.mkOp(PLUS)); } } // namespace test -} // namespace CVC5 +} // namespace cvc5 diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp index f27b30431..ac4542c59 100644 --- a/test/unit/api/result_black.cpp +++ b/test/unit/api/result_black.cpp @@ -14,7 +14,7 @@ #include "test_api.h" -namespace CVC5 { +namespace cvc5 { using namespace api; @@ -26,7 +26,7 @@ class TestApiBlackResult : public TestApi TEST_F(TestApiBlackResult, isNull) { - CVC5::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)); - CVC5::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)); - CVC5::api::Result res; - CVC5::api::Result res2 = d_solver.checkSat(); - CVC5::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)); - CVC5::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()); - CVC5::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()); - CVC5::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); - CVC5::api::Result entailed = d_solver.checkEntailed(a); + cvc5::api::Result entailed = d_solver.checkEntailed(a); ASSERT_TRUE(entailed.isEntailed()); ASSERT_FALSE(entailed.isEntailmentUnknown()); - CVC5::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()); - CVC5::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 CVC5 +} // namespace cvc5 diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 8f15e9017..fef06fa88 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -16,7 +16,7 @@ #include "test_api.h" -namespace CVC5 { +namespace cvc5 { using namespace api; @@ -1422,7 +1422,7 @@ TEST_F(TestApiBlackSolver, getUnsatCore3) { d_solver.assertFormula(t); } - CVC5::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(CVC5::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 CVC5 +} // namespace cvc5 diff --git a/test/unit/api/solver_white.cpp b/test/unit/api/solver_white.cpp index 66a6c70f1..25878f22d 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 CVC5 { +namespace cvc5 { using namespace api; @@ -54,4 +54,4 @@ TEST_F(TestApiWhiteSolver, getOp) } } // namespace test -} // namespace CVC5 +} // namespace cvc5 diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index f1ec0985a..e0507e749 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -16,7 +16,7 @@ #include "test_api.h" -namespace CVC5 { +namespace cvc5 { using namespace api; @@ -603,4 +603,4 @@ TEST_F(TestApiBlackSort, sortScopedToString) } } // namespace test -} // namespace CVC5 +} // namespace cvc5 diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index 7ac1a881e..117b15394 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -14,7 +14,7 @@ #include "test_api.h" -namespace CVC5 { +namespace cvc5 { using namespace api; @@ -848,4 +848,4 @@ TEST_F(TestApiBlackTerm, termScopedToString) ASSERT_EQ(x.toString(), "x"); } } // namespace test -} // namespace CVC5 +} // namespace cvc5 diff --git a/test/unit/api/term_white.cpp b/test/unit/api/term_white.cpp index de8e94227..e7b7a9cd6 100644 --- a/test/unit/api/term_white.cpp +++ b/test/unit/api/term_white.cpp @@ -14,7 +14,7 @@ #include "test_api.h" -namespace CVC5 { +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 CVC5 +} // namespace cvc5 |