STP

STP is a constraint solver (or SMT solver) for the quantifier-free theories of bitvectors, arrays and floating-point. These types of constraints are generated by program analysis tools, theorem provers, automated bug finders, cryptographic attack tools, intelligent fuzzers, model checkers, and by many other applications.

Comprehensive details are provided in the manual and homepage: https://stp.github.io/

Build and install

For a quick install:

sudo apt-get install git build-essential cmake bison flex python3 \
                     libgmp-dev pkg-config zlib1g-dev
git clone https://github.com/stp/stp
cd stp
./configure.sh --auto-download
cmake --build build -j$(nproc)
sudo cmake --install build

CryptoMiniSat is the backend STP solves with by default, and --auto-download covers it like every other dependency: STP clones and builds stp/cryptominisat at a pinned commit. An installed one is found and preferred. libgmp-dev, pkg-config and zlib1g-dev are its packages, not STP's.

CaDiCaL is compiled in alongside it, and is what a build without CryptoMiniSat solves with. --cryptominisat, --cadical or --minisat selects a compiled-in backend for one run.

STP builds CryptoMiniSat with -DNOCADICAL=ON, so it bundles no CaDiCaL of its own and STP links the revision it pins -- which is what keeps --cadical-factor available. That option removes only backbone extraction, which STP never asks for.

There are no submodules: --auto-download fetches every dependency at a pinned revision and builds it with this build's own compiler and flags. Without it, configuration stops and says what to install or where to point it -- nothing here reaches the network unless it is asked to.

Or, using Homebrew:

brew install stp

Or, with Docker, which needs nothing installed but Docker itself and reads the problem on standard input:

git clone https://github.com/stp/stp
cd stp
docker build -t stp .
echo "(set-logic QF_BV)
(assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2)))
(check-sat)
(exit)" | docker run --rm -i stp

Building STP covers the rest: the configuration variables, the SAT backends and how to choose between them, building against dependencies you have built but not installed, static builds, and Windows.

Usage

Run with an SMT-LIB2 file, which is the recommended input format:

stp myproblem.smt2

STP also reads from standard input, as in the Docker example above.

Overflowing a 32-bit integer using the Python interface:

import stp

s = stp.Solver()
x = s.bitvec('x', width=32)
y = s.bitvec('y', width=32)
s.add(x + y < 20)
s.add(x > 10)
s.add(y > 10)
print(s.check())  # True
print(s.model())  # e.g. {'x': 4294967287, 'y': 11}

The manual documents the accepted subset of SMT-LIB2, the C and C++ interfaces, incremental solving and array extensionality, and how STP works. Its sources are in docs/, and docs/README.md says how to build and read it locally.

Contributing

Source code layout describes what lives where, and Testing how to build and run the test suite. STP is written by many people, who work on it in their own time, or because it helps with their work or study.