Retained documentation and evidence#
This catalogue preserves the original Primo documentation at the snapshot taken before this gap-completion pass. Each entry links the current explanatory home and the original record. These are dated records, not current capability or performance claims. The section inventory identifies precise source ranges and decisions within each page. The historical book preserves the original pages and anchors; retired main-book paths redirect there.
Active work#
Current destination: replacement page. Retained record: docs/active-work.md.
Architecture#
Current destination: replacement page. Retained record: docs/architecture.md.
Qualification snapshot before the manual rewrite#
Current destination: replacement page. Retained record: docs/archive/current-status.md.
Arithmetic#
Current destination: replacement page. Retained record: docs/arithmetic.md.
Assumption-based incremental QF_LRA design#
Current destination: replacement page. Retained record: docs/assumption-incremental-lra.md.
Assumption-based incremental QF_UF#
Current destination: replacement page. Retained record: docs/assumption-incremental-uf.md.
Benchmark records in Git with a generated SQLite index#
Current destination: replacement page. Retained record: docs/benchmark-record-storage.md.
Wrong answer: congruence is dropped for Bool-sorted function arguments#
Current destination: replacement page. Retained record: docs/bool-argument-congruence-bug.md.
Boolean DAG representation and bounded associative flattening#
Current destination: replacement page. Retained record: docs/boolean-dag-flattening.md.
Contributing to Primo: draft#
Current destination: replacement page. Retained record: docs/contributing.md.
Current implementation and qualification#
Current destination: replacement page. Retained record: docs/current-status.md.
Failure taxonomy#
Current destination: replacement page. Retained record: docs/debugging.md.
Maintain the documentation#
Current destination: replacement page. Retained record: docs/development/documentation.md.
Difference logic#
Current destination: replacement page. Retained record: docs/difference_logic.md.
Documentation restructuring before public release#
Current destination: replacement page. Retained record: docs/documentation-restructuring.md.
DPLL(T) integration#
Current destination: replacement page. Retained record: docs/dpllt.md.
Boolean Arguments in EUF#
Current destination: replacement page. Retained record: docs/euf-boolean-arguments.md.
EUF And Congruence Closure#
Current destination: replacement page. Retained record: docs/euf.md.
Experiments#
Current destination: replacement page. Retained record: docs/experiments.md.
Finite-Domain Fuzzing#
Current destination: replacement page. Retained record: docs/finite-domain-fuzzing.md.
QF_LRA fuzz coverage#
Current destination: replacement page. Retained record: docs/fuzz-coverage-qf-lra.md.
Build and run Primo#
Current destination: replacement page. Retained record: docs/guide/getting-started.md.
SMT-LIB input and results#
Current destination: replacement page. Retained record: docs/guide/input.md.
Request a model#
Current destination: replacement page. Retained record: docs/guide/models.md.
Repeated queries and scopes#
Current destination: replacement page. Retained record: docs/guide/sessions.md.
Incremental SMT sessions#
Current destination: replacement page. Retained record: docs/incremental-smt.md.
Incremental UF: scan only newly appended atoms#
Current destination: replacement page. Retained record: docs/incremental-uf-atom-scans.md.
Primo documentation#
Current destination: replacement page. Retained record: docs/index.md.
SMT-LIB lexical conformance audit#
Current destination: replacement page. Retained record: docs/lexical-conformance.md.
Literature#
Current destination: replacement page. Retained record: docs/literature.md.
Finalized model interpretations#
Current destination: replacement page. Retained record: docs/model-interpretation.md.
Modular theory combination#
Current destination: replacement page. Retained record: docs/modular-theory-combination.md.
N-component combination migration#
Current destination: replacement page. Retained record: docs/n-way-combination-migration.md.
The Nelson-Oppen QF_LRA regression: evidence, mechanisms, and how to fix it safely#
Current destination: replacement page. Retained record: docs/nelson-oppen-qf-lra-regression.md.
Nelson-Oppen theory combination#
Current destination: replacement page. Retained record: docs/nelson-oppen.md.
Open leads register#
Current destination: replacement page. Retained record: docs/open-leads.md.
OpenSMT on native incremental UF and LRA#
Current destination: replacement page. Retained record: docs/opensmt-incremental-comparison.md.
Arithmetic Solving in Z3#
Current destination: replacement page. Retained record: docs/papers/arithmetic-solving-in-z3.md.
Decision Procedures for Linear Arithmetic (Bromberger’s thesis)#
Current destination: replacement page. Retained record: docs/papers/bromberger-linear-arithmetic-thesis.md.
Clause forgetting: correctness and termination#
Current destination: replacement page. Retained record: docs/papers/clause-forgetting.md.
CVC4 architecture#
Current destination: replacement page. Retained record: docs/papers/cvc4-architecture.md.
Fast and Flexible Difference Constraint Propagation for DPLL(T)#
Current destination: replacement page. Retained record: docs/papers/difference-constraint-propagation.md.
Revisiting Enumerative Instantiation#
Current destination: replacement page. Retained record: docs/papers/enumerative-instantiation.md.
Fair and Adventurous Enumeration of Quantifier Instantiations#
Current destination: replacement page. Retained record: docs/papers/fair-adventurous-enumeration.md.
Fast Congruence Closure Implementation Note#
Current destination: replacement page. Retained record: docs/papers/fast-congruence-closure-implementation.md.
Fast congruence closure and extensions#
Current destination: replacement page. Retained record: docs/papers/fast-congruence-closure.md.
A Fast Linear-Arithmetic Solver for DPLL(T)#
Current destination: replacement page. Retained record: docs/papers/fast-linear-arithmetic-dpllt.md.
FastSMT strategy synthesis#
Current destination: replacement page. Retained record: docs/papers/fastsmt-strategy-synthesis.md.
Using SAT And SMT Solvers For Finite Model Finding With Sorts#
Current destination: replacement page. Retained record: docs/papers/finite-model-finding-sorts.md.
An Effective SMT Engine for Formal Verification (Griggio’s thesis)#
Current destination: replacement page. Retained record: docs/papers/griggio-mathsat-thesis.md.
Integer division, modulo, and absolute value#
Current destination: replacement page. Retained record: docs/papers/integer-division-and-modulo.md.
IPASIR-UP: User Propagators for CDCL#
Current destination: replacement page. Retained record: docs/papers/ipasir-up.md.
Early LRA atom canonicalization#
Current destination: replacement page. Retained record: docs/papers/lra-atom-canonicalization.md.
de Moura-Bjorner Model-Based Theory Combination#
Current destination: replacement page. Retained record: docs/papers/model-based-theory-combination.md.
Monotone (one-sided) variable elimination: what to cite#
Current destination: replacement page. Retained record: docs/papers/monotone-variable-elimination.md.
Nelson-Oppen Closure Methods#
Current destination: replacement page. Retained record: docs/papers/nelson-oppen-closure-methods.md.
Polarity-aware CNF in SMT#
Current destination: replacement page. Retained record: docs/papers/polarity-aware-cnf.md.
Exploiting Symmetry In SMT Problems#
Current destination: replacement page. Retained record: docs/papers/smt-symmetry-breaking.md.
Paper summaries#
Current destination: replacement page. Retained record: docs/papers/summaries.md.
Evidence about useful tactic configurations#
Current destination: replacement page. Retained record: docs/papers/tactic-configuration-evidence.md.
Word-sized GCD: what the literature says#
Current destination: replacement page. Retained record: docs/papers/word-gcd-notes.md.
Yices: architecture, dynamic Ackermannization, and lemma reuse#
Current destination: replacement page. Retained record: docs/papers/yices.md.
Preprocessing#
Current destination: replacement page. Retained record: docs/preprocessing.md.
Public repository migration: draft#
Current destination: replacement page. Retained record: docs/public-repository-migration.md.
QF_LIA: Branch-and-Bound, GCD-Consistency, and Gomory Cuts on the Existing Simplex#
Current destination: replacement page. Retained record: docs/qf-lia-branch-and-bound.md.
Where QF_LIA time actually goes (gprof, 2026-08-21)#
Current destination: replacement page. Retained record: docs/qf-lia-profile.md.
What QF_LRA owes Nelson-Oppen: convexity and equality sharing#
Current destination: replacement page. Retained record: docs/qf-lra-equality-sharing.md.
QF_LRA Speedup Heuristics: Design Note#
Current destination: replacement page. Retained record: docs/qf-lra-heuristics.md.
Convex Nelson-Oppen Merge Plan#
Current destination: replacement page. Retained record: docs/qf-uflra-convex-no-merge-plan.md.
QF_UFLRA Model-Guided Performance Plan#
Current destination: replacement page. Retained record: docs/qf-uflra-model-guided-performance.md.
QF_UF disequality propagation heuristics#
Current destination: replacement page. Retained record: docs/qfuf-disequality-propagation.md.
Entailment checks and fail masks for quantifier instantiation#
Current destination: replacement page. Retained record: docs/quantifier-entailment-design.md.
Quantifiers: parsing and term representation#
Current destination: replacement page. Retained record: docs/quantifiers.md.
LLM2SMT retrospective#
Current destination: replacement page. Retained record: docs/reference/llm2smt-retrospective.md.
Command-line options and output#
Current destination: replacement page. Retained record: docs/reference/options.md.
Root-polarity clausification experiment#
Current destination: replacement page. Retained record: docs/root-polarity-clausification.md.
Run Log#
Current destination: replacement page. Retained record: docs/run-log.md.
SAT backend: IPASIR-UP and CaDiCaL#
Current destination: replacement page. Retained record: docs/sat-ipasir-up.md.
Structural automatic preprocessing selection#
Current destination: replacement page. Retained record: docs/structural-auto-preprocessing.md.
Tactic reference#
Current destination: replacement page. Retained record: docs/tactic-reference.md.
Tactic architecture#
Current destination: replacement page. Retained record: docs/tactics.md.
Docket: TermId-order sensitivity#
Current destination: replacement page. Retained record: docs/termid-order-sensitivity.md.
The tropical-matrix family: what the formulas actually say#
Current destination: replacement page. Retained record: docs/tropical-matrix-structure.md.
Numerical parameters: what exists, what is hardcoded, what to add#
Current destination: replacement page. Retained record: docs/tuning-parameters.md.
Profiling the incremental QF_UF gap to Z3#
Current destination: replacement page. Retained record: docs/uf-z3-profiling.md.
Documentation inventory audit and proposed contents#
Current destination: replacement page. Retained record: docs/work/documentation-audit.md.
Reported QF_LRA results#
Current destination: replacement page. Retained record: docs/papers/primo-qflra-results.md.
Don’t-care reasoning and relevance#
Current destination: replacement page. Retained record: docs/papers/relevance-filtering.md.
Integer-model repair and MIP primal heuristics#
Current destination: replacement page. Retained record: docs/papers/lia-primal-heuristics.md.
Bibliography#
Current destination: replacement page. Retained record: docs/references.md.