.. 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:
.. literalinclude:: ../../../../examples/api/python/quickstart.py
:language: python
- :lines: 150-152
+ :lines: 151-153
This will print:
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)))
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"|}
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))
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)
# 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))
# 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.")
# 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))
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)
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)
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))
)
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")
# 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,
# 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)))
# 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
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.")
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()))
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')
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())
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.")
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)
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:",
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")
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);
# 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
# 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();
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)
# 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)
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.
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)
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)
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])
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()):
# 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})
# 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()):
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})
# 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)
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"
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`',
}
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:],
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))
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)
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())
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)
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())
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)
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())
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())
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)
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)
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"
# 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
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()
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()
# 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()
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()
# 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
def test_supports_floating_point(solver):
- solver.mkRoundingMode(RoundingMode.RoundNearestTiesToEven)
+ solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN)
def test_get_boolean_sort(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()
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):
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):
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):
# 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)
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")
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):
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):
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]
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()
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()
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()
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()
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()
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)))
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")
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()
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)
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")
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):
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())
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)
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()
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
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)
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
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()
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()
# (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()
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)
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)
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)
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]
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()
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())
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)
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()
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
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
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]
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):
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)
-
-
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):
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
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()
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):
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()
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()
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):
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):
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)
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)
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):
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):
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)
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)
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):
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):
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)
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)
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):
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):
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)
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)
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):
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):
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)
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)
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):
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
# 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)
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)
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)
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
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)
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()
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):
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()
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()
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))
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()
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()
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()
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()
projects / cvc5.git / commitdiff