Skip to content

Matching- skip eclasses that do not contain eclass with operator#21

Merged
mwillsey merged 4 commits intoegraphs-good:masterfrom
4e554c4c:skip-eclasses
Apr 16, 2020
Merged

Matching- skip eclasses that do not contain eclass with operator#21
mwillsey merged 4 commits intoegraphs-good:masterfrom
4e554c4c:skip-eclasses

Conversation

@oflatt
Copy link
Copy Markdown
Member

@oflatt oflatt commented Apr 16, 2020

This PR adds a hash table from the "signature" of the top level of a rule, which is the operator and the number of children, to eclasses that contain that signature at least once. For a given rule, it allows us to skip over eclasses that could not contain any matches for the rule because they do not contain an enode of the correct signature.

Timing with the rules from Herbie, this leads to a 3X speedup in searching (1.5X overall speedup) regardless of the node limit.
@mwillsey , could you please run whatever benchmarking you usually do on this PR and see what you find?

Copy link
Copy Markdown
Member

@mwillsey mwillsey left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks promising, but it's failing tests. (It's also not formatted, so will fail on that front too). Could be even faster with changes mentioned in the review!

@mwillsey
Copy link
Copy Markdown
Member

My benchmarks:

master

benching diff_power_harder for 10 seconds...
bench    diff_power_harder:
  n = 11
  μ = 0.9918599499999999
  σ = 0.07366492475522622
Runner report
=============
  Stop reason: IterationLimit(50)
  Iterations: 50
  Rebuilds: 291633, 5832.66 per iter
  Total time: 0.9674673519999998
    Search:  (0.39) 0.374357273
    Apply:   (0.09) 0.09078622899999998
    Rebuild: (0.52) 0.502241622

this pr

benching diff_power_harder for 10 seconds...
bench    diff_power_harder:
  n = 13
  μ = 0.8230608773846154
  σ = 0.015520025769429393
Runner report
=============
  Stop reason: IterationLimit(50)
  Iterations: 50
  Rebuilds: 304051, 6081.02 per iter
  Total time: 0.817320584
    Search:  (0.25) 0.20449594200000004
    Apply:   (0.11) 0.08975624199999997
    Rebuild: (0.64) 0.523041465

@mwillsey mwillsey merged commit db8b568 into egraphs-good:master Apr 16, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants