Btor2Tools
===============================================================================
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.
Download
-------------------------------------------------------------------------------
The latest version of Btor2Tools can be found on GitHub:
https://github.com/boolector/btor2tools
Build
-------------------------------------------------------------------------------
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`.
Usage
-------------------------------------------------------------------------------
### BTOR2 Parser
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
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
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`.
The BTOR2 Format
-------------------------------------------------------------------------------
For a detailed description, please refer to
[BTOR2, BtorMC and Boolector 3.0](https://link.springer.com/chapter/10.1007/978-3-319-96145-3_32)
at [CAV 2018](http://cavconference.org/2018/).
### Input Format
```
<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]+
| <constd>
| <consth>
<state> ::= 'state' <sid>
<bitvec> ::= 'bitvec' <num>
<array> ::= 'array' <sid> <sid>
| <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`).
#### Indexed Operators
| `[su]ext w` | (un)signed extension | `B_[n] -> B_[n+w]` |
| `slice u l` | extraction, `n > u >= l` | `B_[n] -> B_[u-l+1]` |
#### Unary Operators
| `not` | bit-wise | `B_[n] -> B_[n]` |
| `inc`, `dec`, `neg` | arithmetic | `B_[n] -> B_[n]` |
| `redand`, `redor`, `redxor` | reduction | `B_[n] -> B_[1]` |
#### Binary Operators
| `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` |
#### Ternary Operators
| `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]` |
### Witness Format
```
<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>)+ '.'
```