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>

2 files changed, 12 insertions, 24 deletions

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)