Skip to content

Inform schedulers with correct number of matches.#259

Open
gkronber wants to merge 1 commit intoale/3.0from
scheduler_nmatches_quickfix
Open

Inform schedulers with correct number of matches.#259
gkronber wants to merge 1 commit intoale/3.0from
scheduler_nmatches_quickfix

Conversation

@gkronber
Copy link
Collaborator

@gkronber gkronber commented Jan 23, 2025 •
edited
Loading

This PR fixes a bug where the schedulers are informed with the accumulated number of matches over all rules, instead of the number of matches for each individual rule. As a consequence of the bug, the BackoffScheduler deactivated all rules simulataneuously, instead of deactivating only the rules that produce a large number of matches.

As a consequence of the bugfix, the BackoffScheduler now starts to deactivate individual rules later (as intended!), which leads to more matches for the benchmarks and longer runtimes.

A larger change has been tested in #249, but that would require a complete overhaul of the scheduler interface.

@codecov-commenter
Copy link

codecov-commenter commented Jan 23, 2025 •
edited
Loading

⚠️ Please install the 'codecov app svg image' to ensure uploads and comments are reliably processed by Codecov.

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 81.44%. Comparing base (b960db9) to head (521318f).

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

Additional details and impacted files 
@@             Coverage Diff             @@
##           ale/3.0     #259      +/-   ##
===========================================
+ Coverage    81.42%   81.44%   +0.01%     
===========================================
  Files           19       19              
  Lines         1497     1498       +1     
===========================================
+ Hits          1219     1220       +1     
  Misses         278      278

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@github-actions
Copy link

github-actions bot commented Jan 23, 2025

Benchmark Results

egg-sym egg-cust MT@521318ff9d5... MT@b960db95f36... egg-sym/MT@521... egg-cust/MT@52... MT@b960db95f36...
egraph_addexpr 1.45 ms 5.09 ms 4.98 ms 0.285 0.979
basic_maths_simpl2 13.8 ms 5.26 ms 23.3 ms 19.4 ms 0.589 0.225 0.83
prop_logic_freges_theorem 2.55 ms 1.55 ms 1.06 ms 1.05 ms 2.39 1.46 0.989
calc_logic_demorgan 61.1 μs 35.1 μs 77.3 μs 75.7 μs 0.79 0.453 0.979
calc_logic_freges_theorem 22.1 ms 11.6 ms 41.6 ms 41 ms 0.531 0.278 0.987
basic_maths_simpl1 6.39 ms 2.88 ms 51.8 ms 4.61 ms 0.123 0.0555 0.089
egraph_constructor 0.0855 μs 0.0955 μs 0.0963 μs 0.895 1.01
prop_logic_prove1 35.7 ms 13.3 ms 142 ms 41.3 ms 0.252 0.094 0.291
prop_logic_demorgan 81.4 μs 44.8 μs 93.7 μs 94 μs 0.869 0.478 1
while_superinterpreter_while_10 18.1 ms 18 ms 0.995
prop_logic_rewrite 112 μs 112 μs 1.01
time_to_load 119 ms 119 ms 1

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

@gkronber
Copy link
Collaborator Author

gkronber commented Feb 16, 2025

@0x0f0f0f it would be great if you could merge this fix, as it affects the unit tests and benchmarks.

@0x0f0f0f
Copy link
Member

0x0f0f0f commented Feb 17, 2025

@0x0f0f0f it would be great if you could merge this fix, as it affects the unit tests and benchmarks.

Sure, I wanted to take a look at why there was such a big performance drop only on some benchmarks. That may highlight another issue, but since the larger MR also had this performance drop, I doubt it may be the schedulers interface.

What do you think it could be? (other than rules being fired more times) @gkronber

@gkronber
Copy link
Collaborator Author

gkronber commented Feb 17, 2025 •
edited
Loading

What do you think it could be? (other than rules being fired more times)

It really is exactly this. The idea of the BackoffScheduler is to block rules that produce too many matches. Currently, without the fix, the BackoffScheduler instead blocks all rules after a certain number of iterations for ban_length iterations. As a consequence, the iterations are just incremented until the timeout is reached without any matches. The effect is similar as just setting a smaller timeout. Which also means that the current benchmark results are not comparable to egg.

After the fix, BackoffScheduler bans only the rules producing too many matches and allows other rules. This leads to a larger egraph and therefore longer runtimes.

It affects only the benchmarks where the banning logic of BackoffScheduler is triggered.

The basic_maths_simple benchmark is strongly affected. Here is the output for ale/3.0. From iteration 6 onwards, all rules are banned and nothing happens until the timeout.

julia> include("benchmark/benchmarks.jl")
Precompiling Metatheory...
  1 dependency successfully precompiled in 3 seconds. 28 already precompiled.
Benchmark(evals=1, seconds=5.0, samples=10000)

julia> simpl1_math = :(a + b + (0 * c) + d)
:(a + b + 0c + d)

julia> with_logger(ConsoleLogger(Debug)) do
       simplify(
         simpl1_math,
         maths_theory,
         (SaturationParams(; timer = false)),
         postprocess_maths,
       )
       end
┌ Debug: ================ EQSAT ITERATION 1  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
┌ Debug: EGraph{Expr, Nothing} with 9 e-classes:
│   1 => [a]
│   2 => [b]
│   3 => [%1 + %2]
│   4 => [0]
│   5 => [c]
│   6 => [%4 * %5]
│   7 => [%3 + %6]
│   8 => [d]
│   9 => [%7 + %8]
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:335
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: Rule 1: ~a * ~b --> ~b * ~a produced 1 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 5: ~a + ~b --> ~b + ~a produced 3 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 6: (~a + ~b) + ~c --> ~a + (~b + ~c) produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 11: 0 * ~a --> 0 produced 1 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: REBUILT
│   n_unions = 0
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + (0 + d))
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: ================ EQSAT ITERATION 2  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
...
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: Rule 1: ~a * ~b --> ~b * ~a produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 2: (~a * ~b) * ~c --> ~a * (~b * ~c) produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 3: ~a * (~b * ~c) --> (~a * ~b) * ~c produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 5: ~a + ~b --> ~b + ~a produced 10 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 6: (~a + ~b) + ~c --> ~a + (~b + ~c) produced 7 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 7: ~a + (~b + ~c) --> (~a + ~b) + ~c produced 7 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 8: 0 + ~a --> ~a produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 11: 0 * ~a --> 0 produced 1 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 12: ~a * 0 --> 0 produced 1 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: REBUILT
│   n_unions = 2
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + d)
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: ================ EQSAT ITERATION 3  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
...
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: Rule 1: ~a * ~b --> ~b * ~a produced 5 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 2: (~a * ~b) * ~c --> ~a * (~b * ~c) produced 9 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 3: ~a * (~b * ~c) --> (~a * ~b) * ~c produced 9 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 5: ~a + ~b --> ~b + ~a produced 26 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 6: (~a + ~b) + ~c --> ~a + (~b + ~c) produced 36 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 7: ~a + (~b + ~c) --> (~a + ~b) + ~c produced 42 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 8: 0 + ~a --> ~a produced 5 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 11: 0 * ~a --> 0 produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 12: ~a * 0 --> 0 produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: REBUILT
│   n_unions = 5
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + d)
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: ================ EQSAT ITERATION 4  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
...
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: Rule 1: ~a * ~b --> ~b * ~a produced 14 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 2: (~a * ~b) * ~c --> ~a * (~b * ~c) produced 56 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 3: ~a * (~b * ~c) --> (~a * ~b) * ~c produced 56 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 5: ~a + ~b --> ~b + ~a produced 33 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 6: (~a + ~b) + ~c --> ~a + (~b + ~c) produced 93 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 7: ~a + (~b + ~c) --> (~a + ~b) + ~c produced 93 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 8: 0 + ~a --> ~a produced 8 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 11: 0 * ~a --> 0 produced 5 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 12: ~a * 0 --> 0 produced 5 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 13: ~a * (~b + ~c) == ~a * ~b + ~a * ~c produced 30 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 14: ~a + ~b * ~a --> (~b + 1) * ~a produced 5 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: REBUILT
│   n_unions = 3
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + d)
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: ================ EQSAT ITERATION 5  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
...
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: Rule 1: ~a * ~b --> ~b * ~a produced 64 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 2: (~a * ~b) * ~c --> ~a * (~b * ~c) produced 1480 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 3: ~a * (~b * ~c) --> (~a * ~b) * ~c produced 904 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 5: ~a + ~b --> ~b + ~a produced 47 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 6: (~a + ~b) + ~c --> ~a + (~b + ~c) produced 64 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 7: ~a + (~b + ~c) --> (~a + ~b) + ~c produced 64 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 8: 0 + ~a --> ~a produced 8 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 11: 0 * ~a --> 0 produced 30 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 12: ~a * 0 --> 0 produced 18 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 13: ~a * (~b + ~c) == ~a * ~b + ~a * ~c produced 966 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 14: ~a + ~b * ~a --> (~b + 1) * ~a produced 24 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: REBUILT
│   n_unions = 352
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + d)
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: ================ EQSAT ITERATION 6  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
...
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: Rule 1: ~a * ~b --> ~b * ~a produced 1160 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: (~a * ~b) * ~c --> ~a * (~b * ~c) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a * (~b * ~c) --> (~a * ~b) * ~c is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 1 * ~a --> ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a + ~b --> ~b + ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~a + ~b) + ~c --> ~a + (~b + ~c) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a + (~b + ~c) --> (~a + ~b) + ~c is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 0 + ~a --> ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a - ~a --> 0 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a + -(~b) --> ~a - ~b is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 0 * ~a --> 0 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a * 0 --> 0 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a * (~b + ~c) == ~a * ~b + ~a * ~c is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a + ~b * ~a --> (~b + 1) * ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~y) ^ ~n * ~y --> (~y) ^ (~n + 1) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~x) ^ ~n * (~x) ^ ~m == (~x) ^ (~n + ~m) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~x * ~y) ^ ~z == (~x) ^ ~z * (~y) ^ ~z is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ((~x) ^ ~p) ^ ~q == (~x) ^ (~p * ~q) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~x) ^ 0 --> 1 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 0 ^ ~x --> 0 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 1 ^ ~x --> 1 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~x) ^ 1 --> ~x is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: inv(~x) == (~x) ^ -1 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: REBUILT
│   n_unions = 0
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + d)
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: ================ EQSAT ITERATION 7  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
...
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: ~a * ~b --> ~b * ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~a * ~b) * ~c --> ~a * (~b * ~c) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a * (~b * ~c) --> (~a * ~b) * ~c is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 1 * ~a --> ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a + ~b --> ~b + ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~a + ~b) + ~c --> ~a + (~b + ~c) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a + (~b + ~c) --> (~a + ~b) + ~c is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 0 + ~a --> ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a - ~a --> 0 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a + -(~b) --> ~a - ~b is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 0 * ~a --> 0 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a * 0 --> 0 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a * (~b + ~c) == ~a * ~b + ~a * ~c is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a + ~b * ~a --> (~b + 1) * ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~y) ^ ~n * ~y --> (~y) ^ (~n + 1) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~x) ^ ~n * (~x) ^ ~m == (~x) ^ (~n + ~m) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~x * ~y) ^ ~z == (~x) ^ ~z * (~y) ^ ~z is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ((~x) ^ ~p) ^ ~q == (~x) ^ (~p * ~q) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~x) ^ 0 --> 1 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 0 ^ ~x --> 0 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 1 ^ ~x --> 1 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~x) ^ 1 --> ~x is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: inv(~x) == (~x) ^ -1 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: REBUILT
│   n_unions = 0
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + d)
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: ================ EQSAT ITERATION 8  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
...
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: ~a * ~b --> ~b * ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~a * ~b) * ~c --> ~a * (~b * ~c) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a * (~b * ~c) --> (~a * ~b) * ~c is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 1 * ~a --> ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a + ~b --> ~b + ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~a + ~b) + ~c --> ~a + (~b + ~c) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a + (~b + ~c) --> (~a + ~b) + ~c is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 0 + ~a --> ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a - ~a --> 0 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a + -(~b) --> ~a - ~b is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 0 * ~a --> 0 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a * 0 --> 0 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a * (~b + ~c) == ~a * ~b + ~a * ~c is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ~a + ~b * ~a --> (~b + 1) * ~a is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~y) ^ ~n * ~y --> (~y) ^ (~n + 1) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~x) ^ ~n * (~x) ^ ~m == (~x) ^ (~n + ~m) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~x * ~y) ^ ~z == (~x) ^ ~z * (~y) ^ ~z is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: ((~x) ^ ~p) ^ ~q == (~x) ^ (~p * ~q) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~x) ^ 0 --> 1 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 0 ^ ~x --> 0 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: 1 ^ ~x --> 1 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: (~x) ^ 1 --> ~x is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: inv(~x) == (~x) ^ -1 is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: REBUILT
│   n_unions = 0
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + d)
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: Too many iterations
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:359
:(a + b + d)

Here is the same output after the fix. In iteration 6 one rule produces over 100000 new enodes because only a single rule is banned. This is the intended behaviour of the BackoffScheduler. This also highlights again, why it is useful to have a match limit in the ematcher as we do not need to produce all matches when we already know that we are going to ban a rule. This will improve the performance again. I planned to reopen a separate PR for the match limit, but we can also do it in this PR if you perfer.

┌ Debug: ================ EQSAT ITERATION 1  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
┌ Debug: EGraph{Expr, Nothing} with 9 e-classes:
│   1 => [a]
│   2 => [b]
│   3 => [%1 + %2]
│   4 => [0]
│   5 => [c]
│   6 => [%4 * %5]
│   7 => [%3 + %6]
│   8 => [d]
│   9 => [%7 + %8]
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:335
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: Rule 1: ~a * ~b --> ~b * ~a produced 1 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 5: ~a + ~b --> ~b + ~a produced 3 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 6: (~a + ~b) + ~c --> ~a + (~b + ~c) produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 11: 0 * ~a --> 0 produced 1 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: REBUILT
│   n_unions = 0
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + (0 + d))
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: ================ EQSAT ITERATION 2  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
...
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: Rule 1: ~a * ~b --> ~b * ~a produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 2: (~a * ~b) * ~c --> ~a * (~b * ~c) produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 3: ~a * (~b * ~c) --> (~a * ~b) * ~c produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 5: ~a + ~b --> ~b + ~a produced 10 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 6: (~a + ~b) + ~c --> ~a + (~b + ~c) produced 7 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 7: ~a + (~b + ~c) --> (~a + ~b) + ~c produced 7 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 8: 0 + ~a --> ~a produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 11: 0 * ~a --> 0 produced 1 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 12: ~a * 0 --> 0 produced 1 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: REBUILT
│   n_unions = 2
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + d)
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: ================ EQSAT ITERATION 3  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
...
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: Rule 1: ~a * ~b --> ~b * ~a produced 5 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 2: (~a * ~b) * ~c --> ~a * (~b * ~c) produced 9 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 3: ~a * (~b * ~c) --> (~a * ~b) * ~c produced 9 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 5: ~a + ~b --> ~b + ~a produced 26 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 6: (~a + ~b) + ~c --> ~a + (~b + ~c) produced 36 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 7: ~a + (~b + ~c) --> (~a + ~b) + ~c produced 42 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 8: 0 + ~a --> ~a produced 5 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 11: 0 * ~a --> 0 produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 12: ~a * 0 --> 0 produced 2 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: REBUILT
│   n_unions = 5
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + d)
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: ================ EQSAT ITERATION 4  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
...
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: Rule 1: ~a * ~b --> ~b * ~a produced 14 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 2: (~a * ~b) * ~c --> ~a * (~b * ~c) produced 56 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 3: ~a * (~b * ~c) --> (~a * ~b) * ~c produced 56 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 5: ~a + ~b --> ~b + ~a produced 33 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 6: (~a + ~b) + ~c --> ~a + (~b + ~c) produced 93 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 7: ~a + (~b + ~c) --> (~a + ~b) + ~c produced 93 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 8: 0 + ~a --> ~a produced 8 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 11: 0 * ~a --> 0 produced 5 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 12: ~a * 0 --> 0 produced 5 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 13: ~a * (~b + ~c) == ~a * ~b + ~a * ~c produced 30 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 14: ~a + ~b * ~a --> (~b + 1) * ~a produced 5 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: REBUILT
│   n_unions = 3
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + d)
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: ================ EQSAT ITERATION 5  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
...
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: Rule 1: ~a * ~b --> ~b * ~a produced 64 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 2: (~a * ~b) * ~c --> ~a * (~b * ~c) produced 1480 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 3: ~a * (~b * ~c) --> (~a * ~b) * ~c produced 904 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 5: ~a + ~b --> ~b + ~a produced 47 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 6: (~a + ~b) + ~c --> ~a + (~b + ~c) produced 64 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 7: ~a + (~b + ~c) --> (~a + ~b) + ~c produced 64 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 8: 0 + ~a --> ~a produced 8 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 11: 0 * ~a --> 0 produced 30 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 12: ~a * 0 --> 0 produced 18 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 13: ~a * (~b + ~c) == ~a * ~b + ~a * ~c produced 966 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 14: ~a + ~b * ~a --> (~b + 1) * ~a produced 24 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: REBUILT
│   n_unions = 352
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + d)
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: ================ EQSAT ITERATION 6  ================
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:334
...
┌ Debug: SEARCHING
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:79
┌ Debug: Rule 1: ~a * ~b --> ~b * ~a produced 1160 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: (~a * ~b) * ~c --> ~a * (~b * ~c) is banned
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:86
┌ Debug: Rule 3: ~a * (~b * ~c) --> (~a * ~b) * ~c produced 107074 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 5: ~a + ~b --> ~b + ~a produced 367 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 6: (~a + ~b) + ~c --> ~a + (~b + ~c) produced 360 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 7: ~a + (~b + ~c) --> (~a + ~b) + ~c produced 352 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 8: 0 + ~a --> ~a produced 8 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 11: 0 * ~a --> 0 produced 616 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 12: ~a * 0 --> 0 produced 140 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 13: ~a * (~b + ~c) == ~a * ~b + ~a * ~c produced 380782 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Rule 14: ~a + ~b * ~a --> (~b + 1) * ~a produced 184 matches
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:106
┌ Debug: Too many enodes
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:260
┌ Debug: REBUILT
│   n_unions = 0
│   trimmed_nodes = nothing
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:571
┌ Debug: Smallest expression is
│   extract!(g, astsize) = :((a + b) + d)
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:309
┌ Debug: Reason
│   report.reason = :enodelimit
└ @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:348
:(a + b + d)

@0x0f0f0f
Copy link
Member

0x0f0f0f commented Feb 17, 2025

@gkronber

This is the intended behaviour of the BackoffScheduler. This also highlights again, why it is useful to have a match limit in the ematcher as we do not need to produce all matches when we already know that we are going to ban a rule.

Does this happen in egg? Can't recall

@gkronber
Copy link
Collaborator Author

gkronber commented Feb 17, 2025

@gkronber

This is the intended behaviour of the BackoffScheduler. This also highlights again, why it is useful to have a match limit in the ematcher as we do not need to produce all matches when we already know that we are going to ban a rule.

Does this happen in egg? Can't recall

Yes, the changes in #249 are based on the egg code.

@0x0f0f0f
Copy link
Member

0x0f0f0f commented Feb 17, 2025

@gkronber considering the above logs, do you have an egg reference to compare how it behaves on similar rulesets and input expressions?

@0x0f0f0f
Copy link
Member

0x0f0f0f commented Feb 17, 2025

I planned to reopen a separate PR for the match limit, but we can also do it in this PR if you perfer.

@gkronber yes please, I would also triple check that the hyperparameters are equal (or comparable) to egg's in those benchmarks

@gkronber
Copy link
Collaborator Author

gkronber commented Feb 17, 2025

I planned to reopen a separate PR for the match limit, but we can also do it in this PR if you perfer.

@gkronber yes please, I would also triple check that the hyperparameters are equal (or comparable) to egg's in those benchmarks

Yes, I can triple-check the hyperparameters and we can update the benchmark script to report the size of the egraph as well as the runtime to make sure that the behavior is similar.

@gkronber
Copy link
Collaborator Author

gkronber commented Feb 17, 2025

@gkronber considering the above logs, do you have an egg reference to compare how it behaves on similar rulesets and input expressions?

I don't have the logs currently.

@0x0f0f0f
Copy link
Member

0x0f0f0f commented Feb 17, 2025

Yes, I can triple-check the hyperparameters and we can update the benchmark script to report the size of the egraph as well as the runtime to make sure that the behavior is similar.

Yes please

@gkronber
Copy link
Collaborator Author

gkronber commented Feb 18, 2025

Prepared PR #265 to report the egraph sizes for egg and MT for the benchmarks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@gkronber @codecov-commenter @0x0f0f0f

Comments