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/
For a quick install:
sudo apt-get install git build-essential cmake bison flex python3
git clone https://github.com/stp/stp
cd stp
./configure.sh --auto-download
cmake --build build -j$(nproc)
sudo cmake --install build
That builds against CaDiCaL, which is the default SAT backend. CryptoMiniSat, MiniSat and Riss are also supported, asked for at configure time; see Building STP.
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. CryptoMiniSat is the exception, and the one thing libgmp-dev is for: install it, or run ./scripts/deps/setup-cms.sh.
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.
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.
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.