Metatheory.jl
Metatheory.jl copied to clipboard
JuliaSymbolics
3.0 Release
:warning: Please install the to ensure uploads and comments are reliably processed by Codecov.
Codecov Report
Attention: Patch coverage is 87.17519% with 153 lines in your changes missing coverage. Please review.
Project coverage is 80.78%. Comparing base (
a8331d6) to head (1dc53da). Report is 532 commits behind head on master.
| Files | Patch % | Lines |
|---|---|---|
| src/EGraphs/egraph.jl | 87.83% | 27 Missing :warning: |
| src/EGraphs/Schedulers.jl | 43.47% | 26 Missing :warning: |
| src/utils.jl | 7.69% | 24 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
@@ Coverage Diff @@
## master #185 +/- ##
===========================================
+ Coverage 69.17% 80.78% +11.60%
===========================================
Files 16 19 +3
Lines 1353 1504 +151
===========================================
+ Hits 936 1215 +279
+ Misses 417 289 -128
:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.
Benchmark Results
| egg-sym | egg-cust | MT@1dc53daf4c9... | MT@master | egg-sym/MT@1dc... | egg-cust/MT@1d... | MT@master/MT@1... | |
|---|---|---|---|---|---|---|---|
| egraph_addexpr | 1.46 ms | 4.76 ms | 13.8 ms | 0.307 | 2.89 | ||
| basic_maths_simpl2 | 12.6 ms | 5.15 ms | 18.6 ms | 758 ms | 0.681 | 0.277 | 40.9 |
| prop_logic_freges_theorem | 2.5 ms | 1.55 ms | 1.03 ms | 34.7 ms | 2.42 | 1.5 | 33.6 |
| calc_logic_demorgan | 60.4 μs | 35.1 μs | 75.4 μs | 502 μs | 0.801 | 0.466 | 6.65 |
| calc_logic_freges_theorem | 21.9 ms | 11.6 ms | 37.9 ms | 3.1e+03 ms | 0.578 | 0.305 | 81.6 |
| basic_maths_simpl1 | 6.03 ms | 2.81 ms | 4.46 ms | 48 ms | 1.35 | 0.631 | 10.8 |
| egraph_constructor | 0.0831 μs | 0.0912 μs | 0.101 μs | 0.912 | 1.1 | ||
| prop_logic_prove1 | 35.3 ms | 13.9 ms | 39.2 ms | 8.28e+03 ms | 0.899 | 0.354 | 211 |
| prop_logic_demorgan | 79.2 μs | 45.8 μs | 97.1 μs | 730 μs | 0.816 | 0.472 | 7.52 |
| while_superinterpreter_while_10 | 18.6 ms | 92.6 ms | 4.98 | ||||
| prop_logic_rewrite | 119 μs | 119 μs | 0.999 | ||||
| time_to_load | 490 ms | 516 ms | 1.05 |
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).
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}
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
@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 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.
@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 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
I will hold a 5 min lightning talk on thursday 6 pm CET https://egraphs.org/ if interested
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.
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).
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 usIt'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.
@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.
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.
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 @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
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