Adding python API test part 5 (#6743)

This commit (follow #6553) adds more functions and unit tests for python API.
Subsequent PR will include additional missing functions and unit tests.

1. Adding getNullSort() and mkEmptyBag() functions.
2. Allowing mkOp() with a list of arguments (previously allowed at most 2).
3. Allowing mkString() with additional boolean argument useEscSequences.
4. Corresponding changes to the tests.

1 files changed, 32 insertions, 18 deletions

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 874c63c3d..4bb9da3d1 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -470,6 +470,11 @@ cdef class Solver:
         sort.csort = self.csolver.getIntegerSort()
         return sort
 
+    def getNullSort(self):
+        cdef Sort sort = Sort(self)
+        sort.csort = self.csolver.getNullSort()
+        return sort
+
     def getRealSort(self):
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.getRealSort()
@@ -672,8 +677,8 @@ cdef class Solver:
         result.cterm = self.csolver.mkTuple(csorts, cterms)
         return result
 
-
-    def mkOp(self, kind k, arg0=None, arg1 = None):
+    @expand_list_arg(num_req_args=0)
+    def mkOp(self, kind k, *args):
         '''
         Supports the following uses:
                 Op mkOp(Kind kind)
@@ -683,28 +688,30 @@ cdef class Solver:
                 Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)
         '''
         cdef Op op = Op(self)
+        cdef vector[int] v
 
-        if arg0 is None:
+        if len(args) == 0:
             op.cop = self.csolver.mkOp(k.k)
-        elif arg1 is None:
-            if isinstance(arg0, kind):
-                op.cop = self.csolver.mkOp(k.k, (<kind?> arg0).k)
-            elif isinstance(arg0, str):
+        elif len(args) == 1:
+            if isinstance(args[0], str):
                 op.cop = self.csolver.mkOp(k.k,
                                            <const string &>
-                                           arg0.encode())
-            elif isinstance(arg0, int):
-                op.cop = self.csolver.mkOp(k.k, <int?> arg0)
+                                           args[0].encode())
+            elif isinstance(args[0], int):
+                op.cop = self.csolver.mkOp(k.k, <int?> args[0])
+            elif isinstance(args[0], list):
+                for a in args[0]:
+                    v.push_back((<int?> a))
+                op.cop = self.csolver.mkOp(k.k, <const vector[uint32_t]&> v)   
             else:
                 raise ValueError("Unsupported signature"
-                                 " mkOp: {}".format(" X ".join([str(k), str(arg0)])))
-        else:
-            if isinstance(arg0, int) and isinstance(arg1, int):
-                op.cop = self.csolver.mkOp(k.k, <int> arg0,
-                                                       <int> arg1)
+                                 " mkOp: {}".format(" X ".join([str(k), str(args[0])])))
+        elif len(args) == 2:
+            if isinstance(args[0], int) and isinstance(args[1], int):
+                op.cop = self.csolver.mkOp(k.k, <int> args[0], <int> args[1])
             else:
                 raise ValueError("Unsupported signature"
-                                 " mkOp: {}".format(" X ".join([k, arg0, arg1])))
+                                 " mkOp: {}".format(" X ".join([k, args[0], args[1]])))
         return op
 
     def mkTrue(self):
@@ -778,17 +785,24 @@ cdef class Solver:
         term.cterm = self.csolver.mkEmptySet(s.csort)
         return term
 
+    def mkEmptyBag(self, Sort s):
+        cdef Term term = Term(self)
+        term.cterm = self.csolver.mkEmptyBag(s.csort)
+        return term
 
     def mkSepNil(self, Sort sort):
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkSepNil(sort.csort)
         return term
 
-    def mkString(self, str s):
+    def mkString(self, str s, useEscSequences = None):
         cdef Term term = Term(self)
         cdef Py_ssize_t size
         cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
-        term.cterm = self.csolver.mkString(c_wstring(tmp, size))
+        if isinstance(useEscSequences, bool):
+            term.cterm = self.csolver.mkString(s.encode(), <bint> useEscSequences)
+        else:
+            term.cterm = self.csolver.mkString(c_wstring(tmp, size))
         PyMem_Free(tmp)
         return term