Theory of Bit-Vectors: extract
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of the solving capabilities of the cvc5
11 * bit-vector solver.
12 *
13 */
14
15#include <cvc5/cvc5.h>
16
17#include <iostream>
18
19using namespace std;
20using namespace cvc5;
21
22int main()
23{
24 TermManager tm;
25 Solver slv(tm);
26 slv.setLogic("QF_BV"); // Set the logic
27
28 Sort bv32 = tm.mkBitVectorSort(32);
29
30 Term x = tm.mkConst(bv32, "x");
31
32 Op ext_31_1 = tm.mkOp(Kind::BITVECTOR_EXTRACT, {31, 1});
33 Term x_31_1 = tm.mkTerm(ext_31_1, {x});
34
35 Op ext_30_0 = tm.mkOp(Kind::BITVECTOR_EXTRACT, {30, 0});
36 Term x_30_0 = tm.mkTerm(ext_30_0, {x});
37
38 Op ext_31_31 = tm.mkOp(Kind::BITVECTOR_EXTRACT, {31, 31});
39 Term x_31_31 = tm.mkTerm(ext_31_31, {x});
40
41 Op ext_0_0 = tm.mkOp(Kind::BITVECTOR_EXTRACT, {0, 0});
42 Term x_0_0 = tm.mkTerm(ext_0_0, {x});
43
44 Term eq = tm.mkTerm(Kind::EQUAL, {x_31_1, x_30_0});
45 cout << " Asserting: " << eq << endl;
46 slv.assertFormula(eq);
47
48 Term dis = tm.mkTerm(Kind::DISTINCT, {x_31_31, x_0_0});
49 cout << " Check sat assuming: " << dis << endl;
50 cout << " Expect UNSAT." << endl;
51 cout << " cvc5: " << slv.checkSatAssuming(dis) << endl;
52
53 return 0;
54}
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of the solving capabilities of the cvc5
11 * bit-vector solver.
12 *
13 */
14
15#include <cvc5/c/cvc5.h>
16#include <stdio.h>
17
18int main()
19{
20 Cvc5TermManager* tm = cvc5_term_manager_new();
21 Cvc5* slv = cvc5_new(tm);
22 cvc5_set_logic(slv, "QF_BV");
23
24 Cvc5Sort bv32 = cvc5_mk_bv_sort(tm, 32);
25
26 Cvc5Term x = cvc5_mk_const(tm, bv32, "x");
27
28 uint32_t idxs[2] = {31, 1};
29 Cvc5Op ext_31_1 = cvc5_mk_op(tm, CVC5_KIND_BITVECTOR_EXTRACT, 2, idxs);
30 Cvc5Term args1[1] = {x};
31 Cvc5Term x_31_1 = cvc5_mk_term_from_op(tm, ext_31_1, 1, args1);
32
33 idxs[0] = 30;
34 idxs[1] = 0;
35 Cvc5Op ext_30_0 = cvc5_mk_op(tm, CVC5_KIND_BITVECTOR_EXTRACT, 2, idxs);
36 Cvc5Term x_30_0 = cvc5_mk_term_from_op(tm, ext_30_0, 1, args1);
37
38 idxs[0] = 31;
39 idxs[1] = 31;
40 Cvc5Op ext_31_31 = cvc5_mk_op(tm, CVC5_KIND_BITVECTOR_EXTRACT, 2, idxs);
41 Cvc5Term x_31_31 = cvc5_mk_term_from_op(tm, ext_31_31, 1, args1);
42
43 idxs[0] = 0;
44 idxs[1] = 0;
45 Cvc5Op ext_0_0 = cvc5_mk_op(tm, CVC5_KIND_BITVECTOR_EXTRACT, 2, idxs);
46 Cvc5Term x_0_0 = cvc5_mk_term_from_op(tm, ext_0_0, 1, args1);
47
48 Cvc5Term args2[2] = {x_31_1, x_30_0};
49 Cvc5Term eq = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
50 printf(" Asserting: %s\n", cvc5_term_to_string(eq));
51 cvc5_assert_formula(slv, eq);
52
53 args2[0] = x_31_31;
54 args2[1] = x_0_0;
55 Cvc5Term dis = cvc5_mk_term(tm, CVC5_KIND_DISTINCT, 2, args2);
56 printf(" Check sat assuming: %s\n", cvc5_term_to_string(dis));
57 printf(" Expect UNSAT.\n");
58 Cvc5Term assumptions[1] = {dis};
59 printf(" cvc5: %s\n",
60 cvc5_result_to_string(cvc5_check_sat_assuming(slv, 1, assumptions)));
61
62 cvc5_delete(slv);
63 cvc5_term_manager_delete(tm);
64 return 0;
65}
examples/api/java/Extract.java
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of the solving capabilities of the cvc5
11 * bit-vector solver.
12 *
13 */
14
15import io.github.cvc5.*;
16
17public class Extract
18{
19 public static void main(String args[]) throws CVC5ApiException
20 {
21 TermManager tm = new TermManager();
22 Solver slv = new Solver(tm);
23 {
24 slv.setLogic("QF_BV"); // Set the logic
25
26 Sort bitvector32 = tm.mkBitVectorSort(32);
27
28 Term x = tm.mkConst(bitvector32, "a");
29
30 Op ext_31_1 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1);
31 Term x_31_1 = tm.mkTerm(ext_31_1, x);
32
33 Op ext_30_0 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 30, 0);
34 Term x_30_0 = tm.mkTerm(ext_30_0, x);
35
36 Op ext_31_31 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 31, 31);
37 Term x_31_31 = tm.mkTerm(ext_31_31, x);
38
39 Op ext_0_0 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0);
40 Term x_0_0 = tm.mkTerm(ext_0_0, x);
41
42 Term eq = tm.mkTerm(Kind.EQUAL, x_31_1, x_30_0);
43 System.out.println(" Asserting: " + eq);
44 slv.assertFormula(eq);
45
46 Term eq2 = tm.mkTerm(Kind.EQUAL, x_31_31, x_0_0);
47 System.out.println(" Check entailment assuming: " + eq2);
48 System.out.println(" Expect UNSAT. ");
49 System.out.println(" cvc5: " + slv.checkSatAssuming(eq2.notTerm()));
50 }
51 Context.deletePointers();
52 }
53}
examples/api/python/pythonic/extract.py
1###############################################################################
2# This file is part of the cvc5 project.
3#
4# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5# in the top-level source directory and their institutional affiliations.
6# All rights reserved. See the file COPYING in the top-level source
7# directory for licensing information.
8# #############################################################################
9#
10# A simple demonstration of the solving capabilities of the cvc5
11# bit-vector solver.
12##
13from cvc5.pythonic import *
14
15if __name__ == '__main__':
16 x = BitVec('x', 32)
17
18 # Consider the bits of x: 01234567
19 # (we assume 8 bits to make the visualization simple)
20 #
21 # If 1234567
22 # equals 0123456
23 #
24 # then 0 == 7 (by induction over the bits)
25
26 prove(Implies(Extract(31, 1, x) == Extract(30, 0, x),
27 Extract(31, 31, x) == Extract(0, 0, x)))
examples/api/python/extract.py
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# A simple demonstration of the solving capabilities of the cvc5 bit-vector
12# solver through the Python API. This is a direct translation of
13# extract-new.cpp.
14##
15
16from cvc5 import TermManager, Solver, Kind
17
18if __name__ == "__main__":
19 tm = TermManager()
20 slv = Solver(tm)
21 slv.setLogic("QF_BV")
22
23 bitvector32 = tm.mkBitVectorSort(32)
24
25 x = tm.mkConst(bitvector32, "a")
26
27 ext_31_1 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1)
28 x_31_1 = tm.mkTerm(ext_31_1, x)
29
30 ext_30_0 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 30, 0)
31 x_30_0 = tm.mkTerm(ext_30_0, x)
32
33 ext_31_31 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 31, 31)
34 x_31_31 = tm.mkTerm(ext_31_31, x)
35
36 ext_0_0 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0)
37 x_0_0 = tm.mkTerm(ext_0_0, x)
38
39 eq = tm.mkTerm(Kind.EQUAL, x_31_1, x_30_0)
40 print("Asserting:", eq)
41 slv.assertFormula(eq)
42
43 eq2 = tm.mkTerm(Kind.EQUAL, x_31_31, x_0_0)
44 print("Check sat assuming:", eq2.notTerm())
45 print("Expect UNSAT")
46 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))))