Skip to main content

Module egraph

Module egraph 

Source
Expand description

The ARCHITECT — equality saturation over a compiler e-graph (EXODIA Phase 4, sprints 17–22).

Classic egg-style design: a hash-consed term bank over the shared [UnionFind] (the same engine the kernel’s congruence closure uses), a worklist rebuild restoring the congruence invariant after unions, budgeted saturation with a deterministic rule order, and bottom-up cost extraction.

Class facts (scalar kind + integer interval) come from the Oracle and gate the conditional rewrites: x / 2^n → x >> n fires only with a non-negativity proof, the Group-2 boolean laws fire only on proven Bools, and EVERYTHING fails closed when no fact is present.

Re-exports§

pub use enode::CompilerENode;

Modules§

convert
AST ⇄ e-graph conversion and the statement-level Architect pass.
enode
The Architect’s term language — flat, multi-arity, Copy.
extract
Bottom-up cost extraction (cycle-tolerant).
rules
Rewrite rules (EXODIA Groups 1–3) with KERNEL-CHECKED soundness certificates (D11b): the compiler’s e-graph is a sibling of the proof engine, not a stranger.

Structs§

ClassFact
Per-class knowledge, seeded from literals and the Oracle.
CompilerEGraph

Constants§

MAX_NODES
…or when the term bank would exceed this many nodes.
SATURATION_ITERS
Saturation stops after this many fixpoint iterations…

Type Aliases§

NodeId