Python Sort tests (#4639)

This commit ports over the sort_black tests to the pytest infrastructure to test the Python bindings. It also adds missing functionality that was revealed during the testing.

3 files changed, 209 insertions, 6 deletions

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index ee05709b7..940922052 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -21,6 +21,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4":
 cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
     cdef cppclass Datatype:
         Datatype() except +
+        DatatypeConstructor operator[](size_t idx) except +
         DatatypeConstructor operator[](const string& name) except +
         DatatypeConstructor getConstructor(const string& name) except +
         Term getConstructorTerm(const string& name) except +
@@ -39,7 +40,12 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
 
     cdef cppclass DatatypeConstructor:
         DatatypeConstructor() except +
+        DatatypeSelector operator[](size_t idx) except +
         DatatypeSelector operator[](const string& name) except +
+        string getName() except +
+        Term getConstructorTerm() except +
+        Term getTesterTerm() except +
+        size_t getNumSelectors() except +
         DatatypeSelector getSelector(const string& name) except +
         Term getSelectorTerm(const string& name) except +
         string toString() except +
@@ -61,12 +67,16 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
 
     cdef cppclass DatatypeDecl:
         void addConstructor(const DatatypeConstructorDecl& ctor) except +
+        size_t getNumConstructors() except +
         bint isParametric() except +
         string toString() except +
 
 
     cdef cppclass DatatypeSelector:
         DatatypeSelector() except +
+        string getName() except +
+        Term getSelectorTerm() except +
+        Sort getRangeSort() except +
         string toString() except +
 
 
@@ -213,6 +223,10 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         Sort() except +
         bint operator==(const Sort&) except +
         bint operator!=(const Sort&) except +
+        bint operator<(const Sort&) except +
+        bint operator>(const Sort&) except +
+        bint operator<=(const Sort&) except +
+        bint operator>=(const Sort&) except +
         bint isBoolean() except +
         bint isInteger() except +
         bint isReal() except +
@@ -223,6 +237,9 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint isFloatingPoint() except +
         bint isDatatype() except +
         bint isParametricDatatype() except +
+        bint isConstructor() except +
+        bint isSelector() except +
+        bint isTester() except +
         bint isFunction() except +
         bint isPredicate() except +
         bint isTuple() except +
@@ -233,9 +250,31 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint isSortConstructor() except +
         bint isFirstClass() except +
         bint isFunctionLike() except +
+        bint isSubsortOf(Sort s) except +
+        bint isComparableTo(Sort s) except +
         Datatype getDatatype() except +
         Sort instantiate(const vector[Sort]& params) except +
+        size_t getConstructorArity() except +
+        vector[Sort] getConstructorDomainSorts() except +
+        Sort getConstructorCodomainSort() except +
+        size_t getFunctionArity() except +
+        vector[Sort] getFunctionDomainSorts() except +
+        Sort getFunctionCodomainSort() except +
+        Sort getArrayIndexSort() except +
+        Sort getArrayElementSort() except +
+        Sort getSetElementSort() except +
+        string getUninterpretedSortName() except +
         bint isUninterpretedSortParameterized() except +
+        vector[Sort] getUninterpretedSortParamSorts() except +
+        string getSortConstructorName() except +
+        size_t getSortConstructorArity() except +
+        uint32_t getBVSize() except +
+        uint32_t getFPExponentSize() except +
+        uint32_t getFPSignificandSize() except +
+        vector[Sort] getDatatypeParamSorts() except +
+        size_t getDatatypeArity() except +
+        size_t getTupleLength() except +
+        vector[Sort] getTupleSorts() except +
         string toString() except +
 
     cdef cppclass SortHashFunction:
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index ab174ef0d..01660e206 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -65,9 +65,14 @@ cdef class Datatype:
     def __cinit__(self):
         pass
 
-    def __getitem__(self, str name):
+    def __getitem__(self, index):
         cdef DatatypeConstructor dc = DatatypeConstructor()
-        dc.cdc = self.cd[name.encode()]
+        if isinstance(index, int) and index >= 0:
+            dc.cdc = self.cd[(<int?> index)]
+        elif isinstance(index, str):
+            dc.cdc = self.cd[(<const string &> name.encode())]
+        else:
+            raise ValueError("Expecting a non-negative integer or string")
         return dc
 
     def getConstructor(self, str name):
@@ -104,11 +109,32 @@ cdef class DatatypeConstructor:
     def __cinit__(self):
         self.cdc = c_DatatypeConstructor()
 
-    def __getitem__(self, str name):
+    def __getitem__(self, index):
         cdef DatatypeSelector ds = DatatypeSelector()
-        ds.cds = self.cdc[name.encode()]
+        if isinstance(index, int) and index >= 0:
+            ds.cds = self.cdc[(<int?> index)]
+        elif isinstance(index, str):
+            ds.cds = self.cdc[(<const string &> name.encode())]
+        else:
+            raise ValueError("Expecting a non-negative integer or string")
         return ds
 
+    def getName(self):
+        return self.cdc.getName().decode()
+
+    def getConstructorTerm(self):
+        cdef Term term = Term()
+        term.cterm = self.cdc.getConstructorTerm()
+        return term
+
+    def getTesterTerm(self):
+        cdef Term term = Term()
+        term.cterm = self.cdc.getTesterTerm()
+        return term
+
+    def getNumSelectors(self):
+        return self.cdc.getNumSelectors()
+
     def getSelector(self, str name):
         cdef DatatypeSelector ds = DatatypeSelector()
         ds.cds = self.cdc.getSelector(name.encode())
@@ -159,6 +185,9 @@ cdef class DatatypeDecl:
     def addConstructor(self, DatatypeConstructorDecl ctor):
         self.cdd.addConstructor(ctor.cddc)
 
+    def getNumConstructors(self):
+        return self.cdd.getNumConstructors()
+
     def isParametric(self):
         return self.cdd.isParametric()
 
@@ -174,6 +203,19 @@ cdef class DatatypeSelector:
     def __cinit__(self):
         self.cds = c_DatatypeSelector()
 
+    def getName(self):
+        return self.cds.getName().decode()
+
+    def getSelectorTerm(self):
+        cdef Term term = Term()
+        term.cterm = self.cds.getSelectorTerm()
+        return term
+
+    def getRangeSort(self):
+        cdef Sort sort = Sort()
+        sort.csort = self.cds.getRangeSort()
+        return sort
+
     def __str__(self):
         return self.cds.toString().decode()
 
@@ -961,6 +1003,18 @@ cdef class Sort:
     def __ne__(self, Sort other):
         return self.csort != other.csort
 
+    def __lt__(self, Sort other):
+        return self.csort < other.csort
+
+    def __gt__(self, Sort other):
+        return self.csort > other.csort
+
+    def __le__(self, Sort other):
+        return self.csort <= other.csort
+
+    def __ge__(self, Sort other):
+        return self.csort >= other.csort
+
     def __str__(self):
         return self.csort.toString().decode()
 
@@ -1000,6 +1054,15 @@ cdef class Sort:
     def isParametricDatatype(self):
         return self.csort.isParametricDatatype()
 
+    def isConstructor(self):
+        return self.csort.isConstructor()
+
+    def isSelector(self):
+        return self.csort.isSelector()
+
+    def isTester(self):
+        return self.csort.isTester()
+
     def isFunction(self):
         return self.csort.isFunction()
 
@@ -1030,6 +1093,12 @@ cdef class Sort:
     def isFunctionLike(self):
         return self.csort.isFunctionLike()
 
+    def isSubsortOf(self, Sort sort):
+        return self.csort.isSubsortOf(sort.csort)
+
+    def isComparableTo(self, Sort sort):
+        return self.csort.isComparableTo(sort.csort)
+
     def getDatatype(self):
         cdef Datatype d = Datatype()
         d.cd = self.csort.getDatatype()
@@ -1043,9 +1112,104 @@ cdef class Sort:
         sort.csort = self.csort.instantiate(v)
         return sort
 
+    def getConstructorArity(self):
+        return self.csort.getConstructorArity()
+
+    def getConstructorDomainSorts(self):
+        domain_sorts = []
+        for s in self.csort.getConstructorDomainSorts():
+            sort = Sort()
+            sort.csort = s
+            domain_sorts.append(sort)
+        return domain_sorts
+
+    def getConstructorCodomainSort(self):
+        cdef Sort sort = Sort()
+        sort.csort = self.csort.getConstructorCodomainSort()
+        return sort
+
+    def getFunctionArity(self):
+        return self.csort.getFunctionArity()
+
+    def getFunctionDomainSorts(self):
+        domain_sorts = []
+        for s in self.csort.getFunctionDomainSorts():
+            sort = Sort()
+            sort.csort = s
+            domain_sorts.append(sort)
+        return domain_sorts
+
+    def getFunctionCodomainSort(self):
+        cdef Sort sort = Sort()
+        sort.csort = self.csort.getFunctionCodomainSort()
+        return sort
+
+    def getArrayIndexSort(self):
+        cdef Sort sort = Sort()
+        sort.csort = self.csort.getArrayIndexSort()
+        return sort
+
+    def getArrayElementSort(self):
+        cdef Sort sort = Sort()
+        sort.csort = self.csort.getArrayElementSort()
+        return sort
+
+    def getSetElementSort(self):
+        cdef Sort sort = Sort()
+        sort.csort = self.csort.getSetElementSort()
+        return sort
+
+    def getUninterpretedSortName(self):
+        return self.csort.getUninterpretedSortName().decode()
+
     def isUninterpretedSortParameterized(self):
         return self.csort.isUninterpretedSortParameterized()
 
+    def getUninterpretedSortParamSorts(self):
+        param_sorts = []
+        for s in self.csort.getUninterpretedSortParamSorts():
+            sort = Sort()
+            sort.csort = s
+            param_sorts.append(sort)
+        return param_sorts
+
+    def getSortConstructorName(self):
+        return self.csort.getSortConstructorName().decode()
+
+    def getSortConstructorArity(self):
+        return self.csort.getSortConstructorArity()
+
+    def getBVSize(self):
+        return self.csort.getBVSize()
+
+    def getFPExponentSize(self):
+        return self.csort.getFPExponentSize()
+
+    def getFPSignificandSize(self):
+        return self.csort.getFPSignificandSize()
+
+    def getDatatypeParamSorts(self):
+        param_sorts = []
+        for s in self.csort.getDatatypeParamSorts():
+            sort = Sort()
+            sort.csort = s
+            param_sorts.append(sort)
+        return param_sorts
+
+    def getDatatypeArity(self):
+        return self.csort.getDatatypeArity()
+
+    def getTupleLength(self):
+        return self.csort.getTupleLength()
+
+    def getTupleSorts(self):
+        tuple_sorts = []
+        for s in self.csort.getTupleSorts():
+            sort = Sort()
+            sort.csort = s
+            tuple_sorts.append(sort)
+        return tuple_sorts
+
 
 cdef class Term:
     cdef c_Term cterm
diff --git a/src/api/python/genkinds.py b/src/api/python/genkinds.py
index a12c9735c..77b168dea 100755
--- a/src/api/python/genkinds.py
+++ b/src/api/python/genkinds.py
@@ -83,7 +83,7 @@ cdef class kind:
     cdef str name
     def __cinit__(self, int kindint):
         self.k = int2kind[kindint]
-        self.name = int2name[kindint].decode()
+        self.name = str(int2name[kindint])
 
     def __eq__(self, kind other):
         return (<int> self.k) == (<int> other.k)
@@ -111,7 +111,7 @@ kinds.__file__ = kinds.__name__ + ".py"
 KINDS_ATTR_TEMPLATE = \
 r"""
 int2kind[<int> {kind}] = {kind}
-int2name[<int> {kind}] = "{name}".encode()
+int2name[<int> {kind}] = b"{name}"
 cdef kind {name} = kind(<int> {kind})
 setattr(kinds, "{name}", {name})
 """