Adding getters to the python API and testing them (#6652)

This PR adds missing API functions from the cpp Term API to the python API.
Corresponding tests are translated from term_black.cpp.

2 files changed, 83 insertions, 14 deletions

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index fdcbfa997..2ad8cef5c 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -176,6 +176,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Sort mkTupleSort(const vector[Sort]& sorts) except +
         Term mkTerm(Op op) except +
         Term mkTerm(Op op, const vector[Term]& children) except +
+        Term mkTuple(const vector[Sort]& sorts, const vector[Term]& terms) except +
         Op mkOp(Kind kind) except +
         Op mkOp(Kind kind, Kind k) except +
         Op mkOp(Kind kind, const string& arg) except +
@@ -388,6 +389,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
             Term operator*() except +
         const_iterator begin() except +
         const_iterator end() except +
+
+        bint isConstArray() except +
         bint isBooleanValue() except +
         bint getBooleanValue() except +
         bint isStringValue() except +
@@ -398,6 +401,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         string getRealValue() except +
         bint isBitVectorValue() except +
         string getBitVectorValue(uint32_t base) except +
+        bint isAbstractValue() except +
+        string getAbstractValue() except +
         bint isFloatingPointPosZero() except +
         bint isFloatingPointNegZero() except +
         bint isFloatingPointPosInf() except +
@@ -406,7 +411,15 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isFloatingPointValue() except +
 
         tuple[uint32_t, uint32_t, Term] getFloatingPointValue() except +
+        bint isSetValue() except +
+        set[Term] getSetValue() except +
+        bint isSequenceValue() except +
         vector[Term] getSequenceValue() except +
+        bint isUninterpretedValue() except +
+        pair[Sort, int32_t] getUninterpretedValue() except +
+        bint isTupleValue() except +
+        vector[Term] getTupleValue() except +
+
 
     cdef cppclass TermHashFunction:
         TermHashFunction() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 25ded76bb..8599a1cd1 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -658,6 +658,19 @@ cdef class Solver:
             term.cterm = self.csolver.mkTerm((<Op?> op).cop, v)
         return term
 
+    def mkTuple(self, sorts, terms):
+        cdef vector[c_Sort] csorts
+        cdef vector[c_Term] cterms
+
+        for s in sorts:
+            csorts.push_back((<Sort?> s).csort)
+        for s in terms:
+            cterms.push_back((<Term?> s).cterm)
+        cdef Term result = Term(self)
+        result.cterm = self.csolver.mkTuple(csorts, cterms)
+        return result
+
+
     def mkOp(self, kind k, arg0=None, arg1 = None):
         '''
         Supports the following uses:
@@ -1609,19 +1622,6 @@ cdef class Term:
     def isNull(self):
         return self.cterm.isNull()
 
-    def getConstArrayBase(self):
-        cdef Term term = Term(self.solver)
-        term.cterm = self.cterm.getConstArrayBase()
-        return term
-
-    def getSequenceValue(self):
-        elems = []
-        for e in self.cterm.getSequenceValue():
-            term = Term(self.solver)
-            term.cterm = e
-            elems.append(term)
-        return elems
-
     def notTerm(self):
         cdef Term term = Term(self.solver)
         term.cterm = self.cterm.notTerm()
@@ -1657,6 +1657,14 @@ cdef class Term:
         term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm)
         return term
 
+    def isConstArray(self):
+        return self.cterm.isConstArray()
+
+    def getConstArrayBase(self):
+        cdef Term term = Term(self.solver)
+        term.cterm = self.cterm.getConstArrayBase()
+        return term
+
     def isBooleanValue(self):
         return self.cterm.isBooleanValue()
 
@@ -1673,7 +1681,12 @@ cdef class Term:
 
     def isIntegerValue(self):
         return self.cterm.isIntegerValue()
-    
+    def isAbstractValue(self):
+        return self.cterm.isAbstractValue()
+
+    def getAbstractValue(self):
+        return self.cterm.getAbstractValue().decode()
+
     def isFloatingPointPosZero(self):
         return self.cterm.isFloatingPointPosZero()
     
@@ -1698,6 +1711,49 @@ cdef class Term:
         term.cterm = get2(t)
         return (get0(t), get1(t), term)
 
+    def isSetValue(self):
+        return self.cterm.isSetValue()
+
+    def getSetValue(self):
+        elems = set()
+        for e in self.cterm.getSetValue():
+            term = Term(self.solver)
+            term.cterm = e
+            elems.add(term)
+        return elems
+
+    def isSequenceValue(self):
+        return self.cterm.isSequenceValue()
+
+    def getSequenceValue(self):
+        elems = []
+        for e in self.cterm.getSequenceValue():
+            term = Term(self.solver)
+            term.cterm = e
+            elems.append(term)
+        return elems
+
+    def isUninterpretedValue(self):
+        return self.cterm.isUninterpretedValue()
+ 
+    def getUninterpretedValue(self):
+        cdef pair[c_Sort, int32_t] p = self.cterm.getUninterpretedValue()
+        cdef Sort sort = Sort(self.solver)
+        sort.csort = p.first
+        i = p.second
+        return (sort, i)
+
+    def isTupleValue(self):
+        return self.cterm.isTupleValue()
+
+    def getTupleValue(self):
+        elems = []
+        for e in self.cterm.getTupleValue():
+            term = Term(self.solver)
+            term.cterm = e
+            elems.append(term)
+        return elems
+
     def getIntegerValue(self):
         return int(self.cterm.getIntegerValue().decode())