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
109
110
111
112
113
114
115
116
117
118
119
120
|
/***
* 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 <assert.h>
#include <bitwuzla/c/bitwuzla.h>
#include <bitwuzla/c/parser.h>
#include <stdlib.h>
int
main()
{
// First, create a term manager instance.
BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
// Create a Bitwuzla options instance.
BitwuzlaOptions* options = bitwuzla_options_new();
// We will parse example file `smt2/quickstart.smt2`.
// Create parser instance.
const char* infile_name = "../smt2/quickstart.smt2";
BitwuzlaParser* parser =
bitwuzla_parser_new(tm, options, "smt2", 2, "<stdout>");
// Now parse the input file.
const char* error_msg;
printf("Expect: sat\n");
printf("Bitwuzla: ");
bitwuzla_parser_parse(parser, infile_name, false, true, &error_msg);
// We expect no error to occur.
assert(!error_msg);
// Now we retrieve the set of asserted formulas and print them.
size_t size;
const BitwuzlaTerm* assertions =
bitwuzla_get_assertions(bitwuzla_parser_get_bitwuzla(parser), &size);
printf("Assertions:\n");
printf("{\n");
for (size_t i = 0; i < size; ++i)
{
printf(" %s\n", bitwuzla_term_to_string(assertions[i]));
}
printf("}\n");
// Now we add an assertion via parsing from string.
bitwuzla_parser_parse(
parser, "(assert (distinct (select a x) y))", true, false, &error_msg);
// We expect no error to occur.
assert(!error_msg);
// Now the formula is unsat.
BitwuzlaResult result =
bitwuzla_check_sat(bitwuzla_parser_get_bitwuzla(parser));
printf("Expect: unsat\n");
printf("Bitwuzla: %s\n\n", bitwuzla_result_to_string(result));
// For illustration purposes, we now parse in some declarations and terms
// and sorts from string.
// Declare bit-vector sort of size 16.
BitwuzlaSort bv16 =
bitwuzla_parser_parse_sort(parser, "(_ BitVec 16)", &error_msg);
// We expect no error to occur.
assert(!error_msg);
// Create bit-vector sort of size 16 and show that it corresponds to
// its string representation '(_ BitVec16)'.
assert(bv16 == bitwuzla_mk_bv_sort(tm, 16));
// Declare Boolean constants 'c' and 'd'.
// Note: Declarations are commands (not terms) in the SMT-LIB language.
// Commands must be parsed in via bitwuzla_parser_parse(),
// bitwuzla_parser_parse_term() only supports parsing SMT-LIB terms.
bitwuzla_parser_parse(parser,
"(declare-const c Bool)(declare-const d Bool)",
true,
false,
&error_msg);
// Declare bit-vector constant 'b'.
bitwuzla_parser_parse(
parser, "(declare-const b (_ BitVec 16))", true, false, &error_msg);
// We expect no error to occur.
assert(!error_msg);
// Retrieve term representing 'b'.
BitwuzlaTerm b = bitwuzla_parser_parse_term(parser, "b", &error_msg);
// We expect no error to occur.
assert(!error_msg);
// Retrieve term representing 'c'.
BitwuzlaTerm c = bitwuzla_parser_parse_term(parser, "c", &error_msg);
// We expect no error to occur.
assert(!error_msg);
// Retrieve term representing 'd'.
BitwuzlaTerm d = bitwuzla_parser_parse_term(parser, "d", &error_msg);
// We expect no error to occur.
assert(!error_msg);
// Create xor over 'a' and 'c' and show that it corresponds to term
// parsed in from its string representation '(xor c d)'.
assert(bitwuzla_parser_parse_term(parser, "(xor c d)", &error_msg)
== bitwuzla_mk_term2(tm, BITWUZLA_KIND_XOR, c, d));
// Create bit-vector addition over 'b' and bit-vector value
// '1011111010001010' and show that it corresponds to the term parsed in
// from its string representation '(bvadd b #b1011111010001010)'.
assert(bitwuzla_parser_parse_term(
parser, "(bvadd b #b1011111010001010)", &error_msg)
== bitwuzla_mk_term2(
tm,
BITWUZLA_KIND_BV_ADD,
b,
bitwuzla_mk_bv_value(tm, bv16, "1011111010001010", 2)));
// Finally, delete Bitwuzla parser, options, and term manager instance.
bitwuzla_parser_delete(parser);
bitwuzla_options_delete(options);
bitwuzla_term_manager_delete(tm);
return 0;
}
|
