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.

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

  • 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: Defines the C interface (stp/c_interface.h) for parsing input files, constructing expressions, executing queries, etc., and the C++ interface (stp/cpp_interface.h) for invoking STP.

  • 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 parsers for the CVC, SMT-LIB1, and SMT-LIB2 input formats.

  • Printer: Implements various output formatters.

  • Sat: Adapters presenting each supported SAT solver – MiniSat, CryptoMiniSat, CaDiCaL and Riss – 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 that is compiled into STP also lives under lib/:

  • extlib-abc: The ABC package, used to build AIGs and convert them to CNF. A git submodule, pointing at stp/abc rather than at ABC itself. That fork keeps two branches: master mirrors upstream untouched, and stp – the branch the submodule is pinned to – carries our changes as commits on top of the upstream revision we have taken. Bumping ABC means rebasing stp onto a newer master in that repository, then moving the pin here.

    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-cli11: CLI11, the command-line parser of the stp executable. Header-only, so it is compiled into the tool but never into libstp. A git submodule.

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

  • extlib-symfpu: SymFPU, a header-only implementation of the floating-point operations in terms of bitvectors, used by FloatBlaster. A git submodule.

  • extlib-mimalloc: mimalloc, the allocator the STP executables link against by default. A git submodule; see STP_ALLOCATOR in Building STP for the alternatives.

  • extlib-unordered-dense: ankerl::unordered_dense, a densely stored hash map and set, used in place of std::unordered_map where it pays off.

The executables are built from tools/:

  • stp: The main command-line solver.

  • extdiff: Built alongside it, unconditionally. Compares two STP binaries on the same query, which the baseline-differential test uses.

  • test_fpbackend and test_fprewrites: Floating-point checkers, built when either ENABLE_TESTING or BUILD_EXTRA_TOOLS is on; they are registered as tests.

  • 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 additionally needs a build with CryptoMiniSat and is skipped without one.

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