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 c5773fa728f0f383cbbfb81d8f40a1978b7ba777..9cfc7992c8d2317db0df22d249913def5d9b829d 100644 (file)
--- 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 c5eda174184d342e42c33e04de1dc67be07ef29c..ded268d69555c2c77eb3499f41f3eb5fbd8fdda5 100755 (executable)
--- 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 ff25bbabb85545231718abca03eacffab29d3002..037243ea4f30dc0150191a555ead8e2ca35872a9 100644 (file)
--- 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 dcf787b8eaa95f6dd645b72cc22f0a852fe7ee4b..7ccb73bc372e73b29064b88b4bd02e43b8d7c069 100644 (file)
--- 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 b8bf009af658c8d12189fed8aee1ed2d6d6f9d22..bbff6f58b5b2e0dfc75facc09d4b1df6f3db55e2 100644 (file)
--- 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 7e0e2e3c8eff23516a6b26eef7ae9fc60f204a48..d61fed0fcb7e1c74912586444b04ea5730e58861 100644 (file)
--- 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 f252826246e2b9981f5a1d5e17f0a1e3c4d1e3a5..b404dfb134ccd9d528c1d2c4cab89ad5df6a2c21 100644 (file)
--- 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 aea41a42bedc307bf25ce7e7e3abba546d8cf053..6d65574490c3bae2b37e6d3543441a6ce28e1c40 100644 (file)
--- 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 1bac8a28390d0b5287c4b6ad9989441fe9a0c929..42d2dcb25d3cf00d24e3e9c3daa281019150127a 100644 (file)
--- 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 8f63c55ec4c24bcb81f520a71d612b2a102130e7..78d6ee5cc5904e7b92fa04d895bf5cb5c8b17c7c 100644 (file)
--- 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);