Installation on macOS#

Easy installation with Homebrew#

The easiest way to install BLACK on macOS is through Homebrew. It is a popular package manager for open source applications on macOS. If you do not have it installed already, installing it is very easy. Just follow the instructions on their website.

Once Homebrew is installed, BLACK installation is as easy as typing this command:

$ brew install black-sat/black/black-sat

The Homebrew package works both on Intel and Apple Silicon systems.

Note

There is a package called black in the Homebrew repository, which is a popular code formatter for Python. If you run brew install black, you will install this other package, hence pay attention to type the correct command as written above.

If for any reason you want to compile BLACK from source, go ahead to the next section.

Compilation from source#

Dependencies#

To compile BLACK you need the following packages:

  1. CMake 3.10 or above

  2. libfmt 7.x or above

  3. Hopscotch-map 2.x

  4. nlohmann-json 3.5 or above

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

  1. Z3 4.8.x or above

  2. cvc5 1.0 or above (not cvc4)

  3. MathSAT 5.6.7 or later

  4. CryptoMiniSAT 5.x

  5. 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.

All the dependencies are available through Homebrew:

$ brew install cmake hopscotch-map nlohmann-json fmt

Now at least one backend must be chosen and installed.

For Z3:

$ brew install z3

For CryptoMiniSAT:

$ brew install cryptominisat

For MiniSAT:

$ brew install minisat

Currently, there are no Homebrew 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#

First, clone the GitHub repository:

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

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)

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

  2. BLACK_DEFAULT_BACKEND=<backend>: default backend (default: z3, if found).
    Accepted values: mathsat, cmsat, z3, cvc5, minisat

  3. ENABLE_FORMULAS_TESTS=YES/NO: whether to enable the formulas test suite (default YES)

  4. BLACK_TESTS_SAT_BACKEND=<backend>: backend to use when running tests

Also, recall some useful standard cmake options:

  1. 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.
  2. 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.