summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/api/cvc4cpp.cpp9
-rw-r--r--src/api/cvc4cpp.h9
-rw-r--r--src/api/python/cvc4.pxd10
-rw-r--r--src/api/python/cvc4.pxi47
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()
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback