Merge branch 'master' into fixCMSBuildPRfixCMSBuildPR

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"
 }