Skip to content
A generic parser and tool package for the BTOR2 format.
C Shell
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
examples examples: Fix ne/neq. Apr 19, 2019
src btor2parser: Fix parsing ne/neq. Apr 16, 2019
test Clean up tests May 16, 2018
.clang-format Added clang-format file May 4, 2018
.gitignore moved src files to dir 'src' Mar 8, 2016
AUTHORS
LICENSE.txt
README.md Remove udivo from README (#3) Sep 23, 2019
VERSION Added mksrcrelease script May 16, 2018
configure.sh Compile with -std=gnu99. Jun 20, 2018
makefile.in Renamed May 16, 2018
mksrcrelease.sh Added mksrcrelease script May 16, 2018

README.md

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
make

For more build configuration options of Btor2Tools, see configure.sh -h.

All binaries (btorsim, catbtor) are generated into directory btor2tools/bin, and all libraries (libbtor2parser.a, libbtor2parser.so) are generated into directory btor2tools/build.

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 at CAV 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]+
<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).

Indexed Operators

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]

Unary Operators

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]

Binary Operators

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

Ternary Operators

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]

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>)+ '.'
You can’t perform that action at this time.