Building STP

The overview page has the recipe that works from a clean checkout. This page is the detail behind it: what STP depends on, which SAT backend to build against, and the configuration variables worth knowing.

STP is built with CMake, version 3.18 or newer. CMake is a meta build system that generates build files for other tools such as make(1), Visual Studio and Xcode. The 3.18 floor comes from the vendored mimalloc, which is the default allocator; on an older CMake, configure with -DSTP_ALLOCATOR=system to skip it and use the C library’s malloc instead.

Dependencies

STP relies on flex, bison and python3, plus at least one SAT backend. Nothing else has to be installed: with -DENABLE_AUTO_DOWNLOAD=ON the build fetches every library it needs, and lit, which drives the tests, into a virtual environment of its own. Configuration fails if no backend is enabled.

On a Debian-like platform most of it comes from the package manager:

sudo apt-get install git build-essential cmake bison flex python3

A python3 interpreter is needed at build time – it generates the AST kind tables – and also for the Python interface and the test suite. git is needed to fetch the dependencies, which are cloned rather than downloaded as archives where their revision is a commit rather than a release.

The SAT backends bring their own dependencies, which are needed only if you build that backend, and which the scripts/deps script for each one names: CryptoMiniSat needs GMP (libgmp-dev), MiniSat needs zlib (zlib1g-dev). Neither is used by STP itself.

STP has no submodules. Everything it does not contain itself is fetched at a pinned revision, and with -DENABLE_AUTO_DOWNLOAD=ON that needs nothing installed beforehand.

Most are ExternalProjects: built at build time, installed into STP_DEP_DIR, and so built once however many build directories are pointed at the same one. ABC is among them, which matters because it is 920 C files – but it also means every build sharing a dependency directory shares one ABC, compiled with one set of flags. Its optimisation level is whichever configuration built it first; its defines are not left to chance, because STP’s own sources include ABC’s headers and the two have to agree, so they are recorded in the directory’s stamp and a mismatch is reported.

-DABC_DIR points at an existing ABC build, which is how to work on the stp/abc fork – see Source code layout.

mimalloc is the exception: STP configures its build rather than consuming its output, so it is fetched with CMake’s FetchContent, which downloads during configuration so that add_subdirectory has something to descend into. -DFETCHCONTENT_SOURCE_DIR_MIMALLOC names an existing checkout.

The command-line parser CLI11 and the header-only floating-point library SymFPU are headers and nothing more; CLI11_DIR and SYMFPU_INCLUDE_DIRS name existing copies.

One is not vendored: LibBF, which converts the real literals in floating-point input – ((_ to_fp 8 24) RNE 1.5). It is required, and there are three ways to get it, tried in this order:

  • -DLIBBF_DIR=<path> naming a directory that holds libbf.h and a built bf library. With it unset, deps/libbf is used if it holds one, which is where an earlier build put it

  • an installed copy, found the way any library is – including one that an earlier build installed into STP_DEP_DIR (see below)

  • -DENABLE_AUTO_DOWNLOAD=ON, which clones stp/libbf at a pinned commit and builds it as part of this build, with this build’s compiler and flags

Without any of the three, configuration fails and says so. An offline build wants the first.

Upstream LibBF publishes release tarballs and no git repository, which is what stp/libbf is for. It is laid out like STP’s ABC fork: master holds the release tarballs verbatim, one commit each, and stp – the branch the pin names – adds STP’s MSVC portability changes on top. Moving to a newer release means importing its tarball there and rebasing stp onto it, then moving the pin here.

SAT backends

A query with no solver flag on it goes to the first of these that the build compiled in:

  1. CryptoMiniSat

  2. CaDiCaL

  3. MiniSat

CryptoMiniSat is therefore the default wherever it is linked, and CaDiCaL is what a stock build solves with. CaDiCaL is also the one always available: it is enabled when nothing is said, needs no system library, and the build can produce one itself, so a query is never left without a solver. CryptoMiniSat is linked whenever it is installed (-DUSE_CRYPTOMINISAT=AUTO, the default). Either way --cadical, --cryptominisat or --minisat overrides the order for one run.

The two other values are for builds that would rather not depend on what the machine has lying around: -DUSE_CRYPTOMINISAT=ON makes a missing CryptoMiniSat a configuration error, and -DUSE_CRYPTOMINISAT=OFF never looks for one, which is what pins a build’s set of backends to the flags that produced it. With -DENABLE_AUTO_DOWNLOAD=ON there is nothing to do: STP clones and builds stp/cryptominisat at a pinned commit, as it does for its other dependencies. An installed one is found and preferred, including one installed into deps/install:

git clone https://github.com/msoos/cryptominisat
cd cryptominisat
mkdir build && cd build
cmake ..
cmake --build . -j$(nproc)
sudo cmake --install .
command -v ldconfig && sudo ldconfig

It is the one dependency STP does not build for you: it reaches the build as a CMake package rather than as a header and a library, and an ExternalProject would write that package only after the configure that has to read it. Install it, or run the script.

CaDiCaL is compiled in by default, is what a build without CryptoMiniSat solves with, and is worth having on hard bitvector problems. With -DENABLE_AUTO_DOWNLOAD=ON there is nothing to do but ask for it; otherwise an installed CaDiCaL is found the way any library is, or CADICAL_DIR points at a checkout:

git clone https://github.com/arminbiere/cadical
cd cadical
git checkout rel-3.0.1
./configure -fPIC
make

Then configure STP with -DUSE_CADICAL:BOOL=ON -DCADICAL_DIR:PATH=<path>, where <path> is the checkout containing src/cadical.hpp and build/libcadical.a. -fPIC is required, because libcadical.a is linked into STP’s shared library.

Whichever way it arrives, STP works out which CaDiCaL it has: a checkout carries a VERSION file, and an installed copy is asked directly, by compiling and running CaDiCaL::Solver::version(). That decides whether --cadical-factor can be compiled in, and the answer is printed at configure time.

CryptoMiniSat stays the default for a build that has it, and CaDiCaL is the default for one that does not; --cadical, --cryptominisat or --minisat selects a compiled-in backend at run time. With a CaDiCaL 3.x build, --cadical-factor controls CaDiCaL’s bounded variable addition: on – the default – off, or auto, which enables it only for problems with array operations. auto was the default until bounded variable addition was measured on bitvector-only problems and found to pay there too.

CryptoMiniSat and CaDiCaL together

Enabling both is supported and needs nothing said about it. It used to: CryptoMiniSat 5.14 and later fetch, build and install a CaDiCaL of their own, so its prefix held a libcadical.a, a cadical/cadical.hpp and a CMake package under the same names STP’s own CaDiCaL uses – which shadowed STP’s header, captured STP’s lookup, and, when libcryptominisat5 was static, put two sets of CaDiCaL symbols on one link line. Fitting both backends in took a shared CryptoMiniSat in a prefix of its own, or giving up STP’s pinned CaDiCaL for the 2.x copy CryptoMiniSat carried.

STP builds stp/cryptominisat with -DNOCADICAL=ON, which fetches and installs no CaDiCaL at all, so none of that arises. -DUSE_CADICAL=ON -DUSE_CRYPTOMINISAT=ON is an ordinary configure, and the CaDiCaL linked is the one STP pins.

That option is sound because backbone extraction – reached only through CryptoMiniSat’s backbone simplification token or its backbone_simpl() API, and in neither default schedule – is the only thing CryptoMiniSat uses CaDiCaL for, and STP calls neither.

stp --version reports the version of each backend actually linked, so it is the quickest way to confirm what you ended up with.

MiniSat is optional and off by default; enable it with -DUSE_MINISAT:BOOL=ON, which also needs zlib – MiniSat reads gzipped DIMACS and says so in its public headers, so configuration fails without it. With -DENABLE_AUTO_DOWNLOAD=ON there is nothing else to do: STP clones and builds stp/minisat at a pinned commit, which is an updated fork of a MiniSat that has not been touched upstream since 2010 and no longer compiles as it stands. Your distribution’s minisat package works too, as does one built by hand:

git clone https://github.com/stp/minisat
cd minisat
mkdir build && cd build
cmake ..
cmake --build . -j$(nproc)
sudo cmake --install .
command -v ldconfig && sudo ldconfig

Every dependency is fetched and built by the build itself under -DENABLE_AUTO_DOWNLOAD=ON; none of them needs a script beforehand.

Building against non-installed libraries

To build STP’s dependencies without installing them, tell CMake where the artefacts are:

  • -DMINISAT_INCLUDE_DIRS:PATH=<path> and -DMINISAT_LIBDIR:PATH=<path> – the paths to minisat/core/Solver.h and to the minisat libraries

  • -Dcryptominisat5_DIR:PATH=<path> – the path to cryptominisat5Config.cmake

If the development libraries were not installed, MINISAT_LIBDIR can be set to minisat’s build directory, and cryptominisat5_DIR to CryptoMiniSat’s.

Floating-point support

Floating-point support is always built, backed by SymFPU. STP carries four fixes to it that upstream has not taken; they are applied to the copy the build fetches, so there is nothing to do. An existing clone can be used instead, via -DSYMFPU_INCLUDE_DIRS=<directory containing the clone> – that one is taken as-is, so it must already carry those fixes, which are in cmake/deps-utils/symfpu.

STP solves the SMT-LIB floating-point theory and exposes floating-point terms through the C, C++ (stp/fp.hpp) and Python APIs. Real literals under to_fp – ((_ to_fp 8 24) RNE 0.1) – are folded to their exactly-rounded bits while parsing, in any format and under any of the five rounding modes. One operation is format-bounded: fp.rem is refused past roughly binary64-sized formats, because its circuit unrolls one divide step per representable exponent difference, which for Float128 would be some 33000 steps deep.

Configuration variables

These apply to all generators:

  • CMAKE_BUILD_TYPE – the build type, e.g. Release

  • CMAKE_INSTALL_PREFIX – the prefix to install under, e.g. /usr/local

  • ENABLE_ASSERTIONS – build with assertions. Three-valued: ON and OFF are honoured as given, and if it is left unset the build type decides – off for Release, on for everything else. It used to be a plain on/off flag that Release overrode unconditionally, so -DENABLE_ASSERTIONS=ON -DCMAKE_BUILD_TYPE=Release silently produced a build without them; it now produces an asserting Release build

  • ENABLE_TESTING – enable running the tests

  • ENABLE_PYTHON_INTERFACE – build the Python interface (Python 3 only)

  • PYTHON_EXECUTABLE – which Python 3 to use, when more than one is installed

  • SANITIZE – use Clang’s sanitization checks. It sets C++ flags only, and turns on the address and integer sanitizers alongside the undefined one; for the undefined-behaviour build CI runs, which also covers the vendored C, see Running the tests under UndefinedBehaviorSanitizer

  • STATICCOMPILE – build static libraries and binaries instead of dynamic

  • BUILD_SHARED_LIBS – build libstp as a shared library (default ON; forced OFF by STATICCOMPILE)

  • USE_CRYPTOMINISAT – ON requires CryptoMiniSat 5.11 or newer and fails configuration if it is missing or older, AUTO uses it when a new enough one happens to be installed, and OFF – the default – never uses it. (It replaces NOCRYPTOMINISAT and FORCE_CMS, both of which are still accepted and warn)

  • USE_CADICAL and CADICAL_DIR – build the CaDiCaL backend (on by default), optionally against a named checkout

  • USE_MINISAT – build the MiniSat backend

  • TUNE_NATIVE – build with -mtune=native

  • ENABLE_LTO – optimise across translation units, and across STP and the dependencies it compiles. Off by default. On its own it is worth about a percent; most of its value is in what it lets a profile do, and the two are covered together in Link-time and profile-guided optimisation

  • PGO and PGO_DIR – generate or use, and where the profile lives. scripts/pgo-build.sh runs both passes with a training run in between; the same section has the detail

  • WERROR – treat compiler warnings as errors

  • BUILD_MANPAGE – build and install the stp(1) manpage, which needs help2man. Three-valued: ON requires help2man and fails configuration without it, OFF never builds the page, and if it is left unset the page is built when help2man happens to be installed. Packagers who need the page either present or absent for certain should say which

  • SYMFPU_INCLUDE_DIRS – build against an existing SymFPU clone rather than fetching one (point it at the directory containing the clone)

  • CLI11_DIR – build against an existing CLI11 rather than fetching one

  • LIBBF_DIR – where to find an already-built LibBF

  • ENABLE_AUTO_DOWNLOAD – download and build dependencies that were not found, rather than failing. Off by default: a build that reaches the network should be asked to

  • STP_DEPS_LOCAL_ONLY – use no dependency from outside the build directory. Off by default. An installed ABC, CaDiCaL, CLI11, LibBF, MiniSat or SymFPU is not looked for and not used; each is built into STP_DEP_DIR instead, which is inside the build directory unless it was pointed elsewhere. Pair it with ENABLE_AUTO_DOWNLOAD on a cold build directory, or there is nothing left to find and configuration stops – configure.sh --local-deps turns both on.

    A -D<X>_DIR naming a copy is unaffected: that is an answer rather than a search, and the build uses what it was given. LibBF is the one to know about, because the deps/libbf it falls back on when LIBBF_DIR says nothing is a search, and is skipped along with the rest; pass -DLIBBF_DIR=<path> to use a LibBF there anyway. CryptoMiniSat is the exception, being the one dependency STP cannot build: under this option it is used only if cryptominisat5_DIR names one, and -DUSE_CRYPTOMINISAT=ON without that is a configuration error. A static CryptoMiniSat named that way brings a CaDiCaL of its own, which now meets one this build compiled rather than the same installed copy, so the collision described above is reached where it was not before: use a shared CryptoMiniSat, or -DUSE_CADICAL=OFF.

    This is narrower than CMake’s own CMAKE_FIND_USE_CMAKE_SYSTEM_PATH=OFF, and deliberately: the same search also resolves flex, bison, zlib, GMP and python3, none of which STP can build for itself, so disabling it wholesale fails during configuration rather than confining anything

  • STP_DEP_DIR – where dependencies this build downloads are installed, and where dependencies are looked for. It defaults to <build>/deps/install, so a build directory is self-contained. Point several build directories at one path and only the first pays to build anything: the rest find what it installed and download nothing, so they do not even need ENABLE_AUTO_DOWNLOAD. To fill such a directory ahead of time, configure one build with -DSTP_DEP_DIR=<path> -DENABLE_AUTO_DOWNLOAD=ON and build its deps target, which builds the dependencies and nothing else.

    Only the installed dependencies are shared. ExternalProject’s own scratch and stamp files stay in the build directory, so two builds sharing a path cannot corrupt each other’s state – though a shared directory does hold one copy of each library, whatever compiled it, and STP warns when the compiler or sanitizer settings that filled it differ from the ones now building against it

  • STP_ALLOCATOR – which memory allocator the stp binary uses. STP is allocation-heavy and the C library allocator is a significant bottleneck, so this defaults to mimalloc, which is vendored and built as part of STP. Set it to tcmalloc to link a system gperftools instead, or to system for plain malloc – roughly 14% slower, but the lowest peak memory. Only the executables link the allocator; libstp leaves the choice to whatever application embeds it.

There are three ways to set them, in decreasing order of friendliness: run cmake-gui on the source root instead of cmake, which also lets you pick the generator; run ccmake, which is the same idea in an ncurses terminal interface; or pass -D<VARIABLE>=<VALUE> to cmake, which is best kept for scripts. An already-configured build can be changed with make edit_cache, which reconfigures and regenerates.

Working across several worktrees

Working on STP usually means several branches alive at once, and a git worktree each is the pleasant way to hold them: every worktree is a real checkout with its own build directory, so branches do not disturb each other and a long build is never invalidated by switching branch.

git worktree add ../my-feature -b my-feature

The catch is that a fresh worktree looks like a fresh machine to the build. None of the dependencies live inside the repository any more, so a naive worktree downloads and rebuilds all of them. Two caches prevent that, and they are separate because the dependencies come in two kinds.

STP_DEP_DIR, described above, holds the ones STP links. FETCHCONTENT_BASE_DIR holds the ones it compiles: unordered_dense, mimalloc, googletest and OutputCheck. Share that one for the download only, and read the note on it below before pointing two build trees at the same one: FetchContent builds a dependency inside the base directory too, so sharing it shares more than the download.

Warm both once:

export STP_DEP_DIR=~/.cache/stp/deps          # configure.sh honours this
cmake -S . -B warm -G Ninja \
  -DSTP_DEP_DIR=$STP_DEP_DIR \
  -DFETCHCONTENT_BASE_DIR=~/.cache/stp/fetch \
  -DENABLE_AUTO_DOWNLOAD=ON
cmake --build warm --target deps

then in every worktree:

cmake -S . -B build -G Ninja \
  -DSTP_DEP_DIR=$STP_DEP_DIR \
  -DFETCHCONTENT_BASE_DIR=~/.cache/stp/fetch \
  -DENABLE_AUTO_DOWNLOAD=ON \
  -DCMAKE_C_COMPILER_LAUNCHER=ccache -DCMAKE_CXX_COMPILER_LAUNCHER=ccache

ENABLE_AUTO_DOWNLOAD=ON is still wanted even though everything is already local, because a pinned revision can move under you and this is what says the build may go and get it. To promise that it will not, leave it off and pass -DFETCHCONTENT_FULLY_DISCONNECTED=ON instead: CMake then skips the download and update steps outright, and a moved pin becomes an error rather than a download. Nothing is re-fetched either way – against a warm base directory the *-src trees are not touched.

Sharing the compilation

A compiler launcher is worth setting, but on its own it shares nothing between worktrees. STP compiles with -g, and ccache hashes the absolute path of the source when debug information is on, so the same file in two worktrees hashes differently. Measured on one machine, building an identical tree from a second worktree:

Setting

Cross-worktree hits

CMAKE_<LANG>_COMPILER_LAUNCHER=ccache alone

0 / 282 (0%)

plus CCACHE_BASEDIR and CCACHE_NOHASHDIR

131 / 141 (93%)

which took that second build from 26s to 9s. So set them once, for the directory the worktrees live under:

export CCACHE_BASEDIR=~/clones/stp    # the parent of your worktrees
export CCACHE_NOHASHDIR=1

CCACHE_BASEDIR only rewrites paths below it, so keep the build directory inside the worktree (-B build) rather than off in /tmp, or the include paths are left alone and the hits do not come.

The trade is that a cached object’s debug information names the directory of whichever worktree compiled it first. For everyday work that is a fair price; before debugging something subtle, build that worktree with the launcher off.

What invalidates a shared directory

One STP_DEP_DIR holds one copy of each library, whatever compiled it. STP records what filled it in .stp-dep-config and warns when the compiler, sanitizer, toolchain or ABC ABI settings differ from the build now using it. An ASan build in particular wants a directory of its own.

The build type is deliberately not recorded, except on MSVC: sharing a differently-optimised ABC is a choice rather than a fault, but on MSVC the runtime library follows the build type and mixing them does not link.

FETCHCONTENT_BASE_DIR has no such stamp, and it wants more care than STP_DEP_DIR does. The dependencies STP compiles are added with add_subdirectory, and FetchContent builds those in <base>/<name>-build, so sharing the base directory shares the build rather than only the download. Two build trees whose compiler or build type differ then own the same object directory, and each recompiles all of mimalloc the next time it is built – a gcc tree and a clang tree pointed at one base directory leave each other 37 steps to redo on every alternation, indefinitely. This is not a race that running them one after another avoids: both builds legitimately own the path they were given.

Share the sources and keep the builds apart instead. Give each build tree its own base directory, and point each fetched source at one copy:

cmake -S . -B build -G Ninja \
  -DFETCHCONTENT_BASE_DIR=$PWD/build/_deps \
  -DFETCHCONTENT_SOURCE_DIR_MIMALLOC=~/.cache/stp/fetch/mimalloc-src \
  -DFETCHCONTENT_SOURCE_DIR_UNORDEREDDENSE=~/.cache/stp/fetch/unordereddense-src

Name only the sources that exist: FETCHCONTENT_SOURCE_DIR_* pointed at a directory that is not there fails the configure rather than falling back to downloading it.

Tests across worktrees

ENABLE_TESTING=ON also needs lit, which is not a fetched dependency: it is pip-installed into a virtual environment inside the build directory, so it is per-build-tree and none of the above shares it. An installed lit is used if there is one. Otherwise, when configuring with FETCHCONTENT_FULLY_DISCONNECTED=ON and no ENABLE_AUTO_DOWNLOAD, point LIT_TOOL at one – the warm build’s copy will do:

-DLIT_TOOL=$PWD/warm/venv/bin/lit

Doing all of this by hand

Nothing above needs a tool: the flags are the whole of it, and they are written out so that they can be typed, scripted or put in a CMakeUserPresets.json, whichever suits.

If a shell function is what suits, stp.sh is a set of bash and zsh helpers that apply exactly these flags – one command to warm the caches, one to make a worktree, one to build it. It is a convenience kept alongside STP rather than part of it, and it is not what the rest of this page assumes: everything here works without it, and on the platforms it does not cover.

Building a static library and binary

mkdir build && cd build
cmake -DSTATICCOMPILE=ON ..
cmake --build . -j$(nproc)
sudo cmake --install .
command -v ldconfig && sudo ldconfig

Installing

make install installs, make uninstall removes. The root of the installation is CMAKE_INSTALL_PREFIX, set at configure time or changed later through make edit_cache.

Building on Windows

Two toolchains are built and tested: Visual Studio’s cl, and the MSYS2 UCRT64 gcc. Which SAT backend you get follows from which one you pick. Under MSVC that is MiniSat; under MinGW it is CaDiCaL, whose own BUILD.md documents a MinGW build. CryptoMiniSat is not built on Windows at all – upstream supports MinGW there, and STP does not package it – so both configure with -DUSE_CRYPTOMINISAT=OFF.

Everything else is fetched. -DENABLE_AUTO_DOWNLOAD=ON builds ABC, LibBF, SymFPU, CLI11 and the SAT backend as part of the build, with its compiler and its flags, so the toolchain, flex, bison and – for MiniSat – a zlib are all that has to be installed beforehand.

Both use the Ninja generator rather than the Visual Studio one. Ninja parallelises by default, where MSBuild without /m builds one project at a time, and it honours CMAKE_<LANG>_COMPILER_LAUNCHER, which the Visual Studio generator ignores silently, so a compiler cache does nothing there. The cost is that Ninja does not locate the MSVC toolchain for itself: start from an x64 Native Tools developer prompt, or enter the developer shell first.

The two CI jobs – windows (minisat, MSVC) and windows (cadical, MinGW) in .github/workflows/ci.yml – do exactly what is below, and are the reference if a detail here is not enough.

Visual Studio

flex and bison do not come with Visual Studio. winflexbison supplies win_flex.exe and win_bison.exe, which are the names CMake’s FindFLEX and FindBISON look for on Windows. Put its directory on PATH and keep the extracted data/ beside the executables, since bison finds its skeleton files relative to its own path.

MiniSat’s public headers include zlib.h, so a zlib is needed too – vcpkg’s zlib:x64-windows-static, for one. Name the include directory and the library file rather than reaching for ZLIB_ROOT: vcpkg installs that library as zs.lib, which is not one of the names FindZLIB searches for. What STP resolves is passed on to MiniSat’s own build, which searches the default paths only, so one setting covers both.

set ABC_USE_NO_PTHREADS=1

cmake -B build -G Ninja ^
  -DCMAKE_BUILD_TYPE=RelWithDebInfo ^
  -DENABLE_AUTO_DOWNLOAD=ON ^
  -DSTATICCOMPILE=ON ^
  -DUSE_MINISAT=ON -DUSE_CRYPTOMINISAT=OFF -DUSE_CADICAL=OFF ^
  -DENABLE_PYTHON_INTERFACE=OFF ^
  -DZLIB_INCLUDE_DIR=C:/vcpkg/installed/x64-windows-static/include ^
  -DZLIB_LIBRARY=C:/vcpkg/installed/x64-windows-static/lib/zs.lib ^
  .
cmake --build build

ZLIB_LIBRARY names the .lib itself, and vcpkg has not always spelled it the same way, so look in that lib\ directory rather than copying the line verbatim.

ABC_USE_NO_PTHREADS is read by ABC’s makefile while CMake configures. Without it ABC’s threaded paths are compiled, and they do not build with cl.

If a compiler cache is pointed at the build, add -DCMAKE_POLICY_DEFAULT_CMP0141=NEW and -DCMAKE_MSVC_DEBUG_INFORMATION_FORMAT=Embedded. The default /Zi writes a program database shared by every translation unit, which is neither cacheable nor safe to write from several compilations at once; those two move the build onto /Z7.

MinGW (MSYS2 UCRT64)

From a UCRT64 shell:

pacman -S --needed bison flex git make \
    mingw-w64-ucrt-x86_64-cmake \
    mingw-w64-ucrt-x86_64-gcc \
    mingw-w64-ucrt-x86_64-ninja

export ABC_USE_NO_PTHREADS=1
export ABC_USE_STDINT_H=1

cmake -B build -G Ninja \
    -DENABLE_AUTO_DOWNLOAD=ON \
    -DSTATICCOMPILE=ON \
    -DUSE_CADICAL=ON -DUSE_CRYPTOMINISAT=OFF \
    -DENABLE_PYTHON_INTERFACE=OFF \
    .
cmake --build build --parallel "$(nproc)"

ABC_USE_STDINT_H is the one that is easy to miss. ABC’s architecture probe reads eight-byte pointers as 64-bit Linux and picks an integer type that is 32 bits wide under LLP64, and the pointer casts in its headers then do not compile; the variable routes them onto stdint.h instead. ABC_USE_NO_PTHREADS is as above.

CaDiCaL needs nothing extra here: cmake/FindCaDiCaL.cmake drives its configure script and builds the library alone, which is what this toolchain needs it to do.

Common to both

  • Ninja puts the binary at the top of the build tree: build\stp.exe.

  • -DSTATICCOMPILE=ON produces an stp.exe that needs nothing beside it. Under MSVC it also moves STP and its dependencies onto the static CRT, so a dependency directory filled by one choice cannot be linked into a build that wants the other. STP records what filled STP_DEP_DIR and warns when a later build disagrees.

  • The Python interface is off in both jobs and is not exercised on Windows.

  • Neither job runs the lit suite; both run a handful of queries through the binary they built. -DENABLE_TESTING=ON is correspondingly less well trodden there.

Testing

See Testing.