From 506a7b8c4a9e118b46d0417a1f060e0a9da8e647 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 1 Apr 2022 12:45:36 -0700 Subject: [PATCH] Python API: Do not rename enumerators. (#8507) Co-authored-by: Mathias Preiner Co-authored-by: mudathirmahgoub Co-authored-by: Gereon Kremer --- docs/api/python/base/quickstart.rst | 6 +- examples/api/python/bags.py | 50 +-- examples/api/python/bitvectors.py | 30 +- examples/api/python/bitvectors_and_arrays.py | 18 +- examples/api/python/combination.py | 20 +- examples/api/python/datatypes.py | 24 +- examples/api/python/extract.py | 12 +- examples/api/python/floating_point.py | 55 ++- examples/api/python/linear_arith.py | 16 +- examples/api/python/quickstart.py | 21 +- examples/api/python/relations.py | 52 +-- examples/api/python/sequences.py | 12 +- examples/api/python/sets.py | 36 +- examples/api/python/strings.py | 36 +- examples/api/python/sygus-fun.py | 28 +- examples/api/python/sygus-grammar.py | 19 +- examples/api/python/sygus-inv.py | 12 +- examples/api/python/transcendentals.py | 12 +- examples/api/python/utils.py | 2 +- src/api/python/genenums.py.in | 50 +-- test/api/python/issue4889.py | 6 +- test/api/python/issue5074.py | 8 +- test/api/python/issue6111.py | 10 +- test/api/python/proj-issue306.py | 6 +- test/api/python/reset_assertions.py | 6 +- test/api/python/sep_log_api.py | 20 +- test/unit/api/python/test_op.py | 97 ++--- test/unit/api/python/test_solver.py | 387 ++++++++++--------- test/unit/api/python/test_term.py | 167 ++++---- test/unit/api/python/test_to_python_obj.py | 15 +- 30 files changed, 632 insertions(+), 601 deletions(-) diff --git a/docs/api/python/base/quickstart.rst b/docs/api/python/base/quickstart.rst index e1c2993b5..d7ed7b79c 100644 --- a/docs/api/python/base/quickstart.rst +++ b/docs/api/python/base/quickstart.rst @@ -133,13 +133,13 @@ to the assertion command. .. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python - :lines: 135-139 + :lines: 135-140 Now, we check whether the revised assertion is satisfiable. .. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python - :lines: 142, 145-146 + :lines: 143, 146-147 This time the asserted formula is unsatisfiable: @@ -153,7 +153,7 @@ of the assertions that is already unsatisfiable. .. literalinclude:: ../../../../examples/api/python/quickstart.py :language: python - :lines: 150-152 + :lines: 151-153 This will print: diff --git a/examples/api/python/bags.py b/examples/api/python/bags.py index 9172a97f5..b0644534f 100644 --- a/examples/api/python/bags.py +++ b/examples/api/python/bags.py @@ -31,15 +31,16 @@ if __name__ == "__main__": C = slv.mkConst(bag, "C") x = slv.mkConst(slv.getStringSort(), "x") - intersectionAC = slv.mkTerm(Kind.BagInterMin, A, C) - intersectionBC = slv.mkTerm(Kind.BagInterMin, B, C) + intersectionAC = slv.mkTerm(Kind.BAG_INTER_MIN, A, C) + intersectionBC = slv.mkTerm(Kind.BAG_INTER_MIN, B, C) # union disjoint does not distribute over intersection - unionDisjointAB = slv.mkTerm(Kind.BagUnionDisjoint, A, B) - lhs = slv.mkTerm(Kind.BagInterMin, unionDisjointAB, C) - rhs = slv.mkTerm(Kind.BagUnionDisjoint, intersectionAC, intersectionBC) - guess = slv.mkTerm(Kind.Equal, lhs, rhs) - print("cvc5 reports: {} is {}".format(guess.notTerm(), slv.checkSatAssuming(guess.notTerm()))) + unionDisjointAB = slv.mkTerm(Kind.BAG_UNION_DISJOINT, A, B) + lhs = slv.mkTerm(Kind.BAG_INTER_MIN, unionDisjointAB, C) + rhs = slv.mkTerm(Kind.BAG_UNION_DISJOINT, intersectionAC, intersectionBC) + guess = slv.mkTerm(Kind.EQUAL, lhs, rhs) + print("cvc5 reports: {} is {}".format( + guess.notTerm(), slv.checkSatAssuming(guess.notTerm()))) print("{}: {}".format(A, slv.getValue(A))) print("{}: {}".format(B, slv.getValue(B))) @@ -48,16 +49,18 @@ if __name__ == "__main__": print("{}: {}".format(rhs, slv.getValue(rhs))) # union max distributes over intersection - unionMaxAB = slv.mkTerm(Kind.BagUnionMax, A, B) - lhs = slv.mkTerm(Kind.BagInterMin, unionMaxAB, C) - rhs = slv.mkTerm(Kind.BagUnionMax, intersectionAC, intersectionBC) - theorem = slv.mkTerm(Kind.Equal, lhs, rhs) - print("cvc5 reports: {} is {}.".format(theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm()))) + unionMaxAB = slv.mkTerm(Kind.BAG_UNION_MAX, A, B) + lhs = slv.mkTerm(Kind.BAG_INTER_MIN, unionMaxAB, C) + rhs = slv.mkTerm(Kind.BAG_UNION_MAX, intersectionAC, intersectionBC) + theorem = slv.mkTerm(Kind.EQUAL, lhs, rhs) + print("cvc5 reports: {} is {}.".format( + theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm()))) # Verify emptbag is a subbag of any bag emptybag = slv.mkEmptyBag(bag) - theorem = slv.mkTerm(Kind.BagSubbag, emptybag, A) - print("cvc5 reports: {} is {}.".format(theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm()))) + theorem = slv.mkTerm(Kind.BAG_SUBBAG, emptybag, A) + print("cvc5 reports: {} is {}.".format( + theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm()))) # find an element with multiplicity 4 in the disjoint union of # {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|} @@ -69,16 +72,17 @@ if __name__ == "__main__": b = slv.mkString("b") c = slv.mkString("c") - bag_a_2 = slv.mkTerm(Kind.BagMake, a, two) - bag_b_3 = slv.mkTerm(Kind.BagMake, b, three) - bag_b_1 = slv.mkTerm(Kind.BagMake, b, one) - bag_c_2 = slv.mkTerm(Kind.BagMake, c, two) - bag_a_2_b_3 = slv.mkTerm(Kind.BagUnionDisjoint, bag_a_2, bag_b_3) - bag_b_1_c_2 = slv.mkTerm(Kind.BagUnionDisjoint, bag_b_1, bag_c_2) - UnionDisjoint = slv.mkTerm(Kind.BagUnionDisjoint, bag_a_2_b_3, bag_b_1_c_2) + bag_a_2 = slv.mkTerm(Kind.BAG_MAKE, a, two) + bag_b_3 = slv.mkTerm(Kind.BAG_MAKE, b, three) + bag_b_1 = slv.mkTerm(Kind.BAG_MAKE, b, one) + bag_c_2 = slv.mkTerm(Kind.BAG_MAKE, c, two) + bag_a_2_b_3 = slv.mkTerm(Kind.BAG_UNION_DISJOINT, bag_a_2, bag_b_3) + bag_b_1_c_2 = slv.mkTerm(Kind.BAG_UNION_DISJOINT, bag_b_1, bag_c_2) + UnionDisjoint = slv.mkTerm( + Kind.BAG_UNION_DISJOINT, bag_a_2_b_3, bag_b_1_c_2) - count_x = slv.mkTerm(Kind.BagCount, x, UnionDisjoint) - e = slv.mkTerm(Kind.Equal, four, count_x) + count_x = slv.mkTerm(Kind.BAG_COUNT, x, UnionDisjoint) + e = slv.mkTerm(Kind.EQUAL, four, count_x) result = slv.checkSatAssuming(e) print("cvc5 reports: {} is {}.".format(e, result)) diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py index d7c1ae19e..57c4f2f1b 100644 --- a/examples/api/python/bitvectors.py +++ b/examples/api/python/bitvectors.py @@ -50,9 +50,9 @@ if __name__ == "__main__": b = slv.mkConst(bitvector32, "b") # First encode the assumption that x must be equal to a or b - x_eq_a = slv.mkTerm(Kind.Equal, x, a) - x_eq_b = slv.mkTerm(Kind.Equal, x, b) - assumption = slv.mkTerm(Kind.Or, x_eq_a, x_eq_b) + x_eq_a = slv.mkTerm(Kind.EQUAL, x, a) + x_eq_b = slv.mkTerm(Kind.EQUAL, x, b) + assumption = slv.mkTerm(Kind.OR, x_eq_a, x_eq_b) # Assert the assumption slv.assertFormula(assumption) @@ -65,8 +65,8 @@ if __name__ == "__main__": # Encoding code (0) # new_x = x == a ? b : a - ite = slv.mkTerm(Kind.Ite, x_eq_a, b, a) - assignment0 = slv.mkTerm(Kind.Equal, new_x, ite) + ite = slv.mkTerm(Kind.ITE, x_eq_a, b, a) + assignment0 = slv.mkTerm(Kind.EQUAL, new_x, ite) # Assert the encoding of code (0) print("Asserting {} to cvc5".format(assignment0)) @@ -76,13 +76,13 @@ if __name__ == "__main__": # Encoding code (1) # new_x_ = a xor b xor x - a_xor_b_xor_x = slv.mkTerm(Kind.BVXor, a, b, x) - assignment1 = slv.mkTerm(Kind.Equal, new_x_, a_xor_b_xor_x) + a_xor_b_xor_x = slv.mkTerm(Kind.BITVECTOR_XOR, a, b, x) + assignment1 = slv.mkTerm(Kind.EQUAL, new_x_, a_xor_b_xor_x) # Assert encoding to cvc5 in current context print("Asserting {} to cvc5".format(assignment1)) slv.assertFormula(assignment1) - new_x_eq_new_x_ = slv.mkTerm(Kind.Equal, new_x, new_x_) + new_x_eq_new_x_ = slv.mkTerm(Kind.EQUAL, new_x, new_x_) print("Checking sat assuming:", new_x_eq_new_x_.notTerm()) print("Expect UNSAT.") @@ -92,9 +92,9 @@ if __name__ == "__main__": # Encoding code (2) # new_x_ = a + b - x - a_plus_b = slv.mkTerm(Kind.BVAdd, a, b) - a_plus_b_minus_x = slv.mkTerm(Kind.BVSub, a_plus_b, x) - assignment2 = slv.mkTerm(Kind.Equal, new_x_, a_plus_b_minus_x) + a_plus_b = slv.mkTerm(Kind.BITVECTOR_ADD, a, b) + a_plus_b_minus_x = slv.mkTerm(Kind.BITVECTOR_SUB, a_plus_b, x) + assignment2 = slv.mkTerm(Kind.EQUAL, new_x_, a_plus_b_minus_x) # Assert encoding to cvc5 in current context print("Asserting {} to cvc5".format(assignment2)) @@ -105,17 +105,17 @@ if __name__ == "__main__": print("cvc5:", slv.checkSatAssuming(new_x_eq_new_x_.notTerm())) - x_neq_x = slv.mkTerm(Kind.Equal, x, x).notTerm() - query = slv.mkTerm(Kind.And, new_x_eq_new_x_, x_neq_x) + x_neq_x = slv.mkTerm(Kind.EQUAL, x, x).notTerm() + 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())) # Assert that a is odd - extract_op = slv.mkOp(Kind.BVExtract, 0, 0) + extract_op = slv.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0) lsb_of_a = slv.mkTerm(extract_op, a) print("Sort of {} is {}".format(lsb_of_a, lsb_of_a.getSort())) - a_odd = slv.mkTerm(Kind.Equal, lsb_of_a, slv.mkBitVector(1, 1)) + a_odd = slv.mkTerm(Kind.EQUAL, lsb_of_a, slv.mkBitVector(1, 1)) print("Assert", a_odd) print("Check satisifiability") slv.assertFormula(a_odd) diff --git a/examples/api/python/bitvectors_and_arrays.py b/examples/api/python/bitvectors_and_arrays.py index 758e6ba2f..f4121abc9 100644 --- a/examples/api/python/bitvectors_and_arrays.py +++ b/examples/api/python/bitvectors_and_arrays.py @@ -58,29 +58,31 @@ if __name__ == "__main__": constarr0 = slv.mkConstArray(arraySort, slv.mkBitVector(32, 0)) # Asserting that current_array[0] > 0 - current_array0 = slv.mkTerm(Kind.Select, current_array, zero) - current_array0_gt_0 = slv.mkTerm(Kind.BVSgt, + current_array0 = slv.mkTerm(Kind.SELECT, current_array, zero) + current_array0_gt_0 = slv.mkTerm(Kind.BITVECTOR_SGT, current_array0, slv.mkBitVector(32, 0)) slv.assertFormula(current_array0_gt_0) # Building the assertions in the loop unrolling index = slv.mkBitVector(index_size, 0) - old_current = slv.mkTerm(Kind.Select, current_array, index) + old_current = slv.mkTerm(Kind.SELECT, current_array, index) two = slv.mkBitVector(32, 2) assertions = [] for i in range(1, k): index = slv.mkBitVector(index_size, i) - new_current = slv.mkTerm(Kind.BVMult, two, old_current) + new_current = slv.mkTerm(Kind.BITVECTOR_MULT, two, old_current) # current[i] = 2*current[i-1] - current_array = slv.mkTerm(Kind.Store, current_array, index, new_current) + current_array = \ + slv.mkTerm(Kind.STORE, current_array, index, new_current) # current[i-1] < current[i] - current_slt_new_current = slv.mkTerm(Kind.BVSlt, old_current, new_current) + current_slt_new_current = \ + slv.mkTerm(Kind.BITVECTOR_SLT, old_current, new_current) assertions.append(current_slt_new_current) - old_current = slv.mkTerm(Kind.Select, current_array, index) + 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 bb03b1c08..7711d4aba 100644 --- a/examples/api/python/combination.py +++ b/examples/api/python/combination.py @@ -51,17 +51,17 @@ if __name__ == "__main__": one = slv.mkInteger(1) # Terms - f_x = slv.mkTerm(Kind.ApplyUf, f, x) - f_y = slv.mkTerm(Kind.ApplyUf, f, y) - sum_ = slv.mkTerm(Kind.Add, f_x, f_y) - p_0 = slv.mkTerm(Kind.ApplyUf, p, zero) - p_f_y = slv.mkTerm(Kind.ApplyUf, p, f_y) + f_x = slv.mkTerm(Kind.APPLY_UF, f, x) + f_y = slv.mkTerm(Kind.APPLY_UF, f, y) + sum_ = slv.mkTerm(Kind.ADD, f_x, f_y) + p_0 = slv.mkTerm(Kind.APPLY_UF, p, zero) + p_f_y = slv.mkTerm(Kind.APPLY_UF, p, f_y) # 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 + 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)) ) @@ -70,7 +70,7 @@ if __name__ == "__main__": print("Given the following assertions:", assertions, "\n") print("Prove x /= y is entailed.\ncvc5: ", - slv.checkSatAssuming(slv.mkTerm(Kind.Equal, x, y)), "\n") + slv.checkSatAssuming(slv.mkTerm(Kind.EQUAL, x, y)), "\n") print("Call checkSat to show that the assertions are satisfiable") print("cvc5:", slv.checkSat(), "\n") diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py index 0fa8bc237..23704fa7c 100644 --- a/examples/api/python/datatypes.py +++ b/examples/api/python/datatypes.py @@ -34,9 +34,11 @@ def test(slv, consListSort): # which is equivalent to consList["cons"].getConstructor(). Note that # "nil" is a constructor too - t = slv.mkTerm(Kind.ApplyConstructor, consList.getConstructorTerm("cons"), - slv.mkInteger(0), - slv.mkTerm(Kind.ApplyConstructor, consList.getConstructorTerm("nil"))) + t = slv.mkTerm( + Kind.APPLY_CONSTRUCTOR, consList.getConstructorTerm("cons"), + slv.mkInteger(0), + slv.mkTerm( + Kind.APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))) print("t is {}\nsort of cons is {}\n sort of nil is {}".format( t, @@ -49,7 +51,8 @@ def test(slv, consListSort): # consList["cons"]) in order to get the "head" selector symbol # to apply. - t2 = slv.mkTerm(Kind.ApplySelector, consList["cons"].getSelectorTerm("head"), t) + t2 = slv.mkTerm( + Kind.APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t) print("t2 is {}\nsimplify(t2) is {}\n\n".format(t2, slv.simplify(t2))) @@ -63,16 +66,16 @@ def test(slv, consListSort): # You can also define a tester term for constructor 'cons': (_ is cons) t_is_cons = slv.mkTerm( - Kind.ApplyTester, consList["cons"].getTesterTerm(), t) + Kind.APPLY_TESTER, consList["cons"].getTesterTerm(), t) print("t_is_cons is {}\n\n".format(t_is_cons)) slv.assertFormula(t_is_cons) # Updating t at 'head' with value 1 is defined as follows: - t_updated = slv.mkTerm(Kind.ApplyUpdater, + t_updated = slv.mkTerm(Kind.APPLY_UPDATER, consList["cons"]["head"].getUpdaterTerm(), t, slv.mkInteger(1)) print("t_updated is {}\n\n".format(t_updated)) - slv.assertFormula(slv.mkTerm(Kind.Distinct, t, t_updated)) + slv.assertFormula(slv.mkTerm(Kind.DISTINCT, t, t_updated)) # You can also define parameterized datatypes. # This example builds a simple parameterized list of sort T, with one @@ -93,11 +96,14 @@ def test(slv, consListSort): a = slv.mkConst(paramConsIntListSort, "a") print("term {} is of sort {}".format(a, a.getSort())) - head_a = slv.mkTerm(Kind.ApplySelector, paramConsList["cons"].getSelectorTerm("head"), a) + head_a = slv.mkTerm( + Kind.APPLY_SELECTOR, + paramConsList["cons"].getSelectorTerm("head"), + a) print("head_a is {} of sort {}".format(head_a, head_a.getSort())) print("sort of cons is", paramConsList.getConstructorTerm("cons").getSort()) - assertion = slv.mkTerm(Kind.Gt, head_a, slv.mkInteger(50)) + assertion = slv.mkTerm(Kind.GT, head_a, slv.mkInteger(50)) print("Assert", assertion) slv.assertFormula(assertion) print("Expect sat.") diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py index d653522b0..b4c0e8437 100644 --- a/examples/api/python/extract.py +++ b/examples/api/python/extract.py @@ -26,23 +26,23 @@ if __name__ == "__main__": x = slv.mkConst(bitvector32, "a") - ext_31_1 = slv.mkOp(Kind.BVExtract, 31, 1) + ext_31_1 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1) x_31_1 = slv.mkTerm(ext_31_1, x) - ext_30_0 = slv.mkOp(Kind.BVExtract, 30, 0) + ext_30_0 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 30, 0) x_30_0 = slv.mkTerm(ext_30_0, x) - ext_31_31 = slv.mkOp(Kind.BVExtract, 31, 31) + ext_31_31 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 31, 31) x_31_31 = slv.mkTerm(ext_31_31, x) - ext_0_0 = slv.mkOp(Kind.BVExtract, 0, 0) + ext_0_0 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0) x_0_0 = slv.mkTerm(ext_0_0, x) - eq = slv.mkTerm(Kind.Equal, x_31_1, x_30_0) + eq = slv.mkTerm(Kind.EQUAL, x_31_1, x_30_0) print("Asserting:", eq) slv.assertFormula(eq) - eq2 = slv.mkTerm(Kind.Equal, x_31_31, x_0_0) + eq2 = slv.mkTerm(Kind.EQUAL, x_31_31, x_0_0) print("Check sat assuming:", eq2.notTerm()) print("Expect UNSAT") print("cvc5:", slv.checkSatAssuming(eq2.notTerm())) diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index 768c88ba3..b04996463 100644 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -29,7 +29,7 @@ if __name__ == "__main__": fp32 = slv.mkFloatingPointSort(8, 24) # the standard rounding mode - rm = slv.mkRoundingMode(RoundingMode.RoundNearestTiesToEven) + rm = slv.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN) # create a few single-precision variables x = slv.mkConst(fp32, 'x') @@ -37,10 +37,13 @@ if __name__ == "__main__": z = slv.mkConst(fp32, 'z') # check floating-point arithmetic is commutative, i.e. x + y == y + x - commutative = slv.mkTerm(Kind.FPEq, slv.mkTerm(Kind.FPAdd, rm, x, y), slv.mkTerm(Kind.FPAdd, rm, y, x)) + commutative = slv.mkTerm( + Kind.FLOATINGPOINT_EQ, + slv.mkTerm(Kind.FLOATINGPOINT_ADD, rm, x, y), + slv.mkTerm(Kind.FLOATINGPOINT_ADD, rm, y, x)) slv.push() - slv.assertFormula(slv.mkTerm(Kind.Not, commutative)) + slv.assertFormula(slv.mkTerm(Kind.NOT, commutative)) print("Checking floating-point commutativity") print("Expect SAT (property does not hold for NaN and Infinities).") print("cvc5:", slv.checkSat()) @@ -48,10 +51,14 @@ if __name__ == "__main__": print("Model for y:", slv.getValue(y)) # disallow NaNs and Infinities - slv.assertFormula(slv.mkTerm(Kind.Not, slv.mkTerm(Kind.FPIsNan, x))) - slv.assertFormula(slv.mkTerm(Kind.Not, slv.mkTerm(Kind.FPIsInf, x))) - slv.assertFormula(slv.mkTerm(Kind.Not, slv.mkTerm(Kind.FPIsNan, y))) - slv.assertFormula(slv.mkTerm(Kind.Not, slv.mkTerm(Kind.FPIsInf, y))) + slv.assertFormula(slv.mkTerm( + Kind.NOT, slv.mkTerm(Kind.FLOATINGPOINT_IS_NAN, x))) + slv.assertFormula(slv.mkTerm( + Kind.NOT, slv.mkTerm(Kind.FLOATINGPOINT_IS_INF, x))) + slv.assertFormula(slv.mkTerm( + Kind.NOT, slv.mkTerm(Kind.FLOATINGPOINT_IS_NAN, y))) + slv.assertFormula(slv.mkTerm( + Kind.NOT, slv.mkTerm(Kind.FLOATINGPOINT_IS_INF, y))) print("Checking floating-point commutativity assuming x and y are not NaN or Infinity") print("Expect UNSAT.") @@ -70,15 +77,35 @@ if __name__ == "__main__": 24, slv.mkBitVector(32, "01000000010010001111010111000011", 2)) # 3.14 - bounds_x = slv.mkTerm(Kind.And, slv.mkTerm(Kind.FPLeq, a, x), slv.mkTerm(Kind.FPLeq, x, b)) - bounds_y = slv.mkTerm(Kind.And, slv.mkTerm(Kind.FPLeq, a, y), slv.mkTerm(Kind.FPLeq, y, b)) - bounds_z = slv.mkTerm(Kind.And, slv.mkTerm(Kind.FPLeq, a, z), slv.mkTerm(Kind.FPLeq, z, b)) - slv.assertFormula(slv.mkTerm(Kind.And, slv.mkTerm(Kind.And, bounds_x, bounds_y), bounds_z)) + bounds_x = slv.mkTerm( + Kind.AND, + slv.mkTerm(Kind.FLOATINGPOINT_LEQ, a, x), + slv.mkTerm(Kind.FLOATINGPOINT_LEQ, x, b)) + bounds_y = slv.mkTerm( + Kind.AND, + slv.mkTerm(Kind.FLOATINGPOINT_LEQ, a, y), + slv.mkTerm(Kind.FLOATINGPOINT_LEQ, y, b)) + bounds_z = slv.mkTerm( + Kind.AND, + slv.mkTerm(Kind.FLOATINGPOINT_LEQ, a, z), + slv.mkTerm(Kind.FLOATINGPOINT_LEQ, z, b)) + slv.assertFormula(slv.mkTerm( + Kind.AND, slv.mkTerm(Kind.AND, bounds_x, bounds_y), bounds_z)) # (x + y) + z == x + (y + z) - lhs = slv.mkTerm(Kind.FPAdd, rm, slv.mkTerm(Kind.FPAdd, rm, x, y), z) - rhs = slv.mkTerm(Kind.FPAdd, rm, x, slv.mkTerm(Kind.FPAdd, rm, y, z)) - associative = slv.mkTerm(Kind.Not, slv.mkTerm(Kind.FPEq, lhs, rhs)) + lhs = slv.mkTerm( + Kind.FLOATINGPOINT_ADD, + rm, + slv.mkTerm(Kind.FLOATINGPOINT_ADD, rm, x, y), + z) + rhs = slv.mkTerm( + Kind.FLOATINGPOINT_ADD, + rm, + x, + slv.mkTerm(Kind.FLOATINGPOINT_ADD, rm, y, z)) + associative = slv.mkTerm( + Kind.NOT, + slv.mkTerm(Kind.FLOATINGPOINT_EQ, lhs, rhs)) slv.assertFormula(associative) diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py index 4f01acb15..4be3d3ac1 100644 --- a/examples/api/python/linear_arith.py +++ b/examples/api/python/linear_arith.py @@ -40,21 +40,21 @@ if __name__ == "__main__": two_thirds = slv.mkReal(2, 3) # Terms - three_y = slv.mkTerm(Kind.Mult, three, y) - diff = slv.mkTerm(Kind.Sub, y, x) + three_y = slv.mkTerm(Kind.MULT, three, y) + diff = slv.mkTerm(Kind.SUB, y, x) # Formulas - x_geq_3y = slv.mkTerm(Kind.Geq, x, three_y) - x_leq_y = slv.mkTerm(Kind.Leq, x ,y) - neg2_lt_x = slv.mkTerm(Kind.Lt, neg2, x) + x_geq_3y = slv.mkTerm(Kind.GEQ, x, three_y) + x_leq_y = slv.mkTerm(Kind.LEQ, x ,y) + neg2_lt_x = slv.mkTerm(Kind.LT, neg2, x) - assertions = slv.mkTerm(Kind.And, x_geq_3y, x_leq_y, neg2_lt_x) + assertions = slv.mkTerm(Kind.AND, x_geq_3y, x_leq_y, neg2_lt_x) print("Given the assertions", assertions) slv.assertFormula(assertions) slv.push() - diff_leq_two_thirds = slv.mkTerm(Kind.Leq, diff, two_thirds) + diff_leq_two_thirds = slv.mkTerm(Kind.LEQ, diff, two_thirds) print("Prove that", diff_leq_two_thirds, "with cvc5") print("cvc5 should report UNSAT") print("Result from cvc5 is:", @@ -64,7 +64,7 @@ if __name__ == "__main__": print() slv.push() - diff_is_two_thirds = slv.mkTerm(Kind.Equal, diff, two_thirds) + diff_is_two_thirds = slv.mkTerm(Kind.EQUAL, diff, two_thirds) slv.assertFormula(diff_is_two_thirds) print("Show that the assertions are consistent with\n", diff_is_two_thirds, "with cvc5") print("cvc5 should report SAT") diff --git a/examples/api/python/quickstart.py b/examples/api/python/quickstart.py index dc5e36683..153ba5fa5 100644 --- a/examples/api/python/quickstart.py +++ b/examples/api/python/quickstart.py @@ -64,15 +64,15 @@ if __name__ == "__main__": one = solver.mkReal(1); # Next, we construct the term x + y - xPlusY = solver.mkTerm(Kind.Add, x, y); + xPlusY = solver.mkTerm(Kind.ADD, x, y); # Now we can define the constraints. # They use the operators +, <=, and <. # In the API, these are denoted by Plus, Leq, and Lt. - constraint1 = solver.mkTerm(Kind.Lt, zero, x); - constraint2 = solver.mkTerm(Kind.Lt, zero, y); - constraint3 = solver.mkTerm(Kind.Lt, xPlusY, one); - constraint4 = solver.mkTerm(Kind.Leq, x, y); + constraint1 = solver.mkTerm(Kind.LT, zero, x); + constraint2 = solver.mkTerm(Kind.LT, zero, y); + constraint3 = solver.mkTerm(Kind.LT, xPlusY, one); + constraint4 = solver.mkTerm(Kind.LEQ, x, y); # Now we assert the constraints to the solver. solver.assertFormula(constraint1); @@ -95,7 +95,7 @@ if __name__ == "__main__": # It is also possible to get values for compound terms, # even if those did not appear in the original formula. - xMinusY = solver.mkTerm(Kind.Sub, x, y); + xMinusY = solver.mkTerm(Kind.SUB, x, y); xMinusYVal = solver.getValue(xMinusY); # We can now obtain the values as python values @@ -132,11 +132,12 @@ if __name__ == "__main__": # Next, we assert the same assertions above with integers. # This time, we inline the construction of terms # to the assertion command. - solver.assertFormula(solver.mkTerm(Kind.Lt, solver.mkInteger(0), a)); - solver.assertFormula(solver.mkTerm(Kind.Lt, solver.mkInteger(0), b)); + solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a)); + solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b)); solver.assertFormula( - solver.mkTerm(Kind.Lt, solver.mkTerm(Kind.Add, a, b), solver.mkInteger(1))); - solver.assertFormula(solver.mkTerm(Kind.Leq, a, b)); + solver.mkTerm( + Kind.LT, solver.mkTerm(Kind.ADD, a, b), solver.mkInteger(1))); + solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b)); # We check whether the revised assertion is satisfiable. r2 = solver.checkSat(); diff --git a/examples/api/python/relations.py b/examples/api/python/relations.py index 2bf7604b0..96b51f939 100644 --- a/examples/api/python/relations.py +++ b/examples/api/python/relations.py @@ -70,58 +70,60 @@ if __name__ == "__main__": ancestor = solver.mkConst(relationArity2, "ancestor") descendant = solver.mkConst(relationArity2, "descendant") - isEmpty1 = solver.mkTerm(Kind.Equal, males, emptySetTerm) - isEmpty2 = solver.mkTerm(Kind.Equal, females, emptySetTerm) + isEmpty1 = solver.mkTerm(Kind.EQUAL, males, emptySetTerm) + isEmpty2 = solver.mkTerm(Kind.EQUAL, females, emptySetTerm) # (assert (= people (as set.universe (Set (Tuple Person))))) - peopleAreTheUniverse = solver.mkTerm(Kind.Equal, people, universeSet) + peopleAreTheUniverse = solver.mkTerm(Kind.EQUAL, people, universeSet) # (assert (not (= males (as set.empty (Set (Tuple Person)))))) - maleSetIsNotEmpty = solver.mkTerm(Kind.Not, isEmpty1) + maleSetIsNotEmpty = solver.mkTerm(Kind.NOT, isEmpty1) # (assert (not (= females (as set.empty (Set (Tuple Person)))))) - femaleSetIsNotEmpty = solver.mkTerm(Kind.Not, isEmpty2) + femaleSetIsNotEmpty = solver.mkTerm(Kind.NOT, isEmpty2) # (assert (= (set.inter males females) # (as set.empty (Set (Tuple Person))))) - malesFemalesIntersection = solver.mkTerm(Kind.SetInter, males, females) - malesAndFemalesAreDisjoint = solver.mkTerm(Kind.Equal, malesFemalesIntersection, emptySetTerm) + malesFemalesIntersection = solver.mkTerm(Kind.SET_INTER, males, females) + malesAndFemalesAreDisjoint = \ + solver.mkTerm(Kind.EQUAL, malesFemalesIntersection, emptySetTerm) # (assert (not (= father (as set.empty (Set (Tuple Person Person)))))) # (assert (not (= mother (as set.empty (Set (Tuple Person Person)))))) - isEmpty3 = solver.mkTerm(Kind.Equal, father, emptyRelationTerm) - isEmpty4 = solver.mkTerm(Kind.Equal, mother, emptyRelationTerm) - fatherIsNotEmpty = solver.mkTerm(Kind.Not, isEmpty3) - motherIsNotEmpty = solver.mkTerm(Kind.Not, isEmpty4) + isEmpty3 = solver.mkTerm(Kind.EQUAL, father, emptyRelationTerm) + isEmpty4 = solver.mkTerm(Kind.EQUAL, mother, emptyRelationTerm) + fatherIsNotEmpty = solver.mkTerm(Kind.NOT, isEmpty3) + motherIsNotEmpty = solver.mkTerm(Kind.NOT, isEmpty4) # fathers are males # (assert (set.subset (rel.join father people) males)) - fathers = solver.mkTerm(Kind.RelationJoin, father, people) - fathersAreMales = solver.mkTerm(Kind.SetSubset, fathers, males) + fathers = solver.mkTerm(Kind.RELATION_JOIN, father, people) + fathersAreMales = solver.mkTerm(Kind.SET_SUBSET, fathers, males) # mothers are females # (assert (set.subset (rel.join mother people) females)) - mothers = solver.mkTerm(Kind.RelationJoin, mother, people) - mothersAreFemales = solver.mkTerm(Kind.SetSubset, mothers, females) + mothers = solver.mkTerm(Kind.RELATION_JOIN, mother, people) + mothersAreFemales = solver.mkTerm(Kind.SET_SUBSET, mothers, females) # (assert (= parent (set.union father mother))) - unionFatherMother = solver.mkTerm(Kind.SetUnion, father, mother) - parentIsFatherOrMother = solver.mkTerm(Kind.Equal, parent, unionFatherMother) + unionFatherMother = solver.mkTerm(Kind.SET_UNION, father, mother) + parentIsFatherOrMother = \ + solver.mkTerm(Kind.EQUAL, parent, unionFatherMother) # (assert (= ancestor (rel.tclosure parent))) - transitiveClosure = solver.mkTerm(Kind.RelationTclosure, parent) - ancestorFormula = solver.mkTerm(Kind.Equal, ancestor, transitiveClosure) + transitiveClosure = solver.mkTerm(Kind.RELATION_TCLOSURE, parent) + ancestorFormula = solver.mkTerm(Kind.EQUAL, ancestor, transitiveClosure) # (assert (= descendant (rel.transpose ancestor))) - transpose = solver.mkTerm(Kind.RelationTranspose, ancestor) - descendantFormula = solver.mkTerm(Kind.Equal, descendant, transpose) + transpose = solver.mkTerm(Kind.RELATION_TRANSPOSE, ancestor) + descendantFormula = solver.mkTerm(Kind.EQUAL, descendant, transpose) # (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor)))) x = solver.mkVar(personSort, "x") xxTuple = solver.mkTuple([personSort, personSort], [x, x]) - member = solver.mkTerm(Kind.SetMember, xxTuple, ancestor) - notMember = solver.mkTerm(Kind.Not, member) + member = solver.mkTerm(Kind.SET_MEMBER, xxTuple, ancestor) + notMember = solver.mkTerm(Kind.NOT, member) - quantifiedVariables = solver.mkTerm(Kind.VariableList, x) - noSelfAncestor = solver.mkTerm(Kind.Forall, quantifiedVariables, notMember) + quantifiedVariables = solver.mkTerm(Kind.VARIABLE_LIST, x) + noSelfAncestor = solver.mkTerm(Kind.FORALL, quantifiedVariables, notMember) # formulas solver.assertFormula(peopleAreTheUniverse) diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py index bb41e65b2..e68970a38 100644 --- a/examples/api/python/sequences.py +++ b/examples/api/python/sequences.py @@ -39,18 +39,18 @@ if __name__ == "__main__": # Empty sequence empty = slv.mkEmptySequence(slv.getIntegerSort()) # Sequence concatenation: x.y.empty - concat = slv.mkTerm(Kind.SeqConcat, x, y, empty) + concat = slv.mkTerm(Kind.SEQ_CONCAT, x, y, empty) # Sequence length: |x.y.empty| - concat_len = slv.mkTerm(Kind.SeqLength, concat) + concat_len = slv.mkTerm(Kind.SEQ_LENGTH, concat) # |x.y.empty| > 1 - formula1 = slv.mkTerm(Kind.Gt, concat_len, slv.mkInteger(1)) + formula1 = slv.mkTerm(Kind.GT, concat_len, slv.mkInteger(1)) # Sequence unit: seq(1) - unit = slv.mkTerm(Kind.SeqUnit, slv.mkInteger(1)) + unit = slv.mkTerm(Kind.SEQ_UNIT, slv.mkInteger(1)) # x = seq(1) - formula2 = slv.mkTerm(Kind.Equal, x, unit) + formula2 = slv.mkTerm(Kind.EQUAL, x, unit) # Make a query - q = slv.mkTerm(Kind.And, formula1, formula2) + q = slv.mkTerm(Kind.AND, formula1, formula2) # Check satisfiability result = slv.checkSatAssuming(q) diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index ebc856d30..a4b7a3316 100644 --- a/examples/api/python/sets.py +++ b/examples/api/python/sets.py @@ -39,27 +39,27 @@ if __name__ == "__main__": B = slv.mkConst(set_, "B") C = slv.mkConst(set_, "C") - unionAB = slv.mkTerm(Kind.SetUnion, A, B) - lhs = slv.mkTerm(Kind.SetInter, unionAB, C) + unionAB = slv.mkTerm(Kind.SET_UNION, A, B) + lhs = slv.mkTerm(Kind.SET_INTER, unionAB, C) - intersectionAC = slv.mkTerm(Kind.SetInter, A, C) - intersectionBC = slv.mkTerm(Kind.SetInter, B, C) - rhs = slv.mkTerm(Kind.SetUnion, intersectionAC, intersectionBC) + intersectionAC = slv.mkTerm(Kind.SET_INTER, A, C) + intersectionBC = slv.mkTerm(Kind.SET_INTER, B, C) + rhs = slv.mkTerm(Kind.SET_UNION, intersectionAC, intersectionBC) - theorem = slv.mkTerm(Kind.Equal, lhs, rhs) + theorem = slv.mkTerm(Kind.EQUAL, lhs, rhs) - print("cvc5 reports: {} is {}".format(theorem, - slv.checkSatAssuming(theorem.notTerm()))) + print("cvc5 reports: {} is {}".format( + theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm()))) # Verify emptset is a subset of any set A = slv.mkConst(set_, "A") emptyset = slv.mkEmptySet(set_) - theorem = slv.mkTerm(Kind.SetSubset, emptyset, A) + theorem = slv.mkTerm(Kind.SET_SUBSET, emptyset, A) - print("cvc5 reports: {} is {}".format(theorem, - slv.checkSatAssuming(theorem.notTerm()))) + print("cvc5 reports: {} is {}".format( + theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm()))) # Find me an element in 1, 2 intersection 2, 3, if there is one. @@ -67,16 +67,16 @@ if __name__ == "__main__": two = slv.mkInteger(2) three = slv.mkInteger(3) - singleton_one = slv.mkTerm(Kind.SetSingleton, one) - singleton_two = slv.mkTerm(Kind.SetSingleton, two) - singleton_three = slv.mkTerm(Kind.SetSingleton, three) - one_two = slv.mkTerm(Kind.SetUnion, singleton_one, singleton_two) - two_three = slv.mkTerm(Kind.SetUnion, singleton_two, singleton_three) - intersection = slv.mkTerm(Kind.SetInter, one_two, two_three) + singleton_one = slv.mkTerm(Kind.SET_SINGLETON, one) + singleton_two = slv.mkTerm(Kind.SET_SINGLETON, two) + singleton_three = slv.mkTerm(Kind.SET_SINGLETON, three) + one_two = slv.mkTerm(Kind.SET_UNION, singleton_one, singleton_two) + two_three = slv.mkTerm(Kind.SET_UNION, singleton_two, singleton_three) + intersection = slv.mkTerm(Kind.SET_INTER, one_two, two_three) x = slv.mkConst(integer, "x") - e = slv.mkTerm(Kind.SetMember, x, intersection) + e = slv.mkTerm(Kind.SET_MEMBER, x, intersection) result = slv.checkSatAssuming(e) diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py index 30b3fdf7c..798b28453 100644 --- a/examples/api/python/strings.py +++ b/examples/api/python/strings.py @@ -43,38 +43,42 @@ if __name__ == "__main__": z = slv.mkConst(string, "z") # String concatenation: x.ab.y - lhs = slv.mkTerm(Kind.StringConcat, x, ab, y) + lhs = slv.mkTerm(Kind.STRING_CONCAT, x, ab, y) # String concatenation: abc.z - rhs = slv.mkTerm(Kind.StringConcat, abc, z) + rhs = slv.mkTerm(Kind.STRING_CONCAT, abc, z) # x.ab.y = abc.z - formula1 = slv.mkTerm(Kind.Equal, lhs, rhs) + formula1 = slv.mkTerm(Kind.EQUAL, lhs, rhs) # Length of y: |y| - leny = slv.mkTerm(Kind.StringLength, y) + leny = slv.mkTerm(Kind.STRING_LENGTH, y) # |y| >= 0 - formula2 = slv.mkTerm(Kind.Geq, leny, slv.mkInteger(0)) + formula2 = slv.mkTerm(Kind.GEQ, leny, slv.mkInteger(0)) # Regular expression: (ab[c-e]*f)|g|h - r = slv.mkTerm(Kind.RegexpUnion, - slv.mkTerm(Kind.RegexpConcat, - slv.mkTerm(Kind.StringToRegexp, slv.mkString("ab")), - slv.mkTerm(Kind.RegexpStar, - slv.mkTerm(Kind.RegexpRange, slv.mkString("c"), slv.mkString("e"))), - slv.mkTerm(Kind.StringToRegexp, slv.mkString("f"))), - slv.mkTerm(Kind.StringToRegexp, slv.mkString("g")), - slv.mkTerm(Kind.StringToRegexp, slv.mkString("h"))) + r = slv.mkTerm(Kind.REGEXP_UNION, + slv.mkTerm(Kind.REGEXP_CONCAT, + slv.mkTerm(Kind.STRING_TO_REGEXP, + slv.mkString("ab")), + slv.mkTerm(Kind.REGEXP_STAR, + slv.mkTerm(Kind.REGEXP_RANGE, + slv.mkString("c"), + slv.mkString("e"))), + slv.mkTerm(Kind.STRING_TO_REGEXP, + slv.mkString("f"))), + slv.mkTerm(Kind.STRING_TO_REGEXP, slv.mkString("g")), + slv.mkTerm(Kind.STRING_TO_REGEXP, slv.mkString("h"))) # String variables s1 = slv.mkConst(string, "s1") s2 = slv.mkConst(string, "s2") # String concatenation: s1.s2 - s = slv.mkTerm(Kind.StringConcat, s1, s2) + s = slv.mkTerm(Kind.STRING_CONCAT, s1, s2) # s1.s2 in (ab[c-e]*f)|g|h - formula3 = slv.mkTerm(Kind.StringInRegexp, s, r) + formula3 = slv.mkTerm(Kind.STRING_IN_REGEXP, s, r) # Make a query - q = slv.mkTerm(Kind.And, + q = slv.mkTerm(Kind.AND, formula1, formula2, formula3) diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py index 990307041..9781ddb67 100644 --- a/examples/api/python/sygus-fun.py +++ b/examples/api/python/sygus-fun.py @@ -45,13 +45,13 @@ if __name__ == "__main__": zero = slv.mkInteger(0) one = slv.mkInteger(1) - plus = slv.mkTerm(Kind.Add, start, start) - minus = slv.mkTerm(Kind.Sub, start, start) - ite = slv.mkTerm(Kind.Ite, start_bool, start, start) + plus = slv.mkTerm(Kind.ADD, start, start) + minus = slv.mkTerm(Kind.SUB, start, start) + ite = slv.mkTerm(Kind.ITE, start_bool, start, start) - And = slv.mkTerm(Kind.And, start_bool, start_bool) - Not = slv.mkTerm(Kind.Not, start_bool) - leq = slv.mkTerm(Kind.Leq, start, start) + And = slv.mkTerm(Kind.AND, start_bool, start_bool) + Not = slv.mkTerm(Kind.NOT, start_bool) + leq = slv.mkTerm(Kind.LEQ, start, start) # create the grammar object g = slv.mkSygusGrammar([x, y], [start, start_bool]) @@ -69,25 +69,29 @@ if __name__ == "__main__": varX = slv.declareSygusVar("x", integer) varY = slv.declareSygusVar("y", integer) - max_x_y = slv.mkTerm(Kind.ApplyUf, max, varX, varY) - min_x_y = slv.mkTerm(Kind.ApplyUf, min, varX, varY) + max_x_y = slv.mkTerm(Kind.APPLY_UF, max, varX, varY) + min_x_y = slv.mkTerm(Kind.APPLY_UF, min, varX, varY) # add semantic constraints # (constraint (>= (max x y) x)) - slv.addSygusConstraint(slv.mkTerm(Kind.Geq, max_x_y, varX)) + slv.addSygusConstraint(slv.mkTerm(Kind.GEQ, max_x_y, varX)) # (constraint (>= (max x y) y)) - slv.addSygusConstraint(slv.mkTerm(Kind.Geq, max_x_y, varY)) + slv.addSygusConstraint(slv.mkTerm(Kind.GEQ, max_x_y, varY)) # (constraint (or (= x (max x y)) # (= y (max x y)))) slv.addSygusConstraint(slv.mkTerm( - Kind.Or, slv.mkTerm(Kind.Equal, max_x_y, varX), slv.mkTerm(Kind.Equal, max_x_y, varY))) + Kind.OR, + slv.mkTerm(Kind.EQUAL, max_x_y, varX), + slv.mkTerm(Kind.EQUAL, max_x_y, varY))) # (constraint (= (+ (max x y) (min x y)) # (+ x y))) slv.addSygusConstraint(slv.mkTerm( - Kind.Equal, slv.mkTerm(Kind.Add, max_x_y, min_x_y), slv.mkTerm(Kind.Add, varX, varY))) + Kind.EQUAL, + slv.mkTerm(Kind.ADD, max_x_y, min_x_y), + slv.mkTerm(Kind.ADD, varX, varY))) # print solutions if available if (slv.checkSynth().hasSolution()): diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py index c7711dd81..c70b0d9c8 100644 --- a/examples/api/python/sygus-grammar.py +++ b/examples/api/python/sygus-grammar.py @@ -41,8 +41,8 @@ if __name__ == "__main__": # define the rules zero = slv.mkInteger(0) - neg_x = slv.mkTerm(Kind.Neg, x) - plus = slv.mkTerm(Kind.Add, x, start) + neg_x = slv.mkTerm(Kind.NEG, x) + plus = slv.mkTerm(Kind.ADD, x, start) # create the grammar object g1 = slv.mkSygusGrammar({x}, {start}) @@ -71,14 +71,19 @@ if __name__ == "__main__": # declare universal variables. varX = slv.declareSygusVar("x", integer) - id1_x = slv.mkTerm(Kind.ApplyUf, id1, varX) - id2_x = slv.mkTerm(Kind.ApplyUf, id2, varX) - id3_x = slv.mkTerm(Kind.ApplyUf, id3, varX) - id4_x = slv.mkTerm(Kind.ApplyUf, id4, varX) + id1_x = slv.mkTerm(Kind.APPLY_UF, id1, varX) + id2_x = slv.mkTerm(Kind.APPLY_UF, id2, varX) + id3_x = slv.mkTerm(Kind.APPLY_UF, id3, varX) + id4_x = slv.mkTerm(Kind.APPLY_UF, id4, varX) # 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/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py index 0b96e9ccd..8d9e35b93 100644 --- a/examples/api/python/sygus-inv.py +++ b/examples/api/python/sygus-inv.py @@ -42,15 +42,15 @@ if __name__ == "__main__": xp = slv.mkVar(integer, "xp") # (ite (< x 10) (= xp (+ x 1)) (= xp x)) - ite = slv.mkTerm(Kind.Ite, - slv.mkTerm(Kind.Lt, x, ten), - slv.mkTerm(Kind.Equal, xp, slv.mkTerm(Kind.Add, x, one)), - slv.mkTerm(Kind.Equal, xp, x)) + ite = slv.mkTerm(Kind.ITE, + slv.mkTerm(Kind.LT, x, ten), + slv.mkTerm(Kind.EQUAL, xp, slv.mkTerm(Kind.ADD, x, one)), + slv.mkTerm(Kind.EQUAL, xp, x)) # define the pre-conditions, transition relations, and post-conditions - pre_f = slv.defineFun("pre-f", [x], boolean, slv.mkTerm(Kind.Equal, x, zero)) + pre_f = slv.defineFun("pre-f", [x], boolean, slv.mkTerm(Kind.EQUAL, x, zero)) trans_f = slv.defineFun("trans-f", [x, xp], boolean, ite) - post_f = slv.defineFun("post-f", [x], boolean, slv.mkTerm(Kind.Leq, x, ten)) + post_f = slv.defineFun("post-f", [x], boolean, slv.mkTerm(Kind.LEQ, x, ten)) # declare the invariant-to-synthesize inv_f = slv.synthInv("inv-f", {x}) diff --git a/examples/api/python/transcendentals.py b/examples/api/python/transcendentals.py index 2adb9a66c..495c77a61 100644 --- a/examples/api/python/transcendentals.py +++ b/examples/api/python/transcendentals.py @@ -30,14 +30,14 @@ if __name__ == "__main__": # Helper terms two = slv.mkReal(2) pi = slv.mkPi() - twopi = slv.mkTerm(Kind.Mult, two, pi) - ysq = slv.mkTerm(Kind.Mult, y, y) - sinx = slv.mkTerm(Kind.Sine, x) + twopi = slv.mkTerm(Kind.MULT, two, pi) + ysq = slv.mkTerm(Kind.MULT, y, y) + sinx = slv.mkTerm(Kind.SINE, x) # Formulas - x_gt_pi = slv.mkTerm(Kind.Gt, x, pi) - x_lt_tpi = slv.mkTerm(Kind.Lt, x, twopi) - ysq_lt_sinx = slv.mkTerm(Kind.Lt, ysq, sinx) + x_gt_pi = slv.mkTerm(Kind.GT, x, pi) + x_lt_tpi = slv.mkTerm(Kind.LT, x, twopi) + ysq_lt_sinx = slv.mkTerm(Kind.LT, ysq, sinx) slv.assertFormula(x_gt_pi) slv.assertFormula(x_lt_tpi) diff --git a/examples/api/python/utils.py b/examples/api/python/utils.py index 765327eb4..cdae5e50b 100644 --- a/examples/api/python/utils.py +++ b/examples/api/python/utils.py @@ -47,7 +47,7 @@ def print_synth_solutions(terms, sols): for i in range(0, len(terms)): params = [] body = sols[i] - if sols[i].getKind() == Kind.Lambda: + if sols[i].getKind() == Kind.LAMBDA: params += sols[i][0] body = sols[i][1] result += " " + define_fun_to_string(terms[i], params, body) + "\n" diff --git a/src/api/python/genenums.py.in b/src/api/python/genenums.py.in index abfce6a25..a8d20d7c3 100644 --- a/src/api/python/genenums.py.in +++ b/src/api/python/genenums.py.in @@ -62,47 +62,6 @@ class {enum}(Enum): ENUMS_ATTR_TEMPLATE = r''' {name}=c_{enum}.{cpp_name}, """{doc}""" ''' -# Format Kind Names -# special cases for format_name -_IS = '_IS' -# replacements after some preprocessing -replacements = {'Bitvector': 'BV', 'Floatingpoint': 'FP'} - - -def format_name(name): - ''' - In the Python API, each Kind name is reformatted for easier use - - The naming scheme is: - 1. capitalize the first letter of each word (delimited by underscores) - 2. make the rest of the letters lowercase - 3. replace Floatingpoint with FP - 4. replace Bitvector with BV - - There is one exception: - FLOATINGPOINT_IS_NAN --> FPIsNan - - For every "_IS" in the name, there's an underscore added before step 1, - so that the word after "Is" is capitalized - - Examples: - BITVECTOR_ADD --> BVAdd - APPLY_SELECTOR --> ApplySelector - FLOATINGPOINT_IS_NAN --> FPIsNan - SET_MINUS --> Setminus - - See the generated .pxi file for an explicit mapping - ''' - name = name.replace(_IS, _IS + US) - words = [w.capitalize() for w in name.lower().split(US)] - name = "".join(words) - - for og, new in replacements.items(): - name = name.replace(og, new) - - return name - - comment_repls = { '`Solver::([a-zA-Z]+)\(([^)]*)\)[^`]*`': ':py:meth:`pycvc5.Solver.\\1`', } @@ -118,13 +77,6 @@ def gen_pxd(parser: EnumParser, file_prefix, header): with open(file_prefix + ".pxd", "w") as f: for namespace in parser.namespaces: for enum in namespace.enums: - # include the format_name docstring in the generated file - # could be helpful for users to see the formatting rules - for line in format_name.__doc__.split(NL): - f.write(PYCOMMENT) - if not line.isspace(): - f.write(line) - f.write(NL) f.write( ENUMS_PXD_TOP_TEMPLATE.format(header=header[len(SOURCE_DIR) + 1:], @@ -144,7 +96,7 @@ def gen_pxi(parser: EnumParser, file_prefix): for name, value in enum.enumerators.items(): doc = reformat_comment(enum.enumerators_doc.get(name, '')) f.write( - ENUMS_ATTR_TEMPLATE.format(name=format_name(name), + ENUMS_ATTR_TEMPLATE.format(name=name, enum=enum.name, cpp_name=name, doc=doc)) diff --git a/test/api/python/issue4889.py b/test/api/python/issue4889.py index 067c7a66e..929739ab0 100644 --- a/test/api/python/issue4889.py +++ b/test/api/python/issue4889.py @@ -25,7 +25,7 @@ sort_bool = slv.getBooleanSort() const0 = slv.mkConst(sort_fp32, "_c0") const1 = slv.mkConst(sort_fp32, "_c2") const2 = slv.mkConst(sort_bool, "_c4") -ite = slv.mkTerm(Kind.Ite, const2, const1, const0) -rem = slv.mkTerm(Kind.FPRem, ite, const1) -isnan = slv.mkTerm(Kind.FPIsNan, rem) +ite = slv.mkTerm(Kind.ITE, const2, const1, const0) +rem = slv.mkTerm(Kind.FLOATINGPOINT_REM, ite, const1) +isnan = slv.mkTerm(Kind.FLOATINGPOINT_IS_NAN, rem) slv.checkSatAssuming(isnan) diff --git a/test/api/python/issue5074.py b/test/api/python/issue5074.py index f85bdfc83..5dd3f01a6 100644 --- a/test/api/python/issue5074.py +++ b/test/api/python/issue5074.py @@ -18,8 +18,8 @@ from cvc5 import Kind 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) +t6 = slv.mkTerm(Kind.STRING_FROM_CODE, c1) +t12 = slv.mkTerm(Kind.STRING_TO_REGEXP, t6) +t14 = slv.mkTerm(Kind.STRING_REPLACE_RE, t6, t12, t6) +t16 = slv.mkTerm(Kind.STRING_CONTAINS, t14, t14) slv.checkSatAssuming(t16.notTerm()) diff --git a/test/api/python/issue6111.py b/test/api/python/issue6111.py index 6098fb6dc..146a403a3 100644 --- a/test/api/python/issue6111.py +++ b/test/api/python/issue6111.py @@ -22,7 +22,7 @@ bvsort12979 = solver.mkBitVectorSort(12979) input2_1 = solver.mkConst(bvsort12979, "intpu2_1") zero = solver.mkBitVector(bvsort12979.getBitVectorSize(), "0", 10) -bvult_res = solver.mkTerm(Kind.BVUlt, zero, input2_1) +bvult_res = solver.mkTerm(Kind.BITVECTOR_ULT, zero, input2_1) solver.assertFormula(bvult_res) bvsort4 = solver.mkBitVectorSort(4) @@ -33,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.BITVECTOR_EXTRACT, 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.BITVECTOR_EXTRACT, 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 fb9e7913c..9487ff3b0 100644 --- a/test/api/python/proj-issue306.py +++ b/test/api/python/proj-issue306.py @@ -24,8 +24,8 @@ t1 = slv.mkConst(s3, "_x0") t3 = slv.mkConst(s1, "_x2") t11 = slv.mkString("") t14 = slv.mkConst(s3, "_x11") -t42 = slv.mkTerm(Kind.Ite, t3, t14, t1) -t58 = slv.mkTerm(Kind.StringLeq, t14, t11) -t95 = slv.mkTerm(Kind.Equal, t14, t42) +t42 = slv.mkTerm(Kind.ITE, t3, t14, t1) +t58 = slv.mkTerm(Kind.STRING_LEQ, t14, t11) +t95 = slv.mkTerm(Kind.EQUAL, t14, t42) slv.assertFormula(t95) slv.checkSatAssuming(t58) diff --git a/test/api/python/reset_assertions.py b/test/api/python/reset_assertions.py index 02e611f18..8883ea798 100644 --- a/test/api/python/reset_assertions.py +++ b/test/api/python/reset_assertions.py @@ -27,7 +27,7 @@ slv.setOption("incremental", "true") real = slv.getRealSort() x = slv.mkConst(real, "x") four = slv.mkInteger(4) -xEqFour = slv.mkTerm(Kind.Equal, x, four) +xEqFour = slv.mkTerm(Kind.EQUAL, x, four) slv.assertFormula(xEqFour) print(slv.checkSat()) @@ -37,8 +37,8 @@ elementType = slv.getIntegerSort() indexType = slv.getIntegerSort() arrayType = slv.mkArraySort(indexType, elementType) array = slv.mkConst(arrayType, "array") -arrayAtFour = slv.mkTerm(Kind.Select, array, four) +arrayAtFour = slv.mkTerm(Kind.SELECT, array, four) ten = slv.mkInteger(10) -arrayAtFour_eq_ten = slv.mkTerm(Kind.Equal, arrayAtFour, ten) +arrayAtFour_eq_ten = slv.mkTerm(Kind.EQUAL, arrayAtFour, ten) slv.assertFormula(arrayAtFour_eq_ten) print(slv.checkSat()) diff --git a/test/api/python/sep_log_api.py b/test/api/python/sep_log_api.py index 830b5ef76..27d5eb41c 100644 --- a/test/api/python/sep_log_api.py +++ b/test/api/python/sep_log_api.py @@ -43,7 +43,7 @@ def validate_exception(): y = slv.mkConst(integer, "y") # y > x - y_gt_x = slv.mkTerm(Kind.Gt, y, x) + y_gt_x = slv.mkTerm(Kind.GT, y, x) # assert it slv.assertFormula(y_gt_x) @@ -124,18 +124,18 @@ def validate_getters(): p2 = slv.mkConst(integer, "p2") # Constraints on x and y - x_equal_const = slv.mkTerm(Kind.Equal, x, random_constant) - y_gt_x = slv.mkTerm(Kind.Gt, y, x) + x_equal_const = slv.mkTerm(Kind.EQUAL, x, random_constant) + y_gt_x = slv.mkTerm(Kind.GT, y, x) # Points-to expressions - p1_to_x = slv.mkTerm(Kind.SepPto, p1, x) - p2_to_y = slv.mkTerm(Kind.SepPto, p2, y) + p1_to_x = slv.mkTerm(Kind.SEP_PTO, p1, x) + p2_to_y = slv.mkTerm(Kind.SEP_PTO, p2, y) # Heap -- the points-to have to be "starred"! - heap = slv.mkTerm(Kind.SepStar, p1_to_x, p2_to_y) + heap = slv.mkTerm(Kind.SEP_STAR, p1_to_x, p2_to_y) # Constain "nil" to be something random - fix_nil = slv.mkTerm(Kind.Equal, nil, expr_nil_val) + fix_nil = slv.mkTerm(Kind.EQUAL, nil, expr_nil_val) # Add it all to the solver! slv.assertFormula(x_equal_const) @@ -157,11 +157,11 @@ def validate_getters(): nil_expr = slv.getValueSepNil() # If the heap is not a separating conjunction, bail-out - if (heap_expr.getKind() != Kind.SepStar): + if (heap_expr.getKind() != Kind.SEP_STAR): return False # If nil is not a direct equality, bail-out - if (nil_expr.getKind() != Kind.Equal): + if (nil_expr.getKind() != Kind.EQUAL): return False # Obtain the values for our "pointers" @@ -175,7 +175,7 @@ def validate_getters(): # Walk all the children for child in heap_expr: # If we don't have a PTO operator, bail-out - if (child.getKind() != Kind.SepPto): + if (child.getKind() != Kind.SEP_PTO): return False # Find both sides of the PTO operator diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py index c174886c4..710f93ff4 100644 --- a/test/unit/api/python/test_op.py +++ b/test/unit/api/python/test_op.py @@ -28,40 +28,40 @@ def solver(): def test_get_kind(solver): - x = solver.mkOp(Kind.BVExtract, 31, 1) + x = solver.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1) x.getKind() def test_is_null(solver): x = Op(solver) assert x.isNull() - x = solver.mkOp(Kind.BVExtract, 31, 1) + x = solver.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1) assert not x.isNull() def test_op_from_kind(solver): - solver.mkOp(Kind.Add) + solver.mkOp(Kind.ADD) with pytest.raises(RuntimeError): - solver.mkOp(Kind.BVExtract) + solver.mkOp(Kind.BITVECTOR_EXTRACT) def test_get_num_indices(solver): # Operators with 0 indices - plus = solver.mkOp(Kind.Add) + plus = solver.mkOp(Kind.ADD) assert 0 == plus.getNumIndices() # Operators with 1 index - divisible = solver.mkOp(Kind.Divisible, 4) - bitvector_repeat = solver.mkOp(Kind.BVRepeat, 5) - bitvector_zero_extend = solver.mkOp(Kind.BVZeroExtend, 6) - bitvector_sign_extend = solver.mkOp(Kind.BVSignExtend, 7) - bitvector_rotate_left = solver.mkOp(Kind.BVRotateLeft, 8) - bitvector_rotate_right = solver.mkOp(Kind.BVRotateRight, 9) - int_to_bitvector = solver.mkOp(Kind.IntToBV, 10) - iand = solver.mkOp(Kind.Iand, 3) - floatingpoint_to_ubv = solver.mkOp(Kind.FPToUbv, 11) - floatingopint_to_sbv = solver.mkOp(Kind.FPToSbv, 13) + divisible = solver.mkOp(Kind.DIVISIBLE, 4) + bitvector_repeat = solver.mkOp(Kind.BITVECTOR_REPEAT, 5) + bitvector_zero_extend = solver.mkOp(Kind.BITVECTOR_ZERO_EXTEND, 6) + bitvector_sign_extend = solver.mkOp(Kind.BITVECTOR_SIGN_EXTEND, 7) + bitvector_rotate_left = solver.mkOp(Kind.BITVECTOR_ROTATE_LEFT, 8) + bitvector_rotate_right = solver.mkOp(Kind.BITVECTOR_ROTATE_RIGHT, 9) + int_to_bitvector = solver.mkOp(Kind.INT_TO_BITVECTOR, 10) + iand = solver.mkOp(Kind.IAND, 3) + floatingpoint_to_ubv = solver.mkOp(Kind.FLOATINGPOINT_TO_UBV, 11) + floatingopint_to_sbv = solver.mkOp(Kind.FLOATINGPOINT_TO_SBV, 13) assert 1 == divisible.getNumIndices() assert 1 == bitvector_repeat.getNumIndices() @@ -75,14 +75,18 @@ def test_get_num_indices(solver): assert 1 == floatingopint_to_sbv.getNumIndices() # Operators with 2 indices - bitvector_extract = solver.mkOp(Kind.BVExtract, 4, 25) - floatingpoint_to_fp_from_ieee_bv = solver.mkOp(Kind.FPToFpFromIeeeBv, 4, - 25) - floatingpoint_to_fp_from_fp = solver.mkOp(Kind.FPToFpFromFp, 4, 25) - floatingpoint_to_fp_from_real = solver.mkOp(Kind.FPToFpFromReal, 4, 25) - floatingpoint_to_fp_from_sbv = solver.mkOp(Kind.FPToFpFromSbv, 4, 25) - floatingpoint_to_fp_from_ubv = solver.mkOp(Kind.FPToFpFromUbv, 4, 25) - regexp_loop = solver.mkOp(Kind.RegexpLoop, 2, 3) + bitvector_extract = solver.mkOp(Kind.BITVECTOR_EXTRACT, 4, 25) + floatingpoint_to_fp_from_ieee_bv = solver.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 4, 25) + floatingpoint_to_fp_from_fp = solver.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_FP, 4, 25) + floatingpoint_to_fp_from_real = solver.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_REAL, 4, 25) + floatingpoint_to_fp_from_sbv = solver.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_SBV, 4, 25) + floatingpoint_to_fp_from_ubv = solver.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_UBV, 4, 25) + regexp_loop = solver.mkOp(Kind.REGEXP_LOOP, 2, 3) assert 2 == bitvector_extract.getNumIndices() assert 2 == floatingpoint_to_fp_from_ieee_bv.getNumIndices() @@ -94,28 +98,28 @@ def test_get_num_indices(solver): # Operators with n indices indices = [0, 3, 2, 0, 1, 2] - tuple_project_op = solver.mkOp(Kind.TupleProject, *indices) + tuple_project_op = solver.mkOp(Kind.TUPLE_PROJECT, *indices) assert len(indices) == tuple_project_op.getNumIndices() def test_subscript_operator(solver): # Operators with 0 indices - plus = solver.mkOp(Kind.Add) + plus = solver.mkOp(Kind.ADD) with pytest.raises(RuntimeError): plus[0] # Operators with 1 index - divisible = solver.mkOp(Kind.Divisible, 4) - bitvector_repeat = solver.mkOp(Kind.BVRepeat, 5) - bitvector_zero_extend = solver.mkOp(Kind.BVZeroExtend, 6) - bitvector_sign_extend = solver.mkOp(Kind.BVSignExtend, 7) - bitvector_rotate_left = solver.mkOp(Kind.BVRotateLeft, 8) - bitvector_rotate_right = solver.mkOp(Kind.BVRotateRight, 9) - int_to_bitvector = solver.mkOp(Kind.IntToBV, 10) - iand = solver.mkOp(Kind.Iand, 11) - floatingpoint_to_ubv = solver.mkOp(Kind.FPToUbv, 12) - floatingopint_to_sbv = solver.mkOp(Kind.FPToSbv, 13) + divisible = solver.mkOp(Kind.DIVISIBLE, 4) + bitvector_repeat = solver.mkOp(Kind.BITVECTOR_REPEAT, 5) + bitvector_zero_extend = solver.mkOp(Kind.BITVECTOR_ZERO_EXTEND, 6) + bitvector_sign_extend = solver.mkOp(Kind.BITVECTOR_SIGN_EXTEND, 7) + bitvector_rotate_left = solver.mkOp(Kind.BITVECTOR_ROTATE_LEFT, 8) + bitvector_rotate_right = solver.mkOp(Kind.BITVECTOR_ROTATE_RIGHT, 9) + int_to_bitvector = solver.mkOp(Kind.INT_TO_BITVECTOR, 10) + iand = solver.mkOp(Kind.IAND, 11) + floatingpoint_to_ubv = solver.mkOp(Kind.FLOATINGPOINT_TO_UBV, 12) + floatingopint_to_sbv = solver.mkOp(Kind.FLOATINGPOINT_TO_SBV, 13) assert 4 == divisible[0].getIntegerValue() assert 5 == bitvector_repeat[0].getIntegerValue() @@ -129,13 +133,18 @@ def test_subscript_operator(solver): assert 13 == floatingopint_to_sbv[0].getIntegerValue() # Operators with 2 indices - bitvector_extract = solver.mkOp(Kind.BVExtract, 1, 0) - floatingpoint_to_fp_from_ieee_bv = solver.mkOp(Kind.FPToFpFromIeeeBv, 3, 2) - floatingpoint_to_fp_from_fp = solver.mkOp(Kind.FPToFpFromFp, 5, 4) - floatingpoint_to_fp_from_real = solver.mkOp(Kind.FPToFpFromReal, 7, 6) - floatingpoint_to_fp_from_sbv = solver.mkOp(Kind.FPToFpFromSbv, 9, 8) - floatingpoint_to_fp_from_ubv = solver.mkOp(Kind.FPToFpFromUbv, 11, 10) - regexp_loop = solver.mkOp(Kind.RegexpLoop, 15, 14) + bitvector_extract = solver.mkOp(Kind.BITVECTOR_EXTRACT, 1, 0) + floatingpoint_to_fp_from_ieee_bv = solver.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 3, 2) + floatingpoint_to_fp_from_fp = solver.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_FP, 5, 4) + floatingpoint_to_fp_from_real = solver.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6) + floatingpoint_to_fp_from_sbv = solver.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8) + floatingpoint_to_fp_from_ubv = solver.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10) + regexp_loop = solver.mkOp(Kind.REGEXP_LOOP, 15, 14) assert 1 == bitvector_extract[0].getIntegerValue() assert 0 == bitvector_extract[1].getIntegerValue() @@ -154,12 +163,12 @@ def test_subscript_operator(solver): # Operators with n indices indices = [0, 3, 2, 0, 1, 2] - tuple_project_op = solver.mkOp(Kind.TupleProject, *indices) + tuple_project_op = solver.mkOp(Kind.TUPLE_PROJECT, *indices) for i in range(len(indices)): assert indices[i] == tuple_project_op[i].getIntegerValue() def test_op_scoping_to_string(solver): - bitvector_repeat_ot = solver.mkOp(Kind.BVRepeat, 5) + bitvector_repeat_ot = solver.mkOp(Kind.BITVECTOR_REPEAT, 5) op_repr = str(bitvector_repeat_ot) assert str(bitvector_repeat_ot) == op_repr diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 8ef6de932..c27cef850 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -32,7 +32,7 @@ def test_recoverable_exception(solver): def test_supports_floating_point(solver): - solver.mkRoundingMode(RoundingMode.RoundNearestTiesToEven) + solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN) def test_get_boolean_sort(solver): @@ -177,7 +177,7 @@ def test_mk_datatype_sorts(solver): isort1 = dt_sorts[1].instantiate({solver.getBooleanSort()}) t1 = solver.mkConst(isort1, "t") t0 = solver.mkTerm( - Kind.ApplySelector, + Kind.APPLY_SELECTOR, t1.getSort().getDatatype().getSelector("s1").getSelectorTerm(), t1) assert dt_sorts[0].instantiate({solver.getBooleanSort()}) == t0.getSort() @@ -407,15 +407,15 @@ def test_mk_boolean(solver): def test_mk_rounding_mode(solver): assert str(solver.mkRoundingMode( - RoundingMode.RoundNearestTiesToEven)) == "roundNearestTiesToEven" + RoundingMode.ROUND_NEAREST_TIES_TO_EVEN)) == "roundNearestTiesToEven" assert str(solver.mkRoundingMode( - RoundingMode.RoundTowardPositive)) == "roundTowardPositive" + RoundingMode.ROUND_TOWARD_POSITIVE)) == "roundTowardPositive" assert str(solver.mkRoundingMode( - RoundingMode.RoundTowardNegative)) == "roundTowardNegative" + RoundingMode.ROUND_TOWARD_NEGATIVE)) == "roundTowardNegative" assert str(solver.mkRoundingMode( - RoundingMode.RoundTowardZero)) == "roundTowardZero" + RoundingMode.ROUND_TOWARD_ZERO)) == "roundTowardZero" assert str(solver.mkRoundingMode( - RoundingMode.RoundNearestTiesToAway)) == "roundNearestTiesToAway" + RoundingMode.ROUND_NEAREST_TIES_TO_AWAY)) == "roundNearestTiesToAway" def test_mk_floating_point(solver): @@ -511,24 +511,24 @@ def test_mk_floating_point_pos_zero(solver): def test_mk_op(solver): with pytest.raises(ValueError): - solver.mkOp(Kind.BVExtract, Kind.Equal) + solver.mkOp(Kind.BITVECTOR_EXTRACT, Kind.EQUAL) - solver.mkOp(Kind.Divisible, "2147483648") + solver.mkOp(Kind.DIVISIBLE, "2147483648") with pytest.raises(RuntimeError): - solver.mkOp(Kind.BVExtract, "asdf") + solver.mkOp(Kind.BITVECTOR_EXTRACT, "asdf") - solver.mkOp(Kind.Divisible, 1) - solver.mkOp(Kind.BVRotateLeft, 1) - solver.mkOp(Kind.BVRotateRight, 1) + solver.mkOp(Kind.DIVISIBLE, 1) + solver.mkOp(Kind.BITVECTOR_ROTATE_LEFT, 1) + solver.mkOp(Kind.BITVECTOR_ROTATE_RIGHT, 1) with pytest.raises(RuntimeError): - solver.mkOp(Kind.BVExtract, 1) + solver.mkOp(Kind.BITVECTOR_EXTRACT, 1) - solver.mkOp(Kind.BVExtract, 1, 1) + solver.mkOp(Kind.BITVECTOR_EXTRACT, 1, 1) with pytest.raises(RuntimeError): - solver.mkOp(Kind.Divisible, 1, 2) + solver.mkOp(Kind.DIVISIBLE, 1, 2) args = [1, 2, 2] - solver.mkOp(Kind.TupleProject, *args) + solver.mkOp(Kind.TUPLE_PROJECT, *args) def test_mk_pi(solver): @@ -660,19 +660,19 @@ def test_mk_real(solver): def test_mk_regexp_none(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") - solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpNone()) + solver.mkTerm(Kind.STRING_IN_REGEXP, s, solver.mkRegexpNone()) def test_mk_regexp_all(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") - solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpAll()) + solver.mkTerm(Kind.STRING_IN_REGEXP, s, solver.mkRegexpAll()) def test_mk_regexp_allchar(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") - solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpAllchar()) + solver.mkTerm(Kind.STRING_IN_REGEXP, s, solver.mkRegexpAllchar()) def test_mk_sep_emp(solver): @@ -704,92 +704,92 @@ def test_mk_term(solver): # mkTerm(Kind kind) const solver.mkPi() - solver.mkTerm(Kind.Pi) - solver.mkTerm(solver.mkOp(Kind.Pi)) - solver.mkTerm(Kind.RegexpNone) - solver.mkTerm(solver.mkOp(Kind.RegexpNone)) - solver.mkTerm(Kind.RegexpAllchar) - solver.mkTerm(solver.mkOp(Kind.RegexpAllchar)) - solver.mkTerm(Kind.SepEmp) - solver.mkTerm(solver.mkOp(Kind.SepEmp)) + solver.mkTerm(Kind.PI) + solver.mkTerm(solver.mkOp(Kind.PI)) + solver.mkTerm(Kind.REGEXP_NONE) + solver.mkTerm(solver.mkOp(Kind.REGEXP_NONE)) + solver.mkTerm(Kind.REGEXP_ALLCHAR) + solver.mkTerm(solver.mkOp(Kind.REGEXP_ALLCHAR)) + solver.mkTerm(Kind.SEP_EMP) + solver.mkTerm(solver.mkOp(Kind.SEP_EMP)) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.ConstBV) + solver.mkTerm(Kind.CONST_BITVECTOR) # mkTerm(Kind kind, Term child) const - solver.mkTerm(Kind.Not, solver.mkTrue()) + solver.mkTerm(Kind.NOT, solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Not, cvc5.Term(solver)) + solver.mkTerm(Kind.NOT, cvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Not, a) + solver.mkTerm(Kind.NOT, a) with pytest.raises(RuntimeError): - slv.mkTerm(Kind.Not, solver.mkTrue()) + slv.mkTerm(Kind.NOT, solver.mkTrue()) # mkTerm(Kind kind, Term child1, Term child2) const - solver.mkTerm(Kind.Equal, a, b) + solver.mkTerm(Kind.EQUAL, a, b) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Equal, cvc5.Term(solver), b) + solver.mkTerm(Kind.EQUAL, cvc5.Term(solver), b) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Equal, a, cvc5.Term(solver)) + solver.mkTerm(Kind.EQUAL, a, cvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Equal, a, solver.mkTrue()) + solver.mkTerm(Kind.EQUAL, a, solver.mkTrue()) with pytest.raises(RuntimeError): - slv.mkTerm(Kind.Equal, a, b) + slv.mkTerm(Kind.EQUAL, a, b) # mkTerm(Kind kind, Term child1, Term child2, Term child3) const - solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) + solver.mkTerm(Kind.ITE, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Ite, cvc5.Term(solver), solver.mkTrue(), + solver.mkTerm(Kind.ITE, cvc5.Term(solver), solver.mkTrue(), solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Ite, solver.mkTrue(), cvc5.Term(solver), + solver.mkTerm(Kind.ITE, solver.mkTrue(), cvc5.Term(solver), solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), + solver.mkTerm(Kind.ITE, solver.mkTrue(), solver.mkTrue(), cvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), b) + solver.mkTerm(Kind.ITE, solver.mkTrue(), solver.mkTrue(), b) with pytest.raises(RuntimeError): - slv.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), + slv.mkTerm(Kind.ITE, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) - solver.mkTerm(Kind.Equal, a, b) + solver.mkTerm(Kind.EQUAL, a, b) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Equal, a, cvc5.Term(solver)) + solver.mkTerm(Kind.EQUAL, a, cvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Equal, a, solver.mkTrue()) + solver.mkTerm(Kind.EQUAL, a, solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Distinct) + 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.INTS_DIVISION, t_int, t_int, t_int) + solver.mkTerm(solver.mkOp(Kind.INTS_DIVISION), 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.REGEXP_DIFF, t_reg, t_reg, t_reg) + solver.mkTerm(solver.mkOp(Kind.REGEXP_DIFF), 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.HO_APPLY, t_fun, t_bool, t_bool, t_bool) + solver.mkTerm(solver.mkOp(Kind.HO_APPLY), t_fun, t_bool, t_bool, t_bool) def test_mk_term_from_op(solver): bv32 = solver.mkBitVectorSort(32) @@ -798,8 +798,8 @@ def test_mk_term_from_op(solver): slv = cvc5.Solver() # simple operator terms - opterm1 = solver.mkOp(Kind.BVExtract, 2, 1) - opterm2 = solver.mkOp(Kind.Divisible, 1) + opterm1 = solver.mkOp(Kind.BITVECTOR_EXTRACT, 2, 1) + opterm2 = solver.mkOp(Kind.DIVISIBLE, 1) # list datatype sort = solver.mkParamSort("T") @@ -827,40 +827,40 @@ def test_mk_term_from_op(solver): tailTerm2 = lis["cons"]["tail"].getSelectorTerm() # mkTerm(Op op, Term term) const - solver.mkTerm(Kind.ApplyConstructor, nilTerm1) - solver.mkTerm(Kind.ApplyConstructor, nilTerm2) + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm1) + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm2) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.ApplySelector, nilTerm1) + solver.mkTerm(Kind.APPLY_SELECTOR, nilTerm1) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.ApplySelector, consTerm1) + solver.mkTerm(Kind.APPLY_SELECTOR, consTerm1) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.ApplyConstructor, consTerm2) + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm2) with pytest.raises(RuntimeError): solver.mkTerm(opterm1) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.ApplySelector, headTerm1) + solver.mkTerm(Kind.APPLY_SELECTOR, headTerm1) with pytest.raises(RuntimeError): solver.mkTerm(opterm1) with pytest.raises(RuntimeError): - slv.mkTerm(Kind.ApplyConstructor, nilTerm1) + slv.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm1) # mkTerm(Op op, Term child) const solver.mkTerm(opterm1, a) solver.mkTerm(opterm2, solver.mkInteger(1)) - solver.mkTerm(Kind.ApplySelector, headTerm1, c) - solver.mkTerm(Kind.ApplySelector, tailTerm2, c) + solver.mkTerm(Kind.APPLY_SELECTOR, headTerm1, c) + solver.mkTerm(Kind.APPLY_SELECTOR, tailTerm2, c) with pytest.raises(RuntimeError): solver.mkTerm(opterm2, a) with pytest.raises(RuntimeError): solver.mkTerm(opterm1, cvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.ApplyConstructor, consTerm1, solver.mkInteger(0)) + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm1, solver.mkInteger(0)) with pytest.raises(RuntimeError): slv.mkTerm(opterm1, a) # mkTerm(Op op, Term child1, Term child2) const - solver.mkTerm(Kind.ApplyConstructor, consTerm1, solver.mkInteger(0), - solver.mkTerm(Kind.ApplyConstructor, nilTerm1)) + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm1, solver.mkInteger(0), + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm1)) with pytest.raises(RuntimeError): solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2)) with pytest.raises(RuntimeError): @@ -870,10 +870,10 @@ def test_mk_term_from_op(solver): with pytest.raises(RuntimeError): solver.mkTerm(opterm2, cvc5.Term(solver), solver.mkInteger(1)) with pytest.raises(RuntimeError): - slv.mkTerm(Kind.ApplyConstructor,\ + slv.mkTerm(Kind.APPLY_CONSTRUCTOR,\ consTerm1,\ solver.mkInteger(0),\ - solver.mkTerm(Kind.ApplyConstructor, nilTerm1)) + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm1)) # mkTerm(Op op, Term child1, Term child2, Term child3) const with pytest.raises(RuntimeError): @@ -1111,7 +1111,7 @@ def test_uf_iteration(solver): x = solver.mkConst(intSort, "x") y = solver.mkConst(intSort, "y") f = solver.mkConst(funSort, "f") - fxy = solver.mkTerm(Kind.ApplyUf, f, x, y) + fxy = solver.mkTerm(Kind.APPLY_UF, f, x, y) # Expecting the uninterpreted function to be one of the children expected_children = [f, x, y] @@ -1131,7 +1131,7 @@ def test_get_info(solver): def test_get_op(solver): bv32 = solver.mkBitVectorSort(32) a = solver.mkConst(bv32, "a") - ext = solver.mkOp(Kind.BVExtract, 2, 1) + ext = solver.mkOp(Kind.BITVECTOR_EXTRACT, 2, 1) exta = solver.mkTerm(ext, a) assert not a.hasOp() @@ -1155,10 +1155,10 @@ def test_get_op(solver): nilTerm = consList.getConstructorTerm("nil") headTerm = consList["cons"].getSelectorTerm("head") - listnil = solver.mkTerm(Kind.ApplyConstructor, nilTerm) - listcons1 = solver.mkTerm(Kind.ApplyConstructor, consTerm, + listnil = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm) + listcons1 = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm, solver.mkInteger(1), listnil) - listhead = solver.mkTerm(Kind.ApplySelector, headTerm, listcons1) + listhead = solver.mkTerm(Kind.APPLY_SELECTOR, headTerm, listcons1) assert listnil.hasOp() assert listcons1.hasOp() @@ -1301,14 +1301,14 @@ def test_get_unsat_core_and_proof(solver): p = solver.mkConst(intPredSort, "p") zero = solver.mkInteger(0) one = solver.mkInteger(1) - f_x = solver.mkTerm(Kind.ApplyUf, f, x) - f_y = solver.mkTerm(Kind.ApplyUf, f, y) - summ = solver.mkTerm(Kind.Add, f_x, f_y) - p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) - p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) - solver.assertFormula(solver.mkTerm(Kind.Gt, zero, f_x)) - solver.assertFormula(solver.mkTerm(Kind.Gt, zero, f_y)) - solver.assertFormula(solver.mkTerm(Kind.Gt, summ, one)) + f_x = solver.mkTerm(Kind.APPLY_UF, f, x) + f_y = solver.mkTerm(Kind.APPLY_UF, f, y) + summ = solver.mkTerm(Kind.ADD, f_x, f_y) + p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero) + p_f_y = solver.mkTerm(Kind.APPLY_UF, p, f_y) + solver.assertFormula(solver.mkTerm(Kind.GT, zero, f_x)) + solver.assertFormula(solver.mkTerm(Kind.GT, zero, f_y)) + solver.assertFormula(solver.mkTerm(Kind.GT, summ, one)) solver.assertFormula(p_0) solver.assertFormula(p_f_y.notTerm()) assert solver.checkSat().isUnsat() @@ -1336,8 +1336,11 @@ def test_learned_literals2(solver): y = solver.mkConst(intSort, "y") zero = solver.mkInteger(0) ten = solver.mkInteger(10) - f0 = solver.mkTerm(Kind.Geq, x, ten) - f1 = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Geq, zero, x), solver.mkTerm(Kind.Geq, y, zero)) + f0 = solver.mkTerm(Kind.GEQ, x, ten) + f1 = solver.mkTerm( + Kind.OR, + solver.mkTerm(Kind.GEQ, zero, x), + solver.mkTerm(Kind.GEQ, y, zero)) solver.assertFormula(f0) solver.assertFormula(f1) solver.checkSat() @@ -1377,15 +1380,15 @@ def test_get_value3(solver): p = solver.mkConst(intPredSort, "p") zero = solver.mkInteger(0) one = solver.mkInteger(1) - f_x = solver.mkTerm(Kind.ApplyUf, f, x) - f_y = solver.mkTerm(Kind.ApplyUf, f, y) - summ = solver.mkTerm(Kind.Add, f_x, f_y) - p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) - p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) - - solver.assertFormula(solver.mkTerm(Kind.Leq, zero, f_x)) - solver.assertFormula(solver.mkTerm(Kind.Leq, zero, f_y)) - solver.assertFormula(solver.mkTerm(Kind.Leq, summ, one)) + f_x = solver.mkTerm(Kind.APPLY_UF, f, x) + f_y = solver.mkTerm(Kind.APPLY_UF, f, y) + summ = solver.mkTerm(Kind.ADD, f_x, f_y) + p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero) + p_f_y = solver.mkTerm(Kind.APPLY_UF, p, f_y) + + solver.assertFormula(solver.mkTerm(Kind.LEQ, zero, f_x)) + solver.assertFormula(solver.mkTerm(Kind.LEQ, zero, f_y)) + solver.assertFormula(solver.mkTerm(Kind.LEQ, summ, one)) solver.assertFormula(p_0.notTerm()) solver.assertFormula(p_f_y) assert solver.checkSat().isSat() @@ -1418,7 +1421,7 @@ def checkSimpleSeparationConstraints(slv): slv.declareSepHeap(integer, integer) x = slv.mkConst(integer, "x") p = slv.mkConst(integer, "p") - heap = slv.mkTerm(Kind.SepPto, p, x) + heap = slv.mkTerm(Kind.SEP_PTO, p, x) slv.assertFormula(heap) nil = slv.mkSepNil(integer) slv.assertFormula(nil.eqTerm(slv.mkReal(5))) @@ -1562,21 +1565,21 @@ def test_block_model1(solver): solver.assertFormula(x.eqTerm(x)) solver.checkSat() with pytest.raises(RuntimeError): - solver.blockModel(BlockModelsMode.Literals) + solver.blockModel(BlockModelsMode.LITERALS) def test_block_model2(solver): solver.setOption("produce-models", "true") x = solver.mkConst(solver.getBooleanSort(), "x") solver.assertFormula(x.eqTerm(x)) with pytest.raises(RuntimeError): - solver.blockModel(BlockModelsMode.Literals) + solver.blockModel(BlockModelsMode.LITERALS) def test_block_model3(solver): solver.setOption("produce-models", "true") x = solver.mkConst(solver.getBooleanSort(), "x"); solver.assertFormula(x.eqTerm(x)) solver.checkSat() - solver.blockModel(BlockModelsMode.Literals) + solver.blockModel(BlockModelsMode.LITERALS) def test_block_model_values1(solver): solver.setOption("produce-models", "true") @@ -1624,8 +1627,11 @@ def test_get_statistics(solver): y = solver.mkConst(intSort, "y") zero = solver.mkInteger(0) ten = solver.mkInteger(10) - f0 = solver.mkTerm(Kind.Geq, x, ten) - f1 = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Geq, zero, x), solver.mkTerm(Kind.Geq, y, zero)) + f0 = solver.mkTerm(Kind.GEQ, x, ten) + f1 = solver.mkTerm( + Kind.OR, + solver.mkTerm(Kind.GEQ, zero, x), + solver.mkTerm(Kind.GEQ, y, zero)) solver.assertFormula(f0) solver.assertFormula(f1) solver.checkSat() @@ -1686,11 +1692,11 @@ def test_simplify(solver): solver.simplify(a) b = solver.mkConst(bvSort, "b") solver.simplify(b) - x_eq_x = solver.mkTerm(Kind.Equal, x, x) + x_eq_x = solver.mkTerm(Kind.EQUAL, x, x) solver.simplify(x_eq_x) assert solver.mkTrue() != x_eq_x assert solver.mkTrue() == solver.simplify(x_eq_x) - x_eq_b = solver.mkTerm(Kind.Equal, x, b) + x_eq_b = solver.mkTerm(Kind.EQUAL, x, b) solver.simplify(x_eq_b) assert solver.mkTrue() != x_eq_b assert solver.mkTrue() != solver.simplify(x_eq_b) @@ -1700,24 +1706,25 @@ def test_simplify(solver): i1 = solver.mkConst(solver.getIntegerSort(), "i1") solver.simplify(i1) - i2 = solver.mkTerm(Kind.Mult, i1, solver.mkInteger("23")) + i2 = solver.mkTerm(Kind.MULT, i1, solver.mkInteger("23")) solver.simplify(i2) assert i1 != i2 assert i1 != solver.simplify(i2) - i3 = solver.mkTerm(Kind.Add, i1, solver.mkInteger(0)) + i3 = solver.mkTerm(Kind.ADD, i1, solver.mkInteger(0)) solver.simplify(i3) assert i1 != i3 assert i1 == solver.simplify(i3) consList = consListSort.getDatatype() dt1 = solver.mkTerm(\ - Kind.ApplyConstructor,\ + Kind.APPLY_CONSTRUCTOR,\ consList.getConstructorTerm("cons"),\ solver.mkInteger(0),\ - solver.mkTerm(Kind.ApplyConstructor, consList.getConstructorTerm("nil"))) + solver.mkTerm( + Kind.APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))) solver.simplify(dt1) dt2 = solver.mkTerm(\ - Kind.ApplySelector, consList["cons"].getSelectorTerm("head"), dt1) + Kind.APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1) solver.simplify(dt2) b1 = solver.mkVar(bvSort, "b1") @@ -1769,7 +1776,7 @@ def test_check_sat_assuming1(solver): boolSort = solver.getBooleanSort() x = solver.mkConst(boolSort, "x") y = solver.mkConst(boolSort, "y") - z = solver.mkTerm(Kind.And, x, y) + z = solver.mkTerm(Kind.AND, x, y) solver.setOption("incremental", "true") solver.checkSatAssuming(solver.mkTrue()) with pytest.raises(RuntimeError): @@ -1801,31 +1808,31 @@ def test_check_sat_assuming2(solver): zero = solver.mkInteger(0) one = solver.mkInteger(1) # Terms - f_x = solver.mkTerm(Kind.ApplyUf, f, x) - f_y = solver.mkTerm(Kind.ApplyUf, f, y) - summ = solver.mkTerm(Kind.Add, f_x, f_y) - p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) - p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) + f_x = solver.mkTerm(Kind.APPLY_UF, f, x) + f_y = solver.mkTerm(Kind.APPLY_UF, f, y) + summ = solver.mkTerm(Kind.ADD, f_x, f_y) + p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero) + p_f_y = solver.mkTerm(Kind.APPLY_UF, p, f_y) # Assertions assertions =\ - solver.mkTerm(Kind.And,\ - 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 + solver.mkTerm(Kind.AND,\ + 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.mkTerm(Kind.DISTINCT, x, y)) solver.checkSatAssuming( solver.mkFalse(), - solver.mkTerm(Kind.Distinct, x, y)) + 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()) @@ -1855,10 +1862,10 @@ def test_reset_assertions(solver): bvSort = solver.mkBitVectorSort(4) one = solver.mkBitVector(4, 1) x = solver.mkConst(bvSort, "x") - ule = solver.mkTerm(Kind.BVUle, x, one) - srem = solver.mkTerm(Kind.BVSrem, one, x) + ule = solver.mkTerm(Kind.BITVECTOR_ULE, x, one) + srem = solver.mkTerm(Kind.BITVECTOR_SREM, one, x) solver.push(4) - slt = solver.mkTerm(Kind.BVSlt, srem, one) + slt = solver.mkTerm(Kind.BITVECTOR_SLT, srem, one) solver.resetAssertions() solver.checkSatAssuming(slt, ule) @@ -2089,8 +2096,8 @@ def test_get_abduct(solver): x = solver.mkConst(intSort, "x") y = solver.mkConst(intSort, "y") - solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero)) - conj = solver.mkTerm(Kind.Gt, y, zero) + solver.assertFormula(solver.mkTerm(Kind.GT, x, zero)) + conj = solver.mkTerm(Kind.GT, y, zero) output = solver.getAbduct(conj) assert not output.isNull() and output.getSort().isBoolean() @@ -2099,7 +2106,7 @@ def test_get_abduct(solver): start = solver.mkVar(boolean) output2 = cvc5.Term(solver) g = solver.mkSygusGrammar([], [start]) - conj2 = solver.mkTerm(Kind.Gt, x, zero) + conj2 = solver.mkTerm(Kind.GT, x, zero) g.addRule(start, truen) output2 = solver.getAbduct(conj2, g) assert output2 == truen @@ -2111,8 +2118,8 @@ def test_get_abduct2(solver): zero = solver.mkInteger(0) x = solver.mkConst(intSort, "x") y = solver.mkConst(intSort, "y") - solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero)) - conj = solver.mkTerm(Kind.Gt, y, zero) + solver.assertFormula(solver.mkTerm(Kind.GT, x, zero)) + conj = solver.mkTerm(Kind.GT, y, zero) output = cvc5.Term(solver) with pytest.raises(RuntimeError): solver.getAbduct(conj) @@ -2127,8 +2134,8 @@ def test_get_abduct_next(solver): x = solver.mkConst(intSort, "x") y = solver.mkConst(intSort, "y") - solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero)) - conj = solver.mkTerm(Kind.Gt, y, zero) + solver.assertFormula(solver.mkTerm(Kind.GT, x, zero)) + conj = solver.mkTerm(Kind.GT, y, zero) output = solver.getAbduct(conj) output2 = solver.getAbductNext() assert output != output2 @@ -2146,12 +2153,12 @@ def test_get_interpolant(solver): z = solver.mkConst(intSort, "z") solver.assertFormula(solver.mkTerm( - Kind.Gt, solver.mkTerm(Kind.Add, x, y), zero)) - solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero)) + Kind.GT, solver.mkTerm(Kind.ADD, x, y), zero)) + solver.assertFormula(solver.mkTerm(Kind.LT, x, zero)) conj = solver.mkTerm( - Kind.Or, - solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Add, y, z), zero), - solver.mkTerm(Kind.Lt, z, zero)) + Kind.OR, + solver.mkTerm(Kind.GT, solver.mkTerm(Kind.ADD, y, z), zero), + solver.mkTerm(Kind.LT, z, zero)) output = solver.getInterpolant(conj) assert output.getSort().isBoolean() @@ -2167,12 +2174,12 @@ def test_get_interpolant_next(solver): z = solver.mkConst(intSort, "z") solver.assertFormula(solver.mkTerm( - Kind.Gt, solver.mkTerm(Kind.Add, x, y), zero)) - solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero)) + Kind.GT, solver.mkTerm(Kind.ADD, x, y), zero)) + solver.assertFormula(solver.mkTerm(Kind.LT, x, zero)) conj = solver.mkTerm( - Kind.Or, - solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Add, y, z), zero), - solver.mkTerm(Kind.Lt, z, zero)) + Kind.OR, + solver.mkTerm(Kind.GT, solver.mkTerm(Kind.ADD, y, z), zero), + solver.mkTerm(Kind.LT, z, zero)) output = solver.getInterpolant(conj) output2 = solver.getInterpolantNext() @@ -2206,14 +2213,14 @@ def test_define_fun_global(solver): # (assert (or (not f) (not (g true)))) solver.assertFormula( - solver.mkTerm(Kind.Or, f.notTerm(), - solver.mkTerm(Kind.ApplyUf, g, bTrue).notTerm())) + solver.mkTerm(Kind.OR, f.notTerm(), + solver.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm())) assert solver.checkSat().isUnsat() solver.resetAssertions() # (assert (or (not f) (not (g true)))) solver.assertFormula( - solver.mkTerm(Kind.Or, f.notTerm(), - solver.mkTerm(Kind.ApplyUf, g, bTrue).notTerm())) + solver.mkTerm(Kind.OR, f.notTerm(), + solver.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm())) assert solver.checkSat().isUnsat() @@ -2237,7 +2244,7 @@ def test_get_model_domain_elements(solver): x = solver.mkConst(uSort, "x") y = solver.mkConst(uSort, "y") z = solver.mkConst(uSort, "z") - f = solver.mkTerm(Kind.Distinct, x, y, z) + f = solver.mkTerm(Kind.DISTINCT, x, y, z) solver.assertFormula(f) solver.checkSat() solver.getModelDomainElements(uSort) @@ -2251,9 +2258,9 @@ def test_get_model_domain_elements2(solver): uSort = solver.mkUninterpretedSort("u") x = solver.mkVar(uSort, "x") y = solver.mkVar(uSort, "y") - eq = solver.mkTerm(Kind.Equal, x, y) - bvl = solver.mkTerm(Kind.VariableList, x, y) - f = solver.mkTerm(Kind.Forall, bvl, eq) + eq = solver.mkTerm(Kind.EQUAL, x, y) + bvl = solver.mkTerm(Kind.VARIABLE_LIST, x, y) + f = solver.mkTerm(Kind.FORALL, bvl, eq) solver.assertFormula(f) solver.checkSat() solver.getModelDomainElements(uSort) @@ -2396,7 +2403,7 @@ def test_is_model_core_symbol(solver): y = solver.mkConst(uSort, "y") z = solver.mkConst(uSort, "z") zero = solver.mkInteger(0) - f = solver.mkTerm(Kind.Not, solver.mkTerm(Kind.Equal, x, y)) + f = solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, x, y)) solver.assertFormula(f) solver.checkSat() assert solver.isModelCoreSymbol(x) @@ -2412,7 +2419,7 @@ def test_get_model(solver): x = solver.mkConst(uSort, "x") y = solver.mkConst(uSort, "y") z = solver.mkConst(uSort, "z") - f = solver.mkTerm(Kind.Not, solver.mkTerm(Kind.Equal, x, y)) + f = solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, x, y)) solver.assertFormula(f) solver.checkSat() sorts = [uSort] @@ -2452,8 +2459,8 @@ def test_issue5893(solver): arr = solver.mkConst(arrsort, "arr") idx = solver.mkConst(bvsort4, "idx") ten = solver.mkBitVector(8, "10", 10) - sel = solver.mkTerm(Kind.Select, arr, idx) - distinct = solver.mkTerm(Kind.Distinct, sel, ten) + sel = solver.mkTerm(Kind.SELECT, arr, idx) + distinct = solver.mkTerm(Kind.DISTINCT, sel, ten) distinct.getOp() @@ -2465,9 +2472,9 @@ def test_issue7000(solver): t7 = solver.mkConst(s3, "_x5") t37 = solver.mkConst(s2, "_x32") t59 = solver.mkConst(s2, "_x51") - t72 = solver.mkTerm(Kind.Equal, t37, t59) - t74 = solver.mkTerm(Kind.Gt, t4, t7) - query = solver.mkTerm(Kind.And, t72, t74, t72, t72) + t72 = solver.mkTerm(Kind.EQUAL, t37, t59) + t74 = solver.mkTerm(Kind.GT, t4, t7) + query = solver.mkTerm(Kind.AND, t72, t74, t72, t72) # throws logic exception since logic is not higher order by default with pytest.raises(RuntimeError): solver.checkSatAssuming(query.notTerm()) @@ -2539,7 +2546,7 @@ def test_tuple_project(solver): solver.mkBoolean(True), \ solver.mkInteger(3),\ solver.mkString("C"),\ - solver.mkTerm(Kind.SetSingleton, solver.mkString("Z"))] + solver.mkTerm(Kind.SET_SINGLETON, solver.mkString("Z"))] tuple = solver.mkTuple(sorts, elements) @@ -2550,22 +2557,22 @@ def test_tuple_project(solver): indices5 = [4] indices6 = [0, 4] - solver.mkTerm(solver.mkOp(Kind.TupleProject, *indices1), tuple) + solver.mkTerm(solver.mkOp(Kind.TUPLE_PROJECT, *indices1), tuple) - solver.mkTerm(solver.mkOp(Kind.TupleProject, *indices2), tuple) + solver.mkTerm(solver.mkOp(Kind.TUPLE_PROJECT, *indices2), tuple) - solver.mkTerm(solver.mkOp(Kind.TupleProject, *indices3), tuple) + solver.mkTerm(solver.mkOp(Kind.TUPLE_PROJECT, *indices3), tuple) - solver.mkTerm(solver.mkOp(Kind.TupleProject, *indices4), tuple) + solver.mkTerm(solver.mkOp(Kind.TUPLE_PROJECT, *indices4), tuple) with pytest.raises(RuntimeError): - solver.mkTerm(solver.mkOp(Kind.TupleProject, *indices5), tuple) + solver.mkTerm(solver.mkOp(Kind.TUPLE_PROJECT, *indices5), tuple) with pytest.raises(RuntimeError): - solver.mkTerm(solver.mkOp(Kind.TupleProject, *indices6), tuple) + solver.mkTerm(solver.mkOp(Kind.TUPLE_PROJECT, *indices6), tuple) indices = [0, 3, 2, 0, 1, 2] - op = solver.mkOp(Kind.TupleProject, *indices) + op = solver.mkOp(Kind.TUPLE_PROJECT, *indices) projection = solver.mkTerm(op, tuple) datatype = tuple.getSort().getDatatype() @@ -2574,7 +2581,7 @@ def test_tuple_project(solver): for i in indices: selectorTerm = constructor[i].getSelectorTerm() - selectedTerm = solver.mkTerm(Kind.ApplySelector, selectorTerm, tuple) + selectedTerm = solver.mkTerm(Kind.APPLY_SELECTOR, selectorTerm, tuple) simplifiedTerm = solver.simplify(selectedTerm) assert elements[i] == simplifiedTerm @@ -2610,8 +2617,8 @@ def test_get_difficulty3(solver): x = solver.mkConst(intSort, "x") zero = solver.mkInteger(0) ten = solver.mkInteger(10) - f0 = solver.mkTerm(Kind.Geq, x, ten) - f1 = solver.mkTerm(Kind.Geq, zero, x) + f0 = solver.mkTerm(Kind.GEQ, x, ten) + f1 = solver.mkTerm(Kind.GEQ, zero, x) solver.checkSat() dmap = solver.getDifficulty() # difficulty should map assertions to integer values @@ -2625,7 +2632,7 @@ def test_get_model(solver): x = solver.mkConst(uSort, "x") y = solver.mkConst(uSort, "y") z = solver.mkConst(uSort, "z") - f = solver.mkTerm(Kind.Not, solver.mkTerm(Kind.Equal, x, y)); + f = solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, x, y)); solver.assertFormula(f) solver.checkSat() sorts = [uSort] @@ -2662,7 +2669,10 @@ def test_get_option_names(solver): def test_get_quantifier_elimination(solver): x = solver.mkVar(solver.getBooleanSort(), "x") - forall = solver.mkTerm(Kind.Forall, solver.mkTerm(Kind.VariableList, x), solver.mkTerm(Kind.Or, x, solver.mkTerm(Kind.Not, x))) + forall = solver.mkTerm( + Kind.FORALL, + solver.mkTerm(Kind.VARIABLE_LIST, x), + solver.mkTerm(Kind.OR, x, solver.mkTerm(Kind.NOT, x))) with pytest.raises(RuntimeError): solver.getQuantifierElimination(cvc5.Term(solver)) with pytest.raises(RuntimeError): @@ -2671,11 +2681,12 @@ def test_get_quantifier_elimination(solver): def test_get_quantifier_elimination_disjunct(solver): x = solver.mkVar(solver.getBooleanSort(), "x") - forall = solver.mkTerm(Kind.Forall, solver.mkTerm(Kind.VariableList, x), solver.mkTerm(Kind.Or, x, solver.mkTerm(Kind.Not, x))) + forall = solver.mkTerm( + Kind.FORALL, + solver.mkTerm(Kind.VARIABLE_LIST, x), + solver.mkTerm(Kind.OR, x, solver.mkTerm(Kind.NOT, x))) with pytest.raises(RuntimeError): solver.getQuantifierEliminationDisjunct(cvc5.Term(solver)) with pytest.raises(RuntimeError): solver.getQuantifierEliminationDisjunct(cvc5.Solver().mkBoolean(False)) solver.getQuantifierEliminationDisjunct(forall) - - diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index 40514e170..5cac4b89f 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -73,23 +73,23 @@ def test_get_kind(solver): zero = solver.mkInteger(0) zero.getKind() - f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.APPLY_UF, f, x) f_x.getKind() - f_y = solver.mkTerm(Kind.ApplyUf, f, y) + f_y = solver.mkTerm(Kind.APPLY_UF, f, y) f_y.getKind() - sum = solver.mkTerm(Kind.Add, f_x, f_y) + sum = solver.mkTerm(Kind.ADD, f_x, f_y) sum.getKind() - p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero) p_0.getKind() - p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) + p_f_y = solver.mkTerm(Kind.APPLY_UF, p, f_y) p_f_y.getKind() # Sequence kinds do not exist internally, test that the API properly # converts them back. seqSort = solver.mkSequenceSort(intSort) s = solver.mkConst(seqSort, "s") - ss = solver.mkTerm(Kind.SeqConcat, s, s) - assert ss.getKind() == Kind.SeqConcat + ss = solver.mkTerm(Kind.SEQ_CONCAT, s, s) + assert ss.getKind() == Kind.SEQ_CONCAT def test_get_sort(solver): @@ -120,19 +120,19 @@ def test_get_sort(solver): zero.getSort() assert zero.getSort() == intSort - f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.APPLY_UF, f, x) f_x.getSort() assert f_x.getSort() == intSort - f_y = solver.mkTerm(Kind.ApplyUf, f, y) + f_y = solver.mkTerm(Kind.APPLY_UF, f, y) f_y.getSort() assert f_y.getSort() == intSort - sum = solver.mkTerm(Kind.Add, f_x, f_y) + sum = solver.mkTerm(Kind.ADD, f_x, f_y) sum.getSort() assert sum.getSort() == intSort - p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero) p_0.getSort() assert p_0.getSort() == boolSort - p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) + p_f_y = solver.mkTerm(Kind.APPLY_UF, p, f_y) p_f_y.getSort() assert p_f_y.getSort() == boolSort @@ -151,8 +151,8 @@ def test_get_op(solver): with pytest.raises(RuntimeError): x.getOp() - ab = solver.mkTerm(Kind.Select, a, b) - ext = solver.mkOp(Kind.BVExtract, 4, 0) + ab = solver.mkTerm(Kind.SELECT, a, b) + ext = solver.mkOp(Kind.BITVECTOR_EXTRACT, 4, 0) extb = solver.mkTerm(ext, b) assert ab.hasOp() @@ -163,7 +163,7 @@ def test_get_op(solver): assert extb.getOp() == ext f = solver.mkConst(funsort, "f") - fx = solver.mkTerm(Kind.ApplyUf, f, x) + fx = solver.mkTerm(Kind.APPLY_UF, f, x) assert not f.hasOp() with pytest.raises(RuntimeError): @@ -192,11 +192,11 @@ def test_get_op(solver): headOpTerm = list1["cons"].getSelectorTerm("head") tailOpTerm = list1["cons"].getSelectorTerm("tail") - nilTerm = solver.mkTerm(Kind.ApplyConstructor, nilOpTerm) - consTerm = solver.mkTerm(Kind.ApplyConstructor, consOpTerm, + nilTerm = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilOpTerm) + consTerm = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consOpTerm, solver.mkInteger(0), nilTerm) - headTerm = solver.mkTerm(Kind.ApplySelector, headOpTerm, consTerm) - tailTerm = solver.mkTerm(Kind.ApplySelector, tailOpTerm, consTerm) + headTerm = solver.mkTerm(Kind.APPLY_SELECTOR, headOpTerm, consTerm) + tailTerm = solver.mkTerm(Kind.APPLY_SELECTOR, tailOpTerm, consTerm) assert nilTerm.hasOp() assert consTerm.hasOp() @@ -255,15 +255,15 @@ def test_not_term(solver): zero = solver.mkInteger(0) with pytest.raises(RuntimeError): zero.notTerm() - f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.APPLY_UF, f, x) with pytest.raises(RuntimeError): f_x.notTerm() - sum = solver.mkTerm(Kind.Add, f_x, f_x) + sum = solver.mkTerm(Kind.ADD, f_x, f_x) with pytest.raises(RuntimeError): sum.notTerm() - p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero) p_0.notTerm() - p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.APPLY_UF, p, f_x) p_f_x.notTerm() @@ -312,7 +312,7 @@ def test_and_term(solver): zero.andTerm(p) with pytest.raises(RuntimeError): zero.andTerm(zero) - f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.APPLY_UF, f, x) with pytest.raises(RuntimeError): f_x.andTerm(b) with pytest.raises(RuntimeError): @@ -325,7 +325,7 @@ def test_and_term(solver): f_x.andTerm(zero) with pytest.raises(RuntimeError): f_x.andTerm(f_x) - sum = solver.mkTerm(Kind.Add, f_x, f_x) + sum = solver.mkTerm(Kind.ADD, f_x, f_x) with pytest.raises(RuntimeError): sum.andTerm(b) with pytest.raises(RuntimeError): @@ -340,7 +340,7 @@ def test_and_term(solver): sum.andTerm(f_x) with pytest.raises(RuntimeError): sum.andTerm(sum) - p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero) p_0.andTerm(b) with pytest.raises(RuntimeError): p_0.andTerm(x) @@ -355,7 +355,7 @@ def test_and_term(solver): with pytest.raises(RuntimeError): p_0.andTerm(sum) p_0.andTerm(p_0) - p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.APPLY_UF, p, f_x) p_f_x.andTerm(b) with pytest.raises(RuntimeError): p_f_x.andTerm(x) @@ -418,7 +418,7 @@ def test_or_term(solver): zero.orTerm(p) with pytest.raises(RuntimeError): zero.orTerm(zero) - f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.APPLY_UF, f, x) with pytest.raises(RuntimeError): f_x.orTerm(b) with pytest.raises(RuntimeError): @@ -431,7 +431,7 @@ def test_or_term(solver): f_x.orTerm(zero) with pytest.raises(RuntimeError): f_x.orTerm(f_x) - sum = solver.mkTerm(Kind.Add, f_x, f_x) + sum = solver.mkTerm(Kind.ADD, f_x, f_x) with pytest.raises(RuntimeError): sum.orTerm(b) with pytest.raises(RuntimeError): @@ -446,7 +446,7 @@ def test_or_term(solver): sum.orTerm(f_x) with pytest.raises(RuntimeError): sum.orTerm(sum) - p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero) p_0.orTerm(b) with pytest.raises(RuntimeError): p_0.orTerm(x) @@ -461,7 +461,7 @@ def test_or_term(solver): with pytest.raises(RuntimeError): p_0.orTerm(sum) p_0.orTerm(p_0) - p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.APPLY_UF, p, f_x) p_f_x.orTerm(b) with pytest.raises(RuntimeError): p_f_x.orTerm(x) @@ -524,7 +524,7 @@ def test_xor_term(solver): zero.xorTerm(p) with pytest.raises(RuntimeError): zero.xorTerm(zero) - f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.APPLY_UF, f, x) with pytest.raises(RuntimeError): f_x.xorTerm(b) with pytest.raises(RuntimeError): @@ -537,7 +537,7 @@ def test_xor_term(solver): f_x.xorTerm(zero) with pytest.raises(RuntimeError): f_x.xorTerm(f_x) - sum = solver.mkTerm(Kind.Add, f_x, f_x) + sum = solver.mkTerm(Kind.ADD, f_x, f_x) with pytest.raises(RuntimeError): sum.xorTerm(b) with pytest.raises(RuntimeError): @@ -552,7 +552,7 @@ def test_xor_term(solver): sum.xorTerm(f_x) with pytest.raises(RuntimeError): sum.xorTerm(sum) - p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero) p_0.xorTerm(b) with pytest.raises(RuntimeError): p_0.xorTerm(x) @@ -567,7 +567,7 @@ def test_xor_term(solver): with pytest.raises(RuntimeError): p_0.xorTerm(sum) p_0.xorTerm(p_0) - p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.APPLY_UF, p, f_x) p_f_x.xorTerm(b) with pytest.raises(RuntimeError): p_f_x.xorTerm(x) @@ -626,7 +626,7 @@ def test_eq_term(solver): with pytest.raises(RuntimeError): zero.eqTerm(p) zero.eqTerm(zero) - f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.APPLY_UF, f, x) with pytest.raises(RuntimeError): f_x.eqTerm(b) with pytest.raises(RuntimeError): @@ -637,7 +637,7 @@ def test_eq_term(solver): f_x.eqTerm(p) f_x.eqTerm(zero) f_x.eqTerm(f_x) - sum = solver.mkTerm(Kind.Add, f_x, f_x) + sum = solver.mkTerm(Kind.ADD, f_x, f_x) with pytest.raises(RuntimeError): sum.eqTerm(b) with pytest.raises(RuntimeError): @@ -649,7 +649,7 @@ def test_eq_term(solver): sum.eqTerm(zero) sum.eqTerm(f_x) sum.eqTerm(sum) - p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero) p_0.eqTerm(b) with pytest.raises(RuntimeError): p_0.eqTerm(x) @@ -664,7 +664,7 @@ def test_eq_term(solver): with pytest.raises(RuntimeError): p_0.eqTerm(sum) p_0.eqTerm(p_0) - p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.APPLY_UF, p, f_x) p_f_x.eqTerm(b) with pytest.raises(RuntimeError): p_f_x.eqTerm(x) @@ -727,7 +727,7 @@ def test_imp_term(solver): zero.impTerm(p) with pytest.raises(RuntimeError): zero.impTerm(zero) - f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.APPLY_UF, f, x) with pytest.raises(RuntimeError): f_x.impTerm(b) with pytest.raises(RuntimeError): @@ -740,7 +740,7 @@ def test_imp_term(solver): f_x.impTerm(zero) with pytest.raises(RuntimeError): f_x.impTerm(f_x) - sum = solver.mkTerm(Kind.Add, f_x, f_x) + sum = solver.mkTerm(Kind.ADD, f_x, f_x) with pytest.raises(RuntimeError): sum.impTerm(b) with pytest.raises(RuntimeError): @@ -755,7 +755,7 @@ def test_imp_term(solver): sum.impTerm(f_x) with pytest.raises(RuntimeError): sum.impTerm(sum) - p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero) p_0.impTerm(b) with pytest.raises(RuntimeError): p_0.impTerm(x) @@ -770,7 +770,7 @@ def test_imp_term(solver): with pytest.raises(RuntimeError): p_0.impTerm(sum) p_0.impTerm(p_0) - p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.APPLY_UF, p, f_x) p_f_x.impTerm(b) with pytest.raises(RuntimeError): p_f_x.impTerm(x) @@ -827,22 +827,22 @@ def test_ite_term(solver): zero.iteTerm(x, x) with pytest.raises(RuntimeError): zero.iteTerm(x, b) - f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.APPLY_UF, f, x) with pytest.raises(RuntimeError): f_x.iteTerm(b, b) with pytest.raises(RuntimeError): f_x.iteTerm(b, x) - sum = solver.mkTerm(Kind.Add, f_x, f_x) + sum = solver.mkTerm(Kind.ADD, f_x, f_x) with pytest.raises(RuntimeError): sum.iteTerm(x, x) with pytest.raises(RuntimeError): sum.iteTerm(b, x) - p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero) p_0.iteTerm(b, b) p_0.iteTerm(x, x) with pytest.raises(RuntimeError): p_0.iteTerm(x, b) - p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.APPLY_UF, p, f_x) p_f_x.iteTerm(b, b) p_f_x.iteTerm(x, x) with pytest.raises(RuntimeError): @@ -860,8 +860,8 @@ def test_substitute(solver): x = solver.mkConst(solver.getIntegerSort(), "x") one = solver.mkInteger(1) ttrue = solver.mkTrue() - xpx = solver.mkTerm(Kind.Add, x, x) - onepone = solver.mkTerm(Kind.Add, one, one) + xpx = solver.mkTerm(Kind.ADD, x, x) + onepone = solver.mkTerm(Kind.ADD, one, one) assert xpx.substitute(x, one) == onepone assert onepone.substitute(one, x) == xpx @@ -871,8 +871,8 @@ def test_substitute(solver): # simultaneous substitution y = solver.mkConst(solver.getIntegerSort(), "y") - xpy = solver.mkTerm(Kind.Add, x, y) - xpone = solver.mkTerm(Kind.Add, y, one) + xpy = solver.mkTerm(Kind.ADD, x, y) + xpone = solver.mkTerm(Kind.ADD, y, one) es = [] rs = [] es.append(x) @@ -917,8 +917,8 @@ def test_substitute(solver): def test_term_compare(solver): t1 = solver.mkInteger(1) - t2 = solver.mkTerm(Kind.Add, solver.mkInteger(2), solver.mkInteger(2)) - t3 = solver.mkTerm(Kind.Add, solver.mkInteger(2), solver.mkInteger(2)) + t2 = solver.mkTerm(Kind.ADD, solver.mkInteger(2), solver.mkInteger(2)) + t3 = solver.mkTerm(Kind.ADD, solver.mkInteger(2), solver.mkInteger(2)) assert t2 >= t3 assert t2 <= t3 assert (t1 > t2) != (t1 < t2) @@ -928,7 +928,7 @@ def test_term_compare(solver): def test_term_children(solver): # simple term 2+3 two = solver.mkInteger(2) - t1 = solver.mkTerm(Kind.Add, two, solver.mkInteger(3)) + t1 = solver.mkTerm(Kind.ADD, two, solver.mkInteger(3)) assert t1[0] == two assert t1.getNumChildren() == 2 tnull = Term(solver) @@ -939,8 +939,9 @@ def test_term_children(solver): intSort = solver.getIntegerSort() fsort = solver.mkFunctionSort(intSort, intSort) f = solver.mkConst(fsort, "f") - t2 = solver.mkTerm(Kind.ApplyUf, f, two) - # due to our higher-order view of terms, we treat f as a child of Kind.ApplyUf + t2 = solver.mkTerm(Kind.APPLY_UF, f, two) + # due to our higher-order view of terms, we treat f as a child of + # Kind.APPLY_UF assert t2.getNumChildren() == 2 assert t2[0] == f assert t2[1] == two @@ -963,7 +964,7 @@ def test_get_uninterpreted_sort_value(solver): uSort = solver.mkUninterpretedSort("u") x = solver.mkConst(uSort, "x") y = solver.mkConst(uSort, "y") - solver.assertFormula(solver.mkTerm(Kind.Equal, x, y)) + solver.assertFormula(solver.mkTerm(Kind.EQUAL, x, y)) assert solver.checkSat().isSat() vx = solver.getValue(x) vy = solver.getValue(y) @@ -975,7 +976,7 @@ def test_get_uninterpreted_sort_value(solver): def test_is_rounding_mode_value(solver): assert not solver.mkInteger(15).isRoundingModeValue() assert solver.mkRoundingMode( - RoundingMode.RoundNearestTiesToEven).isRoundingModeValue() + RoundingMode.ROUND_NEAREST_TIES_TO_EVEN).isRoundingModeValue() assert not solver.mkConst( solver.getRoundingModeSort()).isRoundingModeValue() @@ -984,20 +985,20 @@ def test_get_rounding_mode_value(solver): with pytest.raises(RuntimeError): solver.mkInteger(15).getRoundingModeValue() assert solver.mkRoundingMode( - RoundingMode.RoundNearestTiesToEven).getRoundingModeValue( - ) == RoundingMode.RoundNearestTiesToEven + RoundingMode.ROUND_NEAREST_TIES_TO_EVEN).getRoundingModeValue( + ) == RoundingMode.ROUND_NEAREST_TIES_TO_EVEN assert solver.mkRoundingMode( - RoundingMode.RoundTowardPositive).getRoundingModeValue( - ) == RoundingMode.RoundTowardPositive + RoundingMode.ROUND_TOWARD_POSITIVE).getRoundingModeValue( + ) == RoundingMode.ROUND_TOWARD_POSITIVE assert solver.mkRoundingMode( - RoundingMode.RoundTowardNegative).getRoundingModeValue( - ) == RoundingMode.RoundTowardNegative + RoundingMode.ROUND_TOWARD_NEGATIVE).getRoundingModeValue( + ) == RoundingMode.ROUND_TOWARD_NEGATIVE assert solver.mkRoundingMode( - RoundingMode.RoundTowardZero).getRoundingModeValue( - ) == RoundingMode.RoundTowardZero + RoundingMode.ROUND_TOWARD_ZERO).getRoundingModeValue( + ) == RoundingMode.ROUND_TOWARD_ZERO assert solver.mkRoundingMode( - RoundingMode.RoundNearestTiesToAway).getRoundingModeValue( - ) == RoundingMode.RoundNearestTiesToAway + RoundingMode.ROUND_NEAREST_TIES_TO_AWAY).getRoundingModeValue( + ) == RoundingMode.ROUND_NEAREST_TIES_TO_AWAY def test_get_tuple(solver): @@ -1022,11 +1023,11 @@ def test_get_set(solver): i2 = solver.mkInteger(7) s1 = solver.mkEmptySet(s) - s2 = solver.mkTerm(Kind.SetSingleton, i1) - s3 = solver.mkTerm(Kind.SetSingleton, i1) - s4 = solver.mkTerm(Kind.SetSingleton, i2) + s2 = solver.mkTerm(Kind.SET_SINGLETON, i1) + s3 = solver.mkTerm(Kind.SET_SINGLETON, i1) + s4 = solver.mkTerm(Kind.SET_SINGLETON, i2) s5 = solver.mkTerm( - Kind.SetUnion, s2, solver.mkTerm(Kind.SetUnion, s3, s4)) + Kind.SET_UNION, s2, solver.mkTerm(Kind.SET_UNION, s3, s4)) assert s1.isSetValue() assert s2.isSetValue() @@ -1050,11 +1051,11 @@ def test_get_sequence(solver): i2 = solver.mkInteger(7) s1 = solver.mkEmptySequence(s) - s2 = solver.mkTerm(Kind.SeqUnit, i1) - s3 = solver.mkTerm(Kind.SeqUnit, i1) - s4 = solver.mkTerm(Kind.SeqUnit, i2) - s5 = solver.mkTerm(Kind.SeqConcat, s2, - solver.mkTerm(Kind.SeqConcat, s3, s4)) + s2 = solver.mkTerm(Kind.SEQ_UNIT, i1) + s3 = solver.mkTerm(Kind.SEQ_UNIT, i1) + s4 = solver.mkTerm(Kind.SEQ_UNIT, i2) + s5 = solver.mkTerm(Kind.SEQ_CONCAT, s2, + solver.mkTerm(Kind.SEQ_CONCAT, s3, s4)) assert s1.isSequenceValue() assert not s2.isSequenceValue() @@ -1265,18 +1266,18 @@ def test_const_array(solver): one = solver.mkInteger(1) constarr = solver.mkConstArray(arrsort, one) - assert constarr.getKind() == Kind.ConstArray + assert constarr.getKind() == Kind.CONST_ARRAY assert constarr.getConstArrayBase() == one with pytest.raises(RuntimeError): a.getConstArrayBase() arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) zero_array = solver.mkConstArray(arrsort, solver.mkReal(0)) - stores = solver.mkTerm(Kind.Store, zero_array, solver.mkReal(1), + stores = solver.mkTerm(Kind.STORE, zero_array, solver.mkReal(1), solver.mkReal(2)) - stores = solver.mkTerm(Kind.Store, stores, solver.mkReal(2), + stores = solver.mkTerm(Kind.STORE, stores, solver.mkReal(2), solver.mkReal(3)) - stores = solver.mkTerm(Kind.Store, stores, solver.mkReal(4), + stores = solver.mkTerm(Kind.STORE, stores, solver.mkReal(4), solver.mkReal(5)) @@ -1285,14 +1286,14 @@ def test_const_sequence_elements(solver): seqsort = solver.mkSequenceSort(realsort) s = solver.mkEmptySequence(seqsort) - assert s.getKind() == Kind.ConstSequence + assert s.getKind() == Kind.CONST_SEQUENCE # empty sequence has zero elements cs = s.getSequenceValue() assert len(cs) == 0 # A seq.unit app is not a constant sequence (regardless of whether it is # applied to a constant). - su = solver.mkTerm(Kind.SeqUnit, solver.mkReal(1)) + su = solver.mkTerm(Kind.SEQ_UNIT, solver.mkReal(1)) with pytest.raises(RuntimeError): su.getSequenceValue() diff --git a/test/unit/api/python/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py index 69de847ca..42f8bccbf 100644 --- a/test/unit/api/python/test_to_python_obj.py +++ b/test/unit/api/python/test_to_python_obj.py @@ -54,9 +54,12 @@ def testGetArray(): solver = cvc5.Solver() arrsort = solver.mkArraySort(solver.getIntegerSort(), solver.getIntegerSort()) zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0)) - stores = solver.mkTerm(Kind.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2)) - stores = solver.mkTerm(Kind.Store, stores, solver.mkInteger(2), solver.mkInteger(3)) - stores = solver.mkTerm(Kind.Store, stores, solver.mkInteger(4), solver.mkInteger(5)) + stores = solver.mkTerm( + Kind.STORE, zero_array, solver.mkInteger(1), solver.mkInteger(2)) + stores = solver.mkTerm( + Kind.STORE, stores, solver.mkInteger(2), solver.mkInteger(3)) + stores = solver.mkTerm( + Kind.STORE, stores, solver.mkInteger(4), solver.mkInteger(5)) array_dict = stores.toPythonObj() @@ -90,7 +93,7 @@ def testGetValueInt(): intsort = solver.getIntegerSort() x = solver.mkConst(intsort, "x") - solver.assertFormula(solver.mkTerm(Kind.Equal, x, solver.mkInteger(6))) + solver.assertFormula(solver.mkTerm(Kind.EQUAL, x, solver.mkInteger(6))) r = solver.checkSat() assert r.isSat() @@ -106,8 +109,8 @@ def testGetValueReal(): realsort = solver.getRealSort() x = solver.mkConst(realsort, "x") y = solver.mkConst(realsort, "y") - solver.assertFormula(solver.mkTerm(Kind.Equal, x, solver.mkReal("6"))) - solver.assertFormula(solver.mkTerm(Kind.Equal, y, solver.mkReal("8.33"))) + solver.assertFormula(solver.mkTerm(Kind.EQUAL, x, solver.mkReal("6"))) + solver.assertFormula(solver.mkTerm(Kind.EQUAL, y, solver.mkReal("8.33"))) r = solver.checkSat() assert r.isSat() -- 2.30.2