Struct FlatCC 

pub struct FlatCC { /* private fields */ }

Flat union-find for congruence closure on term indices.

This is a simpler, more cache-friendly representation than the HashMap-based approach above.

Implementations

impl FlatCC

pub fn new(n: usize) -> Self

Create a new flat CC with n initial singleton classes.

pub fn find(&mut self, i: TermIdx) -> TermIdx

Find the root of the equivalence class containing i.

pub fn union(&mut self, i: TermIdx, j: TermIdx)

Merge the classes of i and j.

pub fn add_node(&mut self) -> TermIdx

Add a new term node, returning its index.

pub fn add_app(&mut self, app: FlatApp)

Register an application.

pub fn are_equal(&mut self, i: TermIdx, j: TermIdx) -> bool

Check if i and j are in the same class.

pub fn num_nodes(&self) -> usize

Get the total number of term nodes.

pub fn num_apps(&self) -> usize

Get the number of registered applications.

pub fn propagate_congruences(&mut self)

Propagate congruences: if fn(i) == fn(j) and arg(i) == arg(j), then result(i) == result(j).

Merges the result classes of congruent applications so that downstream are_equal queries reflect these equalities.