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.
More information about Boolector is available at: https://boolector.github.io
The latest version of Boolector is available on GitHub: https://github.com/boolector/boolector
brew install boolector
Note: this installation doesn't come with Python bindings and it uses Lingeling as backend.
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
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.
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.
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)
For building and usage of Boolector on Windows, please see COMPILING_WINDOWS.md.
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
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 c
684C
opy 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.