Skip to main content
Back to top
Ctrl
+
K
Search
Ctrl
+
K
Search
Ctrl
+
K
Search
Ctrl
+
K
Primo documentation
Work status
Current implementation and qualification
Active work
Open leads register
Using Primo
Build and run Primo
SMT-LIB input and results
Request a model
Repeated queries and scopes
Command-line options and output
Core architecture
Architecture
Incremental SMT sessions
SMT-LIB lexical conformance audit
Assumption-based incremental QF_LRA design
Assumption-based incremental QF_UF
Profiling the incremental QF_UF gap to Z3
Incremental UF: scan only newly appended atoms
OpenSMT on native incremental UF and LRA
Finalized model interpretations
Tactic architecture
Tactic reference
Boolean DAG representation and bounded associative flattening
Root-polarity clausification experiment
SAT backend: IPASIR-UP and CaDiCaL
DPLL(T) integration
Preprocessing
Structural automatic preprocessing selection
Quantifiers: parsing and term representation
Entailment checks and fail masks for quantifier instantiation
Theories
EUF And Congruence Closure
Boolean Arguments in EUF
QF_UF disequality propagation heuristics
Arithmetic
QF_LIA: Branch-and-Bound, GCD-Consistency, and Gomory Cuts on the Existing Simplex
Where QF_LIA time actually goes (gprof, 2026-08-21)
QF_LRA Speedup Heuristics: Design Note
Numerical parameters: what exists, what is hardcoded, what to add
The tropical-matrix family: what the formulas actually say
QF_LRA fuzz coverage
Nelson-Oppen theory combination
Modular theory combination
N-component combination migration
QF_UFLRA Model-Guided Performance Plan
Convex Nelson-Oppen Merge Plan
The Nelson-Oppen QF_LRA regression: evidence, mechanisms, and how to fix it safely
What QF_LRA owes Nelson-Oppen: convexity and equality sharing
Wrong answer: congruence is dropped for Bool-sorted function arguments
Difference logic
Evidence and practice
Contributing to Primo: draft
Public repository migration: draft
Documentation restructuring before public release
Documentation inventory audit and proposed contents
Experiments
Run Log
Benchmark records in Git with a generated SQLite index
Failure taxonomy
Finite-Domain Fuzzing
Docket: TermId-order sensitivity
Maintain the documentation
Qualification snapshot before the manual rewrite
Paper notes
Literature
Paper summaries
LRA Related Work
IPASIR-UP: User Propagators for CDCL
Reported QF_LRA results
Yices: architecture, dynamic Ackermannization, and lemma reuse
Clause forgetting: correctness and termination
Polarity-aware CNF in SMT
Don’t-care reasoning and relevance
CVC4 architecture
FastSMT strategy synthesis
Evidence about useful tactic configurations
Fast congruence closure and extensions
Fast Congruence Closure Implementation Note
Exploiting Symmetry In SMT Problems
Using SAT And SMT Solvers For Finite Model Finding With Sorts
Nelson-Oppen Closure Methods
de Moura-Bjorner Model-Based Theory Combination
A Fast Linear-Arithmetic Solver for DPLL(T)
Arithmetic Solving in Z3
Word-sized GCD: what the literature says
Integer division, modulo, and absolute value
Integer-model repair and MIP primal heuristics
Early LRA atom canonicalization
An Effective SMT Engine for Formal Verification (Griggio’s thesis)
Decision Procedures for Linear Arithmetic (Bromberger’s thesis)
Monotone (one-sided) variable elimination: what to cite
Fast and Flexible Difference Constraint Propagation for DPLL(T)
Revisiting Enumerative Instantiation
Fair and Adventurous Enumeration of Quantifier Instantiations
Reference
Bibliography
LLM2SMT retrospective
Index
