diff options
Diffstat (limited to 'examples')
-rw-r--r-- | examples/api/java/QuickStart.java | 31 | ||||
-rw-r--r-- | examples/api/java/Relations.java | 5 | ||||
-rw-r--r-- | examples/api/python/bitvectors.py | 30 | ||||
-rw-r--r-- | examples/api/python/bitvectors_and_arrays.py | 18 | ||||
-rw-r--r-- | examples/api/python/combination.py | 22 | ||||
-rw-r--r-- | examples/api/python/datatypes.py | 18 | ||||
-rw-r--r-- | examples/api/python/exceptions.py | 2 | ||||
-rw-r--r-- | examples/api/python/extract.py | 15 | ||||
-rw-r--r-- | examples/api/python/floating_point.py | 28 | ||||
-rw-r--r-- | examples/api/python/helloworld.py | 2 | ||||
-rw-r--r-- | examples/api/python/id.py | 1 | ||||
-rw-r--r-- | examples/api/python/linear_arith.py | 18 | ||||
-rw-r--r-- | examples/api/python/quickstart.py | 22 | ||||
-rw-r--r-- | examples/api/python/sequences.py | 14 | ||||
-rw-r--r-- | examples/api/python/sets.py | 30 | ||||
-rw-r--r-- | examples/api/python/strings.py | 34 | ||||
-rw-r--r-- | examples/api/python/sygus-fun.py | 26 | ||||
-rw-r--r-- | examples/api/python/sygus-grammar.py | 16 | ||||
-rw-r--r-- | examples/api/python/sygus-inv.py | 14 | ||||
-rw-r--r-- | examples/api/python/transcendentals.py | 14 | ||||
-rw-r--r-- | examples/api/python/utils.py | 4 |
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" |