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.

Useful configuration variables

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 library
  • ENABLE_ASSERTIONS - If TRUE STP will be built with asserts.
  • ENABLE_TESTING - Enable running tests
  • ENABLE_PYTHON_INTERFACE - Enable building the Python interface
  • PYTHON_EXECUTABLE - Set python executable in case you have more than one python installed
  • SANITIZE - Use Clang's sanitization checks
  • NO_BOOST - Build without using the Boost library
  • TEST_QUERY_FILES - Test STP externally by passing it query files in tests/query-files
  • TUNE_NATIVE - Tune compilation to native architecture

Dependencies

STP 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

CryptoMiniSat4

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

Static library and binary

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

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

Building

Quick start

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

Build directory

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

Configuration & 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).

Testing (optional)

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.

Install (optional)

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

Ninja is a fast alternative to the make. CMake has support for it. To use it you need to run

Quick start

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

More in depth

The instructions are identical to that of the “Using Make” section except that you

  • Instruct CMake to use ninja instead of unix make files.
  • Use ninja instead of make command
  • Specifying -j is not needed. Ninja tries to guess how many jobs to run in parallel.

Visual Studio

TODO