Primo documentation

Primo is a paper-grounded SMT solver built from first principles, developed with LLM assistance. Its SMT layers are original; propositional solving uses CaDiCaL through IPASIR-UP.

New to Primo? Follow Build and run Primo to build the solver and run a first example. Continue with SMT-LIB input and results, Request a model, and Repeated queries and scopes. The option reference explains the command line and output conventions.

Work status

Entrance	What you will find
Done: current behavior	Supported input, modes, limitations, implementation references and qualification evidence.
Active work	Work underway, completed subsets, next steps and remaining acceptance criteria.
Open leads	Ideas and proposed investigations with evidence, prerequisites and falsifiers.

The new manual describes solver source c944fa790c2043ebac93b8d6f63c7b02b0c2c235. Source links such as src/main.cpp are pinned to that commit. Historical reports retain the revisions they measured; their results do not automatically qualify a later checkout.

Understand and contribute

Start at Architecture for module boundaries, Literature for the primary-source reading map, and Contributing to Primo: draft for contribution requirements. Run Log connects experiments to recorded commands, revisions and artifacts.

The user guide and capability map are the first completed rewrite batch. Existing implementation chapters still combine some reference material with history; the rewrite plan tracks their separation. The qualification archive preserves the former status narrative.

Documentation policy

Documentation is reviewed with the code it describes. Implemented behavior, active changes and open hypotheses must remain distinct. Every nontrivial algorithm identifies its paper or original design basis, implemented subset and limitations. A paper summary alone does not establish implementation.

Authoring, source-link conventions, local preview and logo assets are described in Maintain the documentation. Public hosting and editable release packaging remain work in the migration plan.