From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 4 Mar 2021 23:29:00 +0000 (-0800)
Subject: New C++ API: Clean up usage of interal datatype classes. (#6055)
X-Git-Tag: cvc5-1.0.0~2150
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=90ec15d5917ebc72a84345521523b663c5c3fdd0;p=cvc5.git

New C++ API: Clean up usage of interal datatype classes. (#6055)

This disables the temporarily available internals of datatype classes.
---

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<Sort>& 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