From: Gereon Kremer Date: Fri, 1 Apr 2022 16:58:00 +0000 (+0200) Subject: Remove decorator from python API (#8505) X-Git-Tag: cvc5-1.0.0~67 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a7779de22d9cbc31a8a9fb9e52200d02a152a2bd;p=cvc5.git 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 49816ead6..d7c1ae19e 100644 --- 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 72b57d4e8..758e6ba2f 100644 --- 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 d787d14d9..bb03b1c08 100644 --- 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 3cf0d10a9..0fa8bc237 100644 --- 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 8098a56f3..2bf7604b0 100644 --- 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 618bd2069..c7711dd81 100644 --- 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 bfc139b1a..1197e0b00 100644 --- 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( 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 ( ) ) - :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( 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 ) :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 f41ebb16a..f85bdfc83 100644 --- 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 61d5a4ad0..6098fb6dc 100644 --- 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 6db53bb50..fb9e7913c 100644 --- 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 483243a9f..2fb978dbb 100644 --- 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 74dc04620..8ef6de932 100644 --- 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 3f2ecf444..c6168d17f 100644 --- 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 75cac1375..40514e170 100644 --- 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):