Documentation closing review#
Status: 28 October consistency review covers all 97 current-book Markdown pages. The earlier technical findings are closed; reader acceptance remains separate.
The replacement manual is now the main book. make docs-serve previews the
current book at http://localhost:8000; make docs-site assembles both books. Publication
is a separate operation; changing the source tree does not deploy a website.
Coverage and review record#
The 28 October consistency record
lists all 97 pages at baseline e397439, their fingerprints, assigned review
units, findings and dispositions. It also covers the root README, contribution
policy, security policy and pull-request template. The pass checked current prose against selected
owning code, commands, policies and evidence, and removed duplicated lead
summaries from the landing page. Historical results retain their measured
revisions; this review does not rerun solver qualification, re-prove the cited
papers, or independently verify GitHub settings.
The 2 October page-by-page review covered all 84 pages at its own baseline revision, recorded the corrections and listed source findings. The numeric-payload omission in symmetry comparison was confirmed to produce false UNSAT answers, then repaired and qualified on SLURM with regressions, differential fuzzing and separate model checks. The six supporting-tool and resource-control findings were subsequently repaired and qualified.
The preservation audit accounts for 91 old pages, 1,150
section headings, 126 supporting entries, and 1,306 original URL targets.
The old book is retained as editable source in docs-history/ and is built
under archive/original. It preserves the final
old book, including later corrections; all targets from the original
compatibility snapshot were checked against that book before the move.
Page |
Stage |
Source |
Checks |
Review still needed |
|---|---|---|---|---|
index.md |
Verified |
ac0daf4 |
Source admission and entry-point links; first example; strict build; editorial consistency pass 2026-09-26 |
Reader acceptance; reference and contributor procedures now extracted; historical evidence is not a new solver qualification |
development/correctness.md |
Verified |
ac0daf4; Brummayer thesis Chapter 4 |
Make targets and scripts inspected; policy comparison; source links; strict build; supplied thesis sections read for fuzzing/reduction attribution; editorial consistency pass 2026-09-26 |
Reader acceptance; reference and contributor procedures now extracted; historical evidence is not a new solver qualification |
implementation/architecture.md |
Verified |
ac0daf4 |
Owning headers and control flow inspected; source and test links; TikZ/SVG figures rendered and inspected; strict builds; editorial consistency pass 2026-09-26; general driver and QF_UFLIA/quantified-UF callers checked; dedicated Real migration distinguished; Real migration linked to separate open lead |
Reader acceptance; frontend and sessions now have separate chapters |
implementation/core.md |
Verified |
ac0daf4 |
Owning code and 50 source/test links checked; C++ example compiled and run; 4 focused CTest suites; strict builds and rendered review; editorial consistency pass 2026-09-26 |
User review of identity/lifetime explanation; binder algorithms now have a separate quantifier chapter; model algorithms now have a separate construction chapter |
implementation/sat.md |
Verified |
ac0daf4; e6d9fcb bridge removal |
Owning code and paper sections inspected; source links; executable clause/guard example; 5 CTest suites; strict builds and rendered review; superseded encoding removed; SLURM qualification and source-link refresh recorded; editorial consistency pass 2026-09-26 |
Reader acceptance; reference and contributor procedures now extracted; historical evidence is not a new solver qualification |
implementation/dpllt.md |
Verified |
45e25a6; shared assignment migration; previous rollback audit retained; e6d9fcb bridge removal |
All routes use shared assignment views; coordinator protocol and disconnect/reconnect tests; 43 normal/ASan suites; 188 Python tests; whole-tree static review; strict books; superseded encoding removed; signed-premise example; SLURM qualification and source-link refresh recorded; editorial consistency pass 2026-09-26; general driver and QF_UFLIA/quantified-UF callers checked; dedicated Real migration distinguished |
Reader acceptance; reference and contributor procedures now extracted; historical evidence is not a new solver qualification |
implementation/euf.md |
Verified |
e6d9fcb; Nieuwenhuis and Oliveras 2007 Sections 3-5; Sebastiani 2007 Section 6.10 and Proposition 2.3; SMT-LIB 2.6 Definition 8 |
Owning source and primary paper sections inspected; invariant-to-test map; source links; both strict books; HTML links and old page/anchor compatibility checked; editorial consistency pass 2026-09-26; filtering proof and Boolean coverage checked against frontend registration and model completion; primary filtering and Boolean-domain sections read; model TODO resolved by linked construction chapter |
User review of conflict trace and depth; model and combination chapters drafted separately; no solver batch rerun |
implementation/lra.md |
Verified |
bc5d21d; supplied primary arithmetic papers and theses |
Owning code and primary sections read; invariant-to-test mapping; retained evidence inventory; both strict books; source/HTML links and old anchors checked; browser figure review; editorial consistency pass 2026-09-26; default equality producer linked to worked combination examples; outer-loop mutation schedule linked; row-bound sign derivation and reverse example checked; callbacks and cap gates traced; strict-bound explanation and combination crosslinks added; stored target-atom threshold distinguished from stronger derived bound; SOI objective and breakpoint selection derived from code and primary sections; worked pivot and combined conflict; minimizer and termination deviations; rollback state; dated evidence limits; single bounded endpoint debug reproduction found extra zero-step pivot; diagnostic and follow-up recorded; SOI endpoint correction: starting-bound direction changes and fixed bounds tested; 43 normal/ASan groups; 201 Python tests; 36 Z3 seed/regression comparisons; 1000-case SOI gate: 958 agreements and 42 timeouts; no hard failures; integer companion and section preservation map drafted 2026-09-29; 2026-10-01: Fixed-basic elimination and model-phase explanations checked against owners and existing regressions; arithmetic evidence curated; no new solver run |
Reader acceptance; historical measurements retain their original scope; published artifact identities remain evidence work |
implementation/combination.md |
Verified |
e6d9fcb; Nelson-Oppen report; de Moura-Bjorner; DTC; Griggio/King/Bromberger thesis sections; Jovanovic-Barrett 2013 sections 3-4 |
Owning types and both arithmetic routes inspected; primary sections read; clause examples checked algebraically; regression map reviewed; strict books and source/HTML links checked; existing anchors preserved; care-pair example and generator/consumer mapping added; general driver and QF_UFLIA/quantified-UF callers checked; dedicated Real migration distinguished; default equality rules checked against section 5.1 and tableau regressions; bound explanation and basis-gap examples added; mutation scheduling traced through outer loop and both partition calls; sections 4 and 5.2 reread; scratch-state and mutation regressions inspected; proposals extracted into separate open-lead pages; evidence anchor retained; online paired-bound equality delivery and lazy atom registration traced; arithmetic-to-EUF clause chain added with reciprocal propagation links; online-LRA construction guard and already-assigned equality cases clarified; integer stage schedule linked to LIA chapter; 2026-10-01: Connected arithmetic evidence summary to combination records |
Reader acceptance; Real migration remains an implementation lead; no new solver qualification |
implementation/lia.md |
Verified |
bc5d21d; Bjorner and Nachmanson 2024 Sections 4.1-4.5; King thesis Section 4.4.3; Bromberger thesis Chapters 4-6 and 7.2 |
Primary sections and owning implementation read; stage schedule; integer guards; cut and explanation derivations; existing regression map; both strict books; local and Git source links; all prior anchors preserved; browser math and table review; 161 expressions without MathJax errors; existing thesis coverage linked through new reading guide 2026-09-30; GCD derivation and earlier Pugh/Griggio attribution checked; explanation and row-selection ownership clarified; hard-coded target window distinguished from move budget and linked to MIP survey/lead |
Reader acceptance; reference and contributor procedures now extracted; historical evidence is not a new solver qualification |
leads/library-api.md |
Draft |
ac0daf4 |
Initial build targets and interface pointers inspected; editorial consistency pass 2026-09-26 |
API and embedding audit not started; external-consumer prototype and user review pending |
leads/incremental-memory.md |
Draft |
ac0daf4; e6d9fcb flat-term ownership |
Term/session ownership and historical memory-report pointers inspected; official Z3/cvc5 reference-counting documentation checked; flattened index and prepared/working state inspected; editorial consistency pass 2026-09-26 |
Current memory reproduction and ownership design pending; GC risks and flattened-representation lifetime recorded; no reclamation design selected |
leads/term-storage.md |
Draft |
ac0daf4 |
Term/key representation inspected; reproducible layout probe compiled and run; strict book builds; editorial consistency pass 2026-09-26 |
Payload design and solver memory/runtime evaluation deferred; user review pending |
leads/rational-storage.md |
Draft |
e6d9fcb; local GCC 13.3.0/libstdc++ layout |
Fields and deep-copy ownership inspected; reproducible sizeof probe compiled with warnings as errors; strict books and links checked; editorial consistency pass 2026-09-26 |
Lifetime design and implementation deferred; solver memory/runtime evaluation and reader acceptance pending |
papers/yices.md |
Verified |
ac0daf4; local Yices PDFs; CaDiCaL rel-3.0.0 public API |
All three PDFs read; source and historical run-log review; shared note in both books; strict builds and link/render checks; editorial consistency pass 2026-09-26 |
User review; backend deletion behavior and remaining representation audits deferred |
leads/theory-lemmas.md |
Draft |
ac0daf4; papers/yices.md |
Existing Ackermann subset and backend retention contract inspected; scope and acceptance criteria separated; editorial consistency pass 2026-09-26 |
Conflict-driven selection and lemma-retention investigations not started; user review pending |
papers/clause-forgetting.md |
Verified |
ac0daf4; NOT 2006; Blanchette et al. JAR 2018; Gstrein et al. SAT 2025 |
Primary sections read; source links; both strict builds; shared rendering and HTML link/compatibility checks; editorial consistency pass 2026-09-26 |
User review; actual retention and progress policy audit remains open |
leads/theory-lemma-forgetting.md |
Draft |
ac0daf4; papers/clause-forgetting.md |
Theory redundancy; live-reason lifetime; termination; metrics and acceptance conditions separated; editorial consistency pass 2026-09-26 |
Investigation and implementation deferred; user review pending |
papers/polarity-aware-cnf.md |
Verified |
ac0daf4; Masina et al. JAIR 2025; SMTInterpol primary documentation |
Primary sections and owning code read; directional examples checked; strict builds; source and HTML checks; editorial consistency pass 2026-09-26 |
User review; original 1986 full text unavailable; general PG implementation deferred |
leads/statistics-instrumentation.md |
Draft |
ac0daf4; original engineering proposal |
Typed/string updates; timers; diagnostic traversal; conflict-budget consumer inspected; EUF scheduling counter reader identified; editorial consistency pass 2026-09-26 |
Whole-tree classification; build design; correctness qualification and overhead measurement deferred |
leads/lra-floating-point.md |
Draft |
e6d9fcb; Monniaux CAV 2009 Section 3 Algorithm 2; existing D2 lead |
Primary section and current preparation/pivot interfaces inspected; historical investigation retained; strict builds and link checks; editorial consistency pass 2026-09-26 |
User review; integration design and implementation deferred; no solver evaluation |
review.md |
Verified |
current docs branch |
Book selection and previews; source-link convention; ledger coverage; editorial consistency pass 2026-09-26; 2026-10-01: Gap-completion review and full preservation inventory recorded |
Reader acceptance; external access failures are recorded separately from passing local/Git checks |
papers/primo-qflra-results.md |
Verified |
arXiv:2609.16706v1; e6d9fcb option defaults |
Primary PDF read; Tables 1-2 and Figure 3 checked; defaults inspected; strict books and HTML checks; editorial consistency pass 2026-09-26 |
User acceptance; match published tables to exact Primo revisions and raw artifacts; no solver rerun |
leads/care-pair-generation.md |
Draft |
e6d9fcb; Jovanovic-Barrett 2013 Section 4.2 |
Generator and consumer inspected; existing Real cache distinguished from proposed filtering and lazy generation; comparison and correctness criteria recorded |
User review; profiling and prototype selection pending; no solver evaluation |
leads/care-guided-combination.md |
Draft |
e6d9fcb; Jovanovic-Barrett 2013 Section 3 Definitions 6-8 and Section 3.1 Theorem 1; Section 4 |
Primary fixed point and model-extension argument read; current heuristic API and complete model checks inspected; proof and model-construction obligations recorded |
User review; component contract and two-theory-to-collection mapping pending; implementation and evaluation deferred |
leads/lra-equality-basis.md |
Draft |
e6d9fcb; Bromberger thesis Section 5.4; original lead 17 |
Primary normalization and explanation sections reread; existing producer and exact-probe boundary retained; historical investigation linked |
User review; probe-cost profiling; integration design; implementation and evaluation pending |
leads/real-combination-migration.md |
Draft |
e6d9fcb; current component driver; completed n-way migration record |
Current route split and recipe interface inspected; preservation obligations extracted; earlier qualification kept separate |
User review; contract-gap audit and migration planning; implementation and evaluation pending |
leads/model-based-combination.md |
Draft |
e6d9fcb; de Moura-Bjorner Section 4 and Appendix A; retained transition checklist |
Existing driver and mutation protocol distinguished from further transitions; scheduling freedom and progress obligations retained |
User review; bounded component scope and transition mapping; implementation and evaluation pending |
implementation/quantifiers.md |
Verified |
e6d9fcb; TACAS 2018; FMCAD 2021; Chargueraud; SMT-LIB 2.6; Reynolds and Barbosa theses; c944fa7 preprocessing diagnostic routing |
Owning code and primary sections read; binder and polarity examples checked; invariant-to-test map; strict books; source and HTML links; prior anchors preserved; enclosing and nested negation traced through signed SAT encoding and kind/value classification; guarded witness/instance examples and existing polarity regressions inspected; missing dynamic relevance and effect on unknown documented; NNF and fixed-root leads separated; growing-pool basis and fairness stated through TACAS 2018 Theorem 1 and Corollaries 1-2 with implementation limits; 2026-10-01: Indexed-binder rationale and tuple-order evidence extracted; pool checker/exporter inspected; conservative-extension trust boundary corrected in both books and ledger; 2026-10-02: Diagnostic contract and quantified stop reviewed; 43 CTest groups, 202 Python tests, 12 examples and 1000 generated cases on SLURM; normal answers agree with Z3 under six tuple orders; all diagnostic runs stop without search; both strict books and local/Git links pass |
Reader acceptance; unconfirmed answers and export checking obligations remain evidence work; no new solver qualification |
leads/quantifier-instantiation.md |
Draft |
bc5d21d; retained entailment design; TACAS 2018 Sections 3-4.1; FMCAD 2021 Section IV; Ge-de Moura CAV 2009 Section 6 |
Current syntactic pools and persistent tried tuples inspected; representative enumeration and model-based filtering linked to entailment filtering and fail masks; MBQI distinguished; fairness and revisitation obligations; strict books and links |
User review; equality and model query contracts; completeness argument and bounded-work design; implementation and evaluation pending |
implementation/models.md |
Verified |
e6d9fcb; original model-interpretation and typed conversion contracts |
Both construction adapters and callers inspected; Boolean completion; evaluated tuple invariant; reverse replay and epoch example; freeze/check/print boundaries; existing test map; strict books and local/source links |
Reader acceptance; section-level preservation audit; no new solver qualification; user model guide remains separate work |
leads/quantifier-nnf.md |
Draft |
e6d9fcb; existing preprocessing contract; Masina et al. JAIR 2025 Sections 4 and 5.5 and Appendix C |
Existing NNF and quantified route inspected; binder and polarity obligations; normalization variants and evaluation criteria recorded |
User review; binder-extension design and normalization policy pending; no implementation or new solver evaluation |
leads/asserted-quantifiers.md |
Draft |
e6d9fcb; local assertion and quantifier contracts |
Root clausifier and complete-candidate scheduling inspected; signed-root table; scope and progress obligations recorded |
User review; corpus proportion and specialization design pending; no implementation or new solver evaluation |
papers/relevance-filtering.md |
Verified |
e6d9fcb; de Moura-Bjorner 2007 Sections 1-3; Sebastiani 2007 Sections 6.9 and 7.2; Niemetz et al. FMCAD 2014 Sections II-IV; Sebastiani 2020 Sections 3-4 |
Primary sections and current quantifier assignment/completion code read; shared literature note; structural support and projection boundaries distinguished |
User review; relevance-aware completion proof and API pending; no solver changes or qualification |
leads/quantifier-relevance.md |
Draft |
e6d9fcb; papers/relevance-filtering.md; proposed local support contract |
Current all-assigned-atom behavior inspected; worked support examples; generated-obligation and final-acceptance conditions; staged evaluation plan |
User review; support design and completion proof pending; no implementation or new solver evaluation |
coverage/lia.md |
Verified |
bc5d21d; docs/qf-lia-branch-and-bound.md |
Every old heading mapped; mechanism/history split; superseded claims recorded; retained run IDs checked; both strict books; local and Git source links; all prior anchors preserved; all 25 old headings accounted for; 2026-10-01: Contributor extraction completed; complete section inventory linked |
Reader acceptance; installing archive routes at cutover |
papers/bromberger-linear-arithmetic.md |
Verified |
bc5d21d; supplied Bromberger thesis; existing 2026-08-29 literature review |
Selected primary sections reread; cube derivation and coordinate example; current integer callers checked; existing coverage acknowledged; strict books and local/source links |
Reader acceptance; full transformation and preprocessing algorithm reviews before implementation claims; no solver evaluation |
leads/lia-extended-gcd.md |
Draft |
bc5d21d; Bjorner-Nachmanson 2024 Section 4.3; original lead 12e |
Existing check and regression inspected; interval/residue derivation and antecedent requirements recorded; printed inequality direction corrected |
User review; grouping design and census; implementation and SLURM qualification pending |
papers/lia-primal-heuristics.md |
Verified |
bc5d21d; Achterberg-Berthold-Hendel 2011 Sections 2-3; Fischetti-Glover-Lodi 2005 Section 1; Berthold thesis 2014 Sections 7.1-7.3 |
Primary algorithm sections read; code and callers inspected; feasibility and neighborhood-failure boundaries; direct literature-to-state mapping |
User review; selected algorithms need implementation checklists before prototyping; no solver qualification |
leads/lia-patching.md |
Draft |
bc5d21d; papers/lia-primal-heuristics.md |
Hard-coded width and separate move limit checked; parameter proposal and staged comparisons; work and correctness gates recorded |
User review; option implementation and heuristic experiments remain open; SLURM evaluation required |
references.md |
Verified |
docs/references.bib; supplied publication metadata |
Shared citation resolution; metadata-only import; editions and identifiers checked; strict books; local and Git links; rendered references; missing-key rejection; incremental bibliography dependency |
Reader acceptance; add newly cited works as chapters are reviewed; inclusion does not establish reading or implementation |
leads/lia-infinitesimals.md |
Draft |
bc5d21d; King 4.3; Pugh 2.1; Griggio 2.6.1; Dutertre-de Moura report 4.1 |
Bound preparation; patching; integrality; cuts and branch code inspected; primary sections read; current delta regressions read; worked trace and rounding counterexample; strict books and links |
User review; implementation and all-producer invariant audit; dedicated regressions and remote qualification pending |
implementation/tactics.md |
Verified |
bc5d21d; deMoura2013 Section 3 |
Owning code and primary section read; immutable payload and context lifetime; alternatives and fallback; typed outcomes; incremental restrictions; existing test mapping; both strict books; local/source link checker; browser tables and mathematics; documentation self-review 2026-10-01; style review: direct verbs; goal and strategy terminology at first use; branch count clarified; 2026-10-01 |
Reader acceptance; reference and contributor procedures now extracted; historical evidence is not a new solver qualification |
implementation/preprocessing.md |
Verified |
bc5d21d; Bromberger Sections 8.2.2-8.2.4; symmetry Theorem 5 and Lemma 6; c944fa7 preprocessing diagnostic routing |
Owning code and primary sections read; pass order; off and integer profiles; CITE subset; finite-domain snapshots; model reconstruction; existing test mapping; both strict books; local/source link checker; browser tables and mathematics; documentation self-review 2026-10-01; style review: direct verbs; CITE and symmetry explanations; acceptance checks distinguished from logical guards; 2026-10-01; 2026-10-02: Diagnostic contract and quantified stop reviewed; 43 CTest groups, 202 Python tests, 12 examples and 1000 generated cases on SLURM; normal answers agree with Z3 under six tuple orders; all diagnostic runs stop without search; both strict books and local/Git links pass |
Reader acceptance; reference and contributor procedures now extracted; historical evidence is not a new solver qualification |
coverage/tactics-preprocessing.md |
Verified |
bc5d21d; retained chapters and run-log identities |
Section destinations; superseded claims; retained experiments; reference and workflow gaps made explicit; both strict books; local/source link checker; browser tables and mathematics; documentation self-review 2026-10-01; style review: compressed labels replaced with descriptions; historical status retained; 2026-10-01; 2026-10-01: Reference and workflow destinations completed; complete section inventory linked |
Reader acceptance; installing archive routes at cutover |
implementation/frontend.md |
Draft |
bc5d21d |
Definitions; callers; existing tests; primary sections; strict books; 735 Git links and 22257 local links checked |
Reader acceptance; no solver rerun |
implementation/sessions.md |
Draft |
bc5d21d |
Definitions; callers; existing tests; primary sections; strict books; 735 Git links and 22257 local links checked |
Reader acceptance; no solver rerun |
capabilities.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
guide/sessions.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
guide/getting-started.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
guide/input.md |
Verified |
bc5d21d; c944fa7 preprocessing diagnostic routing |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures; 2026-10-02: Diagnostic contract and quantified stop reviewed; 43 CTest groups, 202 Python tests, 12 examples and 1000 generated cases on SLURM; normal answers agree with Z3 under six tuple orders; all diagnostic runs stop without search; both strict books and local/Git links pass |
Reader acceptance; no solver or benchmark rerun |
guide/models.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
reference/policies.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
reference/backend.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
reference/statistics.md |
Verified |
bc5d21d; c944fa7 preprocessing diagnostic routing |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures; 2026-10-02: Diagnostic contract and quantified stop reviewed; 43 CTest groups, 202 Python tests, 12 examples and 1000 generated cases on SLURM; normal answers agree with Z3 under six tuple orders; all diagnostic runs stop without search; both strict books and local/Git links pass |
Reader acceptance; no solver or benchmark rerun |
reference/options.md |
Verified |
bc5d21d; c944fa7 preprocessing diagnostic routing |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures; 2026-10-02: Diagnostic contract and quantified stop reviewed; 43 CTest groups, 202 Python tests, 12 examples and 1000 generated cases on SLURM; normal answers agree with Z3 under six tuple orders; all diagnostic runs stop without search; both strict books and local/Git links pass |
Reader acceptance; no solver or benchmark rerun |
reference/tactics.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
development/tuning.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
development/fuzzing.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
development/documentation.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
development/experiments.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
development/contributing-changes.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
development/validation.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
development/debugging.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
work/results-storage.md |
Verified |
bc5d21d |
Source contracts and script flags inspected; strict books and local/Git link checks; examples reuse existing fixtures |
Reader acceptance; no solver or benchmark rerun |
coverage/frontend-sessions.md |
Verified |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks |
Reader acceptance; historical evidence is not a fresh evaluation; archive installation and publication remain separate |
coverage/index.md |
Verified |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks; 2026-10-01: All 91 source pages and 1150 headings mapped; 126 supporting entries and 1306 compatibility targets validated |
Reader acceptance; archive routes prepared but not installed |
coverage/practice-literature.md |
Verified |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks |
Reader acceptance; historical evidence is not a fresh evaluation; archive installation and publication remain separate |
coverage/solver.md |
Verified |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks |
Reader acceptance; historical evidence is not a fresh evaluation; archive installation and publication remain separate |
evidence/archive.md |
Verified |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks |
Reader acceptance; historical evidence is not a fresh evaluation; archive installation and publication remain separate |
evidence/arithmetic.md |
Verified |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks |
Reader acceptance; historical evidence is not a fresh evaluation; archive installation and publication remain separate |
evidence/quantifiers.md |
Verified |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks |
Reader acceptance; historical evidence is not a fresh evaluation; archive installation and publication remain separate |
leads/compact-distinct.md |
Draft |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks |
Reader acceptance; implementation and evaluation remain pending |
leads/incremental-equations.md |
Draft |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks |
Reader acceptance; implementation and evaluation remain pending |
leads/index.md |
Verified |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks |
Reader acceptance; historical evidence is not a fresh evaluation; archive installation and publication remain separate |
leads/shared-euf-structure.md |
Draft |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks |
Reader acceptance; implementation and evaluation remain pending |
literature.md |
Verified |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks |
Reader acceptance; historical evidence is not a fresh evaluation; archive installation and publication remain separate |
work/documentation.md |
Verified |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks |
Reader acceptance; historical evidence is not a fresh evaluation; archive installation and publication remain separate |
work/evidence.md |
Verified |
bc5d21d (implementation); 1f9f116 (retained records) |
2026-10-01: current contracts and historical records inspected; destinations and status distinctions checked; strict books and local/Git links; see dated review record for inventory and rendered checks |
Reader acceptance; historical evidence is not a fresh evaluation; archive installation and publication remain separate |
The ledger records technical inspections at their original revisions. Its stages do not automatically advance after a successful build. Research leads remain proposals; accepting their descriptions does not approve implementation. The earlier page-by-page review record retains the detailed chronology and literature-reading notes.
Earlier closing corrections, 2 October#
The frontend chapter now distinguishes core terms, theory literals, and SAT literals/clauses. Parser nodes do not cross these solver interfaces.
The model guide distinguishes the rebuild engine from the assumptions engine: the latter constructs a model for
--check-model; SMT-LIBget-modelstill requires:produce-models true.The statistics reference documents session counters and the incremental combined model-check/printing timer.
The dependency introduction includes GMP.
Current guides use the main book paths. Shared prose, examples, assets and bibliography are available without the former draft tree.
Technical verification#
The publication qualification record and follow-up record describe their SLURM checks, bounded fuzzing and model validation at the recorded revisions. Both books build strictly; local targets, pinned source links and historical routes are checked together. The earlier browser inspection covered the project URL prefix, equations, navigation, favicon and an archived route. External-host access failures remain explicit in the link report. Technical checks do not substitute for reader acceptance.
Acceptance review#
Read the introduction/capability map, user guides, implementation chapters, contributor procedures and evidence boundaries as one candidate. Check that examples explain the observable behavior, mathematical notation is introduced, source links identify the owning code, and paper citations distinguish the implemented subset from future work. Inspect equations, figures, navigation, search, old fragment routing, and the project-site URL prefix in the rendered site. Record the reader’s acceptance explicitly after that review.
Publication preparation records verification and external requirements. Evidence work retains unresolved historical mappings and quantifier-checking limits. No full-corpus performance claim follows from the documentation build or the publication qualification sample.