From: makaimann Date: Mon, 29 Jun 2020 21:28:17 +0000 (-0700) Subject: Python Sort tests (#4639) X-Git-Tag: cvc5-1.0.0~3167 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5cd6f0e5e910ad61ebc5045170842078818a3b80;p=cvc5.git 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. --- 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[( index)] + elif isinstance(index, str): + dc.cdc = self.cd[( 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[( index)] + elif isinstance(index, str): + ds.cds = self.cdc[( 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 ( self.k) == ( other.k) @@ -111,7 +111,7 @@ kinds.__file__ = kinds.__name__ + ".py" KINDS_ATTR_TEMPLATE = \ r""" int2kind[ {kind}] = {kind} -int2name[ {kind}] = "{name}".encode() +int2name[ {kind}] = b"{name}" cdef kind {name} = kind( {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)