Struct egg::Runner

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 */
}

Faciliates running rewrites over an EGraph.

One use for EGraphs 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 the EGraph. If none did, then it stops, returning StopReason::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 limit

  You 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 own RewriteScheduler to govern when to run which rules.

  BackoffScheduler is the default scheduler.

Runner generates Iterations 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 Iterations, 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

impl<L, N, IterData> Runner<L, N, IterData>where L: Language, N: Analysis<L>, IterData: IterationData<L, N>,

pub fn new(analysis: N) -> Self

Create a new Runner with the given analysis and default parameters.

pub fn with_iter_limit(self, iter_limit: usize) -> Self

Sets the iteration limit. Default: 30

pub fn with_node_limit(self, node_limit: usize) -> Self

Sets the egraph size limit (in enodes). Default: 10,000

pub fn with_time_limit(self, time_limit: Duration) -> Self

Sets the runner time limit. Default: 5 seconds

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);

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.

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.

pub fn with_egraph(self, egraph: EGraph<L, N>) -> Self

Replace the EGraph of this Runner.

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.

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.

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.

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.

pub fn with_explanations_disabled(self) -> Self

Disable explanations for this runner’s egraph.

pub fn explain_equivalence( &mut self, left: &RecExpr<L>, right: &RecExpr<L> ) -> Explanation<L>

Calls EGraph::explain_equivalence.

pub fn explain_existance(&mut self, expr: &RecExpr<L>) -> Explanation<L>

Calls EGraph::explain_existance.

pub fn explain_existance_pattern( &mut self, pattern: &PatternAst<L>, subst: &Subst ) -> Explanation<L>

Calls EGraph::explain_existance_pattern`.

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.

pub fn print_report(&self)

Prints some information about a runners run.

pub fn report(&self) -> Report

Creates a Report summarizing this Runners run.

Trait Implementations

impl<L, N, IterData> Debug for Runner<L, N, IterData>where L: Language, N: Analysis<L>, IterData: Debug,

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

Formats the value using the given formatter.

impl<L, N> Default for Runner<L, N, ()>where L: Language, N: Analysis<L> + Default,

fn default() -> Self

Returns the “default value” for a type.