Struct EquivManager 

pub struct EquivManager { /* private fields */ }

Equivalence manager for caching def_eq results during type checking.

Provides two layers of caching:

1. A set of expression pairs known to be definitionally equal.
2. A set of expression pairs known to NOT be definitionally equal (failure cache).

The failure cache is critical for performance: when lazy delta reduction tries multiple unfolding strategies, caching failures avoids redundant work.

Implementations

impl EquivManager

pub fn new() -> Self

Create a new empty equivalence manager.

pub fn add_equiv(&mut self, a: &Expr, b: &Expr)

Record that two expressions are definitionally equal.

pub fn is_equiv(&mut self, a: &Expr, b: &Expr) -> bool

Check if two expressions are known to be definitionally equal.

pub fn add_failure(&mut self, a: &Expr, b: &Expr)

Record that two expressions are NOT definitionally equal.

pub fn is_failure(&self, a: &Expr, b: &Expr) -> bool

Check if two expressions are known to NOT be definitionally equal.

pub fn clear(&mut self)

Clear all cached results.

pub fn num_equiv(&self) -> usize

Get the number of cached equivalences.

pub fn num_failures(&self) -> usize

Get the number of cached failures.

Trait Implementations

impl Debug for EquivManager

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for EquivManager

fn default() -> Self

Returns the “default value” for a type.