Struct EGraph 

pub struct EGraph { /* private fields */ }

Extended equality graph for congruence closure with E-node tracking.

Provides richer structure than CongruenceClosure for proof reconstruction.

Implementations

impl EGraph

pub fn new() -> Self

Create an empty E-graph.

pub fn add_expr(&mut self, expr: Expr) -> usize

Add an expression to the E-graph (creating a new singleton class if not present).

pub fn find_class(&self, expr: &Expr) -> Option<usize>

Get the class ID for an expression, if present.

pub fn merge_classes(&mut self, id1: usize, id2: usize, proof: Option<Expr>)

Merge two equivalence classes.

pub fn are_equal(&self, e1: &Expr, e2: &Expr) -> bool

Check if two expressions are in the same class.

pub fn add_equality(&mut self, e1: Expr, e2: Expr, proof: Option<Expr>)

Add an equality e1 = e2 with optional proof.

pub fn num_classes(&self) -> usize

Get the number of equivalence classes.

pub fn get_class(&self, id: usize) -> Option<&ENode>

Get an E-node by class ID.

pub fn representative(&self, expr: &Expr) -> Option<&Expr>

Get the representative of the class containing expr.

pub fn clear(&mut self)

Clear the E-graph.

Trait Implementations

impl Default for EGraph

fn default() -> Self

Returns the “default value” for a type.