Struct EGraph 

pub struct EGraph<L: Language, N: Analysis<L> = ()> {
    pub analysis: N,
    /* private fields */
}

A datastructure to efficiently represent congruence relations on terms with binders.

Fields

analysis: N

Implementations

impl<L: Language, N: Analysis<L>> EGraph<L, N>

pub fn explain_equivalence( &mut self, t1: RecExpr<L>, t2: RecExpr<L>, ) -> ProvenEq

impl<L: Language, N: Analysis<L>> EGraph<L, N>

pub fn is_alive(&self, i: Id) -> bool

Returns whether an id is still alive, or whether it was merged into another class.

pub fn find_applied_id(&self, i: &AppliedId) -> AppliedId

pub fn ids(&self) -> Vec<Id>

impl<L: Language, N: Analysis<L>> EGraph<L, N>

pub fn add_syn_expr(&mut self, re: RecExpr<L>) -> AppliedId

pub fn add_syn(&mut self, enode: L) -> AppliedId

impl<L: Language, N: Analysis<L>> EGraph<L, N>

pub fn add_expr(&mut self, re: RecExpr<L>) -> AppliedId

pub fn add(&mut self, enode: L) -> AppliedId

pub fn lookup(&self, n: &L) -> Option<AppliedId>

impl<L: Language, N: Analysis<L>> EGraph<L, N>

pub fn alloc_empty_eclass(&mut self, slots: &SmallHashSet<Slot>) -> Id

impl<L: Language, N: Analysis<L>> EGraph<L, N>

pub fn union(&mut self, l: &AppliedId, r: &AppliedId) -> bool

pub fn union_justified( &mut self, l: &AppliedId, r: &AppliedId, j: Option<String>, ) -> bool

pub fn union_instantiations( &mut self, from_pat: &Pattern<L>, to_pat: &Pattern<L>, subst: &Subst, justification: Option<String>, ) -> bool

impl<L: Language, N: Analysis<L>> EGraph<L, N>

pub fn mk_identity_applied_id(&self, i: Id) -> AppliedId

pub fn check(&self)

impl<L: Language, N: Analysis<L>> EGraph<L, N>

pub fn new(analysis: N) -> Self

Creates an empty e-graph.

pub fn with_subst_method<S: SubstMethod<L, N>>(analysis: N) -> Self

Creates an empty e-graph, while specifying the substitution method to use.

pub fn slots(&self, id: Id) -> SmallHashSet<Slot>

pub fn analysis_data(&self, i: Id) -> &N::Data

pub fn analysis_data_mut(&mut self, i: Id) -> &mut N::Data

pub fn enodes(&self, i: Id) -> HashSet<L>

pub fn enodes_applied(&self, i: &AppliedId) -> Vec<L>

pub fn total_number_of_nodes(&self) -> usize

pub fn eq(&self, a: &AppliedId, b: &AppliedId) -> bool

Checks that two AppliedIds are semantically equal.

pub fn dump(&self)

Prints the contents of the E-Graph. Helpful for debugging.

pub fn get_syn_expr(&self, i: &AppliedId) -> RecExpr<L>

Returns the canonical term corresponding to i.

This function will use EGraph::get_syn_node repeatedly to build up this term.

pub fn get_syn_node(&self, i: &AppliedId) -> L

Returns the canonical e-node corresponding to i.

impl<L: Language, N: Analysis<L>> EGraph<L, N>

pub fn progress(&self) -> ProgressMeasure

Computes the ProgressMeasure of this E-Graph.

Trait Implementations

impl<L: Language, N: Analysis<L>> Debug for EGraph<L, N>

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

Formats the value using the given formatter.

impl<L: Language, N: Analysis<L> + Default> Default for EGraph<L, N>

fn default() -> Self

Returns the “default value” for a type.