Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 4 commits into from
Apr 16, 2020

Conversation

oflatt
Copy link
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
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!

src/egraph.rs Outdated Show resolved Hide resolved
src/egraph.rs Outdated Show resolved Hide resolved
src/egraph.rs Outdated Show resolved Hide resolved
src/pattern.rs Outdated Show resolved Hide resolved
@mwillsey
Copy link
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