summaryrefslogtreecommitdiff
path: root/test/unit/api
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/api')
-rw-r--r--test/unit/api/datatype_api_black.cpp4
-rw-r--r--test/unit/api/grammar_black.cpp4
-rw-r--r--test/unit/api/op_black.cpp4
-rw-r--r--test/unit/api/op_white.cpp4
-rw-r--r--test/unit/api/result_black.cpp26
-rw-r--r--test/unit/api/solver_black.cpp8
-rw-r--r--test/unit/api/solver_white.cpp4
-rw-r--r--test/unit/api/sort_black.cpp4
-rw-r--r--test/unit/api/term_black.cpp4
-rw-r--r--test/unit/api/term_white.cpp4
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback