1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
###
# Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
#
# Copyright (C) 2023 by the authors listed in the AUTHORS file at
# https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
#
# This file is part of Bitwuzla under the MIT license. See COPYING for more
# information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
##
from bitwuzla import *
if __name__ == "__main__":
# No options configured, create Bitwuzla instance with default options.
tm = TermManager()
bitwuzla = Bitwuzla(tm)
# Create a bit-vector sort of size 1.
sortbv1 = tm.mk_bv_sort(1)
# Create a bit-vector sort of size 2
sortbv2 = tm.mk_bv_sort(2)
# Create bit-vector variables.
# (declare-const o0 (_ BitVec 1))
o0 = tm.mk_const(sortbv1, 'o0')
# (declare-const o1 (_ BitVec 1))
o1 = tm.mk_const(sortbv1, 'o1')
# (declare-const s0 (_ BitVec 2))
s0 = tm.mk_const(sortbv2, 's0')
# (declare-const s1 (_ BitVec 2))
s1 = tm.mk_const(sortbv2, 's1')
# (declare-const s2 (_ BitVec 2))
s2 = tm.mk_const(sortbv2, 's2')
# (declare-const goal (_ BitVec 2))
goal = tm.mk_const(sortbv2, 'goal')
# Create bit-vector values zero, one, three.
zero = tm.mk_bv_zero(sortbv2)
one1 = tm.mk_bv_one(sortbv1)
one2 = tm.mk_bv_one(sortbv2)
three = tm.mk_bv_value(sortbv2, 3)
# Add some assertions.
bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [s0, zero]))
bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL, [goal, three]))
# (check-sat-assuming ((= s0 goal)))
result = bitwuzla.check_sat(tm.mk_term(Kind.EQUAL, [s0, goal]))
print('Expect: unsat')
print(f'Bitwuzla: {result}')
# (assert (= s1 (ite (= o0 (_ sortbv1 1)) (bvadd s0 one) s0)))
bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL,
[s1,
tm.mk_term(Kind.ITE,
[tm.mk_term(Kind.EQUAL, [o0, one1]),
tm.mk_term(Kind.BV_ADD, [s0, one2]),
s0])]))
# (check-sat-assuming ((= s1 goal)))
result = bitwuzla.check_sat(tm.mk_term(Kind.EQUAL, [s1, goal]))
print('Expect: unsat')
print(f'Bitwuzla: {result}')
# (assert (= s2 (ite (= o1 (_ sortbv1 1)) (bvadd s1 one) s1)))
bitwuzla.assert_formula(tm.mk_term(Kind.EQUAL,
[s2,
tm.mk_term(Kind.ITE,
[tm.mk_term(Kind.EQUAL, [o1, one1]),
tm.mk_term(Kind.BV_ADD, [s1, one2]),
s1])]))
# (check-sat-assuming ((= s2 goal)))
result = bitwuzla.check_sat(tm.mk_term(Kind.EQUAL, [s2, goal]))
print('Expect: unsat')
print(f'Bitwuzla: {result}')
|
