diff options
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 9 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 9 | ||||
-rw-r--r-- | src/api/python/cvc4.pxd | 10 | ||||
-rw-r--r-- | src/api/python/cvc4.pxi | 47 |
4 files changed, 67 insertions, 8 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 6c39bfb91..5b3384439 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3148,8 +3148,8 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const } std::vector<Sort> Solver::mkDatatypeSortsInternal( - std::vector<DatatypeDecl>& dtypedecls, - std::set<Sort>& unresolvedSorts) const + const std::vector<DatatypeDecl>& dtypedecls, + const std::set<Sort>& unresolvedSorts) const { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3367,8 +3367,9 @@ std::vector<Sort> Solver::mkDatatypeSorts( CVC4_API_SOLVER_TRY_CATCH_END; } -std::vector<Sort> Solver::mkDatatypeSorts(std::vector<DatatypeDecl>& dtypedecls, - std::set<Sort>& unresolvedSorts) const +std::vector<Sort> Solver::mkDatatypeSorts( + const std::vector<DatatypeDecl>& dtypedecls, + const std::set<Sort>& unresolvedSorts) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts); diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index d92660920..acf34abf9 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2254,8 +2254,9 @@ class CVC4_PUBLIC Solver * @param unresolvedSorts the list of unresolved sorts * @return the datatype sorts */ - std::vector<Sort> mkDatatypeSorts(std::vector<DatatypeDecl>& dtypedecls, - std::set<Sort>& unresolvedSorts) const; + std::vector<Sort> mkDatatypeSorts( + const std::vector<DatatypeDecl>& dtypedecls, + const std::set<Sort>& unresolvedSorts) const; /** * Create function sort. @@ -3353,8 +3354,8 @@ class CVC4_PUBLIC Solver * @return the datatype sorts */ std::vector<Sort> mkDatatypeSortsInternal( - std::vector<DatatypeDecl>& dtypedecls, - std::set<Sort>& unresolvedSorts) const; + const std::vector<DatatypeDecl>& dtypedecls, + const std::set<Sort>& unresolvedSorts) const; /** * Synthesize n-ary function following specified syntactic constraints. diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 841fbb44d..76dcc5317 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -1,6 +1,7 @@ # import dereference and increment operators from cython.operator cimport dereference as deref, preincrement as inc from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t +from libcpp.set cimport set from libcpp.string cimport string from libcpp.vector cimport vector from libcpp.pair cimport pair @@ -27,6 +28,12 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": Term getConstructorTerm(const string& name) except + size_t getNumConstructors() except + bint isParametric() except + + bint isCodatatype() except + + bint isTuple() except + + bint isRecord() except + + bint isFinite() except + + bint isWellFounded() except + + bint hasNestedRecursion() except + string toString() except + cppclass const_iterator: const_iterator() except + @@ -127,6 +134,8 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": Sort mkBitVectorSort(uint32_t size) except + Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) except + Sort mkDatatypeSort(DatatypeDecl dtypedecl) except + + vector[Sort] mkDatatypeSorts(const vector[DatatypeDecl]& dtypedecls, + const set[Sort]& unresolvedSorts) except + Sort mkFunctionSort(Sort domain, Sort codomain) except + Sort mkFunctionSort(const vector[Sort]& sorts, Sort codomain) except + Sort mkParamSort(const string& symbol) except + @@ -313,6 +322,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": Term() bint operator==(const Term&) except + bint operator!=(const Term&) except + + Term operator[](size_t idx) except + Kind getKind() except + Sort getSort() except + Term substitute(const vector[Term] es, const vector[Term] & reps) except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 3caead057..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 @@ -110,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() @@ -449,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) @@ -1354,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() |