Struct EGraph 

pub struct EGraph { /* private fields */ }

Equality graph (e-graph) for congruence closure.

Implementations

impl EGraph

pub fn new() -> Self

Create new e-graph.

pub fn add_term(&mut self, term: TermId) -> EClassId

Add term to e-graph.

pub fn find(&mut self, eclass_id: EClassId) -> EClassId

Find canonical e-class ID (with path compression).

pub fn merge( &mut self, a: EClassId, b: EClassId, explanation: EqualityExplanation, ) -> Result<EClassId, String>

Merge two e-classes.

pub fn process_congruences(&mut self) -> Result<(), String>

Process pending congruences.

pub fn get_representative(&mut self, term: TermId) -> Option<TermId>

Get canonical term for an e-class.

pub fn are_equal(&mut self, a: TermId, b: TermId) -> bool

Check if two terms are in the same e-class.

pub fn get_explanation( &mut self, a: TermId, b: TermId, ) -> Option<EqualityExplanation>

Get explanation for why two terms are equal.

pub fn get_eclass_members(&mut self, term: TermId) -> Vec<TermId>

Get all terms in the same e-class as a term.

pub fn clear(&mut self)

Clear all state.

Trait Implementations

impl Clone for EGraph

fn clone(&self) -> EGraph

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for EGraph

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

Formats the value using the given formatter.

impl Default for EGraph

fn default() -> Self

Returns the “default value” for a type.