README.md
1Btor2Tools
2===============================================================================
3
4The Btor2Tools package provides a generic parser and tools for the BTOR2 format.
5
6For a more detailed description of the BTOR2 format, refer to
7*BTOR2, BtorMC and Boolector 3.0.* Aina Niemetz, Mathias Preiner, Clifford Wolf,
8and Armin Biere. CAV 2018.
9
10Download
11-------------------------------------------------------------------------------
12
13 The latest version of Btor2Tools can be found on GitHub:
14 https://github.com/boolector/btor2tools
15
16Build
17-------------------------------------------------------------------------------
18
19From the Btor2Tools root directory configure and build as follows:
20```
21./configure.sh
22make
23```
24For more build configuration options of Btor2Tools, see `configure.sh -h`.
25
26All binaries (btorsim, catbtor) are generated into directory `btor2tools/bin`,
27and all libraries (libbtor2parser.a, libbtor2parser.so) are generated into
28directory `btor2tools/build`.
29
30
31Usage
32-------------------------------------------------------------------------------
33
34### BTOR2 Parser
35
36Btor2Parser is a generic parser for the BTOR2 format.
37
38```
39Btor2Parser* parser;
40Btor2LineIterator it;
41Btor2Line* line;
42
43parser = btor2parser_new ();
44if (!btor2parser_read_lines (reader, input_file))
45{
46 // parse error
47 const char *err = btor2parser_error (parser);
48 // error handling
49}
50// iterate over parsed lines
51it = btor2parser_iter_init (parser);
52while ((line = btor2parser_iter_next (&it)))
53{
54 // process line
55}
56btor2parser_delete (parser);
57
58```
59
60For a simple example on how to use the BTOR2 parser, refer to `src/catbtor.c`.
61For a more comprehensive example, refer to function `parse_model()` in
62`src/btorsim/btorsim.c`.
63
64
65### BtorSim
66
67BtorSim is a witness simulator and checker for BTOR2 witnesses.
68
69For a list of command line options, refer to `btorsim -h`.
70For examples and instructions on how to use BtorSim, refer to
71`examples/btorsim`.
72
73### Catbtor
74
75Catbtor is a simple tool to parse and print BTOR2 files. It is mainly used for
76debugging purposes.
77
78For a list of command line options, refer to `catbtor -h`.
79
80The BTOR2 Format
81-------------------------------------------------------------------------------
82For a detailed description, please refer to
83[BTOR2, BtorMC and Boolector 3.0](https://link.springer.com/chapter/10.1007/978-3-319-96145-3_32)
84at [CAV 2018](http://cavconference.org/2018/).
85
86### Input Format
87
88```
89<num> ::= positive unsigned integer (greater than zero)
90<uint> ::= unsigned integer (including zero)
91<string> ::= sequence of whitespace and printable characters without '\n'
92<symbol> ::= sequence of printable characters without '\n'
93<comment> ::= ';' <string>
94<nid> ::= <num>
95<sid> ::= <num>
96<const> ::= 'const' <sid> [0-1]+
97<constd> ::= 'constd' <sid> ['-']<uint>
98<consth> ::= 'consth' <sid> [0-9a-fA-F]+
99<input> ::= ('input' | 'one' | 'ones' | 'zero') <sid>
100 | <const>
101 | <constd>
102 | <consth>
103<state> ::= 'state' <sid>
104<bitvec> ::= 'bitvec' <num>
105<array> ::= 'array' <sid> <sid>
106<node> ::= <sid> 'sort' (<array> | <bitvec>)
107 | <nid> (<input> | <state>)
108 | <nid> <opidx> <sid> <nid> <uint> [<uint>]
109 | <nid> <op> <sid> <nid> [<nid> [<nid>]]
110 | <nid> ('init' | 'next') <sid> <nid> <nid>
111 | <nid> ('bad' | 'constraint' | 'fair' | 'output') <nid>
112 | <nid> 'justice' <num> (<nid>)+
113<line> ::= <comment>
114 | <node> [<symbol>] [<comment>]
115<btor> ::= (<line>'\n')+
116
117```
118
119Non-terminals `<opidx>` and `<op>` are indexed and non-indexed operaters
120as defined below (`B_[n]` represents a bit-vector sort of size n, and
121`A_[I -> E]` represents an array sort with index sort `I` and element sort `E`).
122
123#### Indexed Operators
124
125| Operator | Description | Signature |
126| ------------------- | ------------------------- | ------------------------- |
127| `[su]ext w` | (un)signed extension | `B_[n] -> B_[n+w]` |
128| `slice u l` | extraction, `n > u >= l` | `B_[n] -> B_[u-l+1]` |
129
130#### Unary Operators
131
132| Operator | Description | Signature |
133| --------------------------- | ----------------- | ------------------------- |
134| `not` | bit-wise | `B_[n] -> B_[n]` |
135| `inc`, `dec`, `neg` | arithmetic | `B_[n] -> B_[n]` |
136| `redand`, `redor`, `redxor` | reduction | `B_[n] -> B_[1]` |
137
138#### Binary Operators
139
140| Operator | Description | Signature |
141| ------------------------------------------------- | --------------------- | -------------------------- |
142| `iff`, `implies` | Boolean | `B_[1] x B_[1] -> B_[1]` |
143| `eq`, `neq` | (dis)equality | `S x S -> B_[1]` |
144| `[su]gt`, `[su]gte`, `[su]lt`, `[su]lte` | (un)signed inequality | `B_[n] x B_[n] -> B_[1]` |
145| `and`, `nand`, `nor`, `or`, `xnor`, `xor` | bit-wise | `B_[n] x B_[n] -> B_[n]` |
146| `rol`, `ror`, `sll`, `sra`, `srl` | rotate, shift | `B_[n] x B_[n] -> B_[n]` |
147| `add`, `mul`, `[su]div`, `smod`, `[su]rem`, `sub` | arithmetic | `B_[n] x B_[n] -> B_[n]` |
148| `[su]addo`, `[su]divo`, `[su]mulo`, `[su]subo` | overflow | `B_[n] x B_[n] -> B_[1]` |
149| `concat` | concatenation | `B_[n] x B_[m] -> B_[n+m]` |
150| `read` | array read | `A_[I -> E] x I -> E` |
151
152#### Ternary Operators
153
154| Operator | Description | Signature |
155| -------------- | --------------------- | ---------------------------------- |
156| `ite` | conditional | `B_[1] x B_[n] x B_[n] -> B_[n]` |
157| `write` | array write | `A_[I -> E] x I x E -> A_[I -> E]` |
158
159
160### Witness Format
161
162```
163<binary-string> ::= [0-1]+
164<bv-assignment> ::= <binary-string>
165<array-assignment> ::= '['<binary-string>']' <binary-string>
166<assignement> ::= <uint> (<bv-assignment>
167 | <array-assignment>) [<symbol>]
168<model> ::= (<comment>'\n'
169 | <assignment>'\n')+
170<state part> ::= '#'<uint>'\n' <model>
171<input part> ::= '@'<uint>'\n' <model>
172<frame> ::= [<state part>] <input part>
173<prop> ::= ('b' | 'j')<uint>
174<header> ::= 'sat\n' (<prop>)+ '\n'
175<witness> ::= (<comment>'\n')+
176 | <header> (<frame>)+ '.'
177```
178
179