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 bv32 = tm.mkBitVectorSort(32);
32
33 Term x = tm.mkConst(bv32, "x");
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 dis = tm.mkTerm(Kind::DISTINCT, {x_31_31, x_0_0});
52 cout << " Check sat assuming: " << dis << endl;
53 cout << " Expect UNSAT." << endl;
54 cout << " cvc5: " << slv.checkSatAssuming(dis) << endl;
55
56 return 0;
57}
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz
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/c/cvc5.h>
19#include <stdio.h>
20
21int main()
22{
23 Cvc5TermManager* tm = cvc5_term_manager_new();
24 Cvc5* slv = cvc5_new(tm);
25 cvc5_set_logic(slv, "QF_BV");
26
27 Cvc5Sort bv32 = cvc5_mk_bv_sort(tm, 32);
28
29 Cvc5Term x = cvc5_mk_const(tm, bv32, "x");
30
31 uint32_t idxs[2] = {31, 1};
32 Cvc5Op ext_31_1 = cvc5_mk_op(tm, CVC5_KIND_BITVECTOR_EXTRACT, 2, idxs);
33 Cvc5Term args1[1] = {x};
34 Cvc5Term x_31_1 = cvc5_mk_term_from_op(tm, ext_31_1, 1, args1);
35
36 idxs[0] = 30;
37 idxs[1] = 0;
38 Cvc5Op ext_30_0 = cvc5_mk_op(tm, CVC5_KIND_BITVECTOR_EXTRACT, 2, idxs);
39 Cvc5Term x_30_0 = cvc5_mk_term_from_op(tm, ext_30_0, 1, args1);
40
41 idxs[0] = 31;
42 idxs[1] = 31;
43 Cvc5Op ext_31_31 = cvc5_mk_op(tm, CVC5_KIND_BITVECTOR_EXTRACT, 2, idxs);
44 Cvc5Term x_31_31 = cvc5_mk_term_from_op(tm, ext_31_31, 1, args1);
45
46 idxs[0] = 0;
47 idxs[1] = 0;
48 Cvc5Op ext_0_0 = cvc5_mk_op(tm, CVC5_KIND_BITVECTOR_EXTRACT, 2, idxs);
49 Cvc5Term x_0_0 = cvc5_mk_term_from_op(tm, ext_0_0, 1, args1);
50
51 Cvc5Term args2[2] = {x_31_1, x_30_0};
52 Cvc5Term eq = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
53 printf(" Asserting: %s\n", cvc5_term_to_string(eq));
54 cvc5_assert_formula(slv, eq);
55
56 args2[0] = x_31_31;
57 args2[1] = x_0_0;
58 Cvc5Term dis = cvc5_mk_term(tm, CVC5_KIND_DISTINCT, 2, args2);
59 printf(" Check sat assuming: %s\n", cvc5_term_to_string(dis));
60 printf(" Expect UNSAT.\n");
61 Cvc5Term assumptions[1] = {dis};
62 printf(" cvc5: %s\n",
63 cvc5_result_to_string(cvc5_check_sat_assuming(slv, 1, assumptions)));
64
65 cvc5_delete(slv);
66 cvc5_term_manager_delete(tm);
67 return 0;
68}
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 TermManager tm = new TermManager();
25 Solver slv = new Solver(tm);
26 {
27 slv.setLogic("QF_BV"); // Set the logic
28
29 Sort bitvector32 = tm.mkBitVectorSort(32);
30
31 Term x = tm.mkConst(bitvector32, "a");
32
33 Op ext_31_1 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1);
34 Term x_31_1 = tm.mkTerm(ext_31_1, x);
35
36 Op ext_30_0 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 30, 0);
37 Term x_30_0 = tm.mkTerm(ext_30_0, x);
38
39 Op ext_31_31 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 31, 31);
40 Term x_31_31 = tm.mkTerm(ext_31_31, x);
41
42 Op ext_0_0 = tm.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0);
43 Term x_0_0 = tm.mkTerm(ext_0_0, x);
44
45 Term eq = tm.mkTerm(Kind.EQUAL, x_31_1, x_30_0);
46 System.out.println(" Asserting: " + eq);
47 slv.assertFormula(eq);
48
49 Term eq2 = tm.mkTerm(Kind.EQUAL, x_31_31, x_0_0);
50 System.out.println(" Check entailment assuming: " + eq2);
51 System.out.println(" Expect UNSAT. ");
52 System.out.println(" cvc5: " + slv.checkSatAssuming(eq2.notTerm()));
53 }
54 Context.deletePointers();
55 }
56}
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))))