diff options
Diffstat (limited to 'src/api/python/cvc4.pxi')
-rw-r--r-- | src/api/python/cvc4.pxi | 60 |
1 files changed, 56 insertions, 4 deletions
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index a51307d21..8c4bfe5e5 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -3,6 +3,7 @@ import sys from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t from libcpp.pair cimport pair +from libcpp.set cimport set from libcpp.string cimport string from libcpp.vector cimport vector @@ -21,7 +22,8 @@ from cvc4 cimport Grammar as c_Grammar from cvc4 cimport Sort as c_Sort from cvc4 cimport SortHashFunction as c_SortHashFunction from cvc4 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE -from cvc4 cimport ROUND_TOWARD_ZERO, ROUND_NEAREST_TIES_TO_AWAY +from cvc4 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO +from cvc4 cimport ROUND_NEAREST_TIES_TO_AWAY from cvc4 cimport Term as c_Term from cvc4 cimport TermHashFunction as c_TermHashFunction @@ -88,7 +90,7 @@ cdef class Datatype: 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())] + dc.cdc = self.cd[(<const string &> index.encode())] else: raise ValueError("Expecting a non-negative integer or string") return dc @@ -109,6 +111,24 @@ cdef class Datatype: def isParametric(self): return self.cd.isParametric() + def isCodatatype(self): + return self.cd.isCodatatype() + + def isTuple(self): + return self.cd.isTuple() + + def isRecord(self): + return self.cd.isRecord() + + def isFinite(self): + return self.cd.isFinite() + + def isWellFounded(self): + return self.cd.isWellFounded() + + def hasNestedRecursion(self): + return self.cd.hasNestedRecursion() + def __str__(self): return self.cd.toString().decode() @@ -395,6 +415,9 @@ cdef class Solver: def __dealloc__(self): del self.csolver + def supportsFloatingPoint(self): + return self.csolver.supportsFloatingPoint() + def getBooleanSort(self): cdef Sort sort = Sort(self) sort.csort = self.csolver.getBooleanSort() @@ -415,9 +438,9 @@ cdef class Solver: sort.csort = self.csolver.getRegExpSort() return sort - def getRoundingmodeSort(self): + def getRoundingModeSort(self): cdef Sort sort = Sort(self) - sort.csort = self.csolver.getRoundingmodeSort() + sort.csort = self.csolver.getRoundingModeSort() return sort def getStringSort(self): @@ -445,6 +468,26 @@ cdef class Solver: sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd) return sort + def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts): + sorts = [] + + cdef vector[c_DatatypeDecl] decls + for decl in dtypedecls: + decls.push_back((<DatatypeDecl?> decl).cdd) + + cdef set[c_Sort] usorts + for usort in unresolvedSorts: + usorts.insert((<Sort?> usort).csort) + + csorts = self.csolver.mkDatatypeSorts( + <const vector[c_DatatypeDecl]&> decls, <const set[c_Sort]&> usorts) + for csort in csorts: + sort = Sort(self) + sort.csort = csort + sorts.append(sort) + + return sorts + def mkFunctionSort(self, sorts, Sort codomain): cdef Sort sort = Sort(self) @@ -1350,6 +1393,14 @@ cdef class Term: def __ne__(self, Term other): return self.cterm != other.cterm + def __getitem__(self, int index): + cdef Term term = Term(self.solver) + if index >= 0: + term.cterm = self.cterm[index] + else: + raise ValueError("Expecting a non-negative integer or string") + return term + def __str__(self): return self.cterm.toString().decode() @@ -1457,6 +1508,7 @@ cdef class Term: cdef __rounding_modes = { <int> ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven", <int> ROUND_TOWARD_POSITIVE: "RoundTowardPositive", + <int> ROUND_TOWARD_NEGATIVE: "RoundTowardNegative", <int> ROUND_TOWARD_ZERO: "RoundTowardZero", <int> ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway" } |