Update `toPythonObj` to use new getters -- part 1 (#6623)

Following #6496 , this PR adds new getters to the python API, as well as tests for them. This makes toPythonObj simpler.

A future PR will add more getters to the python API.

Co-authored-by: Gereon Kremer nafur42@gmail.com

2 files changed, 99 insertions, 80 deletions

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 205b82918..ef65c9070 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -22,7 +22,10 @@ cdef extern from "<functional>" namespace "std" nogil:
 
 cdef extern from "<string>" namespace "std":
     cdef cppclass wstring:
+        wstring() except +
         wstring(const wchar_t*, size_t) except +
+        const wchar_t* data() except +
+        size_t size() except +
 
 cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
     cdef cppclass Options:
@@ -374,7 +377,16 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
             Term operator*() except +
         const_iterator begin() except +
         const_iterator end() except +
+        bint isBooleanValue() except +
+        bint getBooleanValue() except +
+        bint isStringValue() except +
+        wstring getStringValue() except +
         bint isIntegerValue() except +
+        string getIntegerValue() except +
+        bint isRealValue() except +
+        string getRealValue() except +
+        bint isBitVectorValue() except +
+        string getBitVectorValue(uint32_t base) except +
         vector[Term] getSequenceValue() except +
 
     cdef cppclass TermHashFunction:
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index b2942e0b3..7731f4e71 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -33,6 +33,7 @@ from cvc5kinds cimport Kind as c_Kind
 
 cdef extern from "Python.h":
     wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *)
+    object PyUnicode_FromWideChar(const wchar_t*, Py_ssize_t)
     void PyMem_Free(void*)
 
 ################################## DECORATORS #################################
@@ -759,6 +760,47 @@ cdef class Solver:
         term.cterm = self.csolver.mkUniverseSet(sort.csort)
         return term
 
+    @expand_list_arg(num_req_args=0)
+    def mkBitVector(self, *args):
+        '''
+            Supports the following arguments:
+            Term mkBitVector(int size, int val=0)
+            Term mkBitVector(string val, int base = 2)
+            Term mkBitVector(int size, string val, int base)
+         '''
+        cdef Term term = Term(self)
+        if len(args) == 1:
+            size_or_val = args[0]
+            if isinstance(args[0], int):
+                size = args[0]
+                term.cterm = self.csolver.mkBitVector(<uint32_t> size)
+            else:
+                assert isinstance(args[0], str)
+                val = args[0]
+                term.cterm = self.csolver.mkBitVector(<const string&> str(val).encode())
+        elif len(args) == 2:
+            if isinstance(args[0], int):
+                size = args[0]
+                assert isinstance(args[1], int)
+                val = args[1]
+                term.cterm = self.csolver.mkBitVector(<uint32_t> size, <uint32_t> val)
+            else:
+                assert isinstance(args[0], str)
+                assert isinstance(args[1], int)
+                val = args[0]
+                base = args[1]
+                term.cterm = self.csolver.mkBitVector(<const string&> str(val).encode(), <uint32_t> base)
+        elif len(args) == 3:
+                assert isinstance(args[0], int)
+                assert isinstance(args[1], str)
+                assert isinstance(args[2], int)
+                size = args[0]
+                val = args[1]
+                base = args[2]
+                term.cterm = self.csolver.mkBitVector(<uint32_t> size, <const string&> str(val).encode(), <uint32_t> base)
+        return term
+
+
     def mkBitVector(self, size_or_str, val = None):
         cdef Term term = Term(self)
         if isinstance(size_or_str, int):
@@ -1603,9 +1645,38 @@ cdef class Term:
         term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm)
         return term
 
-    def isInteger(self):
+    def isBooleanValue(self):
+        return self.cterm.isBooleanValue()
+
+    def getBooleanValue(self):
+        return self.cterm.getBooleanValue()
+
+    def isStringValue(self):
+        return self.cterm.isStringValue()
+
+    def getStringValue(self):
+        cdef Py_ssize_t size
+        cdef c_wstring s = self.cterm.getStringValue()
+        return PyUnicode_FromWideChar(s.data(), s.size())
+
+    def isIntegerValue(self):
         return self.cterm.isIntegerValue()
-    
+
+    def getIntegerValue(self):
+        return int(self.cterm.getIntegerValue().decode())
+
+    def isRealValue(self):
+        return self.cterm.isRealValue()
+
+    def getRealValue(self):
+        return float(Fraction(self.cterm.getRealValue().decode()))
+
+    def isBitVectorValue(self):
+        return self.cterm.isBitVectorValue()
+
+    def getBitVectorValue(self, base = 2):
+        return self.cterm.getBitVectorValue(base).decode()
+
     def toPythonObj(self):
         '''
         Converts a constant value Term to a Python object.
@@ -1615,61 +1686,23 @@ cdef class Term:
           Int     -- returns a Python int
           Real    -- returns a Python Fraction
           BV      -- returns a Python int (treats BV as unsigned)
+          String  -- returns a Python Unicode string
           Array   -- returns a Python dict mapping indices to values
                   -- the constant base is returned as the default value
-          String  -- returns a Python Unicode string
         '''
 
-        string_repr = self.cterm.toString().decode()
-        assert string_repr
-        sort = self.getSort()
-        res = None
-        if sort.isBoolean():
-            if string_repr == "true":
-                res = True
-            else:
-                assert string_repr == "false"
-                res = False
-
-        elif sort.isInteger():
-            updated_string_repr = string_repr.strip('()').replace(' ', '')
-            try:
-                res = int(updated_string_repr)
-            except:
-                raise ValueError("Failed to convert"
-                                 " {} to an int".format(string_repr))
-
-        elif sort.isReal():
-            updated_string_repr = string_repr
-            try:
-                # rational format (/ a b) most likely
-                # note: a or b could be negated: (- a)
-                splits = [s.strip('()/')
-                          for s in updated_string_repr.strip('()/') \
-                          .replace('(- ', '(-').split()]
-                assert len(splits) == 2
-                num = int(splits[0])
-                den = int(splits[1])
-                res = Fraction(num, den)
-            except:
-                try:
-                    # could be exact: e.g., 1.0
-                    res = Fraction(updated_string_repr)
-                except:
-                    raise ValueError("Failed to convert "
-                                     "{} to a Fraction".format(string_repr))
-
-        elif sort.isBitVector():
-            # expecting format #b<bits>
-            assert string_repr[:2] == "#b"
-            python_bin_repr = "0" + string_repr[1:]
-            try:
-                res = int(python_bin_repr, 2)
-            except:
-                raise ValueError("Failed to convert bitvector "
-                                 "{} to an int".format(string_repr))
-
-        elif sort.isArray():
+        if self.isBooleanValue():
+            return self.getBooleanValue()
+        elif self.isIntegerValue():
+            return self.getIntegerValue()
+        elif self.isRealValue():
+            return self.getRealValue()
+        elif self.isBitVectorValue():
+            return int(self.getBitVectorValue(), 2)
+        elif self.isStringValue():
+            return self.getStringValue()
+        elif self.getSort().isArray():
+            res = None
             keys = []
             values = []
             base_value = None
@@ -1696,33 +1729,7 @@ cdef class Term:
             for k, v in zip(keys, values):
                 res[k] = v
 
-        elif sort.isString():
-            # Strip leading and trailing double quotes and replace double
-            # double quotes by single quotes
-            string_repr = string_repr[1:-1].replace('""', '"')
-
-            # Convert escape sequences
-            res = ''
-            escape_prefix = '\\u{'
-            i = 0
-            while True:
-              prev_i = i
-              i = string_repr.find(escape_prefix, i)
-              if i == -1:
-                res += string_repr[prev_i:]
-                break
-
-              res += string_repr[prev_i:i]
-              val = string_repr[i + len(escape_prefix):string_repr.find('}', i)]
-              res += chr(int(val, 16))
-              i += len(escape_prefix) + len(val) + 1
-        else:
-            raise ValueError("Cannot convert term {}"
-                             " of sort {} to Python object".format(string_repr,
-                                                                   sort))
-
-        assert res is not None
-        return res
+            return res
 
 
 # Generate rounding modes