Change implementation of BackoffScheduler to match egg.

[gkronber]

For valid performance comparisons, with egg we should produce egraphs that have comparable sizes to the egraphs produced by egg. Currently, this is not the case because MT has a bug when using BackoffScheduler (informed with incorrect number of matches). Additionally, the implementation of BackoffScheduler is different to egg, leading to different egraph sizes (for the same rules, and saturation timeout).

egg allows to limit the number of matches in the ematcher to the threshold calculated from the BackoffScheduler which has additional performance advantages.

Fixes #248.

[codecov-commenter]

⚠️ Please install the to ensure uploads and comments are reliably processed by Codecov.

Codecov Report

Attention: Patch coverage is 77.65957% with 21 lines in your changes missing coverage. Please review.

Project coverage is 80.26%. Comparing base (081a9e6) to head (bfe573e).
Report is 2 commits behind head on ale/3.0.

Files with missing lines	Patch %	Lines
src/EGraphs/Schedulers.jl	70.83%	21 Missing ⚠️

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

Additional details and impacted files

@@             Coverage Diff             @@
##           ale/3.0     #249      +/-   ##
===========================================
- Coverage    81.17%   80.26%   -0.92%     
===========================================
  Files           19       18       -1     
  Lines         1503     1535      +32     
===========================================
+ Hits          1220     1232      +12     
- Misses         283      303      +20     

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

[gkronber]

For bidirectional rules, the LHS and RHS may both match the same eclass. In this case inform! would be called twice for the same rule index and the same eclass in the same iteration. None of the implemented schedulers uses this, but it could be unexpected for people implementing their own scheduler.

[github-actions]

Benchmark Results

	egg-sym	egg-cust	MT@48578d8a3bd...	MT@6814104fbe1...	egg-sym/MT@485...	egg-cust/MT@48...	MT@6814104fbe1...
egraph_addexpr	1.45 ms		5.15 ms	5.14 ms	0.282		0.998
basic_maths_simpl2	13.7 ms	5.2 ms	14.1 ms	20.6 ms	0.973	0.369	1.46
prop_logic_freges_theorem	2.52 ms	1.55 ms	1.22 ms	1.05 ms	2.06	1.27	0.856
calc_logic_demorgan	59.9 μs	34.4 μs	87.7 μs	74.4 μs	0.684	0.392	0.849
calc_logic_freges_theorem	22.6 ms	12 ms	77.7 ms	43.4 ms	0.291	0.155	0.559
basic_maths_simpl1	6.38 ms	2.85 ms	12.1 ms	4.71 ms	0.529	0.237	0.391
egraph_constructor	0.0826 μs		0.0928 μs	0.0956 μs	0.89		1.03
prop_logic_prove1	36.5 ms	14.3 ms	89.1 ms	42.2 ms	0.409	0.16	0.474
prop_logic_demorgan	79.3 μs	45.2 μs	106 μs	92.2 μs	0.751	0.428	0.874
while_superinterpreter_while_10			18.6 ms	18.3 ms			0.985
prop_logic_rewrite			120 μs	122 μs			1.02
time_to_load			119 ms	116 ms			0.979

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]

Explanation for the longer runtimes in the benchmark: before the fix the BackoffScheduler quickly blocked all rules because it was informed with the sum of number of matches over all rules. In the fixed version, the BackoffScheduler blocks rules later (and individually), which leads to larger graph and therefore longer runtime.

We should compare the sizes of the egraphs for all implementations in the benchmark. When the scheduler parameters are the same and the rules are the same then the egraphs (using egg and MT) should be the same after saturation. Otherwise comparing the runtimes is not particularly useful.

I changed the egg-benchmark and MT benchmark script below to produce egraph sizes.

[gkronber]

Further investigation shows that the implementation of BackoffScheduler in MT differs significantly from the implementation in egg.

In egg, the search_rewrite function of schedulers determines how matches for rule are searched https://github.com/egraphs-good/egg/blob/1b2d004f63a01256047154f51568e61317cd4e89/src/run.rs#L935 which gives much more flexibility for scheduling than the implementation in MT, where eqsat_search! communicates with schedulers solely via cansearch and inform! .
An important performance feature is that BackoffScheduler in egg uses the threshold to limit the number of matches in the ematcher.

It is easy to add something similar to MT but requires a change to the interface for AbstractScheduler. I see two options:

• We could change cansearch to a function returning the limit for the number of matches (matchlimit) and leave the structure of searching over eclasses as is. (as in 7dd5848).
• We could implement search_rewrite similarly to egg, which opens up capabilities to implement smarter schedulers. (as in 0fecaa5). I prefer this solution.

[gkronber]

For future reference, egg-benchmark produces the following numbers for egg-sym and the numbers for MT 0fecaa5 are

id	egg_n_classes	egg_n_memo	mt_n_classes	mt_n_memo	note
egraph/addexpr	6771	6771	6650	6650
basic_maths/simpl1	368	2543	635	4351	-
basic_maths/simpl2	440	2836	726	3536	-
calc_logic/demorgan	16	35	12	25	sum over prove steps
calc_logic/freges_theorem	1072	17394	713	14692	sum over prove steps
prop_logic/demorgan	16	42	15	35	sum over prove steps
prop_logic/freges_theorem	316	2315	71	255	sum over prove steps
prop_logic/prove1	7448	35210	1947	16540	sum over prove steps

Differences in the number of eclasses produced by egg and MT to be investigated.

[0x0f0f0f]

@gkronber thanks for all these contributions! 🫶

I will take a look after work

[gkronber]

This PR is a bit messy, because I became aware of an issue in the ematch compiler and the benchmarking code after starting to work on the issue I observed initially.

In the meanwhile I strongly support moving the matching code into the Schedulers (refactoring cansearch, inform). I believe it would be important to fix this and introduce the match limit parameter for the ematchers.

I'm happy to split this PR up into several smaller cleaner PRs if this makes it easier for reviewing.

[gkronber]

Ok, it seems that #252 did not really fix issues with the CAS integration tests. More matches are detected because rules are not disabled all together by the backoffscheduler anymore. The additional matches and unifications mean that the issues in the CAS tests pop up again.

The CAS test has several rules which seem problematic with divison by zero, I suspect that these are the problem. We might need to add semantic analysis to finally fix them. @0x0f0f0f is there source for the CAS tests and rules that we could compare to?
Edit: I found this https://github.com/egraphs-good/egg/blob/main/tests/math.rs which seems similar.