diff options
author | makaimann <makaim@stanford.edu> | 2020-06-29 14:28:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-29 14:28:17 -0700 |
commit | 5cd6f0e5e910ad61ebc5045170842078818a3b80 (patch) | |
tree | 0abfb436badd2bdb2e3616588ece81af0ccbb5ed /src/api | |
parent | 8799bd979c40477d250cada8b498ce344ae61ab6 (diff) |
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.
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/python/cvc4.pxd | 39 | ||||
-rw-r--r-- | src/api/python/cvc4.pxi | 172 | ||||
-rwxr-xr-x | src/api/python/genkinds.py | 4 |
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}) """ |