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.
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#
To compile BLACK you need the following packages:
Possible backends (of which at least one must be present):
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.
$ brew install z3
$ brew install cryptominisat
$ 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:
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
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
ENABLE_MATHSAT=YES/NO: whether to enable the MathSAT backend (default
YES, if found)
ENABLE_CMSAT=YES/NO: whether to enable the CryptoMiniSAT backend
(default YES, if found)
ENABLE_Z3=YES/NO: whether to enable the Z3 backend (default YES, if
ENABLE_CVC5=YES/NO: whether to enable the cvc5 backend (default YES, if
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:
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_INSTALL_PREFIX=<path>: the install prefix used by the
make installcommand.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:
Debugbuilds run the slowest but build quick and ease development.
Releasebuilds are the fastest and are those that should be employed by the users.
RelWithDebInfoare optimized like
Releasebuilds but maintain debug information for easy debugging.