Fix hashing and memoization of enodes (VecExpr)

[gkronber-machine]

This new PR fixes an issue with memoization of enodes, whereby enodes in the memo dictionary are updated, invalidating their hash value. Additional fixes and improvements:

• Fix the check_memo() function to actually check memo
• Fix the implementation of Base.hash for VecExpr
• Improve efficiency of dictionary lookups by using get() / get!()

(related PR: #238 has additional changes to remove caching of hash values for VecExpr)

[codecov-commenter]

:warning: Please install the to ensure uploads and comments are reliably processed by Codecov.

Codecov Report

All modified and coverable lines are covered by tests :white_check_mark:

Project coverage is 81.06%. Comparing base (1dc53da) to head (66ea780).

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

Additional details and impacted files

@@             Coverage Diff             @@
##           ale/3.0     #239      +/-   ##
===========================================
+ Coverage    80.78%   81.06%   +0.28%     
===========================================
  Files           19       19              
  Lines         1504     1500       -4     
===========================================
+ Hits          1215     1216       +1     
+ Misses         289      284       -5     

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

[0x0f0f0f]

@gkronber it it provides a substantial speedup, we could move the UniqueQueue to another PR and merge it when Julia 1.11 is released, setting the min version of Julia to it.

[gkronber]

@gkronber it it provides a substantial speedup, we could move the UniqueQueue to another PR and merge it when Julia 1.11 is released, setting the min version of Julia to it.

In local benchmarks it shows almost no difference.

[0x0f0f0f]

@gkronber it it provides a substantial speedup, we could move the UniqueQueue to another PR and merge it when Julia 1.11 is released, setting the min version of Julia to it.

In local benchmarks it shows almost no difference.

Could you post it here please?

[0x0f0f0f]

@gkronber it it provides a substantial speedup, we could move the UniqueQueue to another PR and merge it when Julia 1.11 is released, setting the min version of Julia to it.

In local benchmarks it shows almost no difference.

Could you post it here please?

(@gkronber I mean this branch against ale/3.0)

[gkronber]

Local benchmark results (66ea780):

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

julia> run(SUITE)
5-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "prop_logic" => 4-element BenchmarkTools.BenchmarkGroup:
          tags: ["egraph", "logic"]
          "freges_theorem" => Trial(1.101 ms)
          "prove1" => Trial(39.136 ms)
          "demorgan" => Trial(96.700 μs)
          "rewrite" => Trial(113.200 μs)
  "basic_maths" => 2-element BenchmarkTools.BenchmarkGroup:
          tags: ["egraphs"]
          "simpl2" => Trial(20.215 ms)
          "simpl1" => Trial(4.877 ms)
  "while_superinterpreter" => 1-element BenchmarkTools.BenchmarkGroup:
          tags: ["egraph"]
          "while_10" => Trial(18.184 ms)
  "egraph" => 2-element BenchmarkTools.BenchmarkGroup:
          tags: ["egraphs"]
          "addexpr" => Trial(5.435 ms)
          "constructor" => Trial(500.000 ns)
  "calc_logic" => 2-element BenchmarkTools.BenchmarkGroup:
          tags: ["egraph", "logic"]
          "freges_theorem" => Trial(38.887 ms)
          "demorgan" => Trial(79.000 μs)

ale/3.0 branch (1dc53daf4c9532811a8db210179b7070f6da2abe):

1 dependency successfully precompiled in 2 seconds. 6 already precompiled.
Benchmark(evals=1, seconds=5.0, samples=10000)

julia> run(SUITE)
5-element BenchmarkTools.BenchmarkGroup:
  tags: []
  "prop_logic" => 4-element BenchmarkTools.BenchmarkGroup:
          tags: ["egraph", "logic"]
          "freges_theorem" => Trial(1.070 ms)
          "prove1" => Trial(35.801 ms)
          "demorgan" => Trial(97.100 μs)
          "rewrite" => Trial(115.000 μs)
  "basic_maths" => 2-element BenchmarkTools.BenchmarkGroup:
          tags: ["egraphs"]
          "simpl2" => Trial(18.172 ms)
          "simpl1" => Trial(4.460 ms)
  "while_superinterpreter" => 1-element BenchmarkTools.BenchmarkGroup:
          tags: ["egraph"]
          "while_10" => Trial(18.715 ms)
  "egraph" => 2-element BenchmarkTools.BenchmarkGroup:
          tags: ["egraphs"]
          "addexpr" => Trial(5.079 ms)
          "constructor" => Trial(500.000 ns)
  "calc_logic" => 2-element BenchmarkTools.BenchmarkGroup:
          tags: ["egraph", "logic"]
          "freges_theorem" => Trial(35.986 ms)
          "demorgan" => Trial(75.800 μs)

[0x0f0f0f]

Amazing. Thank you @gkronber - Merging when you mark this as ready :+1:

[gkronber]

I have a few more changes that I would like to sneak into this PR. They are only tangentially related. @0x0f0f0f, can I add the changes here or should I create a new PR for those?

[0x0f0f0f]

I have a few more changes that I would like to sneak into this PR. They are only tangentially related. @0x0f0f0f, can I add the changes here or should I create a new PR for those?

Another MR would be better, let's merge this one first

[gkronber]

I saw that the MT code deviates from most recent egg code slightly since the changes from https://github.com/egraphs-good/egg/pull/291 which is partially related to this PR and mentions There are also memory usage/performance advantages since EClass.parents, EGraph.pending, and EGraph.analysis_pending, no longer need to store nodes.

It should be straight-forward to make the corresponding changes to MT, I'd be happy to prepare a PR for this. @0x0f0f0f, is there some work in this direction already ?

[0x0f0f0f]

I saw that the MT code deviates from most recent egg code slightly since the changes from egraphs-good/egg#291 which is partially related to this PR and mentions There are also memory usage/performance advantages since EClass.parents, EGraph.pending, and EGraph.analysis_pending, no longer need to store nodes.

It should be straight-forward to make the corresponding changes to MT, I'd be happy to prepare a PR for this. @0x0f0f0f, is there some work in this direction already ?

Some stuff was done in #223 ! But interesting PR, I'll check it out. Let's merge this one first

[0x0f0f0f]

@gkronber I gave you maintainer write access, you should now be able to push to branches of this repository, so that benchmarks will run automatically on your PRs, if you open them from branches of this repo (and not from forks)

:)

[gkronber]

Great, that should simplify things.