Metatheory.jl
Metatheory.jl copied to clipboard
JuliaSymbolics
Detect causes of slowdowns in equality saturation. Improve Schedulers and performance.
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).
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.
Got a greate speedup close to 2x and halved memory usage. Still not close to egg.
@MrVPlusOne could you help out with this issue? Your PRs were really useful
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?
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
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/
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?
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.