Primo

Primo#

Primo is an open-source SMT solver built with LLM assistance. In our published evaluation of quantifier-free linear real arithmetic (QF_LRA), a tuned Primo configuration outperformed OpenSMT, the SMT-COMP 2026 QF_LRA single-query winner, with 20 minutes allowed per instance.

Correctness comes first: wrong answers, invalid models and crashes block acceptance of solver changes. Our goal is to understand every part we build, with clear documentation of the algorithms, design choices, invariants and limitations. Contributions that change solver behavior need explanations, regression tests, fuzzing and reproducible evidence; see Correctness before performance.

Primo is implemented in C++20 from research papers and original design notes. Its SMT implementation is original; propositional search is delegated to CaDiCaL through IPASIR-UP. Primo-owned code and documentation use the MIT license.

Try Primo · Benchmark details · Read the paper · Source code

Published QF_LRA results#

Table 2 of our 2026 paper reports the following measurements on the 519-instance SMT-COMP 2026 QF_LRA selection, with a 1,200-second (20-minute) limit per instance and 7 GB memory per solver run.

Published configuration	Solved / 519	PAR2 (seconds; lower is better)
Primo ⋆ (tuned)	504	47,653
OpenSMT (default)	502	54,584
Yices (default)	495	73,077

Primo ⋆ solved two more instances than default OpenSMT with approximately 13% lower PAR2. PAR2 sums runtimes and charges twice the timeout for each unsolved instance. These are the paper’s measurements; the benchmark report describes the measured configurations, hardware, tuning/test split and comparison with current defaults.

Explore and contribute#

The clickable documentation map follows a query through the solver, links each area to its explanation and open leads, and suggests starting points for contributions in documentation, testing, experiments, and code.

Build and solve a first problem#

From a repository checkout, with a C++20 compiler, CMake 3.20+, GNU Make, Git, Python 3, and a Unix-like shell:

make build
./build/primo --quiet docs/examples/first-solve.smt2

The first build downloads required dependencies into contrib/local and needs network access. Linux is the tested development environment. The example contains:

(set-logic QF_UF)
(declare-sort U 0)
(declare-const a U)
(declare-const b U)
(declare-fun f (U) U)
(assert (= a b))
(assert (distinct (f a) (f b)))
(check-sat)
(exit)

The answer is unsat: equal arguments must give equal results when passed to the same function, so these assertions contradict each other.

Implemented#

The command loop is the executable entry point; IpasirUpBackend defines the SAT boundary.

Primo supports quantifier-free uninterpreted functions, linear Real arithmetic, linear Int arithmetic, and their supported combinations. Integer search is bounded and may return unknown. The quantified UF route supports enumerative instantiation with limited SAT completion; it does not provide general quantifier solving or printed models for quantified assertions. The admitted logic names are checked by SmtSession; quantified assertions take the dedicated UF branch.

The default session engine supports repeated queries and push/pop by rebuilding solving state. Opt-in assumptions engines retain more state for QF_UF and QF_LRA. Arrays, bit-vectors, nonlinear arithmetic, and proof production are outside the implemented scope.

The architecture overview explains the component boundaries; terms, symbols, and ownership explains the core representation and its lifetimes. Goals, tactics, and strategies follows query composition and engine selection. Preprocessing explains the pass order, profile selection, transformations, and model records. Boolean abstraction and SAT integration follows those terms into clauses and describes assumptions and theory callbacks. The full interaction is followed in DPLL(T), including explained conflicts, backtracking, and final consistency checks. The Theories section begins with the theory solver interface, which explains the common assignment, explanation, and model contract and maps it to each solver’s current integration path. EUF: congruence, explanations, and rollback follows the congruence-closure implementation through a conflict and its undo. Linear real arithmetic covers exact numbers, shared polynomial rows, sparse simplex, strict conflicts and rollback, with links to the retained arithmetic development and experiments. Linear integer arithmetic follows the real relaxation through patching, divisibility checks, cuts and branching, including conflict explanations and resource limits. Theory combination explains purification, Nelson–Oppen equality exchange, model-guided choices, and the implemented general component driver used by QF_LIA, QF_UFLIA and quantified UF. QF_UFLRA retains its dedicated coordinator. Quantifiers explains binding, universal instances, existential witnesses, and the current answer boundary. Model construction explains typed values, function tables, and restoration of expressions removed by preprocessing.

The capability matrix and user guides cover building, input, models, and sessions. The reference lists options and effective policies.

The Yices literature survey connects three papers/talks to the code and distinguishes implemented mechanisms from ideas for investigation.

Citing Primo#

If you use Primo in research, please cite Mikoláš Janota and Jan Jakubův, Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA [28], Kalpa Publications in Computing 23, pages 44–56, 2026. DOI: 10.29007/rn52; publisher copy. Also report the commit and configuration used in your experiments.

The BibTeX file contains the entry janota2026primo. Reported QF_LRA results summarizes the paper’s benchmark tables. Published configurations and results are kept separate from current defaults and qualification evidence.

Active work#

Publication preparation records the remaining launch checks and owner decisions. The closing review records the manual’s consistency review; the preservation audit maps the historical material. Evidence work and results storage keep unresolved provenance and the planned storage migration separate from solver implementation.

Open leads#

The research register links proposed algorithmic and engineering investigations and records the outcomes of earlier experiments. It includes arithmetic and combination improvements, quantifier instantiation, memory reclamation, compact storage, and a public library API. Each lead states its current implementation boundary and the evidence needed before acceptance. An open lead is a candidate for investigation, with no implementation commitment.

Build the manual with make docs; preview it with make docs-serve at http://localhost:8000. The historical manual remains available. Publication preparation records launch checks and outstanding owner decisions.