Merge branch 'master' into fixCMSBuildPRfixCMSBuildPR

2 files changed, 68 insertions, 5 deletions

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 16d64b85e..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 +
@@ -116,16 +123,19 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
 
     cdef cppclass Solver:
         Solver(Options*) except +
+        bint supportsFloatingPoint() except +
         Sort getBooleanSort() except +
         Sort getIntegerSort() except +
         Sort getRealSort() except +
         Sort getRegExpSort() except +
-        Sort getRoundingmodeSort() except +
+        Sort getRoundingModeSort() except +
         Sort getStringSort() except +
         Sort mkArraySort(Sort indexSort, Sort elemSort) except +
         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 +
@@ -312,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 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"
 }