# 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.

## The problem: you can't statically link two versions of the same library

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.

```{mermaid}
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:

```c
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:

```cpp
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:

```text
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:

```cpp
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.