Expand description
Shared reification substrate for the arithmetic decision procedures.
ring, lia, and omega all read the same deep embedding of terms
(SLit/SVar/SName/SApp applied via kernel App nodes). The pattern
extractors live here once, and so does VarInterner, which maps named
globals to variable indices.
§Why an interner
Named globals must reify to variable indices that are (a) distinct for
distinct names and (b) stable across every term reified for one goal —
the left- and right-hand sides of an equation, or a hypothesis set and its
conclusion. A hash of the name satisfies (b) but not (a): a collision
identifies two different variables and lets the procedure prove Aa = BB.
The interner satisfies both by construction; callers create one per goal
and thread it through every reification belonging to that goal.
Structs§
- VarInterner
- Per-goal map from global names to variable indices.