search

egraphs-good / extraction-gym

benchmarking e-graph extraction
MIT License
24 stars 15 forks source link

More tests & better checking of extraction results. #26

Closed TrevorHansen closed 6 months ago

TrevorHansen commented 6 months ago

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.

oflatt commented 6 months ago

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

TrevorHansen commented 6 months ago

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 commented 6 months ago

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