Instruction based ematch compiler

[olynch]

A resurrection of #233 with a local branch so CI can run properly.

[0x0f0f0f]

Nice! Just saw the error about convert-ing to Expr. Maybe we can use to_expr instead of convert?

[olynch]

Nice! Just saw the error about convert-ing to Expr. Maybe we can use to_expr instead of convert?

It was a different problem; I just fixed it though!

[olynch]

Now we have a new problem with lambda_theory again, and the behavior of instantiate_actual_param!. Specifically, it seems like this is returning constants some times when the dynamic matches are expecting eclasses, and vice versa. I looked carefully, and I'm pretty sure that I have the same behavior for enode_idx as previous, but maybe something got borked.

What is the rational between sometimes returning an eclass and sometimes returning a constant? That seems pretty janky.

[codecov-commenter]

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

Codecov Report

Attention: Patch coverage is 93.22034% with 8 lines in your changes missing coverage. Please review.

Project coverage is 78.08%. Comparing base (79c1a7b) to head (914804b).

Files with missing lines	Patch %	Lines
src/ematch_compiler.jl	93.22%	8 Missing ⚠️

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

Additional details and impacted files

@@             Coverage Diff             @@
##           ale/3.0     #241      +/-   ##
===========================================
- Coverage    81.06%   78.08%   -2.99%     
===========================================
  Files           19       19              
  Lines         1500     1524      +24     
===========================================
- Hits          1216     1190      -26     
- Misses         284      334      +50     

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

[github-actions]

Benchmark Results

	egg-sym	egg-cust	MT@914804b0385...	MT@79c1a7b9ae2...	egg-sym/MT@914...	egg-cust/MT@91...	MT@79c1a7b9ae2...
egraph_addexpr	1.43 ms		5.18 ms	5.2 ms	0.277		1
basic_maths_simpl2	13.4 ms	4.88 ms	22.1 ms	20 ms	0.61	0.221	0.908
prop_logic_freges_theorem	2.49 ms	1.54 ms	1.25 ms	1.05 ms	1.98	1.23	0.841
calc_logic_demorgan	60.2 μs	35 μs	81 μs	78 μs	0.743	0.432	0.964
calc_logic_freges_theorem	21.6 ms	12.2 ms	50 ms	41.4 ms	0.433	0.244	0.828
basic_maths_simpl1	5.96 ms	2.76 ms	5.07 ms	4.88 ms	1.18	0.545	0.963
egraph_constructor	0.0854 μs		0.0893 μs	0.0907 μs	0.956		1.02
prop_logic_prove1	34.8 ms	13.2 ms	67.4 ms	41.5 ms	0.516	0.196	0.616
prop_logic_demorgan	79.3 μs	44.7 μs	103 μs	98.2 μs	0.772	0.435	0.956
while_superinterpreter_while_10			19.4 ms	18.4 ms			0.949
prop_logic_rewrite			120 μs	120 μs			1
time_to_load			495 ms	497 ms			1.01

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]

@olynch I've updated the benchmark github CI action to compare against the target branch. This introduced a substantial slowdown, which is OK for a first prototype, but before merging I would make sure that there is no slowdown

[olynch]

@0x0f0f0f are you sure that the slowdown is significant?

Also, I believe that the compilation process could be slightly slower because it now has two stages instead of one. If it turns out to generate the same ematcher, and it's just that the compiler is slightly slower, is that acceptable?

[0x0f0f0f]

type parameter?

[olynch]

What do you mean?

[gkronber]

Now we have a new problem with lambda_theory again, and the behavior of instantiate_actual_param!. Specifically, it seems like this is returning constants some times when the dynamic matches are expecting eclasses, and vice versa. I looked carefully, and I'm pretty sure that I have the same behavior for enode_idx as previous, but maybe something got borked.

What is the rational between sometimes returning an eclass and sometimes returning a constant? That seems pretty janky.

Yes, this is quite tricky and probably leads to bugs that are hard to detect. I believe the problem already exists in ale/3.0 branch because the ematcher assumes that indexes of enodes in eclasses are constant, while they may change when rules are applied (invalidating a match in the ematchbuffer).
I tried 7dd5848 as a fix.

[olynch]

I tried 7dd5848 as a fix.

I left a comment there.