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
|
/***
* 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
*/
#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();
// (set-option :produce-models true)
bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);
// Then, create a Bitwuzla instance.
Bitwuzla* bitwuzla = bitwuzla_new(tm, options);
// Create a bit-vector sort of size 3.
BitwuzlaSort sortbv3 = bitwuzla_mk_bv_sort(tm, 3);
// (declare-const x (_ BitVec 3))
BitwuzlaTerm x = bitwuzla_mk_const(tm, sortbv3, "x");
// (assert (= x #b010))
bitwuzla_assert(
bitwuzla,
bitwuzla_mk_term2(tm,
BITWUZLA_KIND_EQUAL,
x,
bitwuzla_mk_bv_value_uint64(tm, sortbv3, 2)));
// (check-sat)
result = bitwuzla_check_sat(bitwuzla);
printf("Expect: sat\n");
printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
// (assert (= x #b001))
bitwuzla_assert(
bitwuzla,
bitwuzla_mk_term2(tm,
BITWUZLA_KIND_EQUAL,
x,
bitwuzla_mk_bv_value_uint64(tm, sortbv3, 1)));
// (check-sat)
result = bitwuzla_check_sat(bitwuzla);
printf("Expect: unsat\n");
printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
// (reset-assertions)
// Note: Bitwuzla does not provide an explicit API function for
// reset-assertions since this is achieved by simply discarding
// the current Bitwuzla instance and creating a new one.
bitwuzla_delete(bitwuzla);
bitwuzla = bitwuzla_new(tm, options);
// (assert (= x #b011))
bitwuzla_assert(
bitwuzla,
bitwuzla_mk_term2(tm,
BITWUZLA_KIND_EQUAL,
x,
bitwuzla_mk_bv_value_uint64(tm, sortbv3, 3)));
// (check-sat)
result = bitwuzla_check_sat(bitwuzla);
printf("Expect: sat\n");
printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));
// (get-model)
printf("(\n");
printf(" (define-fun %s", bitwuzla_term_get_symbol(x));
printf(" () %s", bitwuzla_sort_to_string(bitwuzla_term_get_sort(x)));
printf(" %s)\n", bitwuzla_term_to_string(bitwuzla_get_value(bitwuzla, x)));
printf(")\n");
// Finally, delete the Bitwuzla solver, options, and term manager instances.
bitwuzla_delete(bitwuzla);
bitwuzla_options_delete(options);
bitwuzla_term_manager_delete(tm);
return 0;
}
|
