Installation on Linux#

Binary packages#

We provide binary packages for Ubuntu 20.04, Ubuntu 22.04 (the latest LTS) and Fedora 37 and 38 (the latest versions).

Ubuntu 20.04	Ubuntu 22.04	Fedora 37	Fedora 38

`sudo apt install ⟨file⟩`	`sudo apt install ⟨file⟩`	`sudo dnf install ⟨file⟩`	`sudo dnf install ⟨file⟩`

These packages should work on other Debian-based and RedHat-based distributions as well, and include the Z3 backend. If they do not work for you, or if you want to use other backends, BLACK can be compiled from source. If you think that the packages should work but do not, please open a GitHub issue.

Compilation from source#

To retrieve BLACK’s source code, clone the GitHub repository:

$ git clone https://github.com/black-sat/black.git

Dependencies#

BLACK can be compiled by any C++20 compliant compiler. On Linux, we require Clang 13 or above, and g++ 10 or above.

To compile BLACK you need the following packages:

CMake 3.10 or above
libfmt 7.x or above
Hopscotch-map 2.x
nlohmann-json 3.5 or above

Possible backends (of which at least one must be present):

Z3 4.8.x or above
cvc5 1.0 or above (not cvc4)
MathSAT 5.6.7 or later
CryptoMiniSAT 5.x
MiniSAT 2.2

The MathSAT and MiniSAT backends require zlib 1.x. MathSAT also requires gmp 6.x and its C++ wrapper.

You can choose any of these backends to compile and use BLACK. Note however that not all the backends support the same features. In particular, Z3, cvc5 or MathSAT are required to handle first-order formulas, and only Z3 and cvc5 support quantified first-order formulas.

Debian-based distributions#

Most of the required dependencies can be installed from the package repository:

$ sudo apt install build-essential cmake libtsl-hopscotch-map-dev libfmt-dev

Unfortunately, nlohmann-json is not packaged, so it needs to be installed from source. That is however very easy.

To install nlohmann-json:

$ git clone https://github.com/nlohmann/json.git
$ cd json
$ mkdir build && cd build
$ cmake -DJSON_BuildTests=OFF ..
$ sudo make install

Now at least one backend must be chosen and installed.

For Z3:

$ sudo apt install libz3-dev

For CryptoMiniSAT:

$ sudo apt install libcryptominisat5-dev

For MiniSAT:

$ sudo apt install minisat

Currently, there are no packages for cvc5 and MathSAT. To install cvc5, binary packages are available or it can be built from source. Refer to their website for more information. For MathSAT, we provide a script to download the binary package and put it in a place where BLACK’s build system can find it.

From BLACK’s source directory, run:

$ ./download-mathsat.sh

This will unpack MathSAT into the external/ subdirectory and will not touch your system. The dependencies of MathSAT are available from the package repository:

$ sudo apt install libz-dev libgmp-dev

RedHat-based distributions#

Most of the required dependencies can be installed from the package repository:

$ sudo dnf install make cmake gcc gcc-c++ fmt-devel

Unfortunately, hopscotch-map and nlohmann-json are not packaged, so they need to be installed from source. That is however very easy.

To install hopscotch-map:

$ git clone https://github.com/Tessil/hopscotch-map.git
$ cd hopscotch-map
$ git switch v2.3.0
$ mkdir build && cd build
$ cmake ..
$ make
$ sudo make install

To install nlohmann-json:

$ git clone https://github.com/nlohmann/json.git
$ cd json
$ mkdir build && cd build
$ cmake -DJSON_BuildTests=OFF ..
$ sudo make install

Now at least one backend must be chosen and installed.

For Z3:

$ sudo dnf install z3-devel

For CryptoMiniSAT:

$ sudo dnf install cryptominisat-devel

For MiniSAT:

$ sudo dnf install minisat2-devel

Currently, there are no rpm packages for cvc5 and MathSAT. To install cvc5, stand-alone binary packages are available or it can be built from source. Refer to their website for more information. To install MathSAT, we provide a script to download the binary package and put it in a place where BLACK’s build system can find it.

From BLACK’s source directory, run:

$ ./download-mathsat.sh

This will unpack MathSAT into the external/ subdirectory and will not touch your system. The dependencies of MathSAT are available from the package repository:

$ sudo dnf install zlib-devel gmp-devel gmp-c++

Compilation#

Once installed all the dependencies, you can compile BLACK. First clone the repository (say into the black directory).

Then, compilation and installation are easy:

$ cd black
$ mkdir build
$ cd build
$ cmake ..
$ make
$ sudo make install

To configure the build to your needs, cmake accepts additional options that can be passed as additional parameters with the syntax -DOPTION=value.

1. ENABLE_MATHSAT=YES/NO: whether to enable the MathSAT backend (default YES, if found)

2. ENABLE_CMSAT=YES/NO: whether to enable the CryptoMiniSAT backend (default YES, if found)

3. ENABLE_Z3=YES/NO: whether to enable the Z3 backend (default YES, if found)

4. ENABLE_CVC5=YES/NO: whether to enable the cvc5 backend (default YES, if found)

ENABLE_MINISAT=YES/NO: whether to enable the MiniSAT backend (default YES, if found)
BLACK_DEFAULT_BACKEND=<backend>: default backend (default: z3, if found).

Accepted values: mathsat, cmsat, z3, cvc5, minisat
ENABLE_FORMULAS_TESTS=YES/NO: whether to enable the formulas test suite (default YES)
BLACK_TESTS_SAT_BACKEND=<backend>: backend to use when running tests

Also, recall some useful standard cmake options:

CMAKE_INSTALL_PREFIX=<path>: the install prefix used by the make install command.

Use this option if you do not want to install BLACK system-wise, for example to put it into a local subdirectory of your home directory.
CMAKE_BUILD_TYPE=<configuration>: whether to configure a debug or release build.

Accepted values: Release, Debug, RelWithDebInfo (default: Release).

Debug builds run the slowest but build quick and ease development. Release builds are the fastest and are those that should be employed by the users. RelWithDebInfo are optimized like Release builds but maintain debug information for easy debugging.