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
22using namespace std;
23using namespace cvc5;
24
25int 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(Kind::BITVECTOR_EXTRACT, {31, 1});
35 Term x_31_1 = slv.mkTerm(ext_31_1, {x});
36
37 Op ext_30_0 = slv.mkOp(Kind::BITVECTOR_EXTRACT, {30, 0});
38 Term x_30_0 = slv.mkTerm(ext_30_0, {x});
39
40 Op ext_31_31 = slv.mkOp(Kind::BITVECTOR_EXTRACT, {31, 31});
41 Term x_31_31 = slv.mkTerm(ext_31_31, {x});
42
43 Op ext_0_0 = slv.mkOp(Kind::BITVECTOR_EXTRACT, {0, 0});
44 Term x_0_0 = slv.mkTerm(ext_0_0, {x});
45
46 Term eq = slv.mkTerm(Kind::EQUAL, {x_31_1, x_30_0});
47 cout << " Asserting: " << eq << endl;
48 slv.assertFormula(eq);
49
50 Term eq2 = slv.mkTerm(Kind::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
18import io.github.cvc5.*;
19
20public class Extract
21{
22 public static void main(String args[]) throws CVC5ApiException
23 {
24 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
1from cvc5.pythonic import *
2
3if __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
19from cvc5 import Solver, Kind
20
21if __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))))