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.

Most of the dependencies are available through Homebrew:

$ brew install cmake nlohmann-json fmt llvm

One package is installable through Homebrew but using our tap:

$ brew install black-sat/black/hopscotch-map

Note that the llvm package is required because BLACK does not currently compile with the stock Apple clang version, which does not support enough C++20 features.

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 Homebrew:

$ brew install zlib gmp

Compilation#

First, clone the GitHub repository:

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

Now, we have to set the correct environment variables to use the clang compiler from the Homebrew llvm package:

$ export CC=$(brew --prefix llvm)/bin/clang
$ export CXX=$(brew --prefix llvm)/bin/clang++
$ export LDFLAGS="-L$(brew --prefix llvm)/lib -Wl,-rpath,$(brew --prefix llvm)/lib"
$ export CXXFLAGS="-I$(brew --prefix llvm)/include"

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.