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.

4 files changed, 531 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})
 """
diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
new file mode 100644
index 000000000..507aff2ae
--- /dev/null
+++ b/test/unit/api/python/test_sort.py
@@ -0,0 +1,322 @@
+import pytest
+
+import pycvc4
+from pycvc4 import kinds
+
+
+def testGetDatatype():
+    solver = pycvc4.Solver()
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+
+    # expecting no Error
+    dtypeSort.getDatatype()
+
+    bvSort = solver.mkBitVectorSort(32)
+    with pytest.raises(Exception):
+        # expect an exception
+        bvSort.getDatatype()
+
+
+def testDatatypeSorts():
+    solver = pycvc4.Solver()
+    intSort = solver.getIntegerSort()
+    # create datatype sort to test
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", intSort)
+    cons.addSelectorSelf("tail")
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+    dt = dtypeSort.getDatatype()
+    assert not dtypeSort.isConstructor()
+
+    with pytest.raises(Exception):
+        dtypeSort.getConstructorCodomainSort()
+
+    with pytest.raises(Exception):
+        dtypeSort.getConstructorDomainSorts()
+
+    with pytest.raises(Exception):
+        dtypeSort.getConstructorArity()
+
+    # get constructor
+    dcons = dt[0]
+    consTerm = dcons.getConstructorTerm()
+    consSort = consTerm.getSort()
+    assert consSort.isConstructor()
+    assert not consSort.isTester()
+    assert not consSort.isSelector()
+    assert consSort.getConstructorArity() == 2
+    consDomSorts = consSort.getConstructorDomainSorts()
+    assert consDomSorts[0] == intSort
+    assert consDomSorts[1] == dtypeSort
+    assert consSort.getConstructorCodomainSort() == dtypeSort
+
+    # get tester
+    isConsTerm = dcons.getTesterTerm()
+    assert isConsTerm.getSort().isTester()
+
+    # get selector
+    dselTail = dcons[1]
+    tailTerm = dselTail.getSelectorTerm()
+    assert tailTerm.getSort().isSelector()
+
+
+def testInstantiate():
+    solver = pycvc4.Solver()
+    # instantiate parametric datatype, check should not fail
+    sort = solver.mkParamSort("T")
+    paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort)
+    paramCons = solver.mkDatatypeConstructorDecl("cons")
+    paramNil = solver.mkDatatypeConstructorDecl("nil")
+    paramCons.addSelector("head", sort)
+    paramDtypeSpec.addConstructor(paramCons)
+    paramDtypeSpec.addConstructor(paramNil)
+    paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec)
+    paramDtypeSort.instantiate([solver.getIntegerSort()])
+
+    # instantiate non-parametric datatype sort, check should fail
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+
+    with pytest.raises(Exception):
+        dtypeSort.instantiate([solver.getIntegerSort()])
+
+
+def testGetFunctionArity():
+    solver = pycvc4.Solver()
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
+                                            solver.getIntegerSort())
+    funSort.getFunctionArity()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getFunctionArity()
+
+
+def testGetFunctionDomainSorts():
+    solver = pycvc4.Solver()
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
+                                            solver.getIntegerSort())
+    funSort.getFunctionDomainSorts()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getFunctionDomainSorts()
+
+
+def testGetFunctionCodomainSort():
+    solver = pycvc4.Solver()
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
+                                            solver.getIntegerSort())
+    funSort.getFunctionCodomainSort()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getFunctionCodomainSort()
+
+def testGetArrayIndexSort():
+    solver = pycvc4.Solver()
+    elementSort = solver.mkBitVectorSort(32)
+    indexSort = solver.mkBitVectorSort(32)
+    arraySort = solver.mkArraySort(indexSort, elementSort)
+    arraySort.getArrayIndexSort()
+
+    with pytest.raises(Exception):
+        indexSort.getArrayIndexSort()
+
+def testGetArrayElementSort():
+    solver = pycvc4.Solver()
+    elementSort = solver.mkBitVectorSort(32)
+    indexSort = solver.mkBitVectorSort(32)
+    arraySort = solver.mkArraySort(indexSort, elementSort)
+    arraySort.getArrayElementSort()
+
+    with pytest.raises(Exception):
+        indexSort.getArrayElementSort()
+
+def testGetSetElementSort():
+    solver = pycvc4.Solver()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+    setSort.getSetElementSort()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getSetElementSort()
+
+def testGetUninterpretedSortName():
+    solver = pycvc4.Solver()
+    uSort = solver.mkUninterpretedSort("u")
+    uSort.getUninterpretedSortName()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getUninterpretedSortName()
+
+def testIsUninterpretedSortParameterized():
+    solver = pycvc4.Solver()
+    uSort = solver.mkUninterpretedSort("u")
+    uSort.isUninterpretedSortParameterized()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.isUninterpretedSortParameterized()
+
+def testGetUninterpretedSortParamSorts():
+    solver = pycvc4.Solver()
+    uSort = solver.mkUninterpretedSort("u")
+    uSort.getUninterpretedSortParamSorts()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getUninterpretedSortParamSorts()
+
+def testGetUninterpretedSortConstructorName():
+    solver = pycvc4.Solver()
+    sSort = solver.mkSortConstructorSort("s", 2)
+    sSort.getSortConstructorName()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getSortConstructorName()
+
+def testGetUninterpretedSortConstructorArity():
+    solver = pycvc4.Solver()
+    sSort = solver.mkSortConstructorSort("s", 2)
+    sSort.getSortConstructorArity()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getSortConstructorArity()
+
+def testGetBVSize():
+    solver = pycvc4.Solver()
+    bvSort = solver.mkBitVectorSort(32)
+    bvSort.getBVSize()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+
+    with pytest.raises(Exception):
+        setSort.getBVSize()
+
+def testGetFPExponentSize():
+    solver = pycvc4.Solver()
+    fpSort = solver.mkFloatingPointSort(4, 8)
+    fpSort.getFPExponentSize()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+
+    with pytest.raises(Exception):
+        setSort.getFPExponentSize()
+
+def testGetFPSignificandSize():
+    solver = pycvc4.Solver()
+    fpSort = solver.mkFloatingPointSort(4, 8)
+    fpSort.getFPSignificandSize()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+
+    with pytest.raises(Exception):
+        setSort.getFPSignificandSize()
+
+def testGetDatatypeParamSorts():
+    solver = pycvc4.Solver()
+    # create parametric datatype, check should not fail
+    sort = solver.mkParamSort("T")
+    paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort)
+    paramCons = solver.mkDatatypeConstructorDecl("cons")
+    paramNil = solver.mkDatatypeConstructorDecl("nil")
+    paramCons.addSelector("head", sort)
+    paramDtypeSpec.addConstructor(paramCons)
+    paramDtypeSpec.addConstructor(paramNil)
+    paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec)
+    paramDtypeSort.getDatatypeParamSorts()
+    # create non-parametric datatype sort, check should fail
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+
+    with pytest.raises(Exception):
+        dtypeSort.getDatatypeParamSorts()
+
+
+def testGetDatatypeArity():
+    solver = pycvc4.Solver()
+    # create datatype sort, check should not fail
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+    dtypeSort.getDatatypeArity()
+    # create bv sort, check should fail
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getDatatypeArity()
+
+def testGetTupleLength():
+    solver = pycvc4.Solver()
+    tupleSort = solver.mkTupleSort([solver.getIntegerSort(), solver.getIntegerSort()])
+    tupleSort.getTupleLength()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getTupleLength()
+
+def testGetTupleSorts():
+    solver = pycvc4.Solver()
+    tupleSort = solver.mkTupleSort([solver.getIntegerSort(), solver.getIntegerSort()])
+    tupleSort.getTupleSorts()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getTupleSorts()
+
+def testSortCompare():
+    solver = pycvc4.Solver()
+    boolSort = solver.getBooleanSort()
+    intSort = solver.getIntegerSort()
+    bvSort = solver.mkBitVectorSort(32)
+    bvSort2 = solver.mkBitVectorSort(32)
+    assert bvSort >= bvSort2
+    assert bvSort <= bvSort2
+    assert (intSort > boolSort) != (intSort < boolSort)
+    assert (intSort > bvSort or intSort == bvSort) == (intSort >= bvSort)
+
+def testSortSubtyping():
+    solver = pycvc4.Solver()
+    intSort = solver.getIntegerSort()
+    realSort = solver.getRealSort()
+    assert intSort.isSubsortOf(realSort)
+    assert not realSort.isSubsortOf(intSort)
+    assert intSort.isComparableTo(realSort)
+    assert realSort.isComparableTo(intSort)
+
+    arraySortII = solver.mkArraySort(intSort, intSort)
+    arraySortIR = solver.mkArraySort(intSort, realSort)
+    assert not arraySortII.isComparableTo(intSort)
+    # we do not support subtyping for arrays
+    assert not arraySortII.isComparableTo(arraySortIR)
+
+    setSortI = solver.mkSetSort(intSort)
+    setSortR = solver.mkSetSort(realSort)
+    # we support subtyping for sets
+    assert setSortI.isSubsortOf(setSortR)
+    assert setSortR.isComparableTo(setSortI)