1 files changed, 8 insertions, 57 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index dcf787b8e..7ccb73bc3 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -189,7 +189,6 @@ class CVC4_PUBLIC Sort
 {
   friend class DatatypeConstructorDecl;
   friend class DatatypeDecl;
-  friend class DatatypeSelectorDecl;
   friend class Op;
   friend class Solver;
   friend struct SortHashFunction;
@@ -1138,51 +1137,6 @@ class DatatypeConstructorIterator;
 class DatatypeIterator;
 
 /**
- * A place-holder sort to allow a DatatypeDecl to refer to itself.
- * Self-sorted fields of DatatypeDecls will be properly sorted when a Sort is
- * created for the DatatypeDecl.
- */
-class CVC4_PUBLIC DatatypeDeclSelfSort
-{
-};
-
-/**
- * A CVC4 datatype selector declaration.
- */
-class CVC4_PUBLIC DatatypeSelectorDecl
-{
-  friend class DatatypeConstructorDecl;
-
- public:
-  /**
-   * Constructor.
-   * @param name the name of the datatype selector
-   * @param sort the sort of the datatype selector
-   * @return the DatatypeSelectorDecl
-   */
-  DatatypeSelectorDecl(const std::string& name, Sort sort);
-
-  /**
-   * Constructor.
-   * @param name the name of the datatype selector
-   * @param sort the sort of the datatype selector
-   * @return the DAtatypeSelectorDecl
-   */
-  DatatypeSelectorDecl(const std::string& name, DatatypeDeclSelfSort sort);
-
-  /**
-   * @return a string representation of this datatype selector
-   */
-  std::string toString() const;
-
- private:
-  /* The name of the datatype selector. */
-  std::string d_name;
-  /* The sort of the datatype selector. */
-  Sort d_sort;
-};
-
-/**
  * A CVC4 datatype constructor declaration.
  */
 class CVC4_PUBLIC DatatypeConstructorDecl
@@ -1199,9 +1153,15 @@ class CVC4_PUBLIC DatatypeConstructorDecl
 
   /**
    * Add datatype selector declaration.
-   * @param stor the datatype selector declaration to add
+   * @param name the name of the datatype selector declaration to add
+   * @param sort the range sort of the datatype selector declaration to add
+   */
+  void addSelector(const std::string& name, Sort sort);
+  /**
+   * Add datatype selector declaration whose range type is the datatype itself.
+   * @param name the name of the datatype selector declaration to add
    */
-  void addSelector(const DatatypeSelectorDecl& stor);
+  void addSelectorSelf(const std::string& name);
 
   /**
    * @return a string representation of this datatype constructor declaration
@@ -1768,15 +1728,6 @@ std::ostream& operator<<(std::ostream& out,
                          const std::vector<DatatypeConstructorDecl>& vector);
 
 /**
- * Serialize a datatype selector declaration to given stream.
- * @param out the output stream
- * @param stordecl the datatype selector declaration to be serialized
- * @return the output stream
- */
-std::ostream& operator<<(std::ostream& out,
-                         const DatatypeSelectorDecl& stordecl) CVC4_PUBLIC;
-
-/**
  * Serialize a datatype to given stream.
  * @param out the output stream
  * @param dtdecl the datatype to be serialized to given stream