STP

STP is a constraint solver (or SMT solver) for the quantifier-free theories of bitvectors, arrays, floating-point and linear real arithmetic. 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 that carries the IPASIR-UP propagator interface the linear-arithmetic theory drives. A CryptoMiniSat without the interface still builds STP; the theory then runs full-lazy on it, configure warns about it, and --cadical restores propagation for a run. 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.

Incremental Kissat is an optional backend. Configure STP with --kissat --auto-download to build the pinned fork, then select it with stp --kissat input.smt2. A prebuilt checkout can be selected with --kissat-dir=/path/to/kissat. The Kissat integration guide describes the build options and incremental API.

With --cadical, --cadical-elim=0|1 controls variable elimination, and --cadical-elimmineff=N / --cadical-elimmaxeff=N set its minimum and maximum effort. For example:

stp input.smt2 --cadical --cadical-elim=0
stp input.smt2 --cadical --cadical-elimmineff=10000 --cadical-elimmaxeff=100000

Unspecified options retain the backend settings and STP's automatic policies. Explicit values override the corresponding CADICAL_* environment variables and search-bias settings, survive backend rebuilds, and an explicit --cadical-elim=1 keeps elimination enabled when incremental inprocessing is retired. Invalid values and requests with another backend are rejected before solving. Add -s to see the effective settings. Effort limits follow CaDiCaL's cost model; it can raise the allowance for large formulas, so the maximum is not a hard resolution-count limit. These are tuning controls with measured tradeoffs; none of them is set by default.

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. Running STP describes the command line: input formats, output and exit status, choosing a SAT solver, limits, statistics, and writing CNF.

Overflowing a 32-bit integer using the Python interface:

from stp import *

x, y = BitVecs('x y', 32)
s = Solver()
s.add(ULT(x + y, 20), UGT(x, 10), UGT(y, 10))
print(s.check())  # sat
print(s.model())  # e.g. [x = 4294967288, y = 11]

The manual documents the accepted subset of SMT-LIB2, the C, C++ and Python API, 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, Testing how to build and run the test suite, and Developer tools the programs under tools/ other than stp. STP is written by many people, who work on it in their own time, or because it helps with their work or study.