pub struct Runner<L: Language, N: Analysis<L>, IterData = ()> {
pub egraph: EGraph<L, N>,
pub iterations: Vec<Iteration<IterData>>,
pub roots: Vec<Id>,
pub stop_reason: Option<StopReason>,
pub hooks: Vec<Box<dyn FnMut(&mut Self) -> Result<(), String>>>,
/* private fields */
}
Expand description
Faciliates running rewrites over an EGraph
.
One use for EGraph
s is as the basis of a rewriting system.
Since an egraph never “forgets” state when applying a Rewrite
, you
can apply many rewrites many times quite efficiently.
After the egraph is “full” (the rewrites can no longer find new
equalities) or some other condition, the egraph compactly represents
many, many equivalent expressions.
At this point, the egraph is ready for extraction (see Extractor
)
which can pick the represented expression that’s best according to
some cost function.
This technique is called equality saturation in general. However, there can be many challenges in implementing this “outer loop” of applying rewrites, mostly revolving around which rules to run and when to stop.
Runner
is egg
’s provided equality saturation engine that has
reasonable defaults and implements many useful things like saturation
checking, egraph size limits, and customizable rule
scheduling.
Consider using Runner
before rolling your own outer loop.
Here are some of the things Runner
does for you:
-
Saturation checking
Runner
checks to see if any of the rules added anything new to theEGraph
. If none did, then it stops, returningStopReason::Saturated
. -
Iteration limits
You can set a upper limit of iterations to do in case the search doesn’t stop for some other reason. If this limit is hit, it stops with
StopReason::IterationLimit
. -
EGraph
size limitYou can set a upper limit on the number of enodes in the egraph. If this limit is hit, it stops with
StopReason::NodeLimit
. -
Time limit
You can set a time limit on the runner. If this limit is hit, it stops with
StopReason::TimeLimit
. -
Rule scheduling
Some rules enable themselves, blowing up the
EGraph
and preventing other rewrites from running as many times. To prevent this, you can provide your ownRewriteScheduler
to govern when to run which rules.BackoffScheduler
is the default scheduler.
Runner
generates Iteration
s that record some data about
each iteration.
You can add your own data to this by implementing the
IterationData
trait.
Runner
is generic over the IterationData
that it will be in the
Iteration
s, but by default it uses ()
.
Example
use egg::{*, rewrite as rw};
define_language! {
enum SimpleLanguage {
Num(i32),
"+" = Add([Id; 2]),
"*" = Mul([Id; 2]),
Symbol(Symbol),
}
}
let rules: &[Rewrite<SimpleLanguage, ()>] = &[
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"),
];
pub struct MyIterData {
smallest_so_far: usize,
}
type MyRunner = Runner<SimpleLanguage, (), MyIterData>;
impl IterationData<SimpleLanguage, ()> for MyIterData {
fn make(runner: &MyRunner) -> Self {
let root = runner.roots[0];
let mut extractor = Extractor::new(&runner.egraph, AstSize);
MyIterData {
smallest_so_far: extractor.find_best(root).0,
}
}
}
let start = "(+ 0 (* 1 foo))".parse().unwrap();
// Runner is customizable in the builder pattern style.
let runner = MyRunner::new(Default::default())
.with_iter_limit(10)
.with_node_limit(10_000)
.with_expr(&start)
.with_scheduler(SimpleScheduler)
.run(rules);
// Now we can check our iteration data to make sure that the cost only
// got better over time
for its in runner.iterations.windows(2) {
assert!(its[0].data.smallest_so_far >= its[1].data.smallest_so_far);
}
println!(
"Stopped after {} iterations, reason: {:?}",
runner.iterations.len(),
runner.stop_reason
);
Fields§
§egraph: EGraph<L, N>
The EGraph
used.
iterations: Vec<Iteration<IterData>>
Data accumulated over each Iteration
.
roots: Vec<Id>
The roots of expressions added by the
with_expr
method, in insertion order.
stop_reason: Option<StopReason>
Why the Runner
stopped. This will be None
if it hasn’t
stopped yet.
hooks: Vec<Box<dyn FnMut(&mut Self) -> Result<(), String>>>
The hooks added by the
with_hook
method, in insertion order.
Implementations§
source§impl<L, N, IterData> Runner<L, N, IterData>where
L: Language,
N: Analysis<L>,
IterData: IterationData<L, N>,
impl<L, N, IterData> Runner<L, N, IterData>where L: Language, N: Analysis<L>, IterData: IterationData<L, N>,
sourcepub fn new(analysis: N) -> Self
pub fn new(analysis: N) -> Self
Create a new Runner
with the given analysis and default parameters.
sourcepub fn with_iter_limit(self, iter_limit: usize) -> Self
pub fn with_iter_limit(self, iter_limit: usize) -> Self
Sets the iteration limit. Default: 30
sourcepub fn with_node_limit(self, node_limit: usize) -> Self
pub fn with_node_limit(self, node_limit: usize) -> Self
Sets the egraph size limit (in enodes). Default: 10,000
sourcepub fn with_time_limit(self, time_limit: Duration) -> Self
pub fn with_time_limit(self, time_limit: Duration) -> Self
Sets the runner time limit. Default: 5 seconds
sourcepub fn with_hook<F>(self, hook: F) -> Selfwhere
F: FnMut(&mut Self) -> Result<(), String> + 'static,
pub fn with_hook<F>(self, hook: F) -> Selfwhere F: FnMut(&mut Self) -> Result<(), String> + 'static,
Add a hook to instrument or modify the behavior of a Runner
.
Each hook will run at the beginning of each iteration, i.e. before
all the rewrites.
If your hook modifies the e-graph, make sure to call
rebuild
.
Example
let rules: &[Rewrite<SymbolLang, ()>] = &[
rewrite!("commute-add"; "(+ ?a ?b)" => "(+ ?b ?a)"),
// probably some others ...
];
Runner::<SymbolLang, ()>::default()
.with_expr(&"(+ 5 2)".parse().unwrap())
.with_hook(|runner| {
println!("Egraph is this big: {}", runner.egraph.total_size());
Ok(())
})
.run(rules);
sourcepub fn with_scheduler(
self,
scheduler: impl RewriteScheduler<L, N> + 'static
) -> Self
pub fn with_scheduler( self, scheduler: impl RewriteScheduler<L, N> + 'static ) -> Self
Change out the RewriteScheduler
used by this Runner
.
The default one is BackoffScheduler
.
sourcepub fn with_expr(self, expr: &RecExpr<L>) -> Self
pub fn with_expr(self, expr: &RecExpr<L>) -> Self
Add an expression to the egraph to be run.
The eclass id of this addition will be recorded in the
roots
field, ordered by
insertion order.
sourcepub fn with_egraph(self, egraph: EGraph<L, N>) -> Self
pub fn with_egraph(self, egraph: EGraph<L, N>) -> Self
Replace the EGraph
of this Runner
.
sourcepub fn run<'a, R>(self, rules: R) -> Selfwhere
R: IntoIterator<Item = &'a Rewrite<L, N>>,
L: 'a,
N: 'a,
pub fn run<'a, R>(self, rules: R) -> Selfwhere R: IntoIterator<Item = &'a Rewrite<L, N>>, L: 'a, N: 'a,
Run this Runner
until it stops.
After this, the field
stop_reason
is guaranteed to be
set.
sourcepub fn with_explanations_enabled(self) -> Self
pub fn with_explanations_enabled(self) -> Self
Enable explanations for this runner’s egraph.
This allows the runner to explain why two expressions are
equivalent with the explain_equivalence
function.
sourcepub fn without_explanation_length_optimization(self) -> Self
pub fn without_explanation_length_optimization(self) -> Self
By default, egg runs a greedy algorithm to reduce the size of resulting explanations (without complexity overhead). Use this function to turn this algorithm off.
sourcepub fn with_explanation_length_optimization(self) -> Self
pub fn with_explanation_length_optimization(self) -> Self
By default, egg runs a greedy algorithm to reduce the size of resulting explanations (without complexity overhead). Use this function to turn this algorithm on again if you have turned it off.
sourcepub fn with_explanations_disabled(self) -> Self
pub fn with_explanations_disabled(self) -> Self
Disable explanations for this runner’s egraph.
sourcepub fn explain_equivalence(
&mut self,
left: &RecExpr<L>,
right: &RecExpr<L>
) -> Explanation<L>
pub fn explain_equivalence( &mut self, left: &RecExpr<L>, right: &RecExpr<L> ) -> Explanation<L>
Calls EGraph::explain_equivalence
.
sourcepub fn explain_existance(&mut self, expr: &RecExpr<L>) -> Explanation<L>
pub fn explain_existance(&mut self, expr: &RecExpr<L>) -> Explanation<L>
Calls EGraph::explain_existance
.
sourcepub fn explain_existance_pattern(
&mut self,
pattern: &PatternAst<L>,
subst: &Subst
) -> Explanation<L>
pub fn explain_existance_pattern( &mut self, pattern: &PatternAst<L>, subst: &Subst ) -> Explanation<L>
sourcepub fn explain_matches(
&mut self,
left: &RecExpr<L>,
right: &PatternAst<L>,
subst: &Subst
) -> Explanation<L>
pub fn explain_matches( &mut self, left: &RecExpr<L>, right: &PatternAst<L>, subst: &Subst ) -> Explanation<L>
Get an explanation for why an expression matches a pattern.
sourcepub fn print_report(&self)
pub fn print_report(&self)
Prints some information about a runners run.