summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cvc4cpp.cpp9
-rw-r--r--src/api/cvc4cpp.h61
-rw-r--r--test/unit/api/CMakeLists.txt3
-rw-r--r--test/unit/api/op_black.cpp7
-rw-r--r--test/unit/api/op_white.cpp35
-rw-r--r--test/unit/api/solver_black.cpp5
-rw-r--r--test/unit/api/solver_white.cpp57
-rw-r--r--test/unit/api/term_black.cpp10
-rw-r--r--test/unit/api/term_white.cpp84
9 files changed, 207 insertions, 64 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index c3490938b..410198920 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1577,15 +1577,6 @@ std::string Op::toString() const
}
}
-// !!! This is only temporarily available until the parser is fully migrated
-// to the new API. !!!
-CVC4::Expr Op::getExpr(void) const
-{
- if (d_node->isNull()) return Expr();
- NodeManagerScope scope(d_solver->getNodeManager());
- return d_node->toExpr();
-}
-
std::ostream& operator<<(std::ostream& out, const Op& t)
{
out << t.toString();
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index d503a317e..e52fe2524 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -719,6 +719,7 @@ struct CVC4_PUBLIC SortHashFunction
class CVC4_PUBLIC Op
{
friend class Solver;
+ friend class Term;
friend struct OpHashFunction;
public:
@@ -727,37 +728,6 @@ class CVC4_PUBLIC Op
*/
Op();
- // !!! This constructor is only temporarily public until the parser is fully
- // migrated to the new API. !!!
- /**
- * Constructor for a single kind (non-indexed operator).
- * @param slv the associated solver object
- * @param k the kind of this Op
- */
- Op(const Solver* slv, const Kind k);
-
- // !!! This constructor is only temporarily public until the parser is fully
- // migrated to the new API. !!!
- /**
- * Constructor.
- * @param slv the associated solver object
- * @param k the kind of this Op
- * @param e the internal expression that is to be wrapped by this term
- * @return the Term
- */
- Op(const Solver* slv, const Kind k, const CVC4::Expr& e);
-
- // !!! This constructor is only temporarily public until the parser is fully
- // migrated to the new API. !!!
- /**
- * Constructor.
- * @param slv the associated solver object
- * @param k the kind of this Op
- * @param n the internal node that is to be wrapped by this term
- * @return the Term
- */
- Op(const Solver* slv, const Kind k, const CVC4::Node& n);
-
/**
* Destructor.
*/
@@ -814,12 +784,33 @@ class CVC4_PUBLIC Op
*/
std::string toString() const;
- // !!! This is only temporarily available until the parser is fully migrated
- // to the new API. !!!
- CVC4::Expr getExpr(void) const;
-
private:
/**
+ * Constructor for a single kind (non-indexed operator).
+ * @param slv the associated solver object
+ * @param k the kind of this Op
+ */
+ Op(const Solver* slv, const Kind k);
+
+ /**
+ * Constructor.
+ * @param slv the associated solver object
+ * @param k the kind of this Op
+ * @param e the internal expression that is to be wrapped by this term
+ * @return the Term
+ */
+ Op(const Solver* slv, const Kind k, const CVC4::Expr& e);
+
+ /**
+ * Constructor.
+ * @param slv the associated solver object
+ * @param k the kind of this Op
+ * @param n the internal node that is to be wrapped by this term
+ * @return the Term
+ */
+ Op(const Solver* slv, const Kind k, const CVC4::Node& n);
+
+ /**
* Helper for isNull checks. This prevents calling an API function with
* CVC4_API_CHECK_NOT_NULL
*/
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 3123607c7..ba4ee31e7 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -14,7 +14,10 @@
cvc4_add_unit_test_black(datatype_api_black api)
cvc4_add_unit_test_black(grammar_black api)
cvc4_add_unit_test_black(op_black api)
+cvc4_add_unit_test_white(op_white api)
cvc4_add_unit_test_black(result_black api)
cvc4_add_unit_test_black(solver_black api)
+cvc4_add_unit_test_white(solver_white api)
cvc4_add_unit_test_black(sort_black api)
cvc4_add_unit_test_black(term_black api)
+cvc4_add_unit_test_white(term_white api)
diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp
index 19bd4bb03..379d16850 100644
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/op_black.cpp
@@ -9,7 +9,7 @@
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief Black box testing of the Term class
+ ** \brief Black box testing of the Op class.
**/
#include "test_api.h"
@@ -41,12 +41,7 @@ TEST_F(TestApiBlackOp, isNull)
TEST_F(TestApiBlackOp, opFromKind)
{
- Op plus(&d_solver, PLUS);
- ASSERT_FALSE(plus.isIndexed());
- ASSERT_THROW(plus.getIndices<uint32_t>(), CVC4ApiException);
-
ASSERT_NO_THROW(d_solver.mkOp(PLUS));
- ASSERT_EQ(plus, d_solver.mkOp(PLUS));
ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC4ApiException);
}
diff --git a/test/unit/api/op_white.cpp b/test/unit/api/op_white.cpp
new file mode 100644
index 000000000..6f1ff549f
--- /dev/null
+++ b/test/unit/api/op_white.cpp
@@ -0,0 +1,35 @@
+/********************* */
+/*! \file op_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief White box testing of the Op class.
+ **/
+
+#include "test_api.h"
+
+namespace CVC4 {
+
+using namespace api;
+
+namespace test {
+
+class TestApiWhiteOp : public TestApi
+{
+};
+
+TEST_F(TestApiWhiteOp, opFromKind)
+{
+ Op plus(&d_solver, PLUS);
+ ASSERT_FALSE(plus.isIndexed());
+ ASSERT_THROW(plus.getIndices<uint32_t>(), CVC4ApiException);
+ ASSERT_EQ(plus, d_solver.mkOp(PLUS));
+}
+} // namespace test
+} // namespace CVC4
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 528d697ae..8e67d1287 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1328,13 +1328,8 @@ TEST_F(TestApiBlackSolver, getOp)
Term listhead = d_solver.mkTerm(APPLY_SELECTOR, headTerm, listcons1);
ASSERT_TRUE(listnil.hasOp());
- ASSERT_EQ(listnil.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
-
ASSERT_TRUE(listcons1.hasOp());
- ASSERT_EQ(listcons1.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
-
ASSERT_TRUE(listhead.hasOp());
- ASSERT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR));
}
TEST_F(TestApiBlackSolver, getOption)
diff --git a/test/unit/api/solver_white.cpp b/test/unit/api/solver_white.cpp
new file mode 100644
index 000000000..e360bb2d0
--- /dev/null
+++ b/test/unit/api/solver_white.cpp
@@ -0,0 +1,57 @@
+/********************* */
+/*! \file solver_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of the Solver class of the C++ API.
+ **
+ ** Black box testing of the Solver class of the C++ API.
+ **/
+
+#include "base/configuration.h"
+#include "test_api.h"
+
+namespace CVC4 {
+
+using namespace api;
+
+namespace test {
+
+class TestApiWhiteSolver : public TestApi
+{
+};
+
+TEST_F(TestApiWhiteSolver, getOp)
+{
+ DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+ cons.addSelector("head", d_solver.getIntegerSort());
+ cons.addSelectorSelf("tail");
+ consListSpec.addConstructor(cons);
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+ consListSpec.addConstructor(nil);
+ Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
+ Datatype consList = consListSort.getDatatype();
+
+ Term nilTerm = consList.getConstructorTerm("nil");
+ Term consTerm = consList.getConstructorTerm("cons");
+ Term headTerm = consList["cons"].getSelectorTerm("head");
+
+ Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm);
+ Term listcons1 = d_solver.mkTerm(
+ APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(1), listnil);
+ Term listhead = d_solver.mkTerm(APPLY_SELECTOR, headTerm, listcons1);
+
+ ASSERT_EQ(listnil.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+ ASSERT_EQ(listcons1.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+ ASSERT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR));
+}
+
+} // namespace test
+} // namespace CVC4
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index d43734295..21906f8ed 100644
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -9,7 +9,7 @@
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief Black box testing of the Term class
+ ** \brief Black box testing of the Term class.
**/
#include "test_api.h"
@@ -158,10 +158,8 @@ TEST_F(TestApiBlackTerm, getOp)
Term extb = d_solver.mkTerm(ext, b);
ASSERT_TRUE(ab.hasOp());
- ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT));
ASSERT_FALSE(ab.getOp().isIndexed());
// can compare directly to a Kind (will invoke Op constructor)
- ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT));
ASSERT_TRUE(extb.hasOp());
ASSERT_TRUE(extb.getOp().isIndexed());
ASSERT_EQ(extb.getOp(), ext);
@@ -172,7 +170,6 @@ TEST_F(TestApiBlackTerm, getOp)
ASSERT_FALSE(f.hasOp());
ASSERT_THROW(f.getOp(), CVC4ApiException);
ASSERT_TRUE(fx.hasOp());
- ASSERT_EQ(fx.getOp(), Op(&d_solver, APPLY_UF));
std::vector<Term> children(fx.begin(), fx.end());
// testing rebuild from op and children
ASSERT_EQ(fx, d_solver.mkTerm(fx.getOp(), children));
@@ -208,11 +205,6 @@ TEST_F(TestApiBlackTerm, getOp)
ASSERT_TRUE(headTerm.hasOp());
ASSERT_TRUE(tailTerm.hasOp());
- ASSERT_EQ(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
- ASSERT_EQ(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
- ASSERT_EQ(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
- ASSERT_EQ(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
-
// Test rebuilding
children.clear();
children.insert(children.begin(), headTerm.begin(), headTerm.end());
diff --git a/test/unit/api/term_white.cpp b/test/unit/api/term_white.cpp
new file mode 100644
index 000000000..da1557024
--- /dev/null
+++ b/test/unit/api/term_white.cpp
@@ -0,0 +1,84 @@
+/********************* */
+/*! \file term_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief White box testing of the Term class.
+ **/
+
+#include "test_api.h"
+
+namespace CVC4 {
+
+using namespace api;
+
+namespace test {
+
+class TestApiWhiteTerm : public TestApi
+{
+};
+
+TEST_F(TestApiWhiteTerm, getOp)
+{
+ Sort intsort = d_solver.getIntegerSort();
+ Sort bvsort = d_solver.mkBitVectorSort(8);
+ Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
+ Sort funsort = d_solver.mkFunctionSort(intsort, bvsort);
+
+ Term x = d_solver.mkConst(intsort, "x");
+ Term a = d_solver.mkConst(arrsort, "a");
+ Term b = d_solver.mkConst(bvsort, "b");
+
+ Term ab = d_solver.mkTerm(SELECT, a, b);
+ Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
+ Term extb = d_solver.mkTerm(ext, b);
+
+ ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT));
+ // can compare directly to a Kind (will invoke Op constructor)
+ ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT));
+
+ Term f = d_solver.mkConst(funsort, "f");
+ Term fx = d_solver.mkTerm(APPLY_UF, f, x);
+
+ ASSERT_EQ(fx.getOp(), Op(&d_solver, APPLY_UF));
+ // testing rebuild from op and children
+
+ // Test Datatypes Ops
+ Sort sort = d_solver.mkParamSort("T");
+ DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+ cons.addSelector("head", sort);
+ cons.addSelectorSelf("tail");
+ listDecl.addConstructor(cons);
+ listDecl.addConstructor(nil);
+ Sort listSort = d_solver.mkDatatypeSort(listDecl);
+ Sort intListSort =
+ listSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()});
+ Term c = d_solver.mkConst(intListSort, "c");
+ Datatype list = listSort.getDatatype();
+ // list datatype constructor and selector operator terms
+ Term consOpTerm = list.getConstructorTerm("cons");
+ Term nilOpTerm = list.getConstructorTerm("nil");
+ Term headOpTerm = list["cons"].getSelectorTerm("head");
+ Term tailOpTerm = list["cons"].getSelectorTerm("tail");
+
+ Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm);
+ Term consTerm = d_solver.mkTerm(
+ APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm);
+ Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm);
+ Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm);
+
+ ASSERT_EQ(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+ ASSERT_EQ(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+ ASSERT_EQ(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
+ ASSERT_EQ(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
+}
+} // namespace test
+} // namespace CVC4
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback