From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Wed, 4 May 2022 03:07:29 +0000 (-0700)
Subject: Remove obsolete private methods from API (#8716)
X-Git-Tag: cvc5-1.0.1~176
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d282676a095cbcf3e9c879253bafd1b169089424;p=cvc5.git

Remove obsolete private methods from API (#8716)

This PR removes two private utilities from the API: Sort::sortSetToTypeNodes and one DatatypeDecl constructor.
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index d1146649b..115ecddc9 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1063,17 +1063,6 @@ Sort::~Sort()
   }
 }
 
-std::set<internal::TypeNode> Sort::sortSetToTypeNodes(
-    const std::set<Sort>& sorts)
-{
-  std::set<internal::TypeNode> types;
-  for (const Sort& s : sorts)
-  {
-    types.insert(s.getTypeNode());
-  }
-  return types;
-}
-
 std::vector<internal::TypeNode> Sort::sortVectorToTypeNodes(
     const std::vector<Sort>& sorts)
 {
@@ -3474,16 +3463,6 @@ DatatypeDecl::DatatypeDecl(const Solver* slv,
 {
 }
 
-DatatypeDecl::DatatypeDecl(const Solver* slv,
-                           const std::string& name,
-                           const Sort& param,
-                           bool isCoDatatype)
-    : d_solver(slv),
-      d_dtype(new internal::DType(
-          name, std::vector<internal::TypeNode>{*param.d_type}, isCoDatatype))
-{
-}
-
 DatatypeDecl::DatatypeDecl(const Solver* slv,
                            const std::string& name,
                            const std::vector<Sort>& params,
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index ae50e80ad..6be6831d7 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -826,9 +826,6 @@ class CVC5_EXPORT Sort
   /** @return The internal wrapped TypeNode of this sort. */
   const internal::TypeNode& getTypeNode(void) const;
 
-  /** Helper to convert a set of Sorts to internal TypeNodes. */
-  std::set<internal::TypeNode> static sortSetToTypeNodes(
-      const std::set<Sort>& sorts);
   /** Helper to convert a vector of Sorts to internal TypeNodes. */
   std::vector<internal::TypeNode> static sortVectorToTypeNodes(
       const std::vector<Sort>& sorts);
@@ -1973,19 +1970,6 @@ class CVC5_EXPORT DatatypeDecl
                const std::string& name,
                bool isCoDatatype = false);
 
-  /**
-   * Constructor for parameterized datatype declaration.
-   * Create sorts parameter with Solver::mkParamSort().
-   * @param slv The associated solver object.
-   * @param name The name of the datatype.
-   * @param param The sort parameter.
-   * @param isCoDatatype True if a codatatype is to be constructed.
-   */
-  DatatypeDecl(const Solver* slv,
-               const std::string& name,
-               const Sort& param,
-               bool isCoDatatype = false);
-
   /**
    * Constructor for parameterized datatype declaration.
    * Create sorts parameter with Solver::mkParamSort().