diff options
Diffstat (limited to 'examples/api/python/bitvectors.py')
| -rw-r--r-- | examples/api/python/bitvectors.py | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py index 15973472c..1ddb02d8e 100644 --- a/examples/api/python/bitvectors.py +++ b/examples/api/python/bitvectors.py @@ -16,11 +16,11 @@ # bitvectors-new.cpp. ## -import pycvc4 -from pycvc4 import kinds +import pycvc5 +from pycvc5 import kinds if __name__ == "__main__": - slv = pycvc4.Solver() + slv = pycvc5.Solver() slv.setLogic("QF_BV") # Set the logic # The following example has been adapted from the book A Hacker's Delight by # Henry S. Warren. @@ -38,7 +38,7 @@ if __name__ == "__main__": # #(2) x = a + b - x; # - # We will use CVC4 to prove that the three pieces of code above are all + # We will use cvc5 to prove that the three pieces of code above are all # equivalent by encoding the problem in the bit-vector theory. # Creating a bit-vector type of width 32 @@ -69,7 +69,7 @@ if __name__ == "__main__": assignment0 = slv.mkTerm(kinds.Equal, new_x, ite) # Assert the encoding of code (0) - print("Asserting {} to CVC4".format(assignment0)) + print("Asserting {} to cvc5".format(assignment0)) slv.assertFormula(assignment0) print("Pushing a new context.") slv.push() @@ -79,14 +79,14 @@ if __name__ == "__main__": a_xor_b_xor_x = slv.mkTerm(kinds.BVXor, a, b, x) assignment1 = slv.mkTerm(kinds.Equal, new_x_, a_xor_b_xor_x) - # Assert encoding to CVC4 in current context - print("Asserting {} to CVC4".format(assignment1)) + # 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_) print("Checking entailment assuming:", new_x_eq_new_x_) print("Expect ENTAILED.") - print("CVC4:", slv.checkEntailed(new_x_eq_new_x_)) + print("cvc5:", slv.checkEntailed(new_x_eq_new_x_)) print("Popping context.") slv.pop() @@ -96,20 +96,20 @@ if __name__ == "__main__": 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) - # Assert encoding to CVC4 in current context - print("Asserting {} to CVC4".format(assignment2)) + # Assert encoding to cvc5 in current context + print("Asserting {} to cvc5".format(assignment2)) slv.assertFormula(assignment2) print("Checking entailment assuming:", new_x_eq_new_x_) print("Expect ENTAILED.") - print("CVC4:", slv.checkEntailed(new_x_eq_new_x_)) + print("cvc5:", slv.checkEntailed(new_x_eq_new_x_)) x_neq_x = slv.mkTerm(kinds.Equal, x, x).notTerm() v = [new_x_eq_new_x_, x_neq_x] print("Check entailment assuming: ", v) print("Expect NOT_ENTAILED.") - print("CVC4:", slv.checkEntailed(v)) + print("cvc5:", slv.checkEntailed(v)) # Assert that a is odd extract_op = slv.mkOp(kinds.BVExtract, 0, 0) @@ -120,4 +120,4 @@ if __name__ == "__main__": print("Check satisifiability") slv.assertFormula(a_odd) print("Expect sat") - print("CVC4:", slv.checkSat()) + print("cvc5:", slv.checkSat()) |