From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 12 Mar 2020 03:45:03 +0000 (-0500)
Subject: Simplifications to the Datatypes API (#4040)
X-Git-Tag: cvc5-1.0.0~3505
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f48b987d63fef3f698e02c9a48fdba33ffb1c564;p=cvc5.git

Simplifications to the Datatypes API (#4040)

Removes DatatypeSelectorDecl and DatatypeDeclSelfSort. Add selectors is now inlined. A special case is added for the "self selector", instead of using a class as a dummy argument.

I updated the Python files, although would be helpful to double check this is correct.

Co-authored-by: makaimann <makaim@stanford.edu>
---

diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index c5773fa72..9cfc7992c 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -93,10 +93,8 @@ void test(Solver& slv, Sort& consListSort)
                          sort);  // give the datatype a name
   DatatypeConstructorDecl paramCons("cons");
   DatatypeConstructorDecl paramNil("nil");
-  DatatypeSelectorDecl paramHead("head", sort);
-  DatatypeSelectorDecl paramTail("tail", DatatypeDeclSelfSort());
-  paramCons.addSelector(paramHead);
-  paramCons.addSelector(paramTail);
+  paramCons.addSelector("head", sort);
+  paramCons.addSelectorSelf("tail");
   paramConsListSpec.addConstructor(paramCons);
   paramConsListSpec.addConstructor(paramNil);
 
@@ -147,10 +145,8 @@ int main()
   DatatypeDecl consListSpec =
       slv.mkDatatypeDecl("list");  // give the datatype a name
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", slv.getIntegerSort());
-  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
-  cons.addSelector(head);
-  cons.addSelector(tail);
+  cons.addSelector("head", slv.getIntegerSort());
+  cons.addSelectorSelf("tail");
   consListSpec.addConstructor(cons);
   DatatypeConstructorDecl nil("nil");
   consListSpec.addConstructor(nil);
@@ -172,10 +168,8 @@ int main()
   std::cout << std::endl;
 
   DatatypeConstructorDecl cons2("cons");
-  DatatypeSelectorDecl head2("head", slv.getIntegerSort());
-  DatatypeSelectorDecl tail2("tail", DatatypeDeclSelfSort());
-  cons2.addSelector(head2);
-  cons2.addSelector(tail2);
+  cons2.addSelector("head", slv.getIntegerSort());
+  cons2.addSelectorSelf("tail");
   DatatypeConstructorDecl nil2("nil");
   std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2};
   Sort consListSort2 = slv.declareDatatype("list2", ctors);
diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index c5eda1741..ded268d69 100755
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -67,10 +67,8 @@ def test(slv, consListSort):
     paramConsListSpec = slv.mkDatatypeDecl("paramlist", sort)
     paramCons = pycvc4.DatatypeConstructorDecl("cons")
     paramNil = pycvc4.DatatypeConstructorDecl("nil")
-    paramHead = pycvc4.DatatypeSelectorDecl("head", sort)
-    paramTail = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort())
-    paramCons.addSelector(paramHead)
-    paramCons.addSelector(paramTail)
+    paramCons.addSelector("head", sort)
+    paramCons.addSelectorSelf("tail")
     paramConsListSpec.addConstructor(paramCons)
     paramConsListSpec.addConstructor(paramNil)
 
@@ -105,10 +103,8 @@ if __name__ == "__main__":
 
     consListSpec = slv.mkDatatypeDecl("list") # give the datatype a name
     cons = pycvc4.DatatypeConstructorDecl("cons")
-    head = pycvc4.DatatypeSelectorDecl("head", slv.getIntegerSort())
-    tail = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort())
-    cons.addSelector(head)
-    cons.addSelector(tail)
+    cons.addSelector("head", slv.getIntegerSort())
+    cons.addSelectorSelf("tail")
     consListSpec.addConstructor(cons)
     nil = pycvc4.DatatypeConstructorDecl("nil")
     consListSpec.addConstructor(nil)
@@ -127,10 +123,8 @@ if __name__ == "__main__":
     print("### Alternatively, use declareDatatype")
 
     cons2 = pycvc4.DatatypeConstructorDecl("cons")
-    head2 = pycvc4.DatatypeSelectorDecl("head", slv.getIntegerSort())
-    tail2 = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort())
-    cons2.addSelector(head2)
-    cons2.addSelector(tail2)
+    cons2.addSelector("head", slv.getIntegerSort())
+    cons2.addSelectorSelf("tail")
     nil2 = pycvc4.DatatypeConstructorDecl("nil")
     ctors = [cons2, nil2]
     consListSort2 = slv.declareDatatype("list2", ctors)
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index ff25bbabb..037243ea4 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1737,32 +1737,6 @@ size_t TermHashFunction::operator()(const Term& t) const
 /* Datatypes                                                                  */
 /* -------------------------------------------------------------------------- */
 
-/* DatatypeSelectorDecl ----------------------------------------------------- */
-
-DatatypeSelectorDecl::DatatypeSelectorDecl(const std::string& name, Sort sort)
-    : d_name(name), d_sort(sort)
-{
-}
-
-DatatypeSelectorDecl::DatatypeSelectorDecl(const std::string& name,
-                                           DatatypeDeclSelfSort sort)
-    : d_name(name), d_sort(Sort(CVC4::Type()))
-{
-}
-
-std::string DatatypeSelectorDecl::toString() const
-{
-  std::stringstream ss;
-  ss << d_name << ": " << d_sort;
-  return ss.str();
-}
-
-std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl)
-{
-  out << dtdecl.toString();
-  return out;
-}
-
 /* DatatypeConstructorDecl -------------------------------------------------- */
 
 DatatypeConstructorDecl::DatatypeConstructorDecl(const std::string& name)
@@ -1770,17 +1744,16 @@ DatatypeConstructorDecl::DatatypeConstructorDecl(const std::string& name)
 {
 }
 
-void DatatypeConstructorDecl::addSelector(const DatatypeSelectorDecl& stor)
+void DatatypeConstructorDecl::addSelector(const std::string& name, Sort sort)
 {
-  CVC4::Type t = *stor.d_sort.d_type;
-  if (t.isNull())
-  {
-    d_ctor->addArg(stor.d_name, DatatypeSelfType());
-  }
-  else
-  {
-    d_ctor->addArg(stor.d_name, t);
-  }
+  CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort)
+      << "non-null range sort for selector";
+  d_ctor->addArg(name, *sort.d_type);
+}
+
+void DatatypeConstructorDecl::addSelectorSelf(const std::string& name)
+{
+  d_ctor->addArg(name, DatatypeSelfType());
 }
 
 std::string DatatypeConstructorDecl::toString() const
@@ -1890,10 +1863,9 @@ bool DatatypeDecl::isNull() const { return isNullHelper(); }
 // to the new API. !!!
 CVC4::Datatype& DatatypeDecl::getDatatype(void) const { return *d_dtype; }
 
-std::ostream& operator<<(std::ostream& out,
-                         const DatatypeSelectorDecl& stordecl)
+std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl)
 {
-  out << stordecl.toString();
+  out << dtdecl.toString();
   return out;
 }
 
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;
@@ -1137,51 +1136,6 @@ struct CVC4_PUBLIC OpHashFunction
 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.
  */
@@ -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
@@ -1767,15 +1727,6 @@ std::ostream& operator<<(std::ostream& out,
 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
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index b8bf009af..bbff6f58b 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -55,7 +55,8 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
 
     cdef cppclass DatatypeConstructorDecl:
         DatatypeConstructorDecl(const string& name) except +
-        void addSelector(const DatatypeSelectorDecl& stor) except +
+        void addSelector(const string& name, Sort sort) except +
+        void addSelectorSelf(const string& name) except +
         string toString() except +
 
 
@@ -65,21 +66,11 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         string toString() except +
 
 
-    cdef cppclass DatatypeDeclSelfSort:
-        DatatypeDeclSelfSort() except +
-
-
     cdef cppclass DatatypeSelector:
         DatatypeSelector() except +
         string toString() except +
 
 
-    cdef cppclass DatatypeSelectorDecl:
-        DatatypeSelectorDecl(const string& name, Sort sort) except +
-        DatatypeSelectorDecl(const string& name, DatatypeDeclSelfSort sort) except +
-        string toString() except +
-
-
     cdef cppclass Op:
         Op() except +
         bint operator==(const Op&) except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 7e0e2e3c8..d61fed0fc 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -11,9 +11,7 @@ from cvc4 cimport Datatype as c_Datatype
 from cvc4 cimport DatatypeConstructor as c_DatatypeConstructor
 from cvc4 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl
 from cvc4 cimport DatatypeDecl as c_DatatypeDecl
-from cvc4 cimport DatatypeDeclSelfSort as c_DatatypeDeclSelfSort
 from cvc4 cimport DatatypeSelector as c_DatatypeSelector
-from cvc4 cimport DatatypeSelectorDecl as c_DatatypeSelectorDecl
 from cvc4 cimport Result as c_Result
 from cvc4 cimport RoundingMode as c_RoundingMode
 from cvc4 cimport Op as c_Op
@@ -131,8 +129,10 @@ cdef class DatatypeConstructorDecl:
     def __cinit__(self, str name):
         self.cddc = new c_DatatypeConstructorDecl(name.encode())
 
-    def addSelector(self, DatatypeSelectorDecl stor):
-        self.cddc.addSelector(stor.cdsd[0])
+    def addSelector(self, str name, Sort sort):
+        self.cddc.addSelector(name.encode(), sort.csort)
+    def addSelectorSelf(self, str name):
+        self.cddc.addSelectorSelf(name.encode())
 
     def __str__(self):
         return self.cddc.toString().decode()
@@ -159,12 +159,6 @@ cdef class DatatypeDecl:
         return self.cdd.toString().decode()
 
 
-cdef class DatatypeDeclSelfSort:
-    cdef c_DatatypeDeclSelfSort cddss
-    def __cinit__(self):
-        self.cddss = c_DatatypeDeclSelfSort()
-
-
 cdef class DatatypeSelector:
     cdef c_DatatypeSelector cds
     def __cinit__(self):
@@ -177,24 +171,6 @@ cdef class DatatypeSelector:
         return self.cds.toString().decode()
 
 
-cdef class DatatypeSelectorDecl:
-    cdef c_DatatypeSelectorDecl* cdsd
-    def __cinit__(self, str name, sort):
-        if isinstance(sort, Sort):
-            self.cdsd = new c_DatatypeSelectorDecl(
-                <const string &> name.encode(), (<Sort?> sort).csort)
-        elif isinstance(sort, DatatypeDeclSelfSort):
-            self.cdsd = new c_DatatypeSelectorDecl(
-                <const string &> name.encode(),
-                (<DatatypeDeclSelfSort?> sort).cddss)
-
-    def __str__(self):
-        return self.cdsd.toString().decode()
-
-    def __repr__(self):
-        return self.cdsd.toString().decode()
-
-
 cdef class Op:
     cdef c_Op cop
     def __cinit__(self):
diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h
index f25282624..b404dfb13 100644
--- a/test/unit/api/datatype_api_black.h
+++ b/test/unit/api/datatype_api_black.h
@@ -44,8 +44,7 @@ void DatatypeBlack::testMkDatatypeSort()
 {
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
+  cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil("nil");
   dtypeSpec.addConstructor(nil);
@@ -77,23 +76,18 @@ void DatatypeBlack::testMkDatatypeSorts()
 
   DatatypeDecl tree = d_solver.mkDatatypeDecl("tree");
   DatatypeConstructorDecl node("node");
-  DatatypeSelectorDecl left("left", unresTree);
-  node.addSelector(left);
-  DatatypeSelectorDecl right("right", unresTree);
-  node.addSelector(right);
+  node.addSelector("left", unresTree);
+  node.addSelector("right", unresTree);
   tree.addConstructor(node);
 
   DatatypeConstructorDecl leaf("leaf");
-  DatatypeSelectorDecl data("data", unresList);
-  leaf.addSelector(data);
+  leaf.addSelector("data", unresList);
   tree.addConstructor(leaf);
 
   DatatypeDecl list = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl car("car", unresTree);
-  cons.addSelector(car);
-  DatatypeSelectorDecl cdr("cdr", unresTree);
-  cons.addSelector(cdr);
+  cons.addSelector("car", unresTree);
+  cons.addSelector("cdr", unresTree);
   list.addConstructor(cons);
 
   DatatypeConstructorDecl nil("nil");
@@ -137,10 +131,10 @@ void DatatypeBlack::testDatatypeStructs()
   // create datatype sort to test
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", intSort);
-  cons.addSelector(head);
-  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
-  cons.addSelector(tail);
+  cons.addSelector("head", intSort);
+  cons.addSelectorSelf("tail");
+  Sort nullSort;
+  TS_ASSERT_THROWS(cons.addSelector("null", nullSort), CVC4ApiException&);
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil("nil");
   dtypeSpec.addConstructor(nil);
@@ -172,10 +166,8 @@ void DatatypeBlack::testDatatypeStructs()
   // create codatatype
   DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true);
   DatatypeConstructorDecl consStream("cons");
-  DatatypeSelectorDecl headStream("head", intSort);
-  consStream.addSelector(headStream);
-  DatatypeSelectorDecl tailStream("tail", DatatypeDeclSelfSort());
-  consStream.addSelector(tailStream);
+  consStream.addSelector("head", intSort);
+  consStream.addSelectorSelf("tail");
   dtypeSpecStream.addConstructor(consStream);
   Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream);
   Datatype dtStream = dtypeSortStream.getDatatype();
@@ -213,10 +205,8 @@ void DatatypeBlack::testDatatypeNames()
   TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName());
   TS_ASSERT(dtypeSpec.getName() == std::string("list"));
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", intSort);
-  cons.addSelector(head);
-  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
-  cons.addSelector(tail);
+  cons.addSelector("head", intSort);
+  cons.addSelectorSelf("tail");
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil("nil");
   dtypeSpec.addConstructor(nil);
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index aea41a42b..6d6557449 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -181,8 +181,7 @@ void SolverBlack::testMkDatatypeSort()
 {
   DatatypeDecl dtypeSpec = d_solver->mkDatatypeDecl("list");
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver->getIntegerSort());
-  cons.addSelector(head);
+  cons.addSelector("head", d_solver->getIntegerSort());
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil("nil");
   dtypeSpec.addConstructor(nil);
@@ -631,10 +630,8 @@ void SolverBlack::testMkTermFromOp()
   DatatypeDecl listDecl = d_solver->mkDatatypeDecl("paramlist", sort);
   DatatypeConstructorDecl cons("cons");
   DatatypeConstructorDecl nil("nil");
-  DatatypeSelectorDecl head("head", sort);
-  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
-  cons.addSelector(head);
-  cons.addSelector(tail);
+  cons.addSelector("head", sort);
+  cons.addSelectorSelf("tail");
   listDecl.addConstructor(cons);
   listDecl.addConstructor(nil);
   Sort listSort = d_solver->mkDatatypeSort(listDecl);
@@ -941,10 +938,8 @@ void SolverBlack::testGetOp()
   // Test Datatypes -- more complicated
   DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list");
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver->getIntegerSort());
-  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
-  cons.addSelector(head);
-  cons.addSelector(tail);
+  cons.addSelector("head", d_solver->getIntegerSort());
+  cons.addSelectorSelf("tail");
   consListSpec.addConstructor(cons);
   DatatypeConstructorDecl nil("nil");
   consListSpec.addConstructor(nil);
@@ -1044,10 +1039,8 @@ void SolverBlack::testSimplify()
   Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
   DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list");
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver->getIntegerSort());
-  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
-  cons.addSelector(head);
-  cons.addSelector(tail);
+  cons.addSelector("head", d_solver->getIntegerSort());
+  cons.addSelectorSelf("tail");
   consListSpec.addConstructor(cons);
   DatatypeConstructorDecl nil("nil");
   consListSpec.addConstructor(nil);
diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index 1bac8a283..42d2dcb25 100644
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -64,8 +64,7 @@ void SortBlack::testGetDatatype()
   // create datatype sort, check should not fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
+  cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil("nil");
   dtypeSpec.addConstructor(nil);
@@ -82,10 +81,8 @@ void SortBlack::testDatatypeSorts()
   // create datatype sort to test
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", intSort);
-  cons.addSelector(head);
-  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
-  cons.addSelector(tail);
+  cons.addSelector("head", intSort);
+  cons.addSelectorSelf("tail");
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil("nil");
   dtypeSpec.addConstructor(nil);
@@ -126,8 +123,7 @@ void SortBlack::testInstantiate()
   DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
   DatatypeConstructorDecl paramCons("cons");
   DatatypeConstructorDecl paramNil("nil");
-  DatatypeSelectorDecl paramHead("head", sort);
-  paramCons.addSelector(paramHead);
+  paramCons.addSelector("head", sort);
   paramDtypeSpec.addConstructor(paramCons);
   paramDtypeSpec.addConstructor(paramNil);
   Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
@@ -136,8 +132,7 @@ void SortBlack::testInstantiate()
   // instantiate non-parametric datatype sort, check should fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
+  cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil("nil");
   dtypeSpec.addConstructor(nil);
@@ -272,8 +267,7 @@ void SortBlack::testGetDatatypeParamSorts()
   DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
   DatatypeConstructorDecl paramCons("cons");
   DatatypeConstructorDecl paramNil("nil");
-  DatatypeSelectorDecl paramHead("head", sort);
-  paramCons.addSelector(paramHead);
+  paramCons.addSelector("head", sort);
   paramDtypeSpec.addConstructor(paramCons);
   paramDtypeSpec.addConstructor(paramNil);
   Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
@@ -281,8 +275,7 @@ void SortBlack::testGetDatatypeParamSorts()
   // create non-parametric datatype sort, check should fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
+  cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil("nil");
   dtypeSpec.addConstructor(nil);
@@ -295,8 +288,7 @@ void SortBlack::testGetDatatypeArity()
   // create datatype sort, check should not fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
+  cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil("nil");
   dtypeSpec.addConstructor(nil);
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index 8f63c55ec..78d6ee5cc 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -199,10 +199,8 @@ void TermBlack::testGetOp()
   DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
   DatatypeConstructorDecl cons("cons");
   DatatypeConstructorDecl nil("nil");
-  DatatypeSelectorDecl head("head", sort);
-  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
-  cons.addSelector(head);
-  cons.addSelector(tail);
+  cons.addSelector("head", sort);
+  cons.addSelectorSelf("tail");
   listDecl.addConstructor(cons);
   listDecl.addConstructor(nil);
   Sort listSort = d_solver.mkDatatypeSort(listDecl);