Multi-version CaDiCaL architecture

just_count can solve with any of several bundled CaDiCaL versions, selected at runtime with --cadical-version (see {doc}cli-reference). This page explains why that needs more than “just link CaDiCaL,” how it’s built, and where the pieces live.

CaDiCaL’s public API is a single C++ class, CaDiCaL::Solver, in the CaDiCaL namespace. Two different CaDiCaL releases both define CaDiCaL::Solver::solve(), CaDiCaL::Solver::add(int), and so on — same mangled symbol names. If you statically (or even dynamically, in the ordinary way) link two versions’ object code into one binary, the linker sees duplicate symbol definitions and there’s no way to address “the 2.2.1 add” versus “the 3.0.0 add” — only one definition can win.

This rules out the obvious approach of just building all three versions and picking one via an if/switch in C++ code that calls CaDiCaL::Solver directly.

The solution: one shared-library plugin per version, loaded via dlopen

Each bundled version is built as its own shared library, isolated from the others, exposing only a small, version-independent C ABI (not C++ — no name mangling, no cross-version symbol clashes possible even if two of these .so files were loaded into the same process). just_count picks the right .so at runtime with dlopen() based on --cadical-version, and calls into it through dlsym-resolved function pointers.

flowchart TB
    subgraph build["Build time"]
        direction TB
        src195["CaDiCaL 1.9.5 source\n(built with -fPIC)"] --> lib195["libjc_cadical_1.9.5.so"]
        src221["CaDiCaL 2.2.1 source\n(built with -fPIC)"] --> lib221["libjc_cadical_2.2.1.so"]
        src300["CaDiCaL 3.0.0 source\n(built with -fPIC)"] --> lib300["libjc_cadical_3.0.0.so"]
    end
    subgraph runtime["Runtime"]
        direction TB
        main["just_count\n(--cadical-version 2.2.1)"] -- dlopen --> lib221b["libjc_cadical_2.2.1.so"]
        main -. "not loaded" .-> lib195b["libjc_cadical_1.9.5.so"]
        main -. "not loaded" .-> lib300b["libjc_cadical_3.0.0.so"]
    end

The ABI (include/cadical_plugin_abi.h)

A handful of extern "C" functions covering exactly what just_count needs from a solver:

const char* jc_cadical_version(void);

void* jc_cadical_new(void);
void  jc_cadical_delete(void* solver);

void jc_cadical_freeze(void* solver, int lit);
void jc_cadical_add(void* solver, int lit);
int  jc_cadical_solve(void* solver);
int  jc_cadical_val(void* solver, int lit);

int  jc_cadical_set(void* solver, const char* name, int val);

void* stands in for an opaque CaDiCaL::Solver* — the caller never dereferences it directly, only passes it back into these functions.

This works because freeze, add, solve, val, set, and version have had stable signatures across every bundled version (val’s optional second parameter, added later, is always called with its default, so the single-argument call in the ABI works unmodified on 1.9.5 through 3.0.0).

The implementation (src/cadical_plugin_impl.cpp)

One file, compiled three times — once per bundled version, each time against that version’s cadical.hpp and linked against that version’s libcadical.a — producing three independent .so files:

extern "C" void* jc_cadical_new(void) {
    auto* solver = new CaDiCaL::Solver();
    // See "The factor/ilb quirks" below.
    solver->set("factor", 0);
    return solver;
}

extern "C" void jc_cadical_add(void* solver, int lit) {
    static_cast<CaDiCaL::Solver*>(solver)->add(lit);
}
// ... freeze, solve, val, set, delete, version follow the same pattern

CMake’s add_cadical_plugin(version tag) function (in CMakeLists.txt) does the repetitive part for each version: ExternalProject_Add builds CaDiCaL from source with -fPIC (required — a static library built without position-independent code can’t be linked into a shared library), then a SHARED target compiles src/cadical_plugin_impl.cpp against that source tree and links it into build/cadical-plugins/libjc_cadical_<version>.so.

The loader (src/cadical_backend.cpp, declared in include/cadical_backend.h)

At runtime, CadicalSolverHandle (used by model_counter.cpp) and the free functions available_cadical_versions() / cadical_backend_version() (used by main.cpp for --help text and --version) resolve a requested version string to a loaded plugin:

  1. Find the plugin directory: the directory containing the running executable (readlink("/proc/self/exe", ...)) plus cadical-plugins/. This is why the plugins are placed as siblings of just_count in the build directory — no install step or environment variable is needed for the common case of running straight out of build/.
  2. If no version was requested, use the compile-time default (CADICAL_DEFAULT_VERSION, generated into version.h — currently 1.9.5, the fastest bundled version on our workload, not the newest; see {doc}investigation).
  3. dlopen(".../cadical-plugins/libjc_cadical_<version>.so") and dlsym each of the eight ABI functions. A missing file or missing symbol raises std::runtime_error listing the versions that are available.
  4. Cache the loaded plugin (in a static std::unordered_map) so --cadical-version doesn’t pay the dlopen cost more than once per process, even if count_models() were called multiple times.

CadicalSolverHandle is a thin RAII wrapper: its constructor resolves the backend and calls jc_cadical_new(); its destructor calls jc_cadical_delete(); freeze/add/solve/val/set forward through the cached function pointers.

Why counter_lib no longer depends on CaDiCaL directly

Before this design, model_counter.cpp included cadical.hpp and used CaDiCaL::Solver directly, and main.cpp did too (for the version banner). Neither does anymore — both go through cadical_backend.h only. counter_lib links against ${CMAKE_DL_LIBS} (for dlopen) and nothing CaDiCaL-specific at all; the actual solver code only exists in the three plugin .so files, built independently.

A version-compatibility quirk: factor / factorcheck

CaDiCaL 3.0 added an optional “algebraic factorization” preprocessing technique (factor) with a companion strict-checking option (factorcheck) that, when both are enabled, requires every variable used in add() to have been explicitly declared first via declare_more_variables()/declare_one_more_variable(). just_count doesn’t declare variables that way — it just adds clause literals directly — so solving with the untouched 3.0.0 defaults aborts with:

cadical: fatal error: invalid API usage of 'void CaDiCaL::Solver::add(int)'
in '../src/solver.cpp': adding literal '2' with undeclared variable '2'
(checking that user variables are declared explicitly failed as both
'factor' and 'factorcheck' are enabled)

The fix, baked into jc_cadical_new() in src/cadical_plugin_impl.cpp (shown above), is solver->set("factor", 0). Since Solver::set() returns false (a harmless no-op) for an option name that doesn’t exist in a given version, the same call is safe to make unconditionally across all three bundled versions, even though factor doesn’t exist at all in 1.9.5.

Baked-in defaults: ilb=2, inprocessing off

{doc}investigation found that just_count’s workload — repeated incremental solve() calls, each adding exactly one new blocking clause — performs much better with CaDiCaL’s Incremental Lazy Backtracking (ilb) forced to its strongest mode, and with every general-purpose inprocessing technique turned off (their cost outweighs what they save when re-solving barely-changed formulas thousands of times). Both are baked into jc_cadical_new() in src/cadical_plugin_impl.cpp unconditionally, via the same “harmless no-op on versions without this option” property used for factor above:

static const struct { const char* name; int val; } kDefaultOptions[] = {
    {"factor", 0},
    {"ilb", 2},         // incremental lazy backtracking; off since 2.x
    {"sweep", 0}, {"congruence", 0}, {"backbone", 0}, {"condition", 0},
    {"elim", 0}, {"vivify", 0}, {"probe", 0}, {"subsume", 0},
    {"transred", 0}, {"walk", 0},
};
for (const auto& opt : kDefaultOptions) solver->set(opt.name, opt.val);

Options::set() clamps out-of-range values to the nearest bound rather than rejecting them, so on 1.9.5 (whose ilb is a 0/1 boolean, and which doesn’t have sweep/congruence/backbone/condition at all) this is either a no-op or clamps to 1.9.5’s own existing default — no behavior change on that version beyond disabling elim/vivify/probe/ subsume/transred/walk, which it does have.

Any of these can be overridden per run with --cadical-option NAME=VALUE (--cadical-option sweep=1 turns SAT sweeping back on, for example) — see {doc}investigation for the full numbers behind this choice, and why 3.0.0, not 1.9.5, ended up as CADICAL_DEFAULT_VERSION once this tuning was applied uniformly.