STP is built with CMake, version 2.8.8 or newer.
CMake is a meta build system that generates build files for other tools such as make(1), Visual Studio, Xcode, etc. For a list of generators supported on your platform, consult cmake --help
.
Here are a few interesting configuration variables. These apply to all generators.
CMAKE_BUILD_TYPE
- The build type (e.g. Release)CMAKE_INSTALL_PREFIX
- The prefix for install (e.g. /usr/local )DBUILD_STATIC_BIN
- Build static binary and libraryENABLE_ASSERTIONS
- If TRUE STP will be built with asserts.ENABLE_TESTING
- Enable running testsENABLE_PYTHON_INTERFACE
- Enable building the Python interfacePYTHON_EXECUTABLE
- Set python executable in case you have more than one python installedSANITIZE
- Use Clang's sanitization checksNO_BOOST
- Build without using the Boost libraryTEST_QUERY_FILES
- Test STP externally by passing it query files in tests/query-filesTUNE_NATIVE
- Tune compilation to native architectureSTP relies on a few dependencies, namely boost, flex/bison and minisat. Installing the required header files and binaries can be achieved through the following. (Tested on Ubuntu 14.04.)
$ sudo apt-get install cmake bison flex libboost-all-dev python perl
Installing minisat can be achieved by running
$ git clone https://github.com/stp/minisat.git $ cd minisat $ mkdir build && cd build $ cmake .. $ make $ sudo make install $ sudo ldconfig
STP uses minisat as its SAT solver by default but it also supports other SAT solvers including CryptoMiniSat4 as an optional extra. If it is installed it will be detected during the CMake configure and will be available for use in stp
.
You can get it from https://github.com/msoos/cryptominisat
$ git clone https://github.com/msoos/cryptominisat $ cd cryptominisat $ mkdir build && cd build $ cmake .. $ make $ sudo make install $ sudo ldconfig
In case you wish to use CryptoMiniSat4, you need to build it to create a static library:
$ git clone https://github.com/msoos/cryptominisat $ cd cryptominisat $ mkdir build && cd build $ cmake -DSTATICCOMPILE=ON .. $ make $ sudo make install $ sudo ldconfig
Otherwise, just build STP statically:
$ git clone https://github.com/stp/stp.git $ cd stp $ mkdir build && cd build $ cmake -DBUILD_STATIC_BIN=ON -DBUILD_SHARED_LIBS=OFF .. $ make $ sudo make install $ sudo ldconfig
Testing is optional. STP's testing depends on GoogleTest, lit and OutputCheck. To obtain these run
$ git submodule init $ git submodule update $ pip install lit
To build STP make sure you have its dependencies installed then run
$ mkdir build && cd build $ cmake -G 'Unix Makefiles' /path/to/stp/source/root $ make
If you'd prefer a more in-depth explanation of how to configure, build test and install STP read on...
CMake supports building in and out of source. It is recommended that you build out of source. For example in a directory outside of the STP root source directory run
$ mkdir build
The simplest thing you can do is use the default configuration by running
$ cd build/ $ cmake -G 'Unix Makefiles' /path/to/stp/source/root
You can easily tweak the build configuration in several ways
Run cmake-gui /path/to/stp/source/root
instead of cmake
. This user interface lets you control the value of various configuration variables and lets you pick the build system generator.
Run ccmake
instead of cmake
. This provides an ncurses terminal interface for changing configuration variables.
Pass -D<VARIABLE>=<VALUE>
options to cmake
(not very user friendly). It is probably best if you only configure this way if you are writing scripts.
You can also tweak configuration later by running make edit_cache
. Then edit any configuration variables, reconfigure and then regenerate the build system. After configuration you can build by running make
.
Remember you can use the -j<n>
flag to significantly to decrease build time by running <n>
jobs in parallel (e.g. make -j4
).
To run the tests (CMake must of been configured to enable testing) run make check
. See http://stp.github.io/testing/ for more information on testing.
STP and its library can be used directly from the build directory but it can be installed if desired.
To install run make install
and to uninstall run make uninstall
. The root of installation is controlled by the CMAKE_INSTALL_PREFIX
variable at configure time. Remember you can easily change this at anytime by running make edit_cache
and editing the value of CMAKE_INSTALL_PREFIX
.
Ninja is a fast alternative to the make
. CMake has support for it. To use it you need to run
To build STP make sure you have its dependencies installed then run
$ mkdir build && cd build $ cmake -G 'Ninja' /path/to/stp/source/root $ ninja
The instructions are identical to that of the “Using Make” section except that you
ninja
instead of make
command-j
is not needed. Ninja tries to guess how many jobs to run in parallel.TODO