pub trait Analysis<L: Language>: Sized {
type Data: Debug;
fn make(egraph: &mut EGraph<L, Self>, enode: &L) -> Self::Data;
fn merge(&mut self, a: &mut Self::Data, b: Self::Data) -> DidMerge;
fn pre_union(
egraph: &EGraph<L, Self>,
id1: Id,
id2: Id,
justification: &Option<Justification>
) { ... }
fn modify(egraph: &mut EGraph<L, Self>, id: Id) { ... }
}
Expand description
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: &mut 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));
Associated Types
Required methods
Makes a new Analysis
data for a given e-node.
Note the mutable egraph
parameter: this is needed for some
advanced use cases, but most use cases will not need to mutate
the e-graph in any way.
It is not make
’s responsiblity to insert the e-node;
the e-node is “being inserted” when this function is called.
Doing so will create an infinite loop.
Note that enode
’s children may not be canonical
Defines how to merge two Data
s when their containing
EClass
es 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
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.