Theory of Bit-Vectors:
extract
¶
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Mathias Preiner, Aina Niemetz, Clark Barrett
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 Sort bitvector32 = slv.mkBitVectorSort(32);
31
32 Term x = slv.mkConst(bitvector32, "a");
33
34 Op ext_31_1 = slv.mkOp(BITVECTOR_EXTRACT, {31, 1});
35 Term x_31_1 = slv.mkTerm(ext_31_1, {x});
36
37 Op ext_30_0 = slv.mkOp(BITVECTOR_EXTRACT, {30, 0});
38 Term x_30_0 = slv.mkTerm(ext_30_0, {x});
39
40 Op ext_31_31 = slv.mkOp(BITVECTOR_EXTRACT, {31, 31});
41 Term x_31_31 = slv.mkTerm(ext_31_31, {x});
42
43 Op ext_0_0 = slv.mkOp(BITVECTOR_EXTRACT, {0, 0});
44 Term x_0_0 = slv.mkTerm(ext_0_0, {x});
45
46 Term eq = slv.mkTerm(EQUAL, {x_31_1, x_30_0});
47 cout << " Asserting: " << eq << endl;
48 slv.assertFormula(eq);
49
50 Term eq2 = slv.mkTerm(EQUAL, {x_31_31, x_0_0});
51 cout << " Check sat assuming: " << eq2.notTerm() << endl;
52 cout << " Expect UNSAT. " << endl;
53 cout << " cvc5: " << slv.checkSatAssuming(eq2.notTerm()) << endl;
54
55 return 0;
56 }
examples/api/java/Extract.java
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Andrew Reynolds, Andres Noetzli
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
20 public class Extract
21 {
22 public static void main(String args[]) throws CVC5ApiException
23 {
24 try (Solver slv = new Solver())
25 {
26 slv.setLogic("QF_BV"); // Set the logic
27
28 Sort bitvector32 = slv.mkBitVectorSort(32);
29
30 Term x = slv.mkConst(bitvector32, "a");
31
32 Op ext_31_1 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1);
33 Term x_31_1 = slv.mkTerm(ext_31_1, x);
34
35 Op ext_30_0 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 30, 0);
36 Term x_30_0 = slv.mkTerm(ext_30_0, x);
37
38 Op ext_31_31 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 31, 31);
39 Term x_31_31 = slv.mkTerm(ext_31_31, x);
40
41 Op ext_0_0 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0);
42 Term x_0_0 = slv.mkTerm(ext_0_0, x);
43
44 Term eq = slv.mkTerm(Kind.EQUAL, x_31_1, x_30_0);
45 System.out.println(" Asserting: " + eq);
46 slv.assertFormula(eq);
47
48 Term eq2 = slv.mkTerm(Kind.EQUAL, x_31_31, x_0_0);
49 System.out.println(" Check entailment assuming: " + eq2);
50 System.out.println(" Expect UNSAT. ");
51 System.out.println(" cvc5: " + slv.checkSatAssuming(eq2.notTerm()));
52 }
53 }
54 }
examples/api/python/pythonic/extract.py
1 from cvc5.pythonic import *
2
3 if __name__ == '__main__':
4 x = BitVec('x', 32)
5
6 # Consider the bits of x: 01234567
7 # (we assume 8 bits to make the visualization simple)
8 #
9 # If 1234567
10 # equals 0123456
11 #
12 # then 0 == 7 (by induction over the bits)
13
14 prove(Implies(Extract(31, 1, x) == Extract(30, 0, x),
15 Extract(31, 31, x) == Extract(0, 0, x)))
examples/api/python/extract.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 # extract-new.cpp.
17 ##
18
19 from cvc5 import Solver, Kind
20
21 if __name__ == "__main__":
22 slv = Solver()
23 slv.setLogic("QF_BV")
24
25 bitvector32 = slv.mkBitVectorSort(32)
26
27 x = slv.mkConst(bitvector32, "a")
28
29 ext_31_1 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1)
30 x_31_1 = slv.mkTerm(ext_31_1, x)
31
32 ext_30_0 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 30, 0)
33 x_30_0 = slv.mkTerm(ext_30_0, x)
34
35 ext_31_31 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 31, 31)
36 x_31_31 = slv.mkTerm(ext_31_31, x)
37
38 ext_0_0 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0)
39 x_0_0 = slv.mkTerm(ext_0_0, x)
40
41 eq = slv.mkTerm(Kind.EQUAL, x_31_1, x_30_0)
42 print("Asserting:", eq)
43 slv.assertFormula(eq)
44
45 eq2 = slv.mkTerm(Kind.EQUAL, x_31_31, x_0_0)
46 print("Check sat assuming:", eq2.notTerm())
47 print("Expect UNSAT")
48 print("cvc5:", slv.checkSatAssuming(eq2.notTerm()))
examples/api/smtlib/extract.smt2
1 (set-logic QF_BV)
2
3 (declare-const a (_ BitVec 32))
4
5 (define-const a_31_1 (_ BitVec 31) ((_ extract 31 1) a))
6 (define-const a_30_0 (_ BitVec 31) ((_ extract 30 0) a))
7 (define-const a_31_31 (_ BitVec 1) ((_ extract 31 31) a))
8 (define-const a_0_0 (_ BitVec 1) ((_ extract 0 0) a))
9
10 (echo "Asserting a_31_1 = a_30_0")
11 (assert (= a_31_1 a_30_0))
12
13 (echo "Check unsatisfiability assuming a_31_31 != a_0_0")
14 (check-sat-assuming ((not (= a_31_31 a_0_0))))