The Btor2Tools package provides a generic parser and tools for the BTOR2 format.
For a more detailed description of the BTOR2 format, refer to
BTOR2, BtorMC and Boolector 3.0. Aina Niemetz, Mathias Preiner, Clifford Wolf,
and Armin Biere. CAV 2018.
The latest version of Btor2Tools can be found on GitHub: https://github.com/boolector/btor2tools
From the Btor2Tools root directory configure and build as follows:
./configure.sh
cd build
make
For more build configuration options of Btor2Tools, see configure.sh -h.
All binaries (btorsim, catbtor) are generated into directory build/bin,
and all libraries (libbtor2parser.a, libbtor2parser.so) are generated into
directory build/lib.
Btor2Parser is a generic parser for the BTOR2 format.
Btor2Parser* parser;
Btor2LineIterator it;
Btor2Line* line;
parser = btor2parser_new ();
if (!btor2parser_read_lines (reader, input_file))
{
// parse error
const char *err = btor2parser_error (parser);
// error handling
}
// iterate over parsed lines
it = btor2parser_iter_init (parser);
while ((line = btor2parser_iter_next (&it)))
{
// process line
}
btor2parser_delete (parser);
For a simple example on how to use the BTOR2 parser, refer to src/catbtor.c.
For a more comprehensive example, refer to function parse_model() in
src/btorsim/btorsim.c.
BtorSim is a witness simulator and checker for BTOR2 witnesses.
For a list of command line options, refer to btorsim -h.
For examples and instructions on how to use BtorSim, refer to
examples/btorsim.
Catbtor is a simple tool to parse and print BTOR2 files. It is mainly used for debugging purposes.
For a list of command line options, refer to catbtor -h.
For a detailed description, please refer to BTOR2, BtorMC and Boolector 3.0 at CAV 2018.
<num> ::= positive unsigned integer (greater than zero)
<uint> ::= unsigned integer (including zero)
<string> ::= sequence of whitespace and printable characters without '\n'
<symbol> ::= sequence of printable characters without '\n'
<comment> ::= ';' <string>
<nid> ::= <num>
<sid> ::= <num>
<const> ::= 'const' <sid> [0-1]+
<constd> ::= 'constd' <sid> ['-']<uint>
<consth> ::= 'consth' <sid> [0-9a-fA-F]+
<input> ::= ('input' | 'one' | 'ones' | 'zero') <sid>
| <const>
| <constd>
| <consth>
<state> ::= 'state' <sid>
<bitvec> ::= 'bitvec' <num>
<array> ::= 'array' <sid> <sid>
<node> ::= <sid> 'sort' (<array> | <bitvec>)
| <nid> (<input> | <state>)
| <nid> <opidx> <sid> <nid> <uint> [<uint>]
| <nid> <op> <sid> <nid> [<nid> [<nid>]]
| <nid> ('init' | 'next') <sid> <nid> <nid>
| <nid> ('bad' | 'constraint' | 'fair' | 'output') <nid>
| <nid> 'justice' <num> (<nid>)+
<line> ::= <comment>
| <node> [<symbol>] [<comment>]
<btor> ::= (<line>'\n')+
Non-terminals <opidx> and <op> are indexed and non-indexed operaters
as defined below (B_[n] represents a bit-vector sort of size n, and
A_[I -> E] represents an array sort with index sort I and element sort E).
| Operator | Description | Signature |
|---|---|---|
[su]ext w |
(un)signed extension | B_[n] -> B_[n+w] |
slice u l |
extraction, n > u >= l |
B_[n] -> B_[u-l+1] |
| Operator | Description | Signature |
|---|---|---|
not |
bit-wise | B_[n] -> B_[n] |
inc, dec, neg |
arithmetic | B_[n] -> B_[n] |
redand, redor, redxor |
reduction | B_[n] -> B_[1] |
| Operator | Description | Signature |
|---|---|---|
iff, implies |
Boolean | B_[1] x B_[1] -> B_[1] |
eq, neq |
(dis)equality | S x S -> B_[1] |
[su]gt, [su]gte, [su]lt, [su]lte |
(un)signed inequality | B_[n] x B_[n] -> B_[1] |
and, nand, nor, or, xnor, xor |
bit-wise | B_[n] x B_[n] -> B_[n] |
rol, ror, sll, sra, srl |
rotate, shift | B_[n] x B_[n] -> B_[n] |
add, mul, [su]div, smod, [su]rem, sub |
arithmetic | B_[n] x B_[n] -> B_[n] |
[su]addo, sdivo, [su]mulo, [su]subo |
overflow | B_[n] x B_[n] -> B_[1] |
concat |
concatenation | B_[n] x B_[m] -> B_[n+m] |
read |
array read | A_[I -> E] x I -> E |
| Operator | Description | Signature |
|---|---|---|
ite |
conditional | B_[1] x B_[n] x B_[n] -> B_[n] |
write |
array write | A_[I -> E] x I x E -> A_[I -> E] |
<binary-string> ::= [0-1]+
<bv-assignment> ::= <binary-string>
<array-assignment> ::= '['<binary-string>']' <binary-string>
<assignement> ::= <uint> (<bv-assignment>
| <array-assignment>) [<symbol>]
<model> ::= (<comment>'\n'
| <assignment>'\n')+
<state part> ::= '#'<uint>'\n' <model>
<input part> ::= '@'<uint>'\n' <model>
<frame> ::= [<state part>] <input part>
<prop> ::= ('b' | 'j')<uint>
<header> ::= 'sat\n' (<prop>)+ '\n'
<witness> ::= (<comment>'\n')+
| <header> (<frame>)+ '.'