From 90ec15d5917ebc72a84345521523b663c5c3fdd0 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 4 Mar 2021 15:29:00 -0800 Subject: [PATCH] New C++ API: Clean up usage of interal datatype classes. (#6055) This disables the temporarily available internals of datatype classes. --- src/api/cvc4cpp.cpp | 33 ++---------------- src/api/cvc4cpp.h | 83 +++++++++++++++------------------------------ 2 files changed, 30 insertions(+), 86 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 6f226b295..521ab98ea 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2343,14 +2343,6 @@ std::string DatatypeConstructorDecl::toString() const return ss.str(); } -// !!! This is only temporarily available until the parser is fully migrated -// to the new API. !!! -const CVC4::DTypeConstructor& DatatypeConstructorDecl::getDatatypeConstructor( - void) const -{ - return *d_ctor; -} - std::ostream& operator<<(std::ostream& out, const DatatypeConstructorDecl& ctordecl) { @@ -2444,16 +2436,14 @@ std::string DatatypeDecl::getName() const bool DatatypeDecl::isNull() const { return isNullHelper(); } -// !!! This is only temporarily available until the parser is fully migrated -// to the new API. !!! -CVC4::DType& DatatypeDecl::getDatatype(void) const { return *d_dtype; } - std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) { out << dtdecl.toString(); return out; } +CVC4::DType& DatatypeDecl::getDatatype(void) const { return *d_dtype; } + /* DatatypeSelector --------------------------------------------------------- */ DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {} @@ -2495,13 +2485,6 @@ std::string DatatypeSelector::toString() const return ss.str(); } -// !!! This is only temporarily available until the parser is fully migrated -// to the new API. !!! -CVC4::DTypeSelector DatatypeSelector::getDatatypeConstructorArg(void) const -{ - return *d_stor; -} - std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor) { out << stor.toString(); @@ -2682,14 +2665,6 @@ std::string DatatypeConstructor::toString() const return ss.str(); } -// !!! This is only temporarily available until the parser is fully migrated -// to the new API. !!! -const CVC4::DTypeConstructor& DatatypeConstructor::getDatatypeConstructor( - void) const -{ - return *d_ctor; -} - DatatypeSelector DatatypeConstructor::getSelectorForName( const std::string& name) const { @@ -2800,10 +2775,6 @@ Datatype::const_iterator Datatype::end() const return Datatype::const_iterator(d_solver, *d_dtype, false); } -// !!! This is only temporarily available until the parser is fully migrated -// to the new API. !!! -const CVC4::DType& Datatype::getDatatype(void) const { return *d_dtype; } - DatatypeConstructor Datatype::getConstructorForName( const std::string& name) const { diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index d343bc5a1..962fa55ab 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1419,9 +1419,7 @@ class CVC4_PUBLIC DatatypeConstructorDecl friend class Solver; public: - /** - * Nullary constructor for Cython. - */ + /** Constructor. */ DatatypeConstructorDecl(); /** @@ -1446,10 +1444,6 @@ class CVC4_PUBLIC DatatypeConstructorDecl */ std::string toString() const; - // !!! This is only temporarily available until the parser is fully migrated - // to the new API. !!! - const CVC4::DTypeConstructor& getDatatypeConstructor(void) const; - private: /** * Constructor. @@ -1485,9 +1479,7 @@ class CVC4_PUBLIC DatatypeDecl friend class Grammar; public: - /** - * Nullary constructor for Cython. - */ + /** Constructor. */ DatatypeDecl(); /** @@ -1520,10 +1512,6 @@ class CVC4_PUBLIC DatatypeDecl /** @return the name of this datatype declaration. */ std::string getName() const; - // !!! This is only temporarily available until the parser is fully migrated - // to the new API. !!! - CVC4::DType& getDatatype(void) const; - private: /** * Constructor. @@ -1562,6 +1550,9 @@ class CVC4_PUBLIC DatatypeDecl const std::vector& params, bool isCoDatatype = false); + /** @return the internal wrapped Dtype of this datatype declaration. */ + CVC4::DType& getDatatype(void) const; + /** * Helper for isNull checks. This prevents calling an API function with * CVC4_API_CHECK_NOT_NULL @@ -1595,16 +1586,6 @@ class CVC4_PUBLIC DatatypeSelector */ DatatypeSelector(); - // !!! This constructor is only temporarily public until the parser is fully - // migrated to the new API. !!! - /** - * Constructor. - * @param slv the associated solver object - * @param stor the internal datatype selector to be wrapped - * @return the DatatypeSelector - */ - DatatypeSelector(const Solver* slv, const CVC4::DTypeSelector& stor); - /** * Destructor. */ @@ -1627,11 +1608,15 @@ class CVC4_PUBLIC DatatypeSelector */ std::string toString() const; - // !!! This is only temporarily available until the parser is fully migrated - // to the new API. !!! - CVC4::DTypeSelector getDatatypeConstructorArg(void) const; - private: + /** + * Constructor. + * @param slv the associated solver object + * @param stor the internal datatype selector to be wrapped + * @return the DatatypeSelector + */ + DatatypeSelector(const Solver* slv, const CVC4::DTypeSelector& stor); + /** * The associated solver object. */ @@ -1659,15 +1644,6 @@ class CVC4_PUBLIC DatatypeConstructor */ DatatypeConstructor(); - // !!! This constructor is only temporarily public until the parser is fully - // migrated to the new API. !!! - /** - * Constructor. - * @param ctor the internal datatype constructor to be wrapped - * @return the DatatypeConstructor - */ - DatatypeConstructor(const Solver* slv, const CVC4::DTypeConstructor& ctor); - /** * Destructor. */ @@ -1839,11 +1815,14 @@ class CVC4_PUBLIC DatatypeConstructor */ const_iterator end() const; - // !!! This is only temporarily available until the parser is fully migrated - // to the new API. !!! - const CVC4::DTypeConstructor& getDatatypeConstructor(void) const; - private: + /** + * Constructor. + * @param ctor the internal datatype constructor to be wrapped + * @return the DatatypeConstructor + */ + DatatypeConstructor(const Solver* slv, const CVC4::DTypeConstructor& ctor); + /** * Return selector for name. * @param name The name of selector to find @@ -1873,16 +1852,7 @@ class CVC4_PUBLIC Datatype friend class Sort; public: - // !!! This constructor is only temporarily public until the parser is fully - // migrated to the new API. !!! - /** - * Constructor. - * @param dtype the internal datatype to be wrapped - * @return the Datatype - */ - Datatype(const Solver* slv, const CVC4::DType& dtype); - - // Nullary constructor for Cython + /** Constructor. */ Datatype(); /** @@ -2053,11 +2023,14 @@ class CVC4_PUBLIC Datatype */ const_iterator end() const; - // !!! This is only temporarily available until the parser is fully migrated - // to the new API. !!! - const CVC4::DType& getDatatype(void) const; - private: + /** + * Constructor. + * @param dtype the internal datatype to be wrapped + * @return the Datatype + */ + Datatype(const Solver* slv, const CVC4::DType& dtype); + /** * Return constructor for name. * @param name The name of constructor to find -- 2.30.2