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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
/***
* Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
*
* Copyright (C) 2021 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
*/
#include <bitwuzla/c/bitwuzla.h>
#include <stdio.h>
int
main()
{
BitwuzlaResult result;
// First, create a term manager instance.
BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
// Create a Bitwuzla options instance.
BitwuzlaOptions* options = bitwuzla_options_new();
// Then, create a Bitwuzla instance.
Bitwuzla* bitwuzla = bitwuzla_new(tm, options);
// Create a bit-vector sort of size 1.
BitwuzlaSort sortbv1 = bitwuzla_mk_bv_sort(tm, 1);
// Create a bit-vector sort of size 2
BitwuzlaSort sortbv2 = bitwuzla_mk_bv_sort(tm, 2);
// Create bit-vector variables.
// (declare-const o0 (_ BitVec 1))
BitwuzlaTerm o0 = bitwuzla_mk_const(tm, sortbv1, "o0");
// (declare-const o1 (_ BitVec 1))
BitwuzlaTerm o1 = bitwuzla_mk_const(tm, sortbv1, "o1");
// (declare-const s0 (_ BitVec 2))
BitwuzlaTerm s0 = bitwuzla_mk_const(tm, sortbv2, "s0");
// (declare-const s1 (_ BitVec 2))
BitwuzlaTerm s1 = bitwuzla_mk_const(tm, sortbv2, "s1");
// (declare-const s2 (_ BitVec 2))
BitwuzlaTerm s2 = bitwuzla_mk_const(tm, sortbv2, "s2");
// (declare-const goal (_ BitVec 2))
BitwuzlaTerm goal = bitwuzla_mk_const(tm, sortbv2, "goal");
// Create bit-vector values zero, one, three.
BitwuzlaTerm zero = bitwuzla_mk_bv_zero(tm, sortbv2);
BitwuzlaTerm one1 = bitwuzla_mk_bv_one(tm, sortbv1);
BitwuzlaTerm one2 = bitwuzla_mk_bv_one(tm, sortbv2);
BitwuzlaTerm three = bitwuzla_mk_bv_value_uint64(tm, sortbv2, 3);
// Add some assertions.
bitwuzla_assert(bitwuzla,
bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s0, zero));
bitwuzla_assert(bitwuzla,
bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, goal, three));
// (check-sat-assuming ((= s0 goal)))
BitwuzlaTerm assumptions[1] = {
bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s0, goal)};
result = bitwuzla_check_sat_assuming(bitwuzla, 1, assumptions);
printf("Expect: unsat\n");
printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
// (assert (= s1 (ite (= o0 (_ sortbv1 1)) (bvadd s0 one) s0)))
bitwuzla_assert(bitwuzla,
bitwuzla_mk_term2(
tm,
BITWUZLA_KIND_EQUAL,
s1,
bitwuzla_mk_term3(
tm,
BITWUZLA_KIND_ITE,
bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, o0, one1),
bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ADD, s0, one2),
s0)));
// (check-sat-assuming ((= s1 goal)))
assumptions[0] = bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s1, goal);
result = bitwuzla_check_sat_assuming(bitwuzla, 1, assumptions);
printf("Expect: unsat\n");
printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
// (assert (= s2 (ite (= o1 (_ sortbv1 1)) (bvadd s1 one) s1)))
bitwuzla_assert(bitwuzla,
bitwuzla_mk_term2(
tm,
BITWUZLA_KIND_EQUAL,
s2,
bitwuzla_mk_term3(
tm,
BITWUZLA_KIND_ITE,
bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, o1, one1),
bitwuzla_mk_term2(tm, BITWUZLA_KIND_BV_ADD, s1, one2),
s1)));
// (check-sat-assuming ((= s2 goal)))
assumptions[0] = bitwuzla_mk_term2(tm, BITWUZLA_KIND_EQUAL, s2, goal);
result = bitwuzla_check_sat_assuming(bitwuzla, 1, assumptions);
printf("Expect: unsat\n");
printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
// Finally, delete the Bitwuzla solver, options, and term manager instances.
bitwuzla_delete(bitwuzla);
bitwuzla_options_delete(options);
bitwuzla_term_manager_delete(tm);
return 0;
}
|
