boolector / btor2tools

A generic parser and tool package for the BTOR2 format.

Boolector

Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. It supports the SMT-LIB logics BV, QF_ABV, QF_AUFBV, QF_BV and QF_UFBV. Boolector provides a rich C and Python API and supports incremental solving, both with the SMT-LIB commands push and pop, and as solving under assumptions. The documentation of its API can be found here.

Website

More information about Boolector is available at: https://boolector.github.io

Download

The latest version of Boolector is available on GitHub: https://github.com/boolector/boolector

Installation

On macOS (or Linux) via Homebrew

brew install boolector

Note: this installation doesn't come with Python bindings and it uses Lingeling as backend.

Prerequisites

To build Boolector from source you need:

• cmake >= 3.3
• gcc/clang
• g++/clang++

To build the python module pyboolector you further need:

• Cython >= 0.22

Build

Boolector can be built with support for the SAT solvers CaDiCaL, CryptoMiniSat, Lingeling, MiniSAT, and PicoSAT. To build and setup these solvers you can use the scripts setup-{cadical,cms,lingeling,minisat,picosat}.sh in the contrib directory. Optionally, you can place any of these solvers in a directory on the same level as the Boolector source directory or provide a path to configure.sh. You can build Boolector with support for multiple SAT solvers. Note that using MiniSAT will force libboolector.a to depend not only on libz.so but also on libstdc++.so. Thus, if you want to link libboolector.a with MiniSAT backend against your own programs, you need to use -lz -lstdc++ as linking options.

Boolector has one other external dependency, the BTOR2 format tools package. As with the SAT solvers, you can either use the provided script setup-btor2tools.sh in contrib or clone the BTOR2Tools repository into directory btor2tools on the same level as the Boolector repository or provide a path to configure.sh.

Linux and Unix-like OS

Assume that we build Boolector with support for Lingeling:

# Download and build Boolector
git clone https://github.com/boolector/boolector
cd boolector

# Download and build Lingeling
./contrib/setup-lingeling.sh

# Download and build BTOR2Tools
./contrib/setup-btor2tools.sh

# Build Boolector
./configure.sh && cd build && make

All binaries (boolector, btormc, btormbt, btoruntrace) are generated into directory boolector/build/bin, and all libraries (libboolector.a, libboolector.so) are generated into directory boolector/build/lib.

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

To build Boolector with Python bindings you need to install Cython, and btor2tools and SAT solvers must be compiled with flag -fPIC (see build instructions of these tools for more details on how to build as shared library). The provided setup-*.sh scripts automatically compile all dependencies with -fPIC. Then, from Boolector's root directory configure and build Boolector as follows:

./configure.sh --python
cd build
make

To build the API documentation of Boolector, it is required to install Sphinx (>= version 1.2). Then build Boolector and issue:

cd doc
make html

The documentation is then generated into doc/_build/html. Make sure to build Boolector with Python bindings, else the documentation of its Python API will not be included.

Linking against Boolector in CMake projects

Boolector's build system provides a CMake package configuration, which can be used by the find_package() command to provide information about Boolector's include directories, libraries and it's dependencies.

After installing Boolector you can issue the following commands in your CMake project to link against Boolector.

find_package(Boolector)
target_link_libraries(<your_target> Boolector::boolector)

Windows

For building and usage of Boolector on Windows, please see COMPILING_WINDOWS.md.

Usage

For a list of command line options, refer to boolector -h.

For examples and instructions on how to use Boolector's C API, refer to examples/api/c and the API documentation. To build all examples in examples/api/c issue:

cd build
make examples

For examples and instructions on how to use Boolector's Python API, refer to examples/api/python/api_usage_examples.py and the API documentation.
To run api_usage_examples.py, from Boolector's root directory issue:

PYTHONPATH="build/lib" python examples/api/python/api_usage_examples.py

Contributing

Boolector is distributed under the MIT license (see COPYING file). By submitting a contribution you automatically accept the conditions described in COPYING. Additionally, we ask you to certify that you have the right to submit such contributions. To manage this process we use a mechanism known as Developer Certificate of Origin, which can be acknowledged by signing-off your commits with git commit -s. We require all pull requests to be squashed into a single commit and signed-off.

Developer Certificate of Origin
Version 1.1

Copyright (C) 2004, 2006 The Linux Foundation and its contributors.
1 Letterman Drive
Suite D4700
San Francisco, CA, 94129

Everyone is permitted to copy and distribute verbatim copies of this
license document, but changing it is not allowed.


Developer's Certificate of Origin 1.1

By making a contribution to this project, I certify that:

(a) The contribution was created in whole or in part by me and I
    have the right to submit it under the open source license
    indicated in the file; or

(b) The contribution is based upon previous work that, to the best
    of my knowledge, is covered under an appropriate open source
    license and I have the right under that license to submit that
    work with modifications, whether created in whole or in part
    by me, under the same open source license (unless I am
    permitted to submit under a different license), as indicated
    in the file; or

(c) The contribution was provided directly to me by some other
    person who certified (a), (b) or (c) and I have not modified
    it.

(d) I understand and agree that this project and the contribution
    are public and that a record of the contribution (including all
    personal information I submit with it, including my sign-off) is
    maintained indefinitely and may be redistributed consistent with
    this project or the open source license(s) involved.

btor2tools's Issues

btorsim: incorrect implementation for `BTOR2_tag_sra`

Btorsim's implementation for sra (shift arithmetic right) is wrong for negative inputs. It doesn't correctly check the sign bit of the left operand to determine whether to shift in zeros or ones.

Testcase:

;; -----------------------------------------------------------------------------
;; manually written btor file for testing binary operators
;; -----------------------------------------------------------------------------
1 sort bitvec 1
2 sort bitvec 8
;; -----------------------------------------------------------------------------
;; arithmetic shift right negative
;; -----------------------------------------------------------------------------
3 constd 2 4
4 const 2 10110110
5 const 2 11111011
6 sra 2 4 3
7 eq 1 5 6
8 bad 7 sra-negative

Witness:

#0
@0
.

Negating an array with the minus sign

Consider the following BTOR2 file:

1 sort bitvec 3
2 sort bitvec 24
3 sort array 1 2
4 state 3
5 input 1
6 read 2 -4 5

Although line 6 negates an array with - (which should be invalid), catbtor does not complain about it.

However, if 7 not 3 4 is appended to the file, catbtor reports:

*** catbtor: parse error in 'array_not.btor2' line 7: expected bitvec sort for not

It would be better if catbtor could detect the error of the negated array at line 6.

Build with btor2aiger fails

The following commands to build with btor2aiger produce an error (Ubuntu 18.04.4, commit 9831f99):

git clone https://github.com/Boolector/btor2tools.git
cd btor2tools/
./setup-deps.sh

Error: *** configure.sh: invalid option '-fPIC' (try '-h')

The error occurs when running script deps/boolector/contrib/setup-btor2tools.sh, which is called in ./setup-deps.sh.

The patch below fixes the above error, but the installation flow still fails as follows:

cp: cannot stat 'build/libbtor2parser.a': No such file or directory

diff --git a/setup-deps.sh b/setup-deps.sh
index 4450d4c..b661a5c 100755
--- a/setup-deps.sh
+++ b/setup-deps.sh
@@ -18,6 +18,8 @@ git clone https://github.com/boolector/boolector deps/boolector
 cd deps/boolector
 git checkout bitblast-api
 
+sed "s/-fPIC//g" -i ./contrib/setup-btor2tools.sh
+sed "/configure/a cd build" -i ./contrib/setup-btor2tools.sh
 ./contrib/setup-btor2tools.sh
 ./contrib/setup-lingeling.sh
 ./configure.sh --prefix $(pwd)/../install

btorsim: `BTOR2_tag_iff` not marked as implemented

Btorsim is missing an implementation of the iff operation.

Negative node ids?

I encountered a btor file in your examples that contains a negative node id:

btor2tools/examples/btorsim/twocount2.btor2

Line 13 in 6ba194b

13 ite 2 -3 6 11

Looking at the spec it isn't clear to me what a negative node id means. According to the grammar (nid) := (num) and num is defined as a positive unsigned integer.

I would appreciate any explanation what the meaning of a negative node id is. Thanks!

case 'l' in btor2parser.c

Hi, in btor2parser.c, line 1434 writes: "case 'l': PARSE (state, input); break;"

Is it supposed for some keyword starting with 'l'?

[btor2parser] memory allocation failed

Hello -

We are using the vmt2btor.py to create a btor2 file. However, when we call btor tools on such files, we always encounter the [btor2parser] memory allocation failed problem. Did we miss something? Thanks.

For example, we start from this example given by the AVR model checker: https://github.com/aman-goel/avr/blob/master/examples/vmt/simple.c.vmt

(set-info :source |printed by MathSAT|)
(declare-fun .PC.0 () Bool)
(declare-fun .PC.1 () Bool)
(declare-fun .PC.2 () Bool)
(declare-fun x__1$main () (_ BitVec 32))
(declare-fun __RET__$main.next () (_ BitVec 32))
(declare-fun .PC.0.next () Bool)
(declare-fun .PC.1.next () Bool)
(declare-fun __RET__$main () (_ BitVec 32))
(declare-fun .PC.2.next () Bool)
(declare-fun |__NONDET_INLINE_INIT__4__3$main#0| () (_ BitVec 32))
(declare-fun n__3$main.next () (_ BitVec 32))
(declare-fun x__1$main.next () (_ BitVec 32))
(declare-fun n__3$main () (_ BitVec 32))
(define-fun .def_13 () Bool (! .PC.0 :next |.PC.0.next|))
(define-fun .def_14 () Bool (not .def_13))
(define-fun .def_11 () Bool (! .PC.1 :next |.PC.1.next|))
(define-fun .def_12 () Bool (not .def_11))
(define-fun .def_15 () Bool (and .def_12 .def_14))
(define-fun .def_9 () Bool (! .PC.2 :next |.PC.2.next|))
(define-fun .def_10 () Bool (not .def_9))
(define-fun .def_16 () Bool (! (and .def_10 .def_15) :init true))
(define-fun .def_72 () Bool (= n__3$main.next |__NONDET_INLINE_INIT__4__3$main#0|))
(define-fun .def_70 () Bool (= x__1$main.next (_ bv0 32)))
(define-fun .def_73 () Bool (and .def_70 .def_72))
(define-fun .def_67 () Bool (bvslt n__3$main.next (_ bv1 32)))
(define-fun .def_68 () Bool (not .def_67))
(define-fun .def_74 () Bool (and .def_68 .def_73))
(define-fun .def_29 () (_ BitVec 32) (! __RET__$main :next |__RET__$main.next|))
(define-fun .def_31 () Bool (= .def_29 __RET__$main.next))
(define-fun .def_75 () Bool (and .def_31 .def_74))
(define-fun .def_42 () Bool (not .PC.2.next))
(define-fun .def_18 () Bool (not .PC.1.next))
(define-fun .def_41 () Bool (and .def_18 .PC.0.next))
(define-fun .def_43 () Bool (and .def_41 .def_42))
(define-fun .def_76 () Bool (and .def_43 .def_75))
(define-fun .def_77 () Bool (and .def_16 .def_76))
(define-fun .def_34 () (_ BitVec 32) (! x__1$main :next |x__1$main.next|))
(define-fun .def_27 () (_ BitVec 32) (! n__3$main :next |n__3$main.next|))
(define-fun .def_60 () Bool (bvslt .def_27 .def_34))
(define-fun .def_45 () (_ BitVec 32) (bvadd (_ bv4294967295 32) .def_27))
(define-fun .def_46 () Bool (bvslt .def_45 .def_34))
(define-fun .def_61 () Bool (and .def_46 .def_60))
(define-fun .def_28 () Bool (= n__3$main.next .def_27))
(define-fun .def_62 () Bool (and .def_28 .def_61))
(define-fun .def_63 () Bool (and .def_31 .def_62))
(define-fun .def_35 () Bool (= x__1$main.next .def_34))
(define-fun .def_64 () Bool (and .def_35 .def_63))
(define-fun .def_20 () Bool (not .PC.0.next))
(define-fun .def_58 () Bool (and .PC.1.next .def_20))
(define-fun .def_59 () Bool (and .def_42 .def_58))
(define-fun .def_65 () Bool (and .def_59 .def_64))
(define-fun .def_55 () Bool (and .def_12 .def_13))
(define-fun .def_56 () Bool (and .def_10 .def_55))
(define-fun .def_66 () Bool (and .def_56 .def_65))
(define-fun .def_78 () Bool (or .def_66 .def_77))
(define-fun .def_49 () (_ BitVec 32) (bvadd (_ bv1 32) .def_34))
(define-fun .def_50 () Bool (= x__1$main.next .def_49))
(define-fun .def_47 () Bool (not .def_46))
(define-fun .def_51 () Bool (and .def_47 .def_50))
(define-fun .def_52 () Bool (and .def_28 .def_51))
(define-fun .def_53 () Bool (and .def_31 .def_52))
(define-fun .def_54 () Bool (and .def_43 .def_53))
(define-fun .def_57 () Bool (and .def_54 .def_56))
(define-fun .def_79 () Bool (or .def_57 .def_78))
(define-fun .def_38 () Bool (and .def_11 .def_14))
(define-fun .def_39 () Bool (and .def_10 .def_38))
(define-fun .def_32 () Bool (and .def_28 .def_31))
(define-fun .def_36 () Bool (and .def_32 .def_35))
(define-fun .def_21 () Bool (and .def_18 .def_20))
(define-fun .def_23 () Bool (and .def_21 .PC.2.next))
(define-fun .def_37 () Bool (and .def_23 .def_36))
(define-fun .def_40 () Bool (and .def_37 .def_39))
(define-fun .def_80 () Bool (or .def_40 .def_79))
(define-fun .def_24 () Bool (and .def_9 .def_15))
(define-fun .def_25 () Bool (and .def_23 .def_24))
(define-fun .def_81 () Bool (! (or .def_25 .def_80) :trans true))
(define-fun .def_82 () Bool (! (not .def_24) :invar-property 0))
(assert true)

Then we use vmt2btor.py in the recent version of vmt-lib tools for conversion: https://vmt-lib.fbk.eu/

; generated by vmt2btor.py on Wed May 11 17:04:41 2022
1 sort bitvec 1
2 sort bitvec 32
3 constd 1 1
4 state 1 .PC.0
5 state 1 .PC.1
6 state 1 .PC.2
7 input 2 n__3$main.next
8 input 2 __NONDET_INLINE_INIT__4__3$main#0
9 input 2 x__1$main.next
10 state 2 __RET__$main
11 input 2 __RET__$main.next
12 input 1 .PC.2.next
13 input 1 .PC.1.next
14 input 1 .PC.0.next
15 state 2 x__1$main
16 state 2 n__3$main
17 next 1 4 14
18 next 1 5 13
19 next 1 6 12
20 next 2 10 11
21 next 2 15 9
22 next 2 16 7
; init
23 not 1 14
24 not 1 13
25 and 1 24 23
26 not 1 12
27 and 1 26 25
; trans
28 not 1 5
29 not 1 4
30 and 1 29 28
31 and 1 30 6
32 and 1 12 25
33 and 1 32 31
34 eq 1 7 16
35 eq 1 10 11
36 and 1 35 34
37 eq 1 9 15
38 and 1 37 36
39 and 1 38 32
40 and 1 29 5
41 not 1 6
42 and 1 41 40
43 and 1 42 39
44 constd 2 4294967295
45 add 2 44 16
46 slt 1 45 15
47 not 1 46
48 constd 2 1
49 add 2 48 15
50 eq 1 9 49
51 and 1 50 47
52 and 1 34 51
53 and 1 35 52
54 and 1 24 14
55 and 1 26 54
56 and 1 55 53
57 and 1 4 28
58 and 1 41 57
59 and 1 58 56
60 and 1 13 23
61 and 1 26 60
62 slt 1 16 15
63 and 1 62 46
64 and 1 63 34
65 and 1 35 64
66 and 1 65 37
67 and 1 66 61
68 and 1 67 58
69 slt 1 7 48
70 not 1 69
71 constd 2 0
72 eq 1 9 71
73 eq 1 7 8
74 and 1 73 72
75 and 1 74 70
76 and 1 75 35
77 and 1 76 55
78 and 1 30 41
79 and 1 78 77
80 or 1 79 68
81 or 1 80 59
82 or 1 81 43
83 or 1 82 33
; reset sequence
84 state 1 model-reset0
85 init 1 84 -3
86 next 1 84 3
87 state 1 model-reset1
88 init 1 87 -3
89 next 1 87 84
90 and 1 84 -87
; model var
91 state 1 model-valid
92 init 1 91 -3
94 and 1 91 83
93 ite 1 90 27 94
95 ite 1 84 93 -3
96 next 1 91 95
; property 0
97 not 1 31
98 and 1 91 -97
99 bad 98

Then we call btorsim and encounter this issue.

Parse error for `init`: state id must be greater than id of second operand

Hi,

I am trying to understand the BTOR2 format.
I ran catbtor (built at b8456dd) with the BTOR2 model program.btor2 of the example program in the CAV 2018 paper.

1 sort bitvec 1
2 sort bitvec 32
3 input 1 turn
4 state 2 a
5 state 2 b
6 zero 2
7 init 2 4 6
8 init 2 5 6
9 one 2
10 add 2 4 9
11 add 2 5 9
12 ite 2 3 4 10
13 ite 2 -3 5 11
14 next 2 4 12
15 next 2 5 13
16 constd 2 3
17 eq 1 4 16
18 eq 1 5 16
19 and 1 17 18
20 bad 19

However, I received a parse error:

*** catbtor: parse error in 'program.btor2' line 7: state id must be greater than id of second operand

Is this an intended behavior of the parser?
I could not find information on such restrictions in the CAV paper.
(The file can be successfully parsed if the line 6 zero 2 gets an nid smaller than a's and b's.)

Thanks!

Partial register initialization

In Btor2, both registers (states of bit-vector sort) and memories (states of array sort)
are initialized randomly unless init is used to explicitly initialize their values.
The allows the partial initialization of a register by
applying a bit-mask to an uninitialized register.

For example, consider the Btor2 circuit:

1 sort bitvec 3
2 const 1 001
3 state 1
4 const 1 100
5 and 1 3 4
6 state 1
7 init 1 6 5

The register at line 6 is initialized to ?00 (? indicates a random Boolean value).

If we append the following line to initialize the register at line 3:

8 init 1 3 2

What will the register at line 6 be initialized to in this case?
Will it now become 000 (001 & 100) or remain as ?00?

Semantics of negated signals with the minus sign

Hello,

I noticed that there are negated signals in some BTOR2 files, e.g., hwmcc20/bv/2019/beem/blocks.4.prop1-back-serstep.btor2.

57 and 1 47 -49

However, I could not find the definition of the minus sign in the 2018 CAV paper.

Is the semantics of the minus sign bitwise inversion, i.e., not?
Can we use the minus sign with a bitvec signal with more than one bit?

Many thanks!

btorsim: missing implementation for `BTOR2_tag_rol`, `BTOR2_tag_ror`, and `BTOR2_tag_smod`

Btorsim is missing an implementation of the rotation operations rol, ror, and smod