Skip to main content

Ctrl+K

Primo

Using Primo

Explore Primo and find a contribution
Supported input and capabilities
Build and run Primo
SMT-LIB input and results
Request a model
Repeated queries and scopes

Reference

Command-line options and output
Effective policies and option dependencies
Tactic reference
Statistics reference
SAT backend operations

Contributing

Correctness before performance
Contributing an implementation change
Fuzzing and reducing failures
Independent model and session validation
Debugging and investigating regressions
Static analysis and the LLVM toolchain
Reproducible experiments
Tuning an existing configuration
Writing and checking documentation

Understanding Primo

From commands to an answer
Terms, symbols, and ownership
Frontend: syntax, names, and typed terms
Sessions: scopes, replay, and retained engines
Goals, tactics, and strategies
Preprocessing
Boolean abstraction and SAT integration
DPLL(T): connecting Boolean search and theory reasoning
Models: values, function tables, and reconstruction

Theories

The theory solver interface
EUF: congruence, explanations, and rollback
Linear real arithmetic
Linear integer arithmetic
Quantifiers: binders and instantiation
Theory combination

Literature

Literature and implementation mapping
Bibliography
Reported QF_LRA results
Bromberger: integer search, cubes and preprocessing
Cuts from proofs: integer-infeasible intersections
Integer-model repair and MIP primal heuristics
Yices: architecture, dynamic Ackermannization, and lemma reuse
Clause forgetting: correctness and termination
Conflict explanations, minimization, and shared antecedents
Polarity-aware CNF in SMT
Don’t-care reasoning and relevance

Open leads

Research register
Library API and embedding
Incremental memory and reference counting
Compact term storage and future payloads
Compact rational storage
Statistics instrumentation and build profiles
Dynamic Ackermannization and theory-lemma retention
Safe forgetting of theory lemmas
Symmetry in linear arithmetic
Floating-point-guided LRA basis selection
Complete implied-equality basis
Column-to-row coefficient access
GCD reasoning with bounded variables
Configurable and better-guided integer patching
Avoiding infinitesimals in integer relaxation
More selective and cheaper care-pair generation
Reducing combination obligations with care graphs
Move QF_UFLRA to the general component driver
Further model-based combination transitions
Quantifier instantiation efficiency
Optional NNF through quantifiers
Exploiting directly asserted quantifiers
Skipping irrelevant quantified obligations
Compact handling of large distinct assertions
Equation elimination across queries
Sharing immutable EUF preparation between checks

Active work

Public launch preparation
GitHub publication handoff
Documentation replacement
Evidence work still open
Results storage

Evidence and history

October evaluation refresh
Full-corpus evaluation at longer limits
Publication qualification
Six-finding publication qualification
Static-analysis triage, 27 October 2026
Assignment migration evidence
Arithmetic engineering and retained evidence
QF_LRA option regressions, 11 October 2026
Quantifier decisions and checking evidence
Retained documentation and evidence
Historical documentation review

Documentation review

Documentation closing review

Repository
Open issue

Search

Ctrl+K

By Primo contributors