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

This disables the temporarily available internals of datatype classes.

1 files changed, 28 insertions, 55 deletions

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,12 +1608,16 @@ 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.
    */
   const Solver* d_solver;
@@ -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,12 +1815,15 @@ 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
    * @return the selector object for the name
@@ -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,12 +2023,15 @@ 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
    * @return the constructor object for the name