Theory of Bit-Vectors
examples/api/cpp/bitvectors.cpp
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Liana Hadarean, Andrew Reynolds
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 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
22using namespace std;
23using namespace cvc5;
24
25int main()
26{
27 TermManager tm;
28 Solver slv(tm);
29 slv.setLogic("QF_BV"); // Set the logic
30
31 // The following example has been adapted from the book A Hacker's Delight by
32 // Henry S. Warren.
33 //
34 // Given a variable x that can only have two values, a or b. We want to
35 // assign to x a value other than the current one. The straightforward code
36 // to do that is:
37 //
38 //(0) if (x == a ) x = b;
39 // else x = a;
40 //
41 // Two more efficient yet equivalent methods are:
42 //
43 //(1) x = a ⊕ b ⊕ x;
44 //
45 //(2) x = a + b - x;
46 //
47 // We will use cvc5 to prove that the three pieces of code above are all
48 // equivalent by encoding the problem in the bit-vector theory.
49
50 // Creating a bit-vector type of width 32
51 Sort bitvector32 = tm.mkBitVectorSort(32);
52
53 // Variables
54 Term x = tm.mkConst(bitvector32, "x");
55 Term a = tm.mkConst(bitvector32, "a");
56 Term b = tm.mkConst(bitvector32, "b");
57
58 // First encode the assumption that x must be equal to a or b
59 Term x_eq_a = tm.mkTerm(Kind::EQUAL, {x, a});
60 Term x_eq_b = tm.mkTerm(Kind::EQUAL, {x, b});
61 Term assumption = tm.mkTerm(Kind::OR, {x_eq_a, x_eq_b});
62
63 // Assert the assumption
64 slv.assertFormula(assumption);
65
66 // Introduce a new variable for the new value of x after assignment.
67 Term new_x = tm.mkConst(bitvector32, "new_x"); // x after executing code (0)
68 Term new_x_ =
69 tm.mkConst(bitvector32, "new_x_"); // x after executing code (1) or (2)
70
71 // Encoding code (0)
72 // new_x = x == a ? b : a;
73 Term ite = tm.mkTerm(Kind::ITE, {x_eq_a, b, a});
74 Term assignment0 = tm.mkTerm(Kind::EQUAL, {new_x, ite});
75
76 // Assert the encoding of code (0)
77 cout << "Asserting " << assignment0 << " to cvc5 " << endl;
78 slv.assertFormula(assignment0);
79 cout << "Pushing a new context." << endl;
80 slv.push();
81
82 // Encoding code (1)
83 // new_x_ = a xor b xor x
84 Term a_xor_b_xor_x = tm.mkTerm(Kind::BITVECTOR_XOR, {a, b, x});
85 Term assignment1 = tm.mkTerm(Kind::EQUAL, {new_x_, a_xor_b_xor_x});
86
87 // Assert encoding to cvc5 in current context;
88 cout << "Asserting " << assignment1 << " to cvc5 " << endl;
89 slv.assertFormula(assignment1);
90 Term new_x_eq_new_x_ = tm.mkTerm(Kind::EQUAL, {new_x, new_x_});
91
92 cout << " Check sat assuming: " << new_x_eq_new_x_.notTerm() << endl;
93 cout << " Expect UNSAT. " << endl;
94 cout << " cvc5: " << slv.checkSatAssuming(new_x_eq_new_x_.notTerm()) << endl;
95 cout << " Popping context. " << endl;
96 slv.pop();
97
98 // Encoding code (2)
99 // new_x_ = a + b - x
100 Term a_plus_b = tm.mkTerm(Kind::BITVECTOR_ADD, {a, b});
101 Term a_plus_b_minus_x = tm.mkTerm(Kind::BITVECTOR_SUB, {a_plus_b, x});
102 Term assignment2 = tm.mkTerm(Kind::EQUAL, {new_x_, a_plus_b_minus_x});
103
104 // Assert encoding to cvc5 in current context;
105 cout << "Asserting " << assignment2 << " to cvc5 " << endl;
106 slv.assertFormula(assignment2);
107
108 cout << " Check sat assuming: " << new_x_eq_new_x_.notTerm() << endl;
109 cout << " Expect UNSAT. " << endl;
110 cout << " cvc5: " << slv.checkSatAssuming(new_x_eq_new_x_.notTerm()) << endl;
111
112 Term x_neq_x = tm.mkTerm(Kind::EQUAL, {x, x}).notTerm();
113 std::vector<Term> v{new_x_eq_new_x_, x_neq_x};
114 Term query = tm.mkTerm(Kind::AND, {v});
115 cout << " Check sat assuming: " << query.notTerm() << endl;
116 cout << " Expect SAT. " << endl;
117 cout << " cvc5: " << slv.checkSatAssuming(query.notTerm()) << endl;
118
119 // Assert that a is odd
120 Op extract_op = tm.mkOp(Kind::BITVECTOR_EXTRACT, {0, 0});
121 Term lsb_of_a = tm.mkTerm(extract_op, {a});
122 cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl;
123 Term a_odd = tm.mkTerm(Kind::EQUAL, {lsb_of_a, tm.mkBitVector(1u, 1u)});
124 cout << "Assert " << a_odd << endl;
125 cout << "Check satisfiability." << endl;
126 slv.assertFormula(a_odd);
127 cout << " Expect sat. " << endl;
128 cout << " cvc5: " << slv.checkSat() << endl;
129 return 0;
130}
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-2024 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
18import io.github.cvc5.*;
19import java.util.*;
20
21public class BitVectors
22{
23 public static void main(String args[]) throws CVC5ApiException
24 {
25 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 Context.deletePointers();
128 }
129}
examples/api/python/pythonic/bitvectors.py
1###############################################################################
2# Top contributors (to current version):
3# Alex Ozdemir
4#
5# This file is part of the cvc5 project.
6#
7# Copyright (c) 2009-2024 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##
16from cvc5.pythonic import *
17
18if __name__ == '__main__':
19 # The following example has been adapted from the book A Hacker's Delight
20 # by Henry S. Warren.
21 #
22 # Given a variable x that can only have two values, a or b. We want to
23 # assign to x a value other than the current one. The straightforward code
24 # to do that is:
25 #
26 # (0) if (x == a ) x = b;
27 # else x = a;
28 #
29 # Two more efficient yet equivalent methods are:
30 #
31 # (1) x = a xor b xor x;
32 #
33 # (2) x = a + b - x;
34 #
35 # We will use cvc5 to prove that the three pieces of code above are all
36 # equivalent by encoding the problem in the bit-vector theory.
37
38 x, a, b = BitVecs('x a b', 32)
39 x_is_a_or_b = Or(x == a, x == b)
40
41 # new_x0 set per (0)
42 new_x0 = If(x == a, b, a)
43 # new_x1 set per (1)
44 new_x1 = a ^ b ^ x
45 # new_x2 set per (2)
46 new_x2 = a + b - x
47
48 prove(Implies(x_is_a_or_b, new_x0 == new_x1))
49
50 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-2024 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
19import cvc5
20from cvc5 import Kind
21
22if __name__ == "__main__":
23 tm = cvc5.TermManager()
24 slv = cvc5.Solver(tm)
25 slv.setLogic("QF_BV") # Set the logic
26 # The following example has been adapted from the book A Hacker's Delight by
27 # Henry S. Warren.
28 #
29 # Given a variable x that can only have two values, a or b. We want to
30 # assign to x a value other than the current one. The straightforward code
31 # to do that is:
32 #
33 #(0) if (x == a ) x = b;
34 # else x = a;
35 #
36 # Two more efficient yet equivalent methods are:
37 #
38 #(1) x = a xor b xor x;
39 #
40 #(2) x = a + b - x;
41 #
42 # We will use cvc5 to prove that the three pieces of code above are all
43 # equivalent by encoding the problem in the bit-vector theory.
44
45 # Creating a bit-vector type of width 32
46 bitvector32 = tm.mkBitVectorSort(32)
47
48 # Variables
49 x = tm.mkConst(bitvector32, "x")
50 a = tm.mkConst(bitvector32, "a")
51 b = tm.mkConst(bitvector32, "b")
52
53 # First encode the assumption that x must be equal to a or b
54 x_eq_a = tm.mkTerm(Kind.EQUAL, x, a)
55 x_eq_b = tm.mkTerm(Kind.EQUAL, x, b)
56 assumption = tm.mkTerm(Kind.OR, x_eq_a, x_eq_b)
57
58 # Assert the assumption
59 slv.assertFormula(assumption)
60
61 # Introduce a new variable for the new value of x after assignment.
62 # x after executing code (0)
63 new_x = tm.mkConst(bitvector32, "new_x")
64 # x after executing code (1) or (2)
65 new_x_ = tm.mkConst(bitvector32, "new_x_")
66
67 # Encoding code (0)
68 # new_x = x == a ? b : a
69 ite = tm.mkTerm(Kind.ITE, x_eq_a, b, a)
70 assignment0 = tm.mkTerm(Kind.EQUAL, new_x, ite)
71
72 # Assert the encoding of code (0)
73 print("Asserting {} to cvc5".format(assignment0))
74 slv.assertFormula(assignment0)
75 print("Pushing a new context.")
76 slv.push()
77
78 # Encoding code (1)
79 # new_x_ = a xor b xor x
80 a_xor_b_xor_x = tm.mkTerm(Kind.BITVECTOR_XOR, a, b, x)
81 assignment1 = tm.mkTerm(Kind.EQUAL, new_x_, a_xor_b_xor_x)
82
83 # Assert encoding to cvc5 in current context
84 print("Asserting {} to cvc5".format(assignment1))
85 slv.assertFormula(assignment1)
86 new_x_eq_new_x_ = tm.mkTerm(Kind.EQUAL, new_x, new_x_)
87
88 print("Checking sat assuming:", new_x_eq_new_x_.notTerm())
89 print("Expect UNSAT.")
90 print("cvc5:", slv.checkSatAssuming(new_x_eq_new_x_.notTerm()))
91 print("Popping context.")
92 slv.pop()
93
94 # Encoding code (2)
95 # new_x_ = a + b - x
96 a_plus_b = tm.mkTerm(Kind.BITVECTOR_ADD, a, b)
97 a_plus_b_minus_x = tm.mkTerm(Kind.BITVECTOR_SUB, a_plus_b, x)
98 assignment2 = tm.mkTerm(Kind.EQUAL, new_x_, a_plus_b_minus_x)
99
100 # Assert encoding to cvc5 in current context
101 print("Asserting {} to cvc5".format(assignment2))
102 slv.assertFormula(assignment2)
103
104 print("Checking sat assuming:", new_x_eq_new_x_.notTerm())
105 print("Expect UNSAT.")
106 print("cvc5:", slv.checkSatAssuming(new_x_eq_new_x_.notTerm()))
107
108
109 x_neq_x = tm.mkTerm(Kind.EQUAL, x, x).notTerm()
110 query = tm.mkTerm(Kind.AND, new_x_eq_new_x_, x_neq_x)
111 print("Check sat assuming: ", query.notTerm())
112 print("Expect SAT.")
113 print("cvc5:", slv.checkSatAssuming(query.notTerm()))
114
115 # Assert that a is odd
116 extract_op = tm.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0)
117 lsb_of_a = tm.mkTerm(extract_op, a)
118 print("Sort of {} is {}".format(lsb_of_a, lsb_of_a.getSort()))
119 a_odd = tm.mkTerm(Kind.EQUAL, lsb_of_a, tm.mkBitVector(1, 1))
120 print("Assert", a_odd)
121 print("Check satisifiability")
122 slv.assertFormula(a_odd)
123 print("Expect sat")
124 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)