Theory of Bit-Vectors: extract
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Clark Barrett, 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 Sort bitvector32 = tm.mkBitVectorSort(32);
32
33 Term x = tm.mkConst(bitvector32, "a");
34
35 Op ext_31_1 = tm.mkOp(Kind::BITVECTOR_EXTRACT, {31, 1});
36 Term x_31_1 = tm.mkTerm(ext_31_1, {x});
37
38 Op ext_30_0 = tm.mkOp(Kind::BITVECTOR_EXTRACT, {30, 0});
39 Term x_30_0 = tm.mkTerm(ext_30_0, {x});
40
41 Op ext_31_31 = tm.mkOp(Kind::BITVECTOR_EXTRACT, {31, 31});
42 Term x_31_31 = tm.mkTerm(ext_31_31, {x});
43
44 Op ext_0_0 = tm.mkOp(Kind::BITVECTOR_EXTRACT, {0, 0});
45 Term x_0_0 = tm.mkTerm(ext_0_0, {x});
46
47 Term eq = tm.mkTerm(Kind::EQUAL, {x_31_1, x_30_0});
48 cout << " Asserting: " << eq << endl;
49 slv.assertFormula(eq);
50
51 Term eq2 = tm.mkTerm(Kind::EQUAL, {x_31_31, x_0_0});
52 cout << " Check sat assuming: " << eq2.notTerm() << endl;
53 cout << " Expect UNSAT. " << endl;
54 cout << " cvc5: " << slv.checkSatAssuming(eq2.notTerm()) << endl;
55
56 return 0;
57}
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-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.*;
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 Context.deletePointers();
54 }
55}
examples/api/python/pythonic/extract.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 x = BitVec('x', 32)
20
21 # Consider the bits of x: 01234567
22 # (we assume 8 bits to make the visualization simple)
23 #
24 # If 1234567
25 # equals 0123456
26 #
27 # then 0 == 7 (by induction over the bits)
28
29 prove(Implies(Extract(31, 1, x) == Extract(30, 0, x),
30 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-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# extract-new.cpp.
17##
18
19from cvc5 import TermManager, Solver, Kind
20
21if __name__ == "__main__":
22 tm = TermManager()
23 slv = Solver(tm)
24 slv.setLogic("QF_BV")
25
26 bitvector32 = tm.mkBitVectorSort(32)
27
28 x = tm.mkConst(bitvector32, "a")
29
30 ext_31_1 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1)
31 x_31_1 = tm.mkTerm(ext_31_1, x)
32
33 ext_30_0 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 30, 0)
34 x_30_0 = tm.mkTerm(ext_30_0, x)
35
36 ext_31_31 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 31, 31)
37 x_31_31 = tm.mkTerm(ext_31_31, x)
38
39 ext_0_0 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0)
40 x_0_0 = tm.mkTerm(ext_0_0, x)
41
42 eq = tm.mkTerm(Kind.EQUAL, x_31_1, x_30_0)
43 print("Asserting:", eq)
44 slv.assertFormula(eq)
45
46 eq2 = tm.mkTerm(Kind.EQUAL, x_31_31, x_0_0)
47 print("Check sat assuming:", eq2.notTerm())
48 print("Expect UNSAT")
49 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))))