Remove obsolete private methods from API (#8716)
authorGereon Kremer <gkremer@cs.stanford.edu>
Wed, 4 May 2022 03:07:29 +0000 (20:07 -0700)
committerGitHub <noreply@github.com>
Wed, 4 May 2022 03:07:29 +0000 (03:07 +0000)
This PR removes two private utilities from the API: Sort::sortSetToTypeNodes and one DatatypeDecl constructor.

src/api/cpp/cvc5.cpp
src/api/cpp/cvc5.h

index d1146649b3382d27fcefdd753f29bcc656762649..115ecddc988c35fb3c72fa158f38187b2c14e3f3 100644 (file)
@@ -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,
index ae50e80adbbdeec77f2ea22aec4a30eda5c4a317..6be6831d759bf7e3e957bd2ea330c65d573069f5 100644 (file)
@@ -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().