Remove decorator from python API (#8505)

This PR removes the expand_list_arg decorator from the python API. It was used to allow calling a function f(x, *args) with a list as second argument and automatically expand the list into *args. While it merely allows for calling f(x, l) instead of f(x, *l), it adds considerable complexity to the code and documentation. Thus, following the Zen of python (have only one way to do it) we remove this decorator. This is also consistent with the pythonic API, were we made the same decision.

diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py
index 49816ead6715d6f5a94997995972e79b4e523427..d7c1ae19e82702f9216b9c7c8e2ee081e4e44fef 100644 (file)
--- a/examples/api/python/bitvectors.py
+++ b/examples/api/python/bitvectors.py
@@ -106,8 +106,7 @@ if __name__ == "__main__":
 
 
     x_neq_x = slv.mkTerm(Kind.Equal, x, x).notTerm()
-    v = [new_x_eq_new_x_, x_neq_x]
-    query = slv.mkTerm(Kind.And, v)
+    query = slv.mkTerm(Kind.And, new_x_eq_new_x_, x_neq_x)
     print("Check sat assuming: ", query.notTerm())
     print("Expect SAT.")
     print("cvc5:", slv.checkSatAssuming(query.notTerm()))

diff --git a/examples/api/python/bitvectors_and_arrays.py b/examples/api/python/bitvectors_and_arrays.py
index 72b57d4e8c7bcc3c9560814553bddcc4adca3d1d..758e6ba2f339caa73a143e593a8aea62199e509d 100644 (file)
--- a/examples/api/python/bitvectors_and_arrays.py
+++ b/examples/api/python/bitvectors_and_arrays.py
@@ -80,7 +80,7 @@ if __name__ == "__main__":
         assertions.append(current_slt_new_current)
         old_current = slv.mkTerm(Kind.Select, current_array, index)
 
-    query = slv.mkTerm(Kind.Not, slv.mkTerm(Kind.And, assertions))
+    query = slv.mkTerm(Kind.Not, slv.mkTerm(Kind.And, *assertions))
 
     print("Asserting {} to cvc5".format(query))
     slv.assertFormula(query)

diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
index d787d14d938a07a88d83a66ab8a9b64d51cf9e98..bb03b1c08a3193853c609be017fbf45727594d97 100644 (file)
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -59,13 +59,12 @@ if __name__ == "__main__":
 
     # Construct the assertions
     assertions = slv.mkTerm(Kind.And,
-                            [
-                                slv.mkTerm(Kind.Leq, zero, f_x), # 0 <= f(x)
-                                slv.mkTerm(Kind.Leq, zero, f_y), # 0 <= f(y)
-                                slv.mkTerm(Kind.Leq, sum_, one), # f(x) + f(y) <= 1
-                                p_0.notTerm(), # not p(0)
-                                p_f_y # p(f(y))
-                            ])
+                            slv.mkTerm(Kind.Leq, zero, f_x), # 0 <= f(x)
+                            slv.mkTerm(Kind.Leq, zero, f_y), # 0 <= f(y)
+                            slv.mkTerm(Kind.Leq, sum_, one), # f(x) + f(y) <= 1
+                            p_0.notTerm(), # not p(0)
+                            p_f_y # p(f(y))
+                            )
 
     slv.assertFormula(assertions)
 

diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index 3cf0d10a9d1f575b47f025d9e1e358f4495fae81..0fa8bc2376a1ae08df517d73bbabfe6d996bab22 100644 (file)
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -140,6 +140,5 @@ if __name__ == "__main__":
     cons2.addSelector("head", slv.getIntegerSort())
     cons2.addSelectorSelf("tail")
     nil2 = slv.mkDatatypeConstructorDecl("nil")
-    ctors = [cons2, nil2]
-    consListSort2 = slv.declareDatatype("list2", ctors)
+    consListSort2 = slv.declareDatatype("list2", cons2, nil2)
     test(slv, consListSort2)

diff --git a/examples/api/python/relations.py b/examples/api/python/relations.py
index 8098a56f35b36d1426bb2b6bb6907d9f15d2eaa9..2bf7604b04bc9307f42175b5c084dff30a1c7bc2 100644 (file)
--- a/examples/api/python/relations.py
+++ b/examples/api/python/relations.py
@@ -42,12 +42,12 @@ if __name__ == "__main__":
     personSort = solver.mkUninterpretedSort("Person")
 
     # (Tuple Person)
-    tupleArity1 = solver.mkTupleSort([personSort])
+    tupleArity1 = solver.mkTupleSort(personSort)
     # (Set (Tuple Person))
     relationArity1 = solver.mkSetSort(tupleArity1)
 
     # (Tuple Person Person)
-    tupleArity2 = solver.mkTupleSort([personSort, personSort])
+    tupleArity2 = solver.mkTupleSort(personSort, personSort)
     # (Set (Tuple Person Person))
     relationArity2 = solver.mkSetSort(tupleArity2)
 

diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py
index 618bd206952ec272a6a09a62cffef8e49f0b6f11..c7711dd81e30d6d57438b5a67f1d586c2c456963 100644 (file)
--- a/examples/api/python/sygus-grammar.py
+++ b/examples/api/python/sygus-grammar.py
@@ -78,7 +78,7 @@ if __name__ == "__main__":
 
   # add semantic constraints
   # (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x))
-  slv.addSygusConstraint(slv.mkTerm(Kind.And, [slv.mkTerm(Kind.Equal, id1_x, id2_x), slv.mkTerm(Kind.Equal, id1_x, id3_x), slv.mkTerm(Kind.Equal, id1_x, id4_x), slv.mkTerm(Kind.Equal, id1_x, varX)]))
+  slv.addSygusConstraint(slv.mkTerm(Kind.And, slv.mkTerm(Kind.Equal, id1_x, id2_x), slv.mkTerm(Kind.Equal, id1_x, id3_x), slv.mkTerm(Kind.Equal, id1_x, id4_x), slv.mkTerm(Kind.Equal, id1_x, varX)))
 
   # print solutions if available
   if (slv.checkSynth().hasSolution()):

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index bfc139b1a94f2ee9de358860eb016477517f0318..1197e0b00397e44db7580d6764703cd5899c591c 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -46,23 +46,6 @@ cdef extern from "Python.h":
     object PyUnicode_FromWideChar(const wchar_t*, Py_ssize_t)
     void PyMem_Free(void*)
 
-################################## DECORATORS #################################
-def expand_list_arg(num_req_args=0):
-    """
-        Creates a decorator that looks at index num_req_args of the args,
-        if it's a list, it expands it before calling the function.
-    """
-    def decorator(func):
-        @wraps(func)
-        def wrapper(owner, *args):
-            if len(args) == num_req_args + 1 and \
-               isinstance(args[num_req_args], list):
-                args = list(args[:num_req_args]) + args[num_req_args]
-            return func(owner, *args)
-        return wrapper
-    return decorator
-###############################################################################
-
 # Style Guidelines
 ### Using PEP-8 spacing recommendations
 ### Limit linewidth to 79 characters
@@ -945,13 +928,11 @@ cdef class Solver:
           sort.csort = self.csolver.mkParamSort(symbolname.encode())
         return sort
 
-    @expand_list_arg(num_req_args=0)
     def mkPredicateSort(self, *sorts):
         """
             Create a predicate sort.
 
-            :param sorts: The list of sorts of the predicate, as a list or as
-                          distinct arguments.
+            :param sorts: The list of sorts of the predicate.
             :return: The predicate sort.
         """
         cdef Sort sort = Sort(self)
@@ -961,7 +942,6 @@ cdef class Solver:
         sort.csort = self.csolver.mkPredicateSort(<const vector[c_Sort]&> v)
         return sort
 
-    @expand_list_arg(num_req_args=0)
     def mkRecordSort(self, *fields):
         """
             Create a record sort
@@ -969,8 +949,7 @@ cdef class Solver:
             .. warning:: This method is experimental and may change in future
                          versions.
 
-            :param fields: The list of fields of the record, as a list or as
-                           distinct arguments.
+            :param fields: The list of fields of the record.
             :return: The record sort.
         """
         cdef Sort sort = Sort(self)
@@ -1066,13 +1045,11 @@ cdef class Solver:
               arity, symbol.encode())
         return sort
 
-    @expand_list_arg(num_req_args=0)
     def mkTupleSort(self, *sorts):
         """
             Create a tuple sort.
 
-            :param sorts: Of the elements of the tuple, as a list or as
-                          distinct arguments.
+            :param sorts: Of the elements of the tuple.
             :return: The tuple sort.
         """
         cdef Sort sort = Sort(self)
@@ -1082,7 +1059,6 @@ cdef class Solver:
         sort.csort = self.csolver.mkTupleSort(v)
         return sort
 
-    @expand_list_arg(num_req_args=1)
     def mkTerm(self, kind_or_op, *args):
         """
             Create a term.
@@ -1131,7 +1107,6 @@ cdef class Solver:
         result.cterm = self.csolver.mkTuple(csorts, cterms)
         return result
 
-    @expand_list_arg(num_req_args=0)
     def mkOp(self, k, *args):
         """
             Create operator.
@@ -1378,7 +1353,6 @@ cdef class Solver:
         term.cterm = self.csolver.mkUniverseSet(sort.csort)
         return term
 
-    @expand_list_arg(num_req_args=0)
     def mkBitVector(self, *args):
         """
             Create bit-vector value.
@@ -1914,7 +1888,6 @@ cdef class Solver:
                     grammar.cgrammar)
         return term
 
-    @expand_list_arg(num_req_args=0)
     def checkSatAssuming(self, *assumptions):
         """
             Check satisfiability assuming the given formula.
@@ -1925,8 +1898,7 @@ cdef class Solver:
 
                 ( check-sat-assuming ( <prop_literal> ) )
 
-            :param assumptions: The formulas to assume, as a list or as
-                                distinct arguments.
+            :param assumptions: The formulas to assume.
             :return: The result of the satisfiability check.
         """
         cdef Result r = Result()
@@ -1937,7 +1909,6 @@ cdef class Solver:
         r.cr = self.csolver.checkSatAssuming(<const vector[c_Term]&> v)
         return r
 
-    @expand_list_arg(num_req_args=1)
     def declareDatatype(self, str symbol, *ctors):
         """
             Create datatype sort.
@@ -1949,8 +1920,7 @@ cdef class Solver:
                 ( declare-datatype <symbol> <datatype_decl> )
 
             :param symbol: The name of the datatype sort.
-            :param ctors: The constructor declarations of the datatype sort, as
-                          a list or as distinct arguments.
+            :param ctors: The constructor declarations of the datatype sort.
             :return: The datatype sort.
         """
         cdef Sort sort = Sort(self)

diff --git a/test/api/python/issue5074.py b/test/api/python/issue5074.py
index f41ebb16a6252aa72b7d821346691ed9ca0922c2..f85bdfc83a53997ed38e4fbda22e103d6c5cf316 100644 (file)
--- a/test/api/python/issue5074.py
+++ b/test/api/python/issue5074.py
@@ -20,6 +20,6 @@ slv = cvc5.Solver()
 c1 = slv.mkConst(slv.getIntegerSort())
 t6 = slv.mkTerm(Kind.StringFromCode, c1)
 t12 = slv.mkTerm(Kind.StringToRegexp, t6)
-t14 = slv.mkTerm(Kind.StringReplaceRe, [t6, t12, t6])
-t16 = slv.mkTerm(Kind.StringContains, [t14, t14])
+t14 = slv.mkTerm(Kind.StringReplaceRe, t6, t12, t6)
+t16 = slv.mkTerm(Kind.StringContains, t14, t14)
 slv.checkSatAssuming(t16.notTerm())

diff --git a/test/api/python/issue6111.py b/test/api/python/issue6111.py
index 61d5a4ad0f74ad2ccff52fcfca34b36bfa944b13..6098fb6dca345223491a4a4fa5a062d9e75cdbcb 100644 (file)
--- a/test/api/python/issue6111.py
+++ b/test/api/python/issue6111.py
@@ -22,10 +22,7 @@ bvsort12979 = solver.mkBitVectorSort(12979)
 input2_1 = solver.mkConst(bvsort12979, "intpu2_1")
 zero = solver.mkBitVector(bvsort12979.getBitVectorSize(), "0", 10)
 
-args1 = []
-args1.append(zero)
-args1.append(input2_1)
-bvult_res = solver.mkTerm(Kind.BVUlt, args1)
+bvult_res = solver.mkTerm(Kind.BVUlt, zero, input2_1)
 solver.assertFormula(bvult_res)
 
 bvsort4 = solver.mkBitVectorSort(4)
@@ -36,13 +33,13 @@ concat_result_43 = solver.mkConst(bvsort8, "concat_result_43")
 args2 = []
 args2.append(concat_result_42)
 args2.append(
-    solver.mkTerm(solver.mkOp(Kind.BVExtract, 7, 4), [concat_result_43]))
-solver.assertFormula(solver.mkTerm(Kind.Equal, args2))
+    solver.mkTerm(solver.mkOp(Kind.BVExtract, 7, 4), concat_result_43))
+solver.assertFormula(solver.mkTerm(Kind.Equal, *args2))
 
 args3 = []
 args3.append(concat_result_42)
 args3.append(
-    solver.mkTerm(solver.mkOp(Kind.BVExtract, 3, 0), [concat_result_43]))
-solver.assertFormula(solver.mkTerm(Kind.Equal, args3))
+    solver.mkTerm(solver.mkOp(Kind.BVExtract, 3, 0), concat_result_43))
+solver.assertFormula(solver.mkTerm(Kind.Equal, *args3))
 
 print(solver.checkSat())

diff --git a/test/api/python/proj-issue306.py b/test/api/python/proj-issue306.py
index 6db53bb50c97eb2bccc77c1134adcbc71a7d9a41..fb9e7913cb6b18abfece5282829a83a62681f354 100644 (file)
--- a/test/api/python/proj-issue306.py
+++ b/test/api/python/proj-issue306.py
@@ -28,4 +28,4 @@ t42 = slv.mkTerm(Kind.Ite, t3, t14, t1)
 t58 = slv.mkTerm(Kind.StringLeq, t14, t11)
 t95 = slv.mkTerm(Kind.Equal, t14, t42)
 slv.assertFormula(t95)
-slv.checkSatAssuming([t58])
+slv.checkSatAssuming(t58)

diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py
index 483243a9f1e60c65936292d4a229934f10fc263d..2fb978dbbe725ba37769ca9c8e9ab90dc74d6041 100644 (file)
--- a/test/unit/api/python/test_datatype_api.py
+++ b/test/unit/api/python/test_datatype_api.py
@@ -194,7 +194,7 @@ def test_datatype_structs(solver):
     assert dtStream.isWellFounded()
 
     # create tuple
-    tupSort = solver.mkTupleSort([boolSort])
+    tupSort = solver.mkTupleSort(boolSort)
     dtTuple = tupSort.getDatatype()
     assert dtTuple.isTuple()
     assert not dtTuple.isRecord()
@@ -203,7 +203,7 @@ def test_datatype_structs(solver):
 
     # create record
     fields = [("b", boolSort), ("i", intSort)]
-    recSort = solver.mkRecordSort(fields)
+    recSort = solver.mkRecordSort(*fields)
     assert recSort.isDatatype()
     dtRecord = recSort.getDatatype()
     assert not dtRecord.isTuple()

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 74dc04620f8ec477fcaebb166f2e48f5889cadd4..8ef6de932499717ea72b3a957a89cd825ed00669 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -235,28 +235,27 @@ def test_mk_param_sort(solver):
 
 
 def test_mk_predicate_sort(solver):
-    solver.mkPredicateSort([solver.getIntegerSort()])
+    solver.mkPredicateSort(solver.getIntegerSort())
     with pytest.raises(RuntimeError):
-        solver.mkPredicateSort([])
+        solver.mkPredicateSort()
 
     funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
             solver.getIntegerSort())
     # functions as arguments are allowed
-    solver.mkPredicateSort([solver.getIntegerSort(), funSort])
+    solver.mkPredicateSort(solver.getIntegerSort(), funSort)
 
     slv = cvc5.Solver()
     with pytest.raises(RuntimeError):
-        slv.mkPredicateSort([solver.getIntegerSort()])
+        slv.mkPredicateSort(solver.getIntegerSort())
 
 
 def test_mk_record_sort(solver):
     fields = [("b", solver.getBooleanSort()),\
               ("bv", solver.mkBitVectorSort(8)),\
               ("i", solver.getIntegerSort())]
-    empty = []
-    solver.mkRecordSort(fields)
-    solver.mkRecordSort(empty)
-    recSort = solver.mkRecordSort(fields)
+    solver.mkRecordSort(*fields)
+    solver.mkRecordSort()
+    recSort = solver.mkRecordSort(*fields)
     recSort.getDatatype()
 
 
@@ -307,15 +306,15 @@ def test_mk_sort_constructor_sort(solver):
 
 
 def test_mk_tuple_sort(solver):
-    solver.mkTupleSort([solver.getIntegerSort()])
+    solver.mkTupleSort(solver.getIntegerSort())
     funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
                                     solver.getIntegerSort())
     with pytest.raises(RuntimeError):
-        solver.mkTupleSort([solver.getIntegerSort(), funSort])
+        solver.mkTupleSort(solver.getIntegerSort(), funSort)
 
     slv = cvc5.Solver()
     with pytest.raises(RuntimeError):
-        slv.mkTupleSort([solver.getIntegerSort()])
+        slv.mkTupleSort(solver.getIntegerSort())
 
 
 def test_mk_bit_vector(solver):
@@ -701,32 +700,18 @@ def test_mk_term(solver):
     bv32 = solver.mkBitVectorSort(32)
     a = solver.mkConst(bv32, "a")
     b = solver.mkConst(bv32, "b")
-    v1 = [a, b]
-    v2 = [a, cvc5.Term(solver)]
-    v3 = [a, solver.mkTrue()]
-    v4 = [solver.mkInteger(1), solver.mkInteger(2)]
-    v5 = [solver.mkInteger(1), cvc5.Term(solver)]
-    v6 = []
     slv = cvc5.Solver()
 
     # mkTerm(Kind kind) const
     solver.mkPi()
     solver.mkTerm(Kind.Pi)
-    solver.mkTerm(Kind.Pi, v6)
     solver.mkTerm(solver.mkOp(Kind.Pi))
-    solver.mkTerm(solver.mkOp(Kind.Pi), v6)
     solver.mkTerm(Kind.RegexpNone)
-    solver.mkTerm(Kind.RegexpNone, v6)
     solver.mkTerm(solver.mkOp(Kind.RegexpNone))
-    solver.mkTerm(solver.mkOp(Kind.RegexpNone), v6)
     solver.mkTerm(Kind.RegexpAllchar)
-    solver.mkTerm(Kind.RegexpAllchar, v6)
     solver.mkTerm(solver.mkOp(Kind.RegexpAllchar))
-    solver.mkTerm(solver.mkOp(Kind.RegexpAllchar), v6)
     solver.mkTerm(Kind.SepEmp)
-    solver.mkTerm(Kind.SepEmp, v6)
     solver.mkTerm(solver.mkOp(Kind.SepEmp))
-    solver.mkTerm(solver.mkOp(Kind.SepEmp), v6)
     with pytest.raises(RuntimeError):
         solver.mkTerm(Kind.ConstBV)
 
@@ -767,53 +752,49 @@ def test_mk_term(solver):
         slv.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(),
                    solver.mkTrue())
 
-    solver.mkTerm(Kind.Equal, v1)
+    solver.mkTerm(Kind.Equal, a, b)
     with pytest.raises(RuntimeError):
-        solver.mkTerm(Kind.Equal, v2)
+        solver.mkTerm(Kind.Equal, a, cvc5.Term(solver))
     with pytest.raises(RuntimeError):
-        solver.mkTerm(Kind.Equal, v3)
+        solver.mkTerm(Kind.Equal, a, solver.mkTrue())
     with pytest.raises(RuntimeError):
-        solver.mkTerm(Kind.Distinct, v6)
+        solver.mkTerm(Kind.Distinct)
 
     # Test cases that are nary via the API but have arity = 2 internally
     s_bool = solver.getBooleanSort()
     t_bool = solver.mkConst(s_bool, "t_bool")
-    solver.mkTerm(Kind.Implies, [t_bool, t_bool, t_bool])
-    solver.mkTerm(Kind.Xor, [t_bool, t_bool, t_bool])
-    solver.mkTerm(solver.mkOp(Kind.Xor), [t_bool, t_bool, t_bool])
+    solver.mkTerm(Kind.Implies, t_bool, t_bool, t_bool)
+    solver.mkTerm(Kind.Xor, t_bool, t_bool, t_bool)
+    solver.mkTerm(solver.mkOp(Kind.Xor), t_bool, t_bool, t_bool)
     t_int = solver.mkConst(solver.getIntegerSort(), "t_int")
-    solver.mkTerm(Kind.Division, [t_int, t_int, t_int])
-    solver.mkTerm(solver.mkOp(Kind.Division), [t_int, t_int, t_int])
-    solver.mkTerm(Kind.IntsDivision, [t_int, t_int, t_int])
-    solver.mkTerm(solver.mkOp(Kind.IntsDivision), [t_int, t_int, t_int])
-    solver.mkTerm(Kind.Sub, [t_int, t_int, t_int])
-    solver.mkTerm(solver.mkOp(Kind.Sub), [t_int, t_int, t_int])
-    solver.mkTerm(Kind.Equal, [t_int, t_int, t_int])
-    solver.mkTerm(solver.mkOp(Kind.Equal), [t_int, t_int, t_int])
-    solver.mkTerm(Kind.Lt, [t_int, t_int, t_int])
-    solver.mkTerm(solver.mkOp(Kind.Lt), [t_int, t_int, t_int])
-    solver.mkTerm(Kind.Gt, [t_int, t_int, t_int])
-    solver.mkTerm(solver.mkOp(Kind.Gt), [t_int, t_int, t_int])
-    solver.mkTerm(Kind.Leq, [t_int, t_int, t_int])
-    solver.mkTerm(solver.mkOp(Kind.Leq), [t_int, t_int, t_int])
-    solver.mkTerm(Kind.Geq, [t_int, t_int, t_int])
-    solver.mkTerm(solver.mkOp(Kind.Geq), [t_int, t_int, t_int])
+    solver.mkTerm(Kind.Division, t_int, t_int, t_int)
+    solver.mkTerm(solver.mkOp(Kind.Division), t_int, t_int, t_int)
+    solver.mkTerm(Kind.IntsDivision, t_int, t_int, t_int)
+    solver.mkTerm(solver.mkOp(Kind.IntsDivision), t_int, t_int, t_int)
+    solver.mkTerm(Kind.Sub, t_int, t_int, t_int)
+    solver.mkTerm(solver.mkOp(Kind.Sub), t_int, t_int, t_int)
+    solver.mkTerm(Kind.Equal, t_int, t_int, t_int)
+    solver.mkTerm(solver.mkOp(Kind.Equal), t_int, t_int, t_int)
+    solver.mkTerm(Kind.Lt, t_int, t_int, t_int)
+    solver.mkTerm(solver.mkOp(Kind.Lt), t_int, t_int, t_int)
+    solver.mkTerm(Kind.Gt, t_int, t_int, t_int)
+    solver.mkTerm(solver.mkOp(Kind.Gt), t_int, t_int, t_int)
+    solver.mkTerm(Kind.Leq, t_int, t_int, t_int)
+    solver.mkTerm(solver.mkOp(Kind.Leq), t_int, t_int, t_int)
+    solver.mkTerm(Kind.Geq, t_int, t_int, t_int)
+    solver.mkTerm(solver.mkOp(Kind.Geq), t_int, t_int, t_int)
     t_reg = solver.mkConst(solver.getRegExpSort(), "t_reg")
-    solver.mkTerm(Kind.RegexpDiff, [t_reg, t_reg, t_reg])
-    solver.mkTerm(solver.mkOp(Kind.RegexpDiff), [t_reg, t_reg, t_reg])
+    solver.mkTerm(Kind.RegexpDiff, t_reg, t_reg, t_reg)
+    solver.mkTerm(solver.mkOp(Kind.RegexpDiff), t_reg, t_reg, t_reg)
     t_fun = solver.mkConst(solver.mkFunctionSort(
         [s_bool, s_bool, s_bool], s_bool))
-    solver.mkTerm(Kind.HoApply, [t_fun, t_bool, t_bool, t_bool])
-    solver.mkTerm(solver.mkOp(Kind.HoApply), [t_fun, t_bool, t_bool, t_bool])
+    solver.mkTerm(Kind.HoApply, t_fun, t_bool, t_bool, t_bool)
+    solver.mkTerm(solver.mkOp(Kind.HoApply), t_fun, t_bool, t_bool, t_bool)
 
 def test_mk_term_from_op(solver):
     bv32 = solver.mkBitVectorSort(32)
     a = solver.mkConst(bv32, "a")
     b = solver.mkConst(bv32, "b")
-    v1 = [solver.mkInteger(1), solver.mkInteger(2)]
-    v2 = [solver.mkInteger(1), cvc5.Term(solver)]
-    v3 = []
-    v4 = [solver.mkInteger(5)]
     slv = cvc5.Solver()
 
     # simple operator terms
@@ -901,15 +882,15 @@ def test_mk_term_from_op(solver):
         solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(1),
                       cvc5.Term(solver))
 
-    solver.mkTerm(opterm2, v4)
+    solver.mkTerm(opterm2, solver.mkInteger(5))
     with pytest.raises(RuntimeError):
-        solver.mkTerm(opterm2, v1)
+        solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2))
     with pytest.raises(RuntimeError):
-        solver.mkTerm(opterm2, v2)
+        solver.mkTerm(opterm2, solver.mkInteger(1), cvc5.Term(solver))
     with pytest.raises(RuntimeError):
-        solver.mkTerm(opterm2, v3)
+        solver.mkTerm(opterm2)
     with pytest.raises(RuntimeError):
-        slv.mkTerm(opterm2, v4)
+        slv.mkTerm(opterm2, solver.mkInteger(5))
 
 
 def test_mk_true(solver):
@@ -1828,23 +1809,23 @@ def test_check_sat_assuming2(solver):
     # Assertions
     assertions =\
         solver.mkTerm(Kind.And,\
-                      [solver.mkTerm(Kind.Leq, zero, f_x),  # 0 <= f(x)
+                      solver.mkTerm(Kind.Leq, zero, f_x),  # 0 <= f(x)
                        solver.mkTerm(Kind.Leq, zero, f_y),  # 0 <= f(y)
                        solver.mkTerm(Kind.Leq, summ, one),  # f(x) + f(y) <= 1
                        p_0.notTerm(),                        # not p(0)
                        p_f_y                                 # p(f(y))
-                      ])
+                      )
 
     solver.checkSatAssuming(solver.mkTrue())
     solver.assertFormula(assertions)
     solver.checkSatAssuming(solver.mkTerm(Kind.Distinct, x, y))
     solver.checkSatAssuming(
-        [solver.mkFalse(),
-         solver.mkTerm(Kind.Distinct, x, y)])
+        solver.mkFalse(),
+         solver.mkTerm(Kind.Distinct, x, y))
     with pytest.raises(RuntimeError):
         solver.checkSatAssuming(n)
     with pytest.raises(RuntimeError):
-        solver.checkSatAssuming([n, solver.mkTerm(Kind.Distinct, x, y)])
+        solver.checkSatAssuming(n, solver.mkTerm(Kind.Distinct, x, y))
     slv = cvc5.Solver()
     with pytest.raises(RuntimeError):
         slv.checkSatAssuming(solver.mkTrue())
@@ -1879,7 +1860,7 @@ def test_reset_assertions(solver):
     solver.push(4)
     slt = solver.mkTerm(Kind.BVSlt, srem, one)
     solver.resetAssertions()
-    solver.checkSatAssuming([slt, ule])
+    solver.checkSatAssuming(slt, ule)
 
 
 def test_mk_sygus_grammar(solver):
@@ -2603,9 +2584,9 @@ def test_tuple_project(solver):
 
 
 def test_get_data_type_arity(solver):
-  ctor1 = solver.mkDatatypeConstructorDecl("_x21");
-  ctor2 = solver.mkDatatypeConstructorDecl("_x31");
-  s3 = solver.declareDatatype("_x17", [ctor1, ctor2]);
+  ctor1 = solver.mkDatatypeConstructorDecl("_x21")
+  ctor2 = solver.mkDatatypeConstructorDecl("_x31")
+  s3 = solver.declareDatatype("_x17", ctor1, ctor2)
   assert s3.getDatatypeArity() == 0
 
 

diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
index 3f2ecf444f4b4426b44bc65da8d3e6ccaf93d7d9..c6168d17ff41874fd7f7bdb113e4854f80fe611e 100644 (file)
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -185,7 +185,7 @@ def test_is_tuple(solver):
 
 
 def test_is_record(solver):
-    rec_sort = solver.mkRecordSort([("asdf", solver.getRealSort())])
+    rec_sort = solver.mkRecordSort(("asdf", solver.getRealSort()))
     assert rec_sort.isRecord()
     Sort(solver).isRecord()
 
@@ -519,8 +519,8 @@ def test_get_datatype_arity(solver):
 
 def test_get_tuple_length(solver):
     tupleSort = solver.mkTupleSort(
-        [solver.getIntegerSort(),
-         solver.getIntegerSort()])
+        solver.getIntegerSort(),
+        solver.getIntegerSort())
     tupleSort.getTupleLength()
     bvSort = solver.mkBitVectorSort(32)
     with pytest.raises(RuntimeError):
@@ -529,8 +529,8 @@ def test_get_tuple_length(solver):
 
 def test_get_tuple_sorts(solver):
     tupleSort = solver.mkTupleSort(
-        [solver.getIntegerSort(),
-         solver.getIntegerSort()])
+        solver.getIntegerSort(),
+        solver.getIntegerSort())
     tupleSort.getTupleSorts()
     bvSort = solver.mkBitVectorSort(32)
     with pytest.raises(RuntimeError):

diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
index 75cac1375b3a91d7e52e6ced698644c5d509bac8..40514e17053e57eb9b59a071809edc3e56c68fb3 100644 (file)
--- a/test/unit/api/python/test_term.py
+++ b/test/unit/api/python/test_term.py
@@ -171,7 +171,7 @@ def test_get_op(solver):
     assert fx.hasOp()
     children = [c for c in fx]
     # testing rebuild from op and children
-    assert fx == solver.mkTerm(fx.getOp(), children)
+    assert fx == solver.mkTerm(fx.getOp(), *children)
 
     # Test Datatypes Ops
     sort = solver.mkParamSort("T")
@@ -205,7 +205,7 @@ def test_get_op(solver):
 
     # Test rebuilding
     children = [c for c in headTerm]
-    assert headTerm == solver.mkTerm(headTerm.getOp(), children)
+    assert headTerm == solver.mkTerm(headTerm.getOp(), *children)
 
 
 def test_has_get_symbol(solver):