Open oflatt opened 5 months ago
I have a simple solution: let's just allow a single root per benchmark. If you want to benchmark something with multiple roots, just create multiple benchmarks
Perhaps there's a more general problem with cycles and DAG extractors- if you allow them to extract a particular term, the problem goes away. However, if they must pick a single term per eclass cycles can occur
Some extractors are non-local: for different root eclasses, they extract different sub-terms for the same eclass. However, the current extraction gym does not allow picking two different nodes for the same eclass.
As a result, the
global_greedy_dag
extractor sometimes extracts cycles because it chooses conflicting nodes when extracting different roots.