Source code layout

The lib/ directory is organized into subdirectories for each distinct component of STP. The headers that go with them live under include/stp/.

  • AbsRefineCounterExample: Functions related to abstraction refinement and counterexample construction.

  • Api: The public API, stp/stp.hpp and stp/stp.h (see The 3.x API (C++, C and Python)): the C++ implementation, the C layer over it under c/, and the tables under tables/ from which every language’s kinds, options, errors and statistics are generated (gen/).

  • AST: Implements the abstract syntax tree for parsed solver inputs.

  • Compat2: libstp2, the 2.x C interface (stp/c_interface.h) re-implemented over the C API, for clients that have not moved to it. Its headers, c_interface.h and the header-only fp.hpp and uf.hpp over it, are its own, in lib/Compat2/include/stp/; installed, they sit beside the rest.

  • Extensionality: The decision procedure for equalities between whole arrays, described in Array extensionality.

  • FloatBlaster: Bit-blasting of the floating-point theories, built on the header-only SymFPU library.

  • Globals: The handful of thread-local globals that the parser shares with the rest of STP.

  • Incremental: The driver for incremental solving – push, pop and repeated check-sat against a solver kept alive between queries. See Incremental solving.

  • Interface: The engine’s C++ interface (stp/cpp_interface.h), through which the parser and the API build terms and run queries.

  • NodeFactory: Creates AST nodes. Which factory a client asks for decides how much work happens as nodes are built, from hash consing alone up to the rewriting done by SimplifyingNodeFactory.

  • Parser: Contains the SMT-LIB2 parser.

  • Printer: Implements various output formatters.

  • Sat: Adapters presenting each supported SAT solver – MiniSat, CryptoMiniSat and CaDiCaL – through STP’s common SATSolver interface. The solvers themselves are external; only the wrappers live here.

  • Simplifier: Simplification algorithms for the AST, including the constant bit propagator under constantBitP/.

  • STPManager: Class that holds all the components together.

  • ToSat: Conversion of AST to SAT.

  • Util: Handy utilities for smaller tasks.

Third-party code compiled into STP. Two of these are fetched during configuration rather than living under lib/, because STP builds them as part of itself and so needs their sources present before it configures its own targets; the other two are small enough to be carried in the tree:

  • ABC: The ABC package, used to build AIGs and convert them to CNF. Fetched from stp/abc rather than from ABC itself. In that fork master mirrors upstream untouched and our changes sit as commits on top of an upstream revision we have taken. There are two lines of those: stp, which is where they are reviewed and which sits on a recent upstream, and the line ABC_GIT_TAG in cmake/FindABC.cmake pins, which carries the same set on the older upstream the pin has followed so far. A change to ABC goes onto both, and each bump of the pin is held by a tag named stp-at-<upstream>-pr<NNNN>. Moving the pin onto stp would bump the upstream base along with it; bumping that base is its own piece of work, and means rebasing stp onto a newer master first.

    To work on the fork, clone it, build libabc-pic in it, and configure with -DABC_DIR=<clone>: the build then uses that copy and fetches nothing, so it can be edited, committed and pushed from where it is.

    The fork exists because the changes cannot live upstream: some are fixes that were offered to ABC and not taken, and the rest adjust which parts of ABC get built. STP uses four of its packages – aig/aig, aig/gia, opt/dar and sat/cnf – and ABC’s build compiles every other one too, including SAT solvers that STP already links its own copies of.

  • extlib-constbv: A library that implements multi-word fixed-length integers, based on Steffen Beyer’s Bit::Vector perl module.

  • mimalloc: mimalloc, the allocator the STP executables link against by default. Fetched, and built as part of STP; see STP_ALLOCATOR in Building STP for the alternatives.

  • ankerl::unordered_dense: a densely stored hash map and set, used in place of std::unordered_map where it pays off. A single header, fetched at a pinned commit of stp/unordered_dense.

CLI11, the command-line parser of the stp executable, and SymFPU, the header-only implementation of the floating-point operations in terms of bitvectors that FloatBlaster uses, used to sit here as submodules too. Both are now fetched by cmake/FindCLI11.cmake and cmake/FindSymFPU.cmake – being headers, there is nothing about them for STP’s own build to reach into, which is what keeps ABC and mimalloc here. STP’s fixes to SymFPU are commits on the stp branch of its fork, stp/symfpu, which is what the build fetches.

The executables are built from tools/; Running STP and Developer tools describe how to run them.

  • stp: The main command-line solver.

  • extdiff: Built alongside it, unconditionally. A driver the baseline-differential test compiles against two trees and runs on the same queries, comparing what each reports. It is written against the 2.x C interface, so that the same source builds against an older STP, and links libstp2.

  • test_fpbackend and test_fprewrites: Floating-point checkers, built when either ENABLE_TESTING or BUILD_EXTRA_TOOLS is on; they are registered as tests. c_handle_churn_benchmark, which times C API handle creation, is built under the same condition.

  • The rest are development aids, built only when BUILD_EXTRA_TOOLS is enabled: difficulty_bench measures the difficulty scorer against AIG sizes; fp_rewrite_gen searches for floating-point rewrite rules; rewrite_rule_gen searches for bitvector ones; and propagator_bench times the propagators, checks how much they deduce, and with --bcp-check compares that against what unit propagation on the bit-blasted encoding deduces on its own. propagator_bench and rewrite_rule_gen additionally need a build with CryptoMiniSat and are skipped without one.

The Python package is in bindings/python, and the tests are in tests/ (see Testing).

Changing a dependency

STP builds every dependency from a pinned revision, as that revision stands. When STP needs a dependency to be different – a fix, an interface it needs, a build that works on a platform – the change is a commit in STP’s fork of that dependency, and the pin moves to the commit. It is not a patch file, a PATCH_COMMAND, or CMake that edits the fetched sources: a change made at build time cannot be read where the dependency is read, has to be re-applied by hand at every bump with nothing to say where it stopped applying, and leaves two different programs calling themselves the pinned revision.

scripts/check-dependency-patches.py holds the build to that, and CI runs it. It fails on a tracked *.patch or *.diff, on PATCH_COMMAND, git apply or patch -p, and on CMake that reads a fetched dependency’s sources whole or writes into its source tree. Its ALLOWED list names the exceptions still being worked off, each with the reason, and an entry that no longer excuses anything fails the check as well.

The forks, and the branch each pin is a commit of:

  • ABC: stp/abc, on the pinned line described above, with each change also on stp.

  • CaDiCaL: stp/cadical, stp (3.x); stp-2.1.3 is the 2.x line CI keeps building.

  • CryptoMiniSat: stp/cryptominisat, stp-5.17.0-ipasir-up, which is upstream’s release with the IPASIR-UP interface proposed as msoos/cryptominisat#842.

  • IMath: stp/imath, stp.

  • Kissat: stp/kissat, stp; master and upstream mirror the unmodified upstream revision.

  • LibBF: stp/libbf, stp.

  • MiniSat: stp/minisat, master.

  • SymFPU: stp/symfpu, stp.

  • unordered_dense: stp/unordered_dense, stp.

CLI11, nlohmann/json, mimalloc and GoogleTest are built from upstream releases unmodified, and have no fork; a dependency that needs a change gets one. HiGHS is the exception still on the ALLOWED list: its optional root-cut logging is a patch until it moves to a fork too.

A change that would serve the dependency’s other users belongs upstream as well, and once a release carries it the pin can move back to that release.