Theory of Bit-Vectors
examples/api/cpp/bitvectors.cpp
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Liana Hadarean, Aina Niemetz, Mathias Preiner
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of the solving capabilities of the cvc5
14 * bit-vector solver.
15 *
16 */
17
18 #include <cvc5/cvc5.h>
19
20 #include <iostream>
21
22 using namespace std;
23 using namespace cvc5;
24
25 int main()
26 {
27 Solver slv;
28 slv.setLogic("QF_BV"); // Set the logic
29
30 // The following example has been adapted from the book A Hacker's Delight by
31 // Henry S. Warren.
32 //
33 // Given a variable x that can only have two values, a or b. We want to
34 // assign to x a value other than the current one. The straightforward code
35 // to do that is:
36 //
37 //(0) if (x == a ) x = b;
38 // else x = a;
39 //
40 // Two more efficient yet equivalent methods are:
41 //
42 //(1) x = a ⊕ b ⊕ x;
43 //
44 //(2) x = a + b - x;
45 //
46 // We will use cvc5 to prove that the three pieces of code above are all
47 // equivalent by encoding the problem in the bit-vector theory.
48
49 // Creating a bit-vector type of width 32
50 Sort bitvector32 = slv.mkBitVectorSort(32);
51
52 // Variables
53 Term x = slv.mkConst(bitvector32, "x");
54 Term a = slv.mkConst(bitvector32, "a");
55 Term b = slv.mkConst(bitvector32, "b");
56
57 // First encode the assumption that x must be equal to a or b
58 Term x_eq_a = slv.mkTerm(EQUAL, {x, a});
59 Term x_eq_b = slv.mkTerm(EQUAL, {x, b});
60 Term assumption = slv.mkTerm(OR, {x_eq_a, x_eq_b});
61
62 // Assert the assumption
63 slv.assertFormula(assumption);
64
65 // Introduce a new variable for the new value of x after assignment.
66 Term new_x = slv.mkConst(bitvector32, "new_x"); // x after executing code (0)
67 Term new_x_ =
68 slv.mkConst(bitvector32, "new_x_"); // x after executing code (1) or (2)
69
70 // Encoding code (0)
71 // new_x = x == a ? b : a;
72 Term ite = slv.mkTerm(ITE, {x_eq_a, b, a});
73 Term assignment0 = slv.mkTerm(EQUAL, {new_x, ite});
74
75 // Assert the encoding of code (0)
76 cout << "Asserting " << assignment0 << " to cvc5 " << endl;
77 slv.assertFormula(assignment0);
78 cout << "Pushing a new context." << endl;
79 slv.push();
80
81 // Encoding code (1)
82 // new_x_ = a xor b xor x
83 Term a_xor_b_xor_x = slv.mkTerm(BITVECTOR_XOR, {a, b, x});
84 Term assignment1 = slv.mkTerm(EQUAL, {new_x_, a_xor_b_xor_x});
85
86 // Assert encoding to cvc5 in current context;
87 cout << "Asserting " << assignment1 << " to cvc5 " << endl;
88 slv.assertFormula(assignment1);
89 Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, {new_x, new_x_});
90
91 cout << " Check sat assuming: " << new_x_eq_new_x_.notTerm() << endl;
92 cout << " Expect UNSAT. " << endl;
93 cout << " cvc5: " << slv.checkSatAssuming(new_x_eq_new_x_.notTerm()) << endl;
94 cout << " Popping context. " << endl;
95 slv.pop();
96
97 // Encoding code (2)
98 // new_x_ = a + b - x
99 Term a_plus_b = slv.mkTerm(BITVECTOR_ADD, {a, b});
100 Term a_plus_b_minus_x = slv.mkTerm(BITVECTOR_SUB, {a_plus_b, x});
101 Term assignment2 = slv.mkTerm(EQUAL, {new_x_, a_plus_b_minus_x});
102
103 // Assert encoding to cvc5 in current context;
104 cout << "Asserting " << assignment2 << " to cvc5 " << endl;
105 slv.assertFormula(assignment2);
106
107 cout << " Check sat assuming: " << new_x_eq_new_x_.notTerm() << endl;
108 cout << " Expect UNSAT. " << endl;
109 cout << " cvc5: " << slv.checkSatAssuming(new_x_eq_new_x_.notTerm()) << endl;
110
111 Term x_neq_x = slv.mkTerm(EQUAL, {x, x}).notTerm();
112 std::vector<Term> v{new_x_eq_new_x_, x_neq_x};
113 Term query = slv.mkTerm(AND, {v});
114 cout << " Check sat assuming: " << query.notTerm() << endl;
115 cout << " Expect SAT. " << endl;
116 cout << " cvc5: " << slv.checkSatAssuming(query.notTerm()) << endl;
117
118 // Assert that a is odd
119 Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, {0, 0});
120 Term lsb_of_a = slv.mkTerm(extract_op, {a});
121 cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl;
122 Term a_odd = slv.mkTerm(EQUAL, {lsb_of_a, slv.mkBitVector(1u, 1u)});
123 cout << "Assert " << a_odd << endl;
124 cout << "Check satisfiability." << endl;
125 slv.assertFormula(a_odd);
126 cout << " Expect sat. " << endl;
127 cout << " cvc5: " << slv.checkSat() << endl;
128 return 0;
129 }
examples/api/java/BitVectors.java
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Liana Hadarean, Morgan Deters
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of the solving capabilities of the cvc5
14 * bit-vector solver.
15 *
16 */
17
18 import io.github.cvc5.*;
19 import java.util.*;
20
21 public class BitVectors
22 {
23 public static void main(String args[]) throws CVC5ApiException
24 {
25 try (Solver slv = new Solver())
26 {
27 slv.setLogic("QF_BV"); // Set the logic
28
29 // The following example has been adapted from the book A Hacker's Delight by
30 // Henry S. Warren.
31 //
32 // Given a variable x that can only have two values, a or b. We want to
33 // assign to x a value other than the current one. The straightforward code
34 // to do that is:
35 //
36 //(0) if (x == a ) x = b;
37 // else x = a;
38 //
39 // Two more efficient yet equivalent methods are:
40 //
41 //(1) x = a ⊕ b ⊕ x;
42 //
43 //(2) x = a + b - x;
44 //
45 // We will use cvc5 to prove that the three pieces of code above are all
46 // equivalent by encoding the problem in the bit-vector theory.
47
48 // Creating a bit-vector type of width 32
49 Sort bitvector32 = slv.mkBitVectorSort(32);
50
51 // Variables
52 Term x = slv.mkConst(bitvector32, "x");
53 Term a = slv.mkConst(bitvector32, "a");
54 Term b = slv.mkConst(bitvector32, "b");
55
56 // First encode the assumption that x must be Kind.EQUAL to a or b
57 Term x_eq_a = slv.mkTerm(Kind.EQUAL, x, a);
58 Term x_eq_b = slv.mkTerm(Kind.EQUAL, x, b);
59 Term assumption = slv.mkTerm(Kind.OR, x_eq_a, x_eq_b);
60
61 // Assert the assumption
62 slv.assertFormula(assumption);
63
64 // Introduce a new variable for the new value of x after assignment.
65 Term new_x = slv.mkConst(bitvector32, "new_x"); // x after executing code (0)
66 Term new_x_ = slv.mkConst(bitvector32, "new_x_"); // x after executing code (1) or (2)
67
68 // Encoding code (0)
69 // new_x = x == a ? b : a;
70 Term ite = slv.mkTerm(Kind.ITE, x_eq_a, b, a);
71 Term assignment0 = slv.mkTerm(Kind.EQUAL, new_x, ite);
72
73 // Assert the encoding of code (0)
74 System.out.println("Asserting " + assignment0 + " to cvc5 ");
75 slv.assertFormula(assignment0);
76 System.out.println("Pushing a new context.");
77 slv.push();
78
79 // Encoding code (1)
80 // new_x_ = a xor b xor x
81 Term a_xor_b_xor_x = slv.mkTerm(Kind.BITVECTOR_XOR, a, b, x);
82 Term assignment1 = slv.mkTerm(Kind.EQUAL, new_x_, a_xor_b_xor_x);
83
84 // Assert encoding to cvc5 in current context;
85 System.out.println("Asserting " + assignment1 + " to cvc5 ");
86 slv.assertFormula(assignment1);
87 Term new_x_eq_new_x_ = slv.mkTerm(Kind.EQUAL, new_x, new_x_);
88
89 System.out.println(" Check sat assuming: " + new_x_eq_new_x_.notTerm());
90 System.out.println(" Expect UNSAT. ");
91 System.out.println(" cvc5: " + slv.checkSatAssuming(new_x_eq_new_x_.notTerm()));
92 System.out.println(" Popping context. ");
93 slv.pop();
94
95 // Encoding code (2)
96 // new_x_ = a + b - x
97 Term a_plus_b = slv.mkTerm(Kind.BITVECTOR_ADD, a, b);
98 Term a_plus_b_minus_x = slv.mkTerm(Kind.BITVECTOR_SUB, a_plus_b, x);
99 Term assignment2 = slv.mkTerm(Kind.EQUAL, new_x_, a_plus_b_minus_x);
100
101 // Assert encoding to cvc5 in current context;
102 System.out.println("Asserting " + assignment2 + " to cvc5 ");
103 slv.assertFormula(assignment2);
104
105 System.out.println(" Check sat assuming: " + new_x_eq_new_x_.notTerm());
106 System.out.println(" Expect UNSAT. ");
107 System.out.println(" cvc5: " + slv.checkSatAssuming(new_x_eq_new_x_.notTerm()));
108
109 Term x_neq_x = slv.mkTerm(Kind.EQUAL, x, x).notTerm();
110 Term[] v = new Term[] {new_x_eq_new_x_, x_neq_x};
111 Term query = slv.mkTerm(Kind.AND, v);
112 System.out.println(" Check sat assuming: " + query.notTerm());
113 System.out.println(" Expect SAT. ");
114 System.out.println(" cvc5: " + slv.checkSatAssuming(query.notTerm()));
115
116 // Assert that a is odd
117 Op extract_op = slv.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0);
118 Term lsb_of_a = slv.mkTerm(extract_op, a);
119 System.out.println("Sort of " + lsb_of_a + " is " + lsb_of_a.getSort());
120 Term a_odd = slv.mkTerm(Kind.EQUAL, lsb_of_a, slv.mkBitVector(1, 1));
121 System.out.println("Assert " + a_odd);
122 System.out.println("Check satisfiability.");
123 slv.assertFormula(a_odd);
124 System.out.println(" Expect sat. ");
125 System.out.println(" cvc5: " + slv.checkSat());
126 }
127 }
128 }
examples/api/python/pythonic/bitvectors.py
1 from cvc5.pythonic import *
2
3 if __name__ == '__main__':
4 # The following example has been adapted from the book A Hacker's Delight
5 # by Henry S. Warren.
6 #
7 # Given a variable x that can only have two values, a or b. We want to
8 # assign to x a value other than the current one. The straightforward code
9 # to do that is:
10 #
11 # (0) if (x == a ) x = b;
12 # else x = a;
13 #
14 # Two more efficient yet equivalent methods are:
15 #
16 # (1) x = a xor b xor x;
17 #
18 # (2) x = a + b - x;
19 #
20 # We will use cvc5 to prove that the three pieces of code above are all
21 # equivalent by encoding the problem in the bit-vector theory.
22
23 x, a, b = BitVecs('x a b', 32)
24 x_is_a_or_b = Or(x == a, x == b)
25
26 # new_x0 set per (0)
27 new_x0 = If(x == a, b, a)
28 # new_x1 set per (1)
29 new_x1 = a ^ b ^ x
30 # new_x2 set per (2)
31 new_x2 = a + b - x
32
33 prove(Implies(x_is_a_or_b, new_x0 == new_x1))
34
35 prove(Implies(x_is_a_or_b, new_x0 == new_x2))
examples/api/python/bitvectors.py
1 #!/usr/bin/env python
2 ###############################################################################
3 # Top contributors (to current version):
4 # Makai Mann, Aina Niemetz, Andrew Reynolds
5 #
6 # This file is part of the cvc5 project.
7 #
8 # Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
9 # in the top-level source directory and their institutional affiliations.
10 # All rights reserved. See the file COPYING in the top-level source
11 # directory for licensing information.
12 # #############################################################################
13 #
14 # A simple demonstration of the solving capabilities of the cvc5 bit-vector
15 # solver through the Python API. This is a direct translation of
16 # bitvectors-new.cpp.
17 ##
18
19 import cvc5
20 from cvc5 import Kind
21
22 if __name__ == "__main__":
23 slv = cvc5.Solver()
24 slv.setLogic("QF_BV") # Set the logic
25 # The following example has been adapted from the book A Hacker's Delight by
26 # Henry S. Warren.
27 #
28 # Given a variable x that can only have two values, a or b. We want to
29 # assign to x a value other than the current one. The straightforward code
30 # to do that is:
31 #
32 #(0) if (x == a ) x = b;
33 # else x = a;
34 #
35 # Two more efficient yet equivalent methods are:
36 #
37 #(1) x = a xor b xor x;
38 #
39 #(2) x = a + b - x;
40 #
41 # We will use cvc5 to prove that the three pieces of code above are all
42 # equivalent by encoding the problem in the bit-vector theory.
43
44 # Creating a bit-vector type of width 32
45 bitvector32 = slv.mkBitVectorSort(32)
46
47 # Variables
48 x = slv.mkConst(bitvector32, "x")
49 a = slv.mkConst(bitvector32, "a")
50 b = slv.mkConst(bitvector32, "b")
51
52 # First encode the assumption that x must be equal to a or b
53 x_eq_a = slv.mkTerm(Kind.EQUAL, x, a)
54 x_eq_b = slv.mkTerm(Kind.EQUAL, x, b)
55 assumption = slv.mkTerm(Kind.OR, x_eq_a, x_eq_b)
56
57 # Assert the assumption
58 slv.assertFormula(assumption)
59
60 # Introduce a new variable for the new value of x after assignment.
61 # x after executing code (0)
62 new_x = slv.mkConst(bitvector32, "new_x")
63 # x after executing code (1) or (2)
64 new_x_ = slv.mkConst(bitvector32, "new_x_")
65
66 # Encoding code (0)
67 # new_x = x == a ? b : a
68 ite = slv.mkTerm(Kind.ITE, x_eq_a, b, a)
69 assignment0 = slv.mkTerm(Kind.EQUAL, new_x, ite)
70
71 # Assert the encoding of code (0)
72 print("Asserting {} to cvc5".format(assignment0))
73 slv.assertFormula(assignment0)
74 print("Pushing a new context.")
75 slv.push()
76
77 # Encoding code (1)
78 # new_x_ = a xor b xor x
79 a_xor_b_xor_x = slv.mkTerm(Kind.BITVECTOR_XOR, a, b, x)
80 assignment1 = slv.mkTerm(Kind.EQUAL, new_x_, a_xor_b_xor_x)
81
82 # Assert encoding to cvc5 in current context
83 print("Asserting {} to cvc5".format(assignment1))
84 slv.assertFormula(assignment1)
85 new_x_eq_new_x_ = slv.mkTerm(Kind.EQUAL, new_x, new_x_)
86
87 print("Checking sat assuming:", new_x_eq_new_x_.notTerm())
88 print("Expect UNSAT.")
89 print("cvc5:", slv.checkSatAssuming(new_x_eq_new_x_.notTerm()))
90 print("Popping context.")
91 slv.pop()
92
93 # Encoding code (2)
94 # new_x_ = a + b - x
95 a_plus_b = slv.mkTerm(Kind.BITVECTOR_ADD, a, b)
96 a_plus_b_minus_x = slv.mkTerm(Kind.BITVECTOR_SUB, a_plus_b, x)
97 assignment2 = slv.mkTerm(Kind.EQUAL, new_x_, a_plus_b_minus_x)
98
99 # Assert encoding to cvc5 in current context
100 print("Asserting {} to cvc5".format(assignment2))
101 slv.assertFormula(assignment2)
102
103 print("Checking sat assuming:", new_x_eq_new_x_.notTerm())
104 print("Expect UNSAT.")
105 print("cvc5:", slv.checkSatAssuming(new_x_eq_new_x_.notTerm()))
106
107
108 x_neq_x = slv.mkTerm(Kind.EQUAL, x, x).notTerm()
109 query = slv.mkTerm(Kind.AND, new_x_eq_new_x_, x_neq_x)
110 print("Check sat assuming: ", query.notTerm())
111 print("Expect SAT.")
112 print("cvc5:", slv.checkSatAssuming(query.notTerm()))
113
114 # Assert that a is odd
115 extract_op = slv.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0)
116 lsb_of_a = slv.mkTerm(extract_op, a)
117 print("Sort of {} is {}".format(lsb_of_a, lsb_of_a.getSort()))
118 a_odd = slv.mkTerm(Kind.EQUAL, lsb_of_a, slv.mkBitVector(1, 1))
119 print("Assert", a_odd)
120 print("Check satisifiability")
121 slv.assertFormula(a_odd)
122 print("Expect sat")
123 print("cvc5:", slv.checkSat())
examples/api/smtlib/bitvectors.smt2
1 (set-logic QF_BV)
2 (set-option :incremental true)
3
4 (declare-const x (_ BitVec 32))
5 (declare-const a (_ BitVec 32))
6 (declare-const b (_ BitVec 32))
7 (declare-const new_x (_ BitVec 32))
8 (declare-const new_x_ (_ BitVec 32))
9
10 (echo "Assert the assumption.")
11 (assert (or (= x a) (= x b)))
12
13 (echo "Asserting assignment to cvc5.")
14 (assert (= new_x (ite (= x a) b a)))
15
16 (echo "Pushing a new context.")
17 (push 1)
18
19 (echo "Asserting another assignment to cvc5.")
20 (assert (= new_x_ (bvxor a b x)))
21
22 (echo "Check entailment assuming new_x = new_x_.")
23 (echo "UNSAT (of negation) == ENTAILED")
24 (check-sat-assuming ((not (= new_x new_x_))))
25 (echo "Popping context.")
26 (pop 1)
27
28 (echo "Asserting another assignment to cvc5.")
29 (assert (= new_x_ (bvsub (bvadd a b) x)))
30
31 (echo "Check entailment assuming new_x = new_x_.")
32 (echo "UNSAT (of negation) == ENTAILED")
33 (check-sat-assuming ((not (= new_x new_x_))))
34
35 (echo "Check entailment assuming [new_x = new_x_, x != x.")
36 (echo "UNSAT (of negation) == ENTAILED")
37 (check-sat-assuming ((not (= new_x new_x_)) (not (= x x))))
38
39 (echo "Assert that a is odd, i.e. lsb is one.")
40 (assert (= ((_ extract 0 0) a) (_ bv1 1)))
41 (echo "Check satisfiability, expecting sat.")
42 (check-sat)