Detect causes of slowdowns in equality saturation. Improve Schedulers and performance.

[0x0f0f0f]

See the last lines of https://github.com/0x0f0f0f/Metatheory.jl/blob/master/test/test_logic.jl
After a certain number of iterations, the equality saturation process slows down terribly even if the BackoffScheduler heuristic is applied.
To prove the Constructive Dilemma (:(((p => q) ∧ (r => s) ∧ (p ∨ r)) => (q ∨ s))) in the logic test example, it takes two equality saturation processes with 10 and 5 iterations each (saturate => extract => saturate => extract), instead of a single step with 15 iterations (which is too memory intensive, or too slow).

[0x0f0f0f]

A slowdown could be caused by the ematcher iterating through ALL eclasses in the egraph in every match trial.
An optimization could be keeping a Dict{Any, Vector{Int64}} telling us in which eclasses the given function symbol (does ariety matter?) appears.

[0x0f0f0f]

This optimization was done.

[0x0f0f0f]

Got a greate speedup close to 2x and halved memory usage. Still not close to egg.

[0x0f0f0f]

@MrVPlusOne could you help out with this issue? Your PRs were really useful

[MrVPlusOne]

I can certainly try to work on this later (although I'm not familiar with the e-match algorithm myself and will have to learn more details), but currently, I will have to prioritize debugging the rulesets I was using, and maybe starting by implementing some infrastructure on producing rewrite proofs?

[0x0f0f0f]

The ematch algorithm is detailed here. https://leodemoura.github.io/files/ematching.pdf
I mostly based my implementation from egg. I was thinking today that instead of a virtual machine or staging through metaprogramming the ematcher could be built from closures. The SymbolicUtils.jl pattern matcher builds on closures and is very fast and elegant https://github.com/JuliaSymbolics/SymbolicUtils.jl/blob/master/src/matchers.jl

[0x0f0f0f]

For proofs https://www.cs.upc.edu/~oliveras/espai/papers/rta05.pdf

[0x0f0f0f]

For the ematch thing, I have a branch https://github.com/0x0f0f0f/Metatheory.jl/tree/staged_ematch where I implement @philzook58 staged ematcher http://www.philipzucker.com/staging-patterns/

[MrVPlusOne]

Sounds good. I'll probably only be able to work on MT this weekend since I have a few other deadlines this week.

I was thinking today that instead of a virtual machine or staging through metaprogramming the ematcher could be built from closures. The SymbolicUtils.jl pattern matcher builds on closures and is very fast and elegant https://github.com/JuliaSymbolics/SymbolicUtils.jl/blob/master/src/matchers.jl

Not having to deal with a low-level virtual machine sounds nice to me, as I find the current implementation quite hard to understand from just reading the code. Does the optimization that caches matched e-class depend on what type of e-graph implementation was used? I noticed that you mentioned earlier in this issue that this caching optimization was done, but why is it disabled now?

[0x0f0f0f]

Got some improvements by splitting ENode into ENodeTerm and ENodeLiteral. Got also some improvements by avoiding storing the matched e-nodes if not strictly needed, only storing ids.

[0x0f0f0f]

#177 has decent performance