Correctness before performance

Correctness before performance#

A solver contribution is complete when its behavior is explained and the required checks support it. Wrong answers, invalid models, crashes, and unresolved reference disagreements take priority over tuning. Faster results cannot compensate for a correctness defect.

Documentation improvements, minimized bug reports, tests, and tools are useful contributions alongside solver development. This guide covers the engineering checks required for those contributions.

Start with the contract and a regression#

Identify the invariant or observable behavior being changed. For a bug, retain a reproducer and add a test that fails for the original defect. For an algorithm, read the primary source and write a design checklist covering the implemented subset, owned data, operations, invariants, and proof obligations. Stop if a required paper cannot be obtained. Explain partial implementations and deviations explicitly.

Primo is a clean-room implementation. Other solvers can provide behavioral comparisons; their source, tests, build files, parser grammars, and documentation must not supply implementation material. Contributions must also respect the layer and ownership boundaries.

Update the affected documentation with the code. Keep implemented behavior, active work, and open leads distinct. A passing unit test alone does not establish an algorithm’s invariant or qualify a new default.

Run the applicable checks#

Run commands from the repository root in the chosen test environment. Contributors may use any suitable machine. In the maintainer’s workspace, solver test, fuzzing and model-validation batches must run in a SLURM allocation; see the execution policy and workspace preparation. Documentation builds and other non-solver checks can run locally.

make check
make docs
make docs-full

make check runs formatting/lint checks, C++ tests, and Python tests. It does not run fuzzing, independent model validation, or the documentation build. Python lint requires Ruff; a missing installation fails make lint and make check. Install the CI-pinned tool with .venv/bin/python -m pip install ruff==0.16.1 after creating .venv. The Python lint configuration enables EXE001 (Python shebangs require an executable file), I001 (sorted import blocks), and PLW1510 (explicit subprocess.run(..., check=...) arguments) for scripts, dependency installers, and Python tests, alongside Ruff’s recommended checks and the existing core checks. make format sorts imports before formatting Python files. Commit executable-bit changes with the script; setting the bit only in an uncommitted checkout does not fix CI. For local previews, make docs reuses the previous build; the full target above re-reads every page for validation. The current Makefile defines the required lint, formatting, and check targets; the test and sanitizer targets define their commands. Memory-sensitive C++ changes also require make asan-test, including changes to parsing, term storage, ownership, or the SAT backend. Apply the repository’s code-review and static-analysis requirements in AGENTS.md and skills/code-review/SKILL.md.

Documentation-only prose changes normally need factual review and the strict build of each affected book. Execute changed examples separately; notebook execution is disabled in the book builds. An infrastructure check that could not run remains incomplete, with its failed command and reason recorded.

Choose a fuzz gate#

Fuzzing and reduction sources#

Robert Daniel Brummayer, Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays, PhD thesis, Johannes Kepler University Linz, September 2009, Chapter 4, explains why grammar-based generation must reach solver internals with valid formulas, and how structure- and type-aware delta debugging reduces failures while preserving the observed defect. Section 4.4.2 covers FuzzSMT’s extension beyond bit-vectors, including linear arithmetic.

This complements Brummayer and Biere’s Fuzzing and Delta-Debugging SMT Solvers (SMT 2009), already recorded in the literature notes. Primo uses external generators and reduction tools. The gate counts below are project policy, not thresholds established by that thesis.

Gate size and coverage#

Fresh fuzzing is required for changes to parsing, printing, type checking, terms, rewriting, preprocessing, clausification, SAT integration, solver control flow, theories, generated lemmas, models, and options that alter behavior. Use the candidate revision and the exact options being claimed. Repeat the applicable gate after a behavior-changing fix. Contributors may use any suitable machine; acceptance depends on the coverage, results, and reproducible evidence recorded below.

Gate	Applicable change	Minimum coverage
Smoke	Narrow parser/printer/core work with low solver impact	100 generated or mutated inputs plus focused tests. Insufficient for SAT, theory, preprocessing, or default-profile changes.
Merge	Ordinary solver, theory, SAT, or preprocessing behavior	1,000 generated or mutated inputs compared with a trusted reference.
Campaign	Promotion of a profile, propagation mode, preprocessing transformation, theory engine, or SAT interaction to default/headline status	3,000 generated QF_UF cases for QF_UF work, or comparable coverage for other logics, plus mutation of representative real seeds when available.

Choose formula shapes and seeds that exercise the changed mechanism. Inspect its activation counters where available. Thousands of inputs that bypass the relevant path are weak evidence. In particular, generated answers do not test model printing, and one-shot inputs do not cover session scoping.

For a QF_UF differential run:

make build contrib-fuzzsmt contrib-z3
PATH="$PWD/contrib/local/bin:$PATH" python3 scripts/fuzz_external.py \
  --fuzzer fuzzsmt --solver './build/primo --quiet' --refs z3 \
  --logic QF_UF --count 1000 --seed 20260924 --timeout 5 \
  --fuzzer-args '-ms 1 -Ms 2 -mv 1 -Mv 2 -mf 1 -mp 1 -ma 1 -Ma 2' \
  --out fuzz-results/contribution-qf-uf-20260924

Use a new output directory for each run. Adapt the shape/size parameters to the change; this command is a QF_UF starting point, not a gate for every component. The current make fuzzsmt shortcut runs only 20 cases. make fuzz is a short mutation entry point. Neither automatically meets the table’s thresholds. See the convenience recipes and 20-case recipe.

Inspect the wrapper’s summary.csv, actual generated count, and available references. The external-fuzzer wrapper can return success after a missing-fuzzer skip, and its generic YinYang/STORM wrappers are placeholders. Use scripts/yinyang_fuzz.sh for the implemented YinYang workflow. A zero exit code or requested case count is not by itself evidence that those tests ran.

The fuzzing guide links the logic-specific workflows and explains finite-domain activation and seed coverage. Install missing dependencies when feasible. For long campaigns or inaccessible infrastructure, record the remaining gate and arrange a maintainer handoff before merge.

Investigate every failure#

Preserve the original input, candidate/reference commands and versions, and stdout/stderr. Reduce the input using a predicate that retains the same failure, then add a regression for a confirmed bug. Do not reduce a wrong answer into an unsupported-input error and call the defect reproduced. The minimizer entry point accepts the failure predicate; the fuzzer’s classify function shows how differential outcomes are separated. Check the minimizer’s output: without ddSMT it copies the original input and returns success, so that outcome is not a successful reduction.

Classify wrong answers, crashes, parser/type errors on valid input, invalid models, and reference disagreements separately. A disagreement requires investigation; an external solver is not automatically correct. Demonstrated unsupported cases need an explicit limitation, not a pass label.

Report timeouts and unknown separately. They are inconclusive results and reduce coverage; a timeout alone is not proof of a correctness failure. Rerun saved failures against the candidate before relying on an old bugs/ directory.

Validate models independently#

Agreement on sat does not validate the model Primo prints. The internal --check-model check is useful but shares implementation with Primo. Full evaluations and default promotions require a separate correctness stage covering every successful candidate SAT row for each claimed profile.

Use scripts/validate_model.py with --require-dolmen-pass for supported single-query inputs; it delegates to the Dolmen validator. Use scripts/validate_incremental.py for scoped sessions. Follow skills/primo-model-validation/SKILL.md for exact invocation and coverage requirements. Preserve the measured binary, input hashes, options, and query identity. Do not replace session models with models from fresh independent Primo queries.

Record direct Dolmen passes, invalid models, changed answers, solver errors, timeouts, unsupported inputs, and missing rows. A validator timeout or unsupported input leaves coverage incomplete. Model-production and validation time must stay outside the original runtime/PAR2 measurements. Model checking does not certify UNSAT answers.

Attach reproducible evidence#

Every fuzz gate and substantial experiment needs a record in the run ledger. Include the run ID, candidate commit and binary identity, reference versions and commands, logic/corpus/manifest, generator and seed, actual counts, options, timeout and other resource limits, host or SLURM job ID, outcome counts, and artifact locations. Preserve failure inputs and logs. The separate Git-results repository and generated SQLite index remain planned; the existing ledger is still authoritative. The recording contract defines the required metadata.

Use the maintained fuzzing, validation, debugging, experiment, and tuning procedures alongside these acceptance requirements. The statistics reference explains counter meanings.

The pull request should state what changed, the violated or preserved invariant, the documentation updated, checks run, linked run records, and remaining limitations. Missing checks stay visible until completed. Do not promote performance claims while correctness failures or required qualification remain unresolved.