From: Aina Niemetz Date: Thu, 4 Mar 2021 01:17:17 +0000 (-0800) Subject: New C++ API: Clean up usage of internal types in Op. (#6045) X-Git-Tag: cvc5-1.0.0~2161 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=27d6a284f34ff787882a952572519233ec12b939;p=cvc5.git New C++ API: Clean up usage of internal types in Op. (#6045) This disables the temporarily available internals of Op. --- 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,11 +784,32 @@ 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(), 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(), 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 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{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