Trait egg::Analysis

pub trait Analysis<L: Language>: Sized {
    type Data: Debug;

    // Required methods
    fn make(egraph: &EGraph<L, Self>, enode: &L) -> Self::Data;
    fn merge(&mut self, a: &mut Self::Data, b: Self::Data) -> DidMerge;

    // Provided methods
    fn pre_union(
        egraph: &EGraph<L, Self>,
        id1: Id,
        id2: Id,
        justification: &Option<Justification>
    ) { ... }
    fn modify(egraph: &mut EGraph<L, Self>, id: Id) { ... }
}

Arbitrary data associated with an EClass.

egg allows you to associate arbitrary data with each eclass. The Analysis allows that data to behave well even across eclasses merges.

Analysis can prove useful in many situtations. One common one is constant folding, a kind of partial evaluation. In that case, the metadata is basically Option<L>, storing the cheapest constant expression (if any) that’s equivalent to the enodes in this eclass. See the test files math.rs and prop.rs for more complex examples on this usage of Analysis.

If you don’t care about Analysis, () implements it trivally, just use that.

Example

use egg::{*, rewrite as rw};

define_language! {
    enum SimpleMath {
        "+" = Add([Id; 2]),
        "*" = Mul([Id; 2]),
        Num(i32),
        Symbol(Symbol),
    }
}

// in this case, our analysis itself doesn't require any data, so we can just
// use a unit struct and derive Default
#[derive(Default)]
struct ConstantFolding;
impl Analysis<SimpleMath> for ConstantFolding {
    type Data = Option<i32>;

    fn merge(&mut self, to: &mut Self::Data, from: Self::Data) -> DidMerge {
        egg::merge_max(to, from)
    }

    fn make(egraph: &EGraph<SimpleMath, Self>, enode: &SimpleMath) -> Self::Data {
        let x = |i: &Id| egraph[*i].data;
        match enode {
            SimpleMath::Num(n) => Some(*n),
            SimpleMath::Add([a, b]) => Some(x(a)? + x(b)?),
            SimpleMath::Mul([a, b]) => Some(x(a)? * x(b)?),
            _ => None,
        }
    }

    fn modify(egraph: &mut EGraph<SimpleMath, Self>, id: Id) {
        if let Some(i) = egraph[id].data {
            let added = egraph.add(SimpleMath::Num(i));
            egraph.union(id, added);
        }
    }
}

let rules = &[
    rw!("commute-add"; "(+ ?a ?b)" => "(+ ?b ?a)"),
    rw!("commute-mul"; "(* ?a ?b)" => "(* ?b ?a)"),

    rw!("add-0"; "(+ ?a 0)" => "?a"),
    rw!("mul-0"; "(* ?a 0)" => "0"),
    rw!("mul-1"; "(* ?a 1)" => "?a"),
];

let expr = "(+ 0 (* (+ 4 -3) foo))".parse().unwrap();
let mut runner = Runner::<SimpleMath, ConstantFolding, ()>::default().with_expr(&expr).run(rules);
let just_foo = runner.egraph.add_expr(&"foo".parse().unwrap());
assert_eq!(runner.egraph.find(runner.roots[0]), runner.egraph.find(just_foo));

Required Associated Types

type Data: Debug

The per-EClass data for this analysis.

Required Methods

fn make(egraph: &EGraph<L, Self>, enode: &L) -> Self::Data

Makes a new Analysis for a given enode Analysis.

fn merge(&mut self, a: &mut Self::Data, b: Self::Data) -> DidMerge

Defines how to merge two Datas when their containing EClasses merge.

This should update a to correspond to the merged analysis data.

The result is a DidMerge(a_merged, b_merged) indicating whether the merged result is different from a and b respectively.

Since merge can modify a, let a0/a1 be the value of a before/after the call to merge, respectively.

If a0 != a1 the result must have a_merged == true. This may be conservative – it may be true even if even if a0 == a1.

If b != a1 the result must have b_merged == true. This may be conservative – it may be true even if even if b == a1.

This function may modify the Analysis, which can be useful as a way to store information for the Analysis::modify hook to process, since modify has access to the e-graph.

Provided Methods

fn pre_union(
egraph: &EGraph<L, Self>,
id1: Id,
id2: Id,
justification: &Option<Justification>
)

An optional hook that allows inspection before a union occurs. When explanations are enabled, it gives two ids that represent the two particular terms being unioned, not the canonical ids for the two eclasses. It also gives a justification for the union when explanations are enabled.

By default it does nothing.

pre_union is called a lot, so doing anything significant (like printing) will cause things to slow down.

fn modify(egraph: &mut EGraph<L, Self>, id: Id)

A hook that allows the modification of the EGraph.

By default this does nothing.

This function is called immediately following Analysis::merge when unions are performed.

Implementations on Foreign Types

impl<L: Language> Analysis<L> for ()

type Data = ()

fn make(_egraph: &EGraph<L, Self>, _enode: &L) -> Self::Data

fn merge(&mut self, _: &mut Self::Data, _: Self::Data) -> DidMerge

Implementors