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.

2 files changed, 36 insertions, 19 deletions

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 9d980267d..623b2f943 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -153,6 +153,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Solver(Options*) except +
         Sort getBooleanSort() except +
         Sort getIntegerSort() except +
+        Sort getNullSort() except +
         Sort getRealSort() except +
         Sort getRegExpSort() except +
         Sort getRoundingModeSort() except +
@@ -178,10 +179,10 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         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 +
         Op mkOp(Kind kind, uint32_t arg) except +
         Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) except +
+        Op mkOp(Kind kind, const vector[uint32_t]& args) except +
         # Sygus related functions
         Grammar mkSygusGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except +
         Term mkSygusVar(Sort sort, const string& symbol) except +
@@ -207,9 +208,11 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term mkRegexpEmpty() except +
         Term mkRegexpSigma() except +
         Term mkEmptySet(Sort s) except +
+        Term mkEmptyBag(Sort s) except +
         Term mkSepNil(Sort sort) except +
         Term mkString(const string& s) except +
         Term mkString(const wstring& s) except +
+        Term mkString(const string& s, bint useEscSequences) except +
         Term mkEmptySequence(Sort sort) except +
         Term mkUniverseSet(Sort sort) except +
         Term mkBitVector(uint32_t size) except +
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