Some additions to the datatypes python API (#6640)

This commit makes the following additions, in order to sync the python API with the cpp API.

1. adding `getName` functions to datatypes related classes
2. allowing `mkDatatypeSorts` with 1 or 2 arguments (previously allowed only 2).
3. In case there is a second argument to `mkDatatypeSorts`, we make sure it is a set.
4. Corresponding changes to the tests.

2 files changed, 14 insertions, 4 deletions

diff --git a/test/python/unit/api/test_datatype_api.py b/test/python/unit/api/test_datatype_api.py
index f0c1c0ea9..708942e98 100644
--- a/test/python/unit/api/test_datatype_api.py
+++ b/test/python/unit/api/test_datatype_api.py
@@ -84,6 +84,7 @@ def test_mk_datatype_sorts(solver):
     for i in range(0, len(dtdecls)):
         assert dtsorts[i].isDatatype()
         assert not dtsorts[i].getDatatype().isFinite()
+        assert dtsorts[i].getDatatype().getName() == dtdecls[i].getName()
     # verify the resolution was correct
     dtTree = dtsorts[0].getDatatype()
     dtcTreeNode = dtTree[0]
@@ -98,6 +99,8 @@ def test_mk_datatype_sorts(solver):
     dtdeclsBad = []
     emptyD = solver.mkDatatypeDecl("emptyD")
     dtdeclsBad.append(emptyD)
+    with pytest.raises(RuntimeError):
+        solver.mkDatatypeSorts(dtdeclsBad)
 
 
 def test_datatype_structs(solver):
@@ -177,6 +180,8 @@ def test_datatype_names(solver):
 
     # create datatype sort to test
     dtypeSpec = solver.mkDatatypeDecl("list")
+    dtypeSpec.getName()
+    assert dtypeSpec.getName() == "list"
     cons = solver.mkDatatypeConstructorDecl("cons")
     cons.addSelector("head", intSort)
     cons.addSelectorSelf("tail")
@@ -185,6 +190,7 @@ def test_datatype_names(solver):
     dtypeSpec.addConstructor(nil)
     dtypeSort = solver.mkDatatypeSort(dtypeSpec)
     dt = dtypeSort.getDatatype()
+    assert dt.getName() == "list"
     dt.getConstructor("nil")
     dt["cons"]
     with pytest.raises(RuntimeError):
@@ -209,6 +215,10 @@ def test_datatype_names(solver):
     with pytest.raises(RuntimeError):
         dt.getSelector("cons")
 
+    # possible to construct null datatype declarations if not using mkDatatypeDecl
+    with pytest.raises(RuntimeError):
+        DatatypeDecl(solver).getName()
+
 
 def test_parametric_datatype(solver):
     v = []
diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index c7224022e..67174ad8e 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -143,19 +143,19 @@ def test_mk_datatype_sorts(solver):
     dtypeSpec2.addConstructor(nil2)
 
     decls = [dtypeSpec1, dtypeSpec2]
-    solver.mkDatatypeSorts(decls, [])
+    solver.mkDatatypeSorts(decls, set([]))
 
     with pytest.raises(RuntimeError):
-        slv.mkDatatypeSorts(decls, [])
+        slv.mkDatatypeSorts(decls, set([]))
 
     throwsDtypeSpec = solver.mkDatatypeDecl("list")
     throwsDecls = [throwsDtypeSpec]
     with pytest.raises(RuntimeError):
-        solver.mkDatatypeSorts(throwsDecls, [])
+        solver.mkDatatypeSorts(throwsDecls, set([]))
 
     # with unresolved sorts
     unresList = solver.mkUninterpretedSort("ulist")
-    unresSorts = [unresList]
+    unresSorts = set([unresList])
     ulist = solver.mkDatatypeDecl("ulist")
     ucons = solver.mkDatatypeConstructorDecl("ucons")
     ucons.addSelector("car", unresList)