summaryrefslogtreecommitdiff
path: root/examples
diff options
context:
space:
mode:
Diffstat (limited to 'examples')
-rw-r--r--examples/api/java/QuickStart.java31
-rw-r--r--examples/api/java/Relations.java5
-rw-r--r--examples/api/python/bitvectors.py30
-rw-r--r--examples/api/python/bitvectors_and_arrays.py18
-rw-r--r--examples/api/python/combination.py22
-rw-r--r--examples/api/python/datatypes.py18
-rw-r--r--examples/api/python/exceptions.py2
-rw-r--r--examples/api/python/extract.py15
-rw-r--r--examples/api/python/floating_point.py28
-rw-r--r--examples/api/python/helloworld.py2
-rw-r--r--examples/api/python/id.py1
-rw-r--r--examples/api/python/linear_arith.py18
-rw-r--r--examples/api/python/quickstart.py22
-rw-r--r--examples/api/python/sequences.py14
-rw-r--r--examples/api/python/sets.py30
-rw-r--r--examples/api/python/strings.py34
-rw-r--r--examples/api/python/sygus-fun.py26
-rw-r--r--examples/api/python/sygus-grammar.py16
-rw-r--r--examples/api/python/sygus-inv.py14
-rw-r--r--examples/api/python/transcendentals.py14
-rw-r--r--examples/api/python/utils.py4
21 files changed, 191 insertions, 173 deletions
diff --git a/examples/api/java/QuickStart.java b/examples/api/java/QuickStart.java
index a79263cbf..c815278cc 100644
--- a/examples/api/java/QuickStart.java
+++ b/examples/api/java/QuickStart.java
@@ -106,11 +106,32 @@ public class QuickStart
Term xMinusY = solver.mkTerm(Kind.MINUS, x, y);
Term xMinusYVal = solver.getValue(xMinusY);
- // Further, we can convert the values to java types,
- Pair<BigInteger, BigInteger> xRational = xVal.getRealValue();
- Pair<BigInteger, BigInteger> yRational = yVal.getRealValue();
- System.out.println("value for x: " + xRational.first + "/" + xRational.second);
- System.out.println("value for y: " + yRational.first + "/" + yRational.second);
+ // Further, we can convert the values to java types
+ Pair<BigInteger, BigInteger> xPair = xVal.getRealValue();
+ Pair<BigInteger, BigInteger> yPair = yVal.getRealValue();
+ Pair<BigInteger, BigInteger> xMinusYPair = xMinusYVal.getRealValue();
+
+ System.out.println("value for x: " + xPair.first + "/" + xPair.second);
+ System.out.println("value for y: " + yPair.first + "/" + yPair.second);
+ System.out.println("value for x - y: " + xMinusYPair.first + "/" + xMinusYPair.second);
+
+ // Another way to independently compute the value of x - y would be
+ // to perform the (rational) arithmetic manually.
+ // However, for more complex terms,
+ // it is easier to let the solver do the evaluation.
+ Pair<BigInteger, BigInteger> xMinusYComputed =
+ new Pair(xPair.first.multiply(yPair.second).subtract(xPair.second.multiply(yPair.first)),
+ xPair.second.multiply(yPair.second));
+ BigInteger g = xMinusYComputed.first.gcd(xMinusYComputed.second);
+ xMinusYComputed = new Pair(xMinusYComputed.first.divide(g), xMinusYComputed.second.divide(g));
+ if (xMinusYComputed.equals(xMinusYPair))
+ {
+ System.out.println("computed correctly");
+ }
+ else
+ {
+ System.out.println("computed incorrectly");
+ }
// Next, we will check satisfiability of the same formula,
// only this time over integer variables a and b.
diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java
index a3e2b2a7e..95aede591 100644
--- a/examples/api/java/Relations.java
+++ b/examples/api/java/Relations.java
@@ -152,10 +152,9 @@ public class Relations
Term transpose = solver.mkTerm(RELATION_TRANSPOSE, descendant);
Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose);
- // (assert (forall ((x Person)) (not (set.member (mkTuple x x) ancestor))))
+ // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
Term x = solver.mkVar(personSort, "x");
- DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0);
- Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), x, x);
+ Term xxTuple = solver.mkTuple(new Sort[]{personSort, personSort}, new Term[] {x, x});
Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor);
Term notMember = solver.mkTerm(NOT, member);
diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py
index ff99bd785..e785fd790 100644
--- a/examples/api/python/bitvectors.py
+++ b/examples/api/python/bitvectors.py
@@ -17,7 +17,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
@@ -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(kinds.Equal, x, a)
- x_eq_b = slv.mkTerm(kinds.Equal, x, b)
- assumption = slv.mkTerm(kinds.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(kinds.Ite, x_eq_a, b, a)
- assignment0 = slv.mkTerm(kinds.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(kinds.BVXor, a, b, x)
- assignment1 = slv.mkTerm(kinds.Equal, 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)
# Assert encoding to cvc5 in current context
print("Asserting {} to cvc5".format(assignment1))
slv.assertFormula(assignment1)
- new_x_eq_new_x_ = slv.mkTerm(kinds.Equal, new_x, new_x_)
+ new_x_eq_new_x_ = slv.mkTerm(Kind.Equal, new_x, new_x_)
print("Checking entailment assuming:", new_x_eq_new_x_)
print("Expect ENTAILED.")
@@ -92,9 +92,9 @@ if __name__ == "__main__":
# Encoding code (2)
# new_x_ = a + b - x
- a_plus_b = slv.mkTerm(kinds.BVAdd, a, b)
- a_plus_b_minus_x = slv.mkTerm(kinds.BVSub, a_plus_b, x)
- assignment2 = slv.mkTerm(kinds.Equal, new_x_, a_plus_b_minus_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)
# Assert encoding to cvc5 in current context
print("Asserting {} to cvc5".format(assignment2))
@@ -105,17 +105,17 @@ if __name__ == "__main__":
print("cvc5:", slv.checkEntailed(new_x_eq_new_x_))
- x_neq_x = slv.mkTerm(kinds.Equal, x, x).notTerm()
+ x_neq_x = slv.mkTerm(Kind.Equal, x, x).notTerm()
v = [new_x_eq_new_x_, x_neq_x]
print("Check entailment assuming: ", v)
print("Expect NOT_ENTAILED.")
print("cvc5:", slv.checkEntailed(v))
# Assert that a is odd
- extract_op = slv.mkOp(kinds.BVExtract, 0, 0)
+ extract_op = slv.mkOp(Kind.BVExtract, 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(kinds.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 be38077ca..d3c8caf75 100644
--- a/examples/api/python/bitvectors_and_arrays.py
+++ b/examples/api/python/bitvectors_and_arrays.py
@@ -17,7 +17,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
import math
@@ -58,29 +58,29 @@ if __name__ == "__main__":
constarr0 = slv.mkConstArray(arraySort, slv.mkBitVector(32, 0))
# Asserting that current_array[0] > 0
- current_array0 = slv.mkTerm(kinds.Select, current_array, zero)
- current_array0_gt_0 = slv.mkTerm(kinds.BVSgt,
+ current_array0 = slv.mkTerm(Kind.Select, current_array, zero)
+ current_array0_gt_0 = slv.mkTerm(Kind.BVSgt,
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(kinds.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(kinds.BVMult, two, old_current)
+ new_current = slv.mkTerm(Kind.BVMult, two, old_current)
# current[i] = 2*current[i-1]
- current_array = slv.mkTerm(kinds.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(kinds.BVSlt, old_current, new_current)
+ current_slt_new_current = slv.mkTerm(Kind.BVSlt, old_current, new_current)
assertions.append(current_slt_new_current)
- old_current = slv.mkTerm(kinds.Select, current_array, index)
+ old_current = slv.mkTerm(Kind.Select, current_array, index)
- query = slv.mkTerm(kinds.Not, slv.mkTerm(kinds.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 990149434..bceb7e738 100644
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -17,7 +17,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
def prefixPrintGetValue(slv, t, level=0):
print("slv.getValue({}): {}".format(t, slv.getValue(t)))
@@ -51,18 +51,18 @@ if __name__ == "__main__":
one = slv.mkInteger(1)
# Terms
- f_x = slv.mkTerm(kinds.ApplyUf, f, x)
- f_y = slv.mkTerm(kinds.ApplyUf, f, y)
- sum_ = slv.mkTerm(kinds.Plus, f_x, f_y)
- p_0 = slv.mkTerm(kinds.ApplyUf, p, zero)
- p_f_y = slv.mkTerm(kinds.ApplyUf, p, f_y)
+ f_x = slv.mkTerm(Kind.ApplyUf, f, x)
+ f_y = slv.mkTerm(Kind.ApplyUf, f, y)
+ sum_ = slv.mkTerm(Kind.Plus, f_x, f_y)
+ p_0 = slv.mkTerm(Kind.ApplyUf, p, zero)
+ p_f_y = slv.mkTerm(Kind.ApplyUf, p, f_y)
# Construct the assertions
- assertions = slv.mkTerm(kinds.And,
+ assertions = slv.mkTerm(Kind.And,
[
- slv.mkTerm(kinds.Leq, zero, f_x), # 0 <= f(x)
- slv.mkTerm(kinds.Leq, zero, f_y), # 0 <= f(y)
- slv.mkTerm(kinds.Leq, sum_, one), # f(x) + f(y) <= 1
+ 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))
])
@@ -71,7 +71,7 @@ if __name__ == "__main__":
print("Given the following assertions:", assertions, "\n")
print("Prove x /= y is entailed.\ncvc5: ",
- slv.checkEntailed(slv.mkTerm(kinds.Distinct, x, y)), "\n")
+ slv.checkEntailed(slv.mkTerm(Kind.Distinct, 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 96116da08..cc4ca719a 100644
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -17,7 +17,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
def test(slv, consListSort):
# Now our old "consListSpec" is useless--the relevant information
@@ -34,9 +34,9 @@ def test(slv, consListSort):
# which is equivalent to consList["cons"].getConstructor(). Note that
# "nil" is a constructor too
- t = slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("cons"),
+ t = slv.mkTerm(Kind.ApplyConstructor, consList.getConstructorTerm("cons"),
slv.mkInteger(0),
- slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("nil")))
+ slv.mkTerm(Kind.ApplyConstructor, consList.getConstructorTerm("nil")))
print("t is {}\nsort of cons is {}\n sort of nil is {}".format(
t,
@@ -49,7 +49,7 @@ def test(slv, consListSort):
# consList["cons"]) in order to get the "head" selector symbol
# to apply.
- t2 = slv.mkTerm(kinds.ApplySelector, consList["cons"].getSelectorTerm("head"), t)
+ t2 = slv.mkTerm(Kind.ApplySelector, consList["cons"].getSelectorTerm("head"), t)
print("t2 is {}\nsimplify(t2) is {}\n\n".format(t2, slv.simplify(t2)))
@@ -63,16 +63,16 @@ def test(slv, consListSort):
# You can also define a tester term for constructor 'cons': (_ is cons)
t_is_cons = slv.mkTerm(
- kinds.ApplyTester, consList["cons"].getTesterTerm(), t)
+ Kind.ApplyTester, 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(kinds.ApplyUpdater,
+ t_updated = slv.mkTerm(Kind.ApplyUpdater,
consList["cons"]["head"].getUpdaterTerm(),
t,
slv.mkInteger(1))
print("t_updated is {}\n\n".format(t_updated))
- slv.assertFormula(slv.mkTerm(kinds.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 +93,11 @@ def test(slv, consListSort):
a = slv.mkConst(paramConsIntListSort, "a")
print("term {} is of sort {}".format(a, a.getSort()))
- head_a = slv.mkTerm(kinds.ApplySelector, paramConsList["cons"].getSelectorTerm("head"), a)
+ head_a = slv.mkTerm(Kind.ApplySelector, 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(kinds.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/exceptions.py b/examples/api/python/exceptions.py
index a4597d12b..dcfff09e4 100644
--- a/examples/api/python/exceptions.py
+++ b/examples/api/python/exceptions.py
@@ -17,7 +17,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
import sys
diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py
index 4e7026e97..fa7350285 100644
--- a/examples/api/python/extract.py
+++ b/examples/api/python/extract.py
@@ -16,8 +16,7 @@
# extract-new.cpp.
##
-from pycvc5 import Solver
-from pycvc5.kinds import BVExtract, Equal
+from pycvc5 import Solver, Kind
if __name__ == "__main__":
slv = Solver()
@@ -27,26 +26,26 @@ if __name__ == "__main__":
x = slv.mkConst(bitvector32, "a")
- ext_31_1 = slv.mkOp(BVExtract, 31, 1)
+ ext_31_1 = slv.mkOp(Kind.BVExtract, 31, 1)
x_31_1 = slv.mkTerm(ext_31_1, x)
- ext_30_0 = slv.mkOp(BVExtract, 30, 0)
+ ext_30_0 = slv.mkOp(Kind.BVExtract, 30, 0)
x_30_0 = slv.mkTerm(ext_30_0, x)
- ext_31_31 = slv.mkOp(BVExtract, 31, 31)
+ ext_31_31 = slv.mkOp(Kind.BVExtract, 31, 31)
x_31_31 = slv.mkTerm(ext_31_31, x)
- ext_0_0 = slv.mkOp(BVExtract, 0, 0)
+ ext_0_0 = slv.mkOp(Kind.BVExtract, 0, 0)
x_0_0 = slv.mkTerm(ext_0_0, x)
# test getting indices
assert ext_30_0.getIndices() == (30, 0)
- eq = slv.mkTerm(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(Equal, x_31_31, x_0_0)
+ eq2 = slv.mkTerm(Kind.Equal, x_31_31, x_0_0)
print("Check entailment assuming:", eq2)
print("Expect ENTAILED")
print("cvc5:", slv.checkEntailed(eq2))
diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py
index d6ba8d754..29f0d16d7 100644
--- a/examples/api/python/floating_point.py
+++ b/examples/api/python/floating_point.py
@@ -17,7 +17,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
@@ -37,10 +37,10 @@ if __name__ == "__main__":
z = slv.mkConst(fp32, 'z')
# check floating-point arithmetic is commutative, i.e. x + y == y + x
- commutative = slv.mkTerm(kinds.FPEq, slv.mkTerm(kinds.FPAdd, rm, x, y), slv.mkTerm(kinds.FPAdd, rm, y, x))
+ commutative = slv.mkTerm(Kind.FPEq, slv.mkTerm(Kind.FPAdd, rm, x, y), slv.mkTerm(Kind.FPAdd, rm, y, x))
slv.push()
- slv.assertFormula(slv.mkTerm(kinds.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 +48,10 @@ if __name__ == "__main__":
print("Model for y:", slv.getValue(y))
# disallow NaNs and Infinities
- slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsNan, x)))
- slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsInf, x)))
- slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsNan, y)))
- slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsInf, y)))
+ 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)))
print("Checking floating-point commutativity assuming x and y are not NaN or Infinity")
print("Expect UNSAT.")
@@ -70,15 +70,15 @@ if __name__ == "__main__":
24,
slv.mkBitVector(32, "01000000010010001111010111000011", 2)) # 3.14
- bounds_x = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, x), slv.mkTerm(kinds.FPLeq, x, b))
- bounds_y = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, y), slv.mkTerm(kinds.FPLeq, y, b))
- bounds_z = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, z), slv.mkTerm(kinds.FPLeq, z, b))
- slv.assertFormula(slv.mkTerm(kinds.And, slv.mkTerm(kinds.And, bounds_x, bounds_y), bounds_z))
+ 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))
# (x + y) + z == x + (y + z)
- lhs = slv.mkTerm(kinds.FPAdd, rm, slv.mkTerm(kinds.FPAdd, rm, x, y), z)
- rhs = slv.mkTerm(kinds.FPAdd, rm, x, slv.mkTerm(kinds.FPAdd, rm, y, z))
- associative = slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPEq, lhs, rhs))
+ 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))
slv.assertFormula(associative)
diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py
index 6e6ce32ab..b437efc86 100644
--- a/examples/api/python/helloworld.py
+++ b/examples/api/python/helloworld.py
@@ -15,7 +15,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
diff --git a/examples/api/python/id.py b/examples/api/python/id.py
index fb3672dbc..c7a2ed0bc 100644
--- a/examples/api/python/id.py
+++ b/examples/api/python/id.py
@@ -16,7 +16,6 @@
##
import pycvc5
-from pycvc5 import kinds
if __name__ == "__main__":
slv = pycvc5.Solver()
diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py
index f8dad6a71..a2f303a5d 100644
--- a/examples/api/python/linear_arith.py
+++ b/examples/api/python/linear_arith.py
@@ -17,7 +17,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
@@ -40,21 +40,21 @@ if __name__ == "__main__":
two_thirds = slv.mkReal(2, 3)
# Terms
- three_y = slv.mkTerm(kinds.Mult, three, y)
- diff = slv.mkTerm(kinds.Minus, y, x)
+ three_y = slv.mkTerm(Kind.Mult, three, y)
+ diff = slv.mkTerm(Kind.Minus, y, x)
# Formulas
- x_geq_3y = slv.mkTerm(kinds.Geq, x, three_y)
- x_leq_y = slv.mkTerm(kinds.Leq, x ,y)
- neg2_lt_x = slv.mkTerm(kinds.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(kinds.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(kinds.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 ENTAILED")
print("Result from cvc5 is:",
@@ -64,7 +64,7 @@ if __name__ == "__main__":
print()
slv.push()
- diff_is_two_thirds = slv.mkTerm(kinds.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 389e08be1..8261b3d70 100644
--- a/examples/api/python/quickstart.py
+++ b/examples/api/python/quickstart.py
@@ -15,7 +15,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
# Create a solver
@@ -64,15 +64,15 @@ if __name__ == "__main__":
one = solver.mkReal(1);
# Next, we construct the term x + y
- xPlusY = solver.mkTerm(kinds.Plus, x, y);
+ xPlusY = solver.mkTerm(Kind.Plus, 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(kinds.Lt, zero, x);
- constraint2 = solver.mkTerm(kinds.Lt, zero, y);
- constraint3 = solver.mkTerm(kinds.Lt, xPlusY, one);
- constraint4 = solver.mkTerm(kinds.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(kinds.Minus, x, y);
+ xMinusY = solver.mkTerm(Kind.Minus, x, y);
xMinusYVal = solver.getValue(xMinusY);
# We can now obtain the values as python values
@@ -132,11 +132,11 @@ 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(kinds.Lt, solver.mkInteger(0), a));
- solver.assertFormula(solver.mkTerm(kinds.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(kinds.Lt, solver.mkTerm(kinds.Plus, a, b), solver.mkInteger(1)));
- solver.assertFormula(solver.mkTerm(kinds.Leq, a, b));
+ solver.mkTerm(Kind.Lt, solver.mkTerm(Kind.Plus, 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/sequences.py b/examples/api/python/sequences.py
index f9fd925fb..66a4c1353 100644
--- a/examples/api/python/sequences.py
+++ b/examples/api/python/sequences.py
@@ -16,7 +16,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
@@ -39,18 +39,18 @@ if __name__ == "__main__":
# Empty sequence
empty = slv.mkEmptySequence(slv.getIntegerSort())
# Sequence concatenation: x.y.empty
- concat = slv.mkTerm(kinds.SeqConcat, x, y, empty)
+ concat = slv.mkTerm(Kind.SeqConcat, x, y, empty)
# Sequence length: |x.y.empty|
- concat_len = slv.mkTerm(kinds.SeqLength, concat)
+ concat_len = slv.mkTerm(Kind.SeqLength, concat)
# |x.y.empty| > 1
- formula1 = slv.mkTerm(kinds.Gt, concat_len, slv.mkInteger(1))
+ formula1 = slv.mkTerm(Kind.Gt, concat_len, slv.mkInteger(1))
# Sequence unit: seq(1)
- unit = slv.mkTerm(kinds.SeqUnit, slv.mkInteger(1))
+ unit = slv.mkTerm(Kind.SeqUnit, slv.mkInteger(1))
# x = seq(1)
- formula2 = slv.mkTerm(kinds.Equal, x, unit)
+ formula2 = slv.mkTerm(Kind.Equal, x, unit)
# Make a query
- q = slv.mkTerm(kinds.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 31f20dfeb..4bd6c4029 100644
--- a/examples/api/python/sets.py
+++ b/examples/api/python/sets.py
@@ -16,7 +16,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
@@ -39,14 +39,14 @@ if __name__ == "__main__":
B = slv.mkConst(set_, "B")
C = slv.mkConst(set_, "C")
- unionAB = slv.mkTerm(kinds.SetUnion, A, B)
- lhs = slv.mkTerm(kinds.SetInter, unionAB, C)
+ unionAB = slv.mkTerm(Kind.SetUnion, A, B)
+ lhs = slv.mkTerm(Kind.SetInter, unionAB, C)
- intersectionAC = slv.mkTerm(kinds.SetInter, A, C)
- intersectionBC = slv.mkTerm(kinds.SetInter, B, C)
- rhs = slv.mkTerm(kinds.SetUnion, intersectionAC, intersectionBC)
+ intersectionAC = slv.mkTerm(Kind.SetInter, A, C)
+ intersectionBC = slv.mkTerm(Kind.SetInter, B, C)
+ rhs = slv.mkTerm(Kind.SetUnion, intersectionAC, intersectionBC)
- theorem = slv.mkTerm(kinds.Equal, lhs, rhs)
+ theorem = slv.mkTerm(Kind.Equal, lhs, rhs)
print("cvc5 reports: {} is {}".format(theorem,
slv.checkEntailed(theorem)))
@@ -56,7 +56,7 @@ if __name__ == "__main__":
A = slv.mkConst(set_, "A")
emptyset = slv.mkEmptySet(set_)
- theorem = slv.mkTerm(kinds.SetSubset, emptyset, A)
+ theorem = slv.mkTerm(Kind.SetSubset, emptyset, A)
print("cvc5 reports: {} is {}".format(theorem,
slv.checkEntailed(theorem)))
@@ -67,16 +67,16 @@ if __name__ == "__main__":
two = slv.mkInteger(2)
three = slv.mkInteger(3)
- singleton_one = slv.mkTerm(kinds.SetSingleton, one)
- singleton_two = slv.mkTerm(kinds.SetSingleton, two)
- singleton_three = slv.mkTerm(kinds.SetSingleton, three)
- one_two = slv.mkTerm(kinds.SetUnion, singleton_one, singleton_two)
- two_three = slv.mkTerm(kinds.SetUnion, singleton_two, singleton_three)
- intersection = slv.mkTerm(kinds.SetInter, one_two, two_three)
+ 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)
x = slv.mkConst(integer, "x")
- e = slv.mkTerm(kinds.SetMember, x, intersection)
+ e = slv.mkTerm(Kind.SetMember, x, intersection)
result = slv.checkSatAssuming(e)
diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py
index 64ce06548..c1087eaac 100644
--- a/examples/api/python/strings.py
+++ b/examples/api/python/strings.py
@@ -16,7 +16,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
@@ -43,38 +43,38 @@ if __name__ == "__main__":
z = slv.mkConst(string, "z")
# String concatenation: x.ab.y
- lhs = slv.mkTerm(kinds.StringConcat, x, ab, y)
+ lhs = slv.mkTerm(Kind.StringConcat, x, ab, y)
# String concatenation: abc.z
- rhs = slv.mkTerm(kinds.StringConcat, abc, z)
+ rhs = slv.mkTerm(Kind.StringConcat, abc, z)
# x.ab.y = abc.z
- formula1 = slv.mkTerm(kinds.Equal, lhs, rhs)
+ formula1 = slv.mkTerm(Kind.Equal, lhs, rhs)
# Length of y: |y|
- leny = slv.mkTerm(kinds.StringLength, y)
+ leny = slv.mkTerm(Kind.StringLength, y)
# |y| >= 0
- formula2 = slv.mkTerm(kinds.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(kinds.RegexpUnion,
- slv.mkTerm(kinds.RegexpConcat,
- slv.mkTerm(kinds.StringToRegexp, slv.mkString("ab")),
- slv.mkTerm(kinds.RegexpStar,
- slv.mkTerm(kinds.RegexpRange, slv.mkString("c"), slv.mkString("e"))),
- slv.mkTerm(kinds.StringToRegexp, slv.mkString("f"))),
- slv.mkTerm(kinds.StringToRegexp, slv.mkString("g")),
- slv.mkTerm(kinds.StringToRegexp, slv.mkString("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")))
# String variables
s1 = slv.mkConst(string, "s1")
s2 = slv.mkConst(string, "s2")
# String concatenation: s1.s2
- s = slv.mkTerm(kinds.StringConcat, s1, s2)
+ s = slv.mkTerm(Kind.StringConcat, s1, s2)
# s1.s2 in (ab[c-e]*f)|g|h
- formula3 = slv.mkTerm(kinds.StringInRegexp, s, r)
+ formula3 = slv.mkTerm(Kind.StringInRegexp, s, r)
# Make a query
- q = slv.mkTerm(kinds.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 d2ad1feb4..3cacc33d2 100644
--- a/examples/api/python/sygus-fun.py
+++ b/examples/api/python/sygus-fun.py
@@ -18,7 +18,7 @@
import copy
import pycvc5
import utils
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
@@ -45,13 +45,13 @@ if __name__ == "__main__":
zero = slv.mkInteger(0)
one = slv.mkInteger(1)
- plus = slv.mkTerm(kinds.Plus, start, start)
- minus = slv.mkTerm(kinds.Minus, start, start)
- ite = slv.mkTerm(kinds.Ite, start_bool, start, start)
+ plus = slv.mkTerm(Kind.Plus, start, start)
+ minus = slv.mkTerm(Kind.Minus, start, start)
+ ite = slv.mkTerm(Kind.Ite, start_bool, start, start)
- And = slv.mkTerm(kinds.And, start_bool, start_bool)
- Not = slv.mkTerm(kinds.Not, start_bool)
- leq = slv.mkTerm(kinds.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,25 @@ if __name__ == "__main__":
varX = slv.mkSygusVar(integer, "x")
varY = slv.mkSygusVar(integer, "y")
- max_x_y = slv.mkTerm(kinds.ApplyUf, max, varX, varY)
- min_x_y = slv.mkTerm(kinds.ApplyUf, min, varX, varY)
+ max_x_y = slv.mkTerm(Kind.ApplyUf, max, varX, varY)
+ min_x_y = slv.mkTerm(Kind.ApplyUf, min, varX, varY)
# add semantic constraints
# (constraint (>= (max x y) x))
- slv.addSygusConstraint(slv.mkTerm(kinds.Geq, max_x_y, varX))
+ slv.addSygusConstraint(slv.mkTerm(Kind.Geq, max_x_y, varX))
# (constraint (>= (max x y) y))
- slv.addSygusConstraint(slv.mkTerm(kinds.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(
- kinds.Or, slv.mkTerm(kinds.Equal, max_x_y, varX), slv.mkTerm(kinds.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(
- kinds.Equal, slv.mkTerm(kinds.Plus, max_x_y, min_x_y), slv.mkTerm(kinds.Plus, varX, varY)))
+ Kind.Equal, slv.mkTerm(Kind.Plus, max_x_y, min_x_y), slv.mkTerm(Kind.Plus, varX, varY)))
# print solutions if available
if (slv.checkSynth().isUnsat()):
diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py
index 02a7dff48..466e2cdd3 100644
--- a/examples/api/python/sygus-grammar.py
+++ b/examples/api/python/sygus-grammar.py
@@ -19,7 +19,7 @@
import copy
import utils
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
@@ -42,8 +42,8 @@ if __name__ == "__main__":
# define the rules
zero = slv.mkInteger(0)
- neg_x = slv.mkTerm(kinds.Uminus, x)
- plus = slv.mkTerm(kinds.Plus, x, start)
+ neg_x = slv.mkTerm(Kind.Uminus, x)
+ plus = slv.mkTerm(Kind.Plus, x, start)
# create the grammar object
g1 = slv.mkSygusGrammar({x}, {start})
@@ -72,14 +72,14 @@ if __name__ == "__main__":
# declare universal variables.
varX = slv.mkSygusVar(integer, "x")
- id1_x = slv.mkTerm(kinds.ApplyUf, id1, varX)
- id2_x = slv.mkTerm(kinds.ApplyUf, id2, varX)
- id3_x = slv.mkTerm(kinds.ApplyUf, id3, varX)
- id4_x = slv.mkTerm(kinds.ApplyUf, id4, varX)
+ 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)
# add semantic constraints
# (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x))
- slv.addSygusConstraint(slv.mkTerm(kinds.And, [slv.mkTerm(kinds.Equal, id1_x, id2_x), slv.mkTerm(kinds.Equal, id1_x, id3_x), slv.mkTerm(kinds.Equal, id1_x, id4_x), slv.mkTerm(kinds.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().isUnsat()):
diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py
index 50fa3f04f..3af4ac5ec 100644
--- a/examples/api/python/sygus-inv.py
+++ b/examples/api/python/sygus-inv.py
@@ -18,7 +18,7 @@
import utils
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
@@ -42,15 +42,15 @@ if __name__ == "__main__":
xp = slv.mkVar(integer, "xp")
# (ite (< x 10) (= xp (+ x 1)) (= xp x))
- ite = slv.mkTerm(kinds.Ite,
- slv.mkTerm(kinds.Lt, x, ten),
- slv.mkTerm(kinds.Equal, xp, slv.mkTerm(kinds.Plus, x, one)),
- slv.mkTerm(kinds.Equal, xp, x))
+ ite = slv.mkTerm(Kind.Ite,
+ slv.mkTerm(Kind.Lt, x, ten),
+ slv.mkTerm(Kind.Equal, xp, slv.mkTerm(Kind.Plus, 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(kinds.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(kinds.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 39bb343c7..ffeb0c775 100644
--- a/examples/api/python/transcendentals.py
+++ b/examples/api/python/transcendentals.py
@@ -15,7 +15,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
@@ -30,14 +30,14 @@ if __name__ == "__main__":
# Helper terms
two = slv.mkReal(2)
pi = slv.mkPi()
- twopi = slv.mkTerm(kinds.Mult, two, pi)
- ysq = slv.mkTerm(kinds.Mult, y, y)
- sinx = slv.mkTerm(kinds.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(kinds.Gt, x, pi)
- x_lt_tpi = slv.mkTerm(kinds.Lt, x, twopi)
- ysq_lt_sinx = slv.mkTerm(kinds.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 6d42325b5..cf906bc7a 100644
--- a/examples/api/python/utils.py
+++ b/examples/api/python/utils.py
@@ -15,7 +15,7 @@
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
# Get the string version of define-fun command.
# @param f the function to print
@@ -47,7 +47,7 @@ def print_synth_solutions(terms, sols):
result = ""
for i in range(0, len(terms)):
params = []
- if sols[i].getKind() == kinds.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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback