Literature and implementation mapping

The bibliography identifies publications; this page explains where their algorithmic content belongs. A citation or reading note does not establish that an entire algorithm is implemented. The owning implementation chapter states the actual subset, deviations, invariants and tests.

SAT, EUF, and Boolean structure

Source or topic	Current role and retained reading note
IPASIR-UP	SAT integration owns callbacks, reasons and the adapter boundary. The interface reading note retains the paper checklist; Primo delegates propositional search.
Nieuwenhuis–Oliveras, fast congruence closure	EUF maps flattening, congruence, explanation and rollback to Primo. The algorithm note and implementation comparison preserve optimizations not adopted wholesale.
CVC4 architecture	Combination explains care pairs and the general component interface. The reading note is architectural context, not a copied implementation.
Yices	Survey: dynamic Ackermannization and theory-lemma reuse are distinct from Primo’s existing bounded propagators.
Clause forgetting	Survey: logical redundancy, reason lifetime and termination are separate obligations.
Learned-clause minimization and all-UIP shrinking	Survey and probe design: Sörensson–Biere 2009, Feng–Bacchus 2020 and Fleury–Biere 2021 distinguish literal deletion from replacement by shared antecedents. Backend configuration and benefit remain to be measured.
Plaisted–Greenbaum and SMT encodings	Survey: direction-sensitive definitions remain an open extension; the rejected root-only prototype is retained history.
Relevance and don’t-cares	Survey and quantifier relevance: deciding which obligation matters differs from filtering instances of an active obligation.

Arithmetic papers and theses

Source	Current role and retained reading note
Arithmetic symmetry	Open lead and reading scope: SyMT detection results, CVC4-SymBreak, and related LP/ILP work. These motivate investigation beyond the current finite-choice pass; they do not establish a QF_LIA/QF_LRA speedup for Primo.
Dutertre–de Moura, integrating simplex with DPLL(T)	LRA covers preparation, bound repair, strict arithmetic, conflicts and rollback. The base-paper checklist records departures and later optional methods.
Tim King, Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic, PhD thesis, 2014	LRA sparse operations, finite fallback, SOI and conflict construction. The chapter’s source table distinguishes Primo’s representation from the complete thesis designs.
Alberto Griggio, An Effective SMT Engine for Formal Verification, PhD thesis, 2009	Sparse engineering, violation selection and early-pruning context. The thesis note retains exact sections and the corrected least-violated attribution.
Martin Bromberger, Decision Procedures for Linear Arithmetic, PhD thesis, 2019	Reading guide, LIA and preprocessing. Complete equality bases, cube/bounding methods and other unimplemented algorithms remain comparisons/leads. The original thesis checklist retains the full intake.
Monniaux, CAV 2009	LRA normalization, direct bounds and sparse-pivot motivation. Floating-point assistance is unimplemented; leading-coefficient-one normalization differs from the paper’s integer normalization.
King–Barrett–Dutertre, SOI	LRA’s optional SOI section states the implemented objective, breakpoint method, conflict explanation and finite fallback; it does not describe the default sparse repair loop.
King, ordinary-conflict strengthening and provenance	Missing-section intake: thesis §§2.2.4 and 2.2.9 describe regression to assertions and greedy bound weakening. These are not implemented as general LRA explanation transformations; SOI row reduction is separate.
Bjørner–Nachmanson, Arithmetic Solving in Z3	LRA’s optional model-unit producer and LIA’s selected patching/GCD/cut mechanisms. The paper map preserves broader unimplemented integer/nonlinear procedures.
Dillig–Dillig–Aiken, Cuts from proofs (2011 journal version)	Reading note: HNF certificates, general integer splits, coefficient bounds and the bounded-region termination argument. Deferred; current Gomory cuts and coordinate DFS do not implement this procedure.
Word GCD and integer divisibility	LIA states row integrality preconditions; word-GCD notes are an engineering comparison, not the origin of the mathematical divisibility test.
Integer division and modulo	LIA and preprocessing describe the constant-divisor subset; the reading note retains excluded variants.
LP/MIP presolve and primal heuristics	Repair survey, patching lead, and monotone-elimination note keep rounding/repair and elimination obligations distinct.
Atom canonicalization	Current normalization is explained in preprocessing and LRA; the comparison note retains rejected/default-off policy evidence.
Difference constraints	Reading note motivates a future dedicated route. It is not implemented difference-logic admission.

The arithmetic related-work index retains additional comparisons. Arithmetic evidence separates implementation choices from the measurements that accepted or rejected them. Primo’s published results have their own configuration and unresolved artifact mapping.

Preprocessing, strategies, and combination

Source/topic	Current role and retained note
de Moura–Passmore, The Strategy Challenge in SMT Solving	Tactics maps §3 to Primo’s formula-valued composition and model conversion, with explicit limits.
FastSMT and tactic configuration	The FastSMT note and configuration evidence motivate future strategy selection. Primo has no implemented learned strategy system or parallel tactic scheduler.
Symmetry breaking and value precedence	Preprocessing states the finite-domain/permutation conditions. The symmetry note and finite-model note retain broader comparisons; Primo is not a general finite-model finder.
Nelson–Oppen closure methods	Combination explains shared variables, equality exchange and completeness assumptions; the closure note is the retained algorithm intake.
de Moura–Bjørner, model-based combination	The reading note and current combination chapter distinguish model mutation, guessed equalities, explanations, and exact fallback. This is separate from Ge–de Moura MBQI.
MathSAT5; Bjørner–Fazekas incremental preprocessing	Sessions maps labels and safe preprocessing restrictions. Restoration/replay algorithms remain open work.

Quantifiers, syntax, and testing

Reynolds, Barbosa and Fontaine’s enumerative-instantiation results and Janota, Barbosa, Fontaine and Reynolds’s tuple-order work are mapped in quantifiers. The enumeration note and tuple-order note preserve their reading checklists and historical evaluations. Entailment filtering, fail masks, equality representatives, model-refining filters and Ge–de Moura MBQI are distinct proposals in quantifier leads. The old statement that an unknown from one order is logically “weaker” is superseded: every unknown is inconclusive; fairness concerns the unbounded enumeration procedure, not a hierarchy of bounded unknown answers.

The chapter also maps Andrew Reynolds’s 2013 thesis, Finite Model Finding in Satisfiability Modulo Theories, §§3.1.1–3.1.2, and Haniel Barbosa’s 2017 thesis, New Techniques for Instantiation and Proof Production in SMT Solving, §5.1 and §§7.1.1–7.1.2. These supply the finite-model/instantiation distinction and formula-processing comparisons; Primo does not implement their complete finite-model-finding or proof-production frameworks.

SMT-LIB 2.7 supplies the syntax/binding/session specification used by frontend and sessions. Robert Daniel Brummayer’s 2009 PhD thesis, Chapter 4, grounds fuzzing and reduction. The general reading summaries and original literature register retain initial questions and comparisons. Their old milestone language does not override the current capability or lead registers.

Maintaining the reading record

Publication identity belongs in the bibliography, not an ignored PDF filename. For new work, read the relevant primary section and record operations, data, invariants, cost assumptions, proof obligations, tests, and implemented subset. If the required source is unavailable, record the access blocker rather than substituting another solver’s implementation or a secondary summary.