3.0 Release

[0x0f0f0f]

Release 3.0 when merged

[codecov-commenter]

:warning: Please install the to ensure uploads and comments are reliably processed by Codecov.

Codecov Report

Attention: Patch coverage is 87.56303% with 148 lines in your changes missing coverage. Please review.

Project coverage is 81.06%. Comparing base (a8331d6) to head (0b2e6c9). Report is 532 commits behind head on master.

Files with missing lines	Patch %	Lines
src/EGraphs/Schedulers.jl	43.47%	26 Missing :warning:
src/utils.jl	7.69%	24 Missing :warning:
src/EGraphs/egraph.jl	89.95%	22 Missing :warning:
src/Syntax.jl	88.66%	17 Missing :warning:
src/Patterns.jl	74.46%	12 Missing :warning:
src/EGraphs/saturation.jl	95.20%	7 Missing :warning:
src/Rules.jl	83.33%	7 Missing :warning:
ext/Plotting.jl	0.00%	6 Missing :warning:
src/Rewriters.jl	53.84%	6 Missing :warning:
src/ematch_compiler.jl	95.83%	6 Missing :warning:
... and 6 more

:exclamation: Your organization needs to install the Codecov GitHub app to enable full functionality.

Additional details and impacted files

```diff @@ Coverage Diff @@ ## master #185 +/- ## =========================================== + Coverage 69.17% 81.06% +11.88% =========================================== Files 16 19 +3 Lines 1353 1500 +147 =========================================== + Hits 936 1216 +280 + Misses 417 284 -133 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

[github-actions[bot]]

Benchmark Results

	egg-sym	egg-cust	MT@0b2e6c9f11b...	MT@master	egg-sym/MT@0b2...	egg-cust/MT@0b...	MT@master/MT@0...
egraph_addexpr	1.47 ms		5.16 ms	13.8 ms	0.284		2.68
basic_maths_simpl2	12.6 ms	5.16 ms	19.4 ms	782 ms	0.651	0.266	40.3
prop_logic_freges_theorem	2.51 ms	1.55 ms	1.06 ms	35.1 ms	2.37	1.47	33.2
calc_logic_demorgan	59.7 μs	34.6 μs	77.6 μs	499 μs	0.769	0.445	6.43
calc_logic_freges_theorem	22 ms	11.6 ms	41 ms	3.12e+03 ms	0.537	0.284	76.2
basic_maths_simpl1	6.02 ms	2.82 ms	4.82 ms	48.8 ms	1.25	0.585	10.1
egraph_constructor	0.0831 μs		0.09 μs	0.101 μs	0.923		1.12
prop_logic_prove1	35.4 ms	14 ms	40.6 ms	8.3e+03 ms	0.872	0.345	204
prop_logic_demorgan	78.1 μs	45.5 μs	97.9 μs	732 μs	0.798	0.465	7.48
while_superinterpreter_while_10			18.3 ms	91.5 ms			5
prop_logic_rewrite			120 μs	120 μs			0.999
time_to_load			495 ms	528 ms			1.07

Benchmark Plots

A plot of the benchmark results have been uploaded as an artifact to the workflow run for this PR. Go to "Actions"->"Benchmark a pull request"->[the most recent run]->"Artifacts" (at the bottom).

[0x0f0f0f]

This is 14.5 times faster than egg in rust!

Julia Code

using Metatheory, BenchmarkTools

t = @theory a b begin
  a + b --> b + a
  a * b --> b * a
  a + 0 --> a
  a * 0 --> 0
  a * 1 --> a
end

using BenchmarkTools

p = SaturationParams(; timer = false)

function simpl(ex)
  g = EGraph(ex)
  saturate!(g, t, p)
  extract!(g, astsize)
end

ex = :(0 + (1 * foo) * 0 + (a * 0) + a)

simpl(ex)

@btime simpl(ex)

94.462 μs (1412 allocations: 66.08 KiB)

Rust code

use egg::{rewrite as rw, *};
//use std::time::Duration;
fn main() {
    env_logger::init();
    use egg::*;

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

    fn make_rules() -> Vec<Rewrite<SimpleLanguage, ()>> {
        vec![
            rewrite!("commute-add"; "(+ ?a ?b)" => "(+ ?b ?a)"),
            rewrite!("commute-mul"; "(* ?a ?b)" => "(* ?b ?a)"),
            rewrite!("add-0"; "(+ ?a 0)" => "?a"),
            rewrite!("mul-0"; "(* ?a 0)" => "0"),
            rewrite!("mul-1"; "(* ?a 1)" => "?a"),
        ]
    }

    /// parse an expression, simplify it using egg, and pretty print it back out
    fn simplify(s: &str) -> String {
        // parse the expression, the type annotation tells it which Language to use
        let expr: RecExpr<SimpleLanguage> = s.parse().unwrap();

        // simplify the expression using a Runner, which creates an e-graph with
        // the given expression and runs the given rules over it
        let runner = Runner::default().with_expr(&expr).run(&make_rules());

        // the Runner knows which e-class the expression given with `with_expr` is in
        let root = runner.roots[0];

        // use an Extractor to pick the best element of the root eclass
        let extractor = Extractor::new(&runner.egraph, AstSize);
        let (best_cost, best) = extractor.find_best(root);
        println!("Simplified {} to {} with cost {}", expr, best, best_cost);
        best.to_string()
    }

    // assert_eq!(simplify("(* 0 42)"), "0");
    let apply_time: std::time::Instant = instant::Instant::now();
    // assert_eq!(simplify("(+ 0 (* 1 foo))"), "foo");
    assert_eq!(simplify("(+ (+ (+ 0 (* (* 1 foo) 0)) (* a 0)) a)"), "a");
    let apply_time = apply_time.elapsed().as_secs_f64();
    println!("simplification time {}", apply_time);
}

simplification time 0.001375786 seconds which is 1375.786microseconds

1375.786 / 94.462 = 14.56x faster

well

[0x0f0f0f]

@gkronber I have just updated this branch to include the latest release of https://github.com/JuliaSymbolics/TermInterface.jl - the interface for custom types has changed, please let me know if you encounter any issue

[gkronber]

@gkronber I have just updated this branch to include the latest release of https://github.com/JuliaSymbolics/TermInterface.jl - the interface for custom types has changed, please let me know if you encounter any issue

Thanks for the heads up. I only had to make minor changes because of the changed names for functions in VecExpr.

[shashi]

@0x0f0f0f Can you summarize the changes in this PR? What's the huge number of deletions from? And what's the huge performance gain from? This is awesome.

[0x0f0f0f]

@0x0f0f0f Can you summarize the changes in this PR? What's the huge number of deletions from? And what's the huge performance gain from? This is awesome.

@shashi I removed some unnecessary parts of the codebase, and basically changed the core types used for rewriting. The trick for performance was basically packing e-nodes in Vector{UInt64} such that loops (which happens hundreds of thousands of times) can be vectorized. Instead of having a struct with operation, hash, flags... fields, I just encode and pack everything into UInt64.

https://github.com/JuliaSymbolics/Metatheory.jl/blob/8f228fd0f8a5e1f97fd0ed986cb1c7e94cbce5c8/src/vecexpr.jl

Also some algorithms were updated, as the egg repo now has more efficient versions of parts of equality saturation (rebuilding) that were in the original paper

[0x0f0f0f]

I will hold a 5 min lightning talk on thursday 6 pm CET https://egraphs.org/ if interested

[chriselrod]

For fun, I benchmarked this PR

julia> @benchmark simpl(ex)
BenchmarkTools.Trial: 10000 samples with 1 evaluation.
 Range (min … max):  74.508 μs …   8.173 ms  ┊ GC (min … max): 0.00% … 97.73%
 Time  (median):     80.918 μs               ┊ GC (median):    0.00%
 Time  (mean ± σ):   87.298 μs ± 150.197 μs  ┊ GC (mean ± σ):  5.42% ±  3.34%

   ▂▃▂   ▄▇█▇▆▆▆▅▄▅▅▅▄▃▃▃▂▂▂▁▁▁ ▁▁▁▁ ▁                         ▂
  █████▆▇██████████████████████████████▇▇▇▇▇▇█▇▇▆▆▆▆▅▆▄▅▂▅▂▄▅▅ █
  74.5 μs       Histogram: log(frequency) by time       107 μs <

 Memory estimate: 55.08 KiB, allocs estimate: 1003.

> target/release/eggvsmetatheory                               (base) 
Simplified (+ (+ (+ 0 (* (* 1 foo) 0)) (* a 0)) a) to a with cost 1
simplification time 46.603975 us

It's still slower than egg for that example, but this is a huge improvement compared to being like 300x slower the last time I compared them.

I modified the Rust script so that we aren't benchmarking printing, and also taking the average of 1000 runs:

    let apply_time: std::time::Instant = instant::Instant::now();
    for _i in 0..1000 {
        simplify("(+ (+ (+ 0 (* (* 1 foo) 0)) (* a 0)) a)", false);
    }
    let apply_time = apply_time.elapsed().as_secs_f64();
    println!("simplification time {} us", apply_time*1e3);

where simplify takes a print: bool arg for whether or not it should print.

[shashi]

Let's go!!!

[0x0f0f0f]

It's still slower than egg for that example, but this is a huge improvement compared to being like 300x slower the last time I compared them.

I modified the Rust script so that we aren't benchmarking printing, and also taking the average of 1000 runs:

@chriselrod we just published a preprint with some results here https://arxiv.org/pdf/2404.08751.pdf

@nmheim is working on https://github.com/nmheim/egg-benchmark which should be the repository containing benchmarks for egg against the ones in the benchmarks directory in repository (1-1 comparison with same hyperparameters/rules where possible).

[0x0f0f0f]

For fun, I benchmarked this PR

julia> @benchmark simpl(ex)
BenchmarkTools.Trial: 10000 samples with 1 evaluation.
 Range (min … max):  74.508 μs …   8.173 ms  ┊ GC (min … max): 0.00% … 97.73%
 Time  (median):     80.918 μs               ┊ GC (median):    0.00%
 Time  (mean ± σ):   87.298 μs ± 150.197 μs  ┊ GC (mean ± σ):  5.42% ±  3.34%

   ▂▃▂   ▄▇█▇▆▆▆▅▄▅▅▅▄▃▃▃▂▂▂▁▁▁ ▁▁▁▁ ▁                         ▂
  █████▆▇██████████████████████████████▇▇▇▇▇▇█▇▇▆▆▆▆▅▆▄▅▂▅▂▄▅▅ █
  74.5 μs       Histogram: log(frequency) by time       107 μs <

 Memory estimate: 55.08 KiB, allocs estimate: 1003.

> target/release/eggvsmetatheory                               (base) 
Simplified (+ (+ (+ 0 (* (* 1 foo) 0)) (* a 0)) a) to a with cost 1
simplification time 46.603975 us

It's still slower than egg for that example, but this is a huge improvement compared to being like 300x slower the last time I compared them.

@chriselrod try now on latest commit!!!

julia> @benchmark simpl(ex)
BenchmarkTools.Trial: 10000 samples with 1 evaluation.
 Range (min … max):  36.052 μs …  4.479 ms  ┊ GC (min … max): 0.00% … 94.02%
 Time  (median):     42.267 μs              ┊ GC (median):    0.00%
 Time  (mean ± σ):   50.441 μs ± 98.863 μs  ┊ GC (mean ± σ):  4.48% ±  2.47%

  ▅█▇▄▃▂▂▁ ▁▁▁▁                                               ▂
  ███████████████▆▆▄▄▅▃▄▃▃▄▄▁▅▃▅▁▁▁▁▃▄▁▃▁▁▁▄▃▄▁▃▁▁▁▃▄▁▃▄▃▁▃▄▄ █
  36.1 μs      Histogram: log(frequency) by time       227 μs <

 Memory estimate: 33.66 KiB, allocs estimate: 330.

[0x0f0f0f]

@nmheim has just added a fully automated benchmark against egg that will report the compared performance of MT 2.0, egg and MT3.0 in a markdown table in the PR comments.

[chriselrod]

I get

julia> @benchmark simpl($ex)
BenchmarkTools.Trial: 10000 samples with 1 evaluation.
 Range (min … max):  64.553 μs …   9.810 ms  ┊ GC (min … max): 0.00% … 98.36%
 Time  (median):     69.119 μs               ┊ GC (median):    0.00%
 Time  (mean ± σ):   73.625 μs ± 157.327 μs  ┊ GC (mean ± σ):  5.14% ±  2.56%

    █▇▁     ▆▇▂                                                 
  ▂████▅▃▂▂▆███▇▆▆▆▄▄▆▆▄▃▃▂▂▂▂▂▂▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁ ▃
  64.6 μs         Histogram: frequency by time         88.8 μs <

 Memory estimate: 33.66 KiB, allocs estimate: 330.

julia> @benchmark simpl(ex)
BenchmarkTools.Trial: 10000 samples with 1 evaluation.
 Range (min … max):  64.589 μs …   4.956 ms  ┊ GC (min … max): 0.00% … 97.61%
 Time  (median):     69.263 μs               ┊ GC (median):    0.00%
 Time  (mean ± σ):   73.508 μs ± 134.227 μs  ┊ GC (mean ± σ):  5.08% ±  2.74%

   ▁▆▆▂     ▃█▇▃▁▁                                              
  ▂████▆▄▃▂▄███████▇▅▄▄▄▃▃▂▂▂▂▂▂▂▂▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁▁ ▃
  64.6 μs         Histogram: frequency by time         87.7 μs <

 Memory estimate: 33.66 KiB, allocs estimate: 330.

vs Rust

> target/release/eggvsmetatheory 
Simplified (+ (+ (+ 0 (* (* 1 foo) 0)) (* a 0)) a) to a with cost 1
simplification time 59.480913 us

on commit

> g lg                                                                                                                                                             (base) 
6c692a5 - (HEAD -> ale/3.0, origin/ale/3.0) benchmark pr (10 hours ago) [a]
aa38d76 - (origin/master, origin/HEAD) benchmark pr (10 hours ago) [a]
e407dd8 - Merge pull request #201 from nmheim/nh/bench-action (10 hours ago) [Alessandro]

so it is getting pretty close.

[quffaro]

Hey @0x0f0f0f I'm working on adopting this package but would like to use the 3.0 release. Do you know what else needs to be done in order to release 3.0, and can I assist? Very excited!

[0x0f0f0f]

Hey @0x0f0f0f I'm working on adopting this package but would like to use the 3.0 release. Do you know what else needs to be done in order to release 3.0, and can I assist? Very excited!

Hey! @quffaro nice meeting you. Yes. There are a lot of things.

https://github.com/JuliaSymbolics/Metatheory.jl/issues/210 https://github.com/JuliaSymbolics/Metatheory.jl/issues/209 https://github.com/JuliaSymbolics/Metatheory.jl/issues/142 https://github.com/JuliaSymbolics/Metatheory.jl/issues/89 https://github.com/JuliaSymbolics/Metatheory.jl/issues/111 https://github.com/JuliaSymbolics/Metatheory.jl/issues/89

[0x0f0f0f]

Hey @0x0f0f0f I'm working on adopting this package but would like to use the 3.0 release. Do you know what else needs to be done in order to release 3.0, and can I assist? Very excited!

Hey! @quffaro nice meeting you. Yes. There are a lot of things.

210 #209 #142 #89 #111 #89

@quffaro I will post more later