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

More tests & better checking of extraction results. #26

Merged
merged 4 commits into from
Dec 28, 2023

Conversation

TrevorHansen
Copy link
Contributor

In creating the nicer ILP extractor (#16) I've had lots of annoying rare errors that have been hard to pin down. So I've made a fuzzer that randomly generates egraphs, then I run different extractors on those random egraphs.

Because the ILP extractors (ilp-cbc & faster-ilp-cbc) are optimal for DAG-extraction, the DAG-extractions from the other extractiors should never be cheaper on a given egraph. The effect of all this is that the extractors get tested on tens of millions of egraphs. It's found lots of problems with the extractors.

That's the back story.

Anyway, this PR contains some egraph that the fuzzer has generated, some that I've handcrafted to check extreme cases and better testing of extraction results.

These extra tests reveal problems with the faster-greedy-dag & global-greedy-dag extractors. Both of which fail on some instances.

The faster-greedy-dag returns extractions with cycles and the global-greedy-dag sometimes returns extractions with the wrong nodes selected (i.e. a node will be selected for the wrong class). I'll create cases for these.

Copy link
Member

@oflatt oflatt left a comment

Choose a reason for hiding this comment

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

Looks like a great change to me!

@@ -78,11 +78,9 @@ fn main() {

let start_time = std::time::Instant::now();
let result = extractor.extract(&egraph, &egraph.root_eclasses);
result.check(&egraph);
Copy link
Member

Choose a reason for hiding this comment

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

should this check happen after we measure the time? (line 83)

@oflatt
Copy link
Member

oflatt commented Dec 27, 2023

Does this PR contain the cases where global-greedy-dag fails, or not?

@TrevorHansen
Copy link
Contributor Author

TrevorHansen commented Dec 27, 2023

Does this PR contain the cases where global-greedy-dag fails, or not?

Yes, the global-greedy-dag extractor fails, in that it chooses nodes from the wrong class, on some of the egraphs in this PR.

target/release/extraction-gym data/fuzz/5.json --extractor=global-greedy-dag --out=output/fuzz/5.json-global-greedy-dag.json
iteration 1
iteration 2
thread 'main' panicked at 'assertion failed: node.eclass == *cid', src/extract/mod.rs:84:13
``

@oflatt
Copy link
Member

oflatt commented Dec 28, 2023

Oh, we should change the CI so that it actually runs all the extractors then. After we fix the bugs!

@oflatt oflatt merged commit a42b0f0 into egraphs-good:main Dec 28, 2023
2 checks passed
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