Struct CongruenceClosure 

pub struct CongruenceClosure { /* private fields */ }

Congruence closure for tracking equalities.

Uses union-find with path compression for efficient equivalence class management, plus congruence propagation for f(a) = f(b) when a = b.

Implementations

impl CongruenceClosure

pub fn new() -> Self

Create a new congruence closure.

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

Find the representative of an expression (with path compression).

pub fn add_equality(&mut self, e1: Expr, e2: Expr)

Add an equality with an optional proof term.

pub fn add_equality_with_proof(&mut self, e1: Expr, e2: Expr, proof: Expr)

Add an equality with a proof term.

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

Check if two expressions are equal.

pub fn get_class(&mut self, expr: &Expr) -> Vec<Expr>

Get all expressions in the same equivalence class as expr.

pub fn num_classes(&mut self) -> usize

Get the number of equivalence classes.

pub fn get_proof(&self, e1: &Expr, e2: &Expr) -> Option<&Expr>

Get a proof that two expressions are equal (if available).

pub fn clear(&mut self)

Clear all state.

Trait Implementations

impl Default for CongruenceClosure

fn default() -> Self

Returns the “default value” for a type.