Expose extraction support APIs#934
Conversation
|
@coderabbitai full review |
✅ Action performedFull review finished. |
📝 WalkthroughWalkthroughRefactors the extraction cost model API from a single ChangesIndexed column-matching scan
Extraction cost model and API refactor
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Possibly related PRs
Suggested labels
Suggested reviewers
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
|
@coderabbitai full review |
✅ Action performedFull review finished. |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #934 +/- ##
==========================================
- Coverage 86.85% 86.72% -0.14%
==========================================
Files 91 92 +1
Lines 27290 28731 +1441
==========================================
+ Hits 23703 24917 +1214
- Misses 3587 3814 +227 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@src/extract/dag_extract.rs`:
- Around line 336-342: The hot path in discover_node is cloning the full
constructor list from extractable_funcs_by_output_sort just to drop the borrow
before mutating self. Change the builder/storage type for that map to
Arc<[String]> and convert the lists once in prepare so the lookup at
discover_node can keep using .cloned() but only performs a cheap Arc clone;
verify func_names.iter() still works unchanged in the downstream loop.
In `@src/lib.rs`:
- Around line 1692-1694: The variant-count check in the extraction path
currently panics on a negative value, which can abort the interpreter when a
user-supplied expression evaluates to a bad count. Update the logic in the
extraction routine that handles n so it returns an Error instead of calling
panic, and propagate that error through the surrounding extraction/evaluation
flow so malformed input is reported cleanly without crashing.
In `@src/proofs/proof_extraction.rs`:
- Around line 94-97: The proof-term extraction path in proof_extraction.rs drops
the underlying error by using unwrap_or_else(|_| ...), so the panic message
loses the failure cause. Update the extract_best_for_proofs handling in the
proof extraction logic to bind the error value and include it in the panic
message alongside func.name, so failures from extract_best_for_proofs report the
actual Error details.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: e682c190-3fe6-4637-aca1-44bf610e9938
⛔ Files ignored due to path filters (4)
Cargo.lockis excluded by!**/*.locktests/greedy-dag-taylor.eggis excluded by!**/*.eggtests/greedy-dag-vec-extract.eggis excluded by!**/*.eggtests/snapshots/files__proof_unsupported_files.snapis excluded by!**/*.snap
📒 Files selected for processing (21)
.agents/logs/2026-06-24-greedy-dag-extractor-perf.md.github/workflows/build.ymlCargo.tomlcore-relations/src/free_join/mod.rscore-relations/src/lib.rsegglog-bridge/src/lib.rssrc/ast/desugar.rssrc/ast/mod.rssrc/ast/parse.rssrc/extract.rssrc/extract/dag_extract.rssrc/extract/secondary_map.rssrc/lib.mdsrc/lib.rssrc/prelude.rssrc/proofs/proof_encoding.rssrc/proofs/proof_encoding_helpers.rssrc/proofs/proof_extraction.rssrc/typechecking.rstests/files.rstests/integration_test.rs
📜 Review details
⏰ Context from checks skipped due to timeout. (15)
- GitHub Check: benchmark (ubuntu-latest, greedy-dag-vec-extract)
- GitHub Check: benchmark (ubuntu-latest, taylor51)
- GitHub Check: benchmark (ubuntu-latest, math-microbenchmark)
- GitHub Check: benchmark (ubuntu-latest, greedy-dag-taylor)
- GitHub Check: benchmark (ubuntu-latest, herbie)
- GitHub Check: benchmark (ubuntu-latest, stresstest_large_expr)
- GitHub Check: benchmark (ubuntu-latest, math_normal)
- GitHub Check: benchmark (ubuntu-latest, proof_testing_math)
- GitHub Check: benchmark (ubuntu-latest, proof_testing_eqsat-basic)
- GitHub Check: benchmark (ubuntu-latest, conv1d_128)
- GitHub Check: benchmark (ubuntu-latest, rectangle)
- GitHub Check: benchmark (ubuntu-latest, rust_rule_tableaction_hot_path)
- GitHub Check: benchmark (ubuntu-latest, eggcc-2mm)
- GitHub Check: test
- GitHub Check: coverage
🧰 Additional context used
📓 Path-based instructions (1)
**/*.{md,txt,rs}
📄 CodeRabbit inference engine (CLAUDE.md)
Keep documentation concise and avoid duplicate information
Files:
src/prelude.rssrc/ast/desugar.rscore-relations/src/lib.rssrc/typechecking.rssrc/lib.mdsrc/proofs/proof_encoding_helpers.rstests/files.rscore-relations/src/free_join/mod.rssrc/proofs/proof_encoding.rssrc/ast/mod.rssrc/extract/dag_extract.rsegglog-bridge/src/lib.rssrc/ast/parse.rstests/integration_test.rssrc/proofs/proof_extraction.rssrc/lib.rssrc/extract/secondary_map.rssrc/extract.rs
🔇 Additional comments (30)
tests/integration_test.rs (2)
10-115: LGTM!
578-710: LGTM!tests/files.rs (1)
271-280: LGTM!.agents/logs/2026-06-24-greedy-dag-extractor-perf.md (1)
1-1123: LGTM!.github/workflows/build.yml (1)
72-73: 🩺 Stability & AvailabilityBenchmark input files confirmed present.
Both
greedy-dag-vec-extract.eggandgreedy-dag-taylor.eggare checked in under thetestsdirectory. The build job will not fail due to missing inputs.src/extract/dag_extract.rs (3)
20-89: LGTM!
389-660: LGTM!
662-870: LGTM!src/lib.rs (3)
49-49: LGTM!Also applies to: 1659-1690
1695-1720: LGTM!
1791-1803: LGTM!src/proofs/proof_extraction.rs (2)
1-6: LGTM!
98-109: LGTM!src/ast/desugar.rs (1)
167-169: LGTM!src/ast/mod.rs (1)
77-77: LGTM!Also applies to: 162-169, 276-283, 846-847, 962-967, 1754-1756, 1850-1855, 1975-1982
src/ast/parse.rs (1)
114-131: LGTM!Also applies to: 653-683
src/proofs/proof_encoding.rs (1)
1335-1335: LGTM!Also applies to: 1353-1353
Cargo.toml (1)
152-152: LGTM!src/lib.md (1)
41-41: LGTM!core-relations/src/lib.rs (1)
39-39: LGTM!src/typechecking.rs (1)
460-460: LGTM!Also applies to: 482-482
src/proofs/proof_encoding_helpers.rs (1)
564-564: LGTM!src/extract/secondary_map.rs (3)
27-225: LGTM!
227-530: LGTM!
532-650: LGTM!src/extract.rs (2)
6-54: LGTM!Also applies to: 56-94, 105-183, 200-314, 526-639, 647-677, 741-818, 848-879
148-156: 🚀 Performance & Scalability
find_canonicaldoes a full UF-table scan on every call; use the new indexed lookup.This iterates the entire UF parent table via
for_eachfor each invocation, even though the comment describes it as a one-hop "lookup". The greedy-DAG extractor callsfind_canonicalper node (compute_cost_node,discover_node,reconstruct_termdag_node_helper), so extraction becomes roughlyO(nodes × uf_table_size)— directly at odds with this PR's performance goal. Thefor_each_matching_colhelper added in this PR resolves matches via the lazy column index (with a scan fallback), and the single-parent invariant guarantees at most one matching row, so semantics are preserved.⚡ Proposed switch to indexed column lookup
let mut canonical = value; egraph .backend - .for_each(uf_func.backend_id, |row: egglog_bridge::ScanEntry<'_>| { - // UF table has (child, parent) as inputs - if row.vals[0] == value { - canonical = row.vals[1]; - } - }); + .for_each_matching_col(uf_func.backend_id, 0, value, |row| { + // UF table has (child, parent) as inputs + canonical = row.vals[1]; + }); canonicalsrc/prelude.rs (1)
93-93: LGTM!core-relations/src/free_join/mod.rs (1)
31-34: LGTM!Also applies to: 777-802
egglog-bridge/src/lib.rs (1)
475-520: LGTM!
Merging this PR will not alter performance
Comparing 
Footnotes
|
saulshanabrook
changed the title
|
Things to look into from talking to @oflatt:
|
saulshanabrook
force-pushed
the
codex/greedy-dag-extractor
branch
from
4e48f01 to
225396e
Compare
saulshanabrook
force-pushed
the
codex/greedy-dag-extractor
branch
from
225396e to
d94c326
Compare
saulshanabrook
changed the title
|
@coderabbitai full review |
✅ Action performedFull review finished. |
There was a problem hiding this comment.
Actionable comments posted: 7
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@src/extract.rs`:
- Around line 638-645: The public extract_variants_with_sort / extract_variants
path is unwrapping an Option from compute_cost_hyperedge and panicking when a
candidate variant is uncostable because one of its children cannot be extracted.
Update the extraction loop to treat compute_cost_hyperedge returning None as a
skipped candidate, continue searching for other variants, and stop early if no
more extractable candidates remain. Make sure the behavior returns fewer
ExtractedTerm results rather than crashing, and keep the change localized around
extract_variants_with_sort and the candidate selection logic it uses.
- Around line 355-364: The cost calculation in the extraction path is using the
internal Function instead of the extraction-facing constructor, which can cause
custom cost models to see a different name than reconstruction. Update the call
from the extraction logic in extract.rs so total_enode_cost receives the same
constructor identifier used by extraction_term_name(), likely by passing the
extraction-facing Function/term name from the extraction flow rather than the
view/internal func. Ensure the symbols extraction_output_index(),
extraction_term_name(), and total_enode_cost stay aligned so func.name() in
custom models matches reconstruction.
In `@src/lib.rs`:
- Around line 362-365: The public helper is_constructor() in lib.rs is narrower
than the extraction-visible table set because it only checks
FunctionSubtype::Constructor and misses view tables marked by
term_constructor.is_some(). Update this API so downstream users of
is_constructor() get the same table classification used by extract.rs, either by
expanding the method to include the view-table case or by renaming it to make
the current behavior explicit and adding a separate helper for the
extraction-visible rule.
- Around line 1800-1807: The extraction loop in the write path can partially
append to disk before encountering an invalid root, so the output file may be
left in a half-written state. In the code around the `extracted.terms` loop,
first validate and collect every root into `TermId`s from `extract_best`’s full
batch, then perform the `writeln!` calls only after all roots have successfully
resolved; keep the existing `Error::ExtractError` and `Error::IoError` handling,
but move writing behind the upfront validation step.
In `@tests/api_query.rs`:
- Around line 143-185: The current enodes_for_eclass test only covers singleton
eclasses, so it does not verify behavior for merged representatives or subsumed
rows. Extend the test in enodes_for_eclass_basic to create two Add terms that
are unioned into the same eclass, then assert rs.enodes_for_eclass returns both
rows for that representative; also include a subsumed row in the same assertion
path to validate the subsumed flag mapping.
In `@tests/integration_test.rs`:
- Around line 589-591: The integration test in extracted.terms only checks that
the first entry is Some, which can miss a wrong term for the extractable root.
Tighten the assertion in the shared-TermDag multi-root extraction test so the
first result is verified to reconstruct the visible term "(visible)" using the
extracted term from the batch, while keeping the second result asserted as None.
- Around line 550-554: The current assertion in the integration test only checks
the pretty-printed TermDag output, so it can miss reconstruction regressions.
Update the test around the extracted TermDag and root/value setup to also verify
semantic round-tripping by asserting the reconstructed term/value equals the
original value, using the existing extracted, root, and value symbols in this
test. Keep the existing string assertion, but add an equality check that
exercises the value-reconstruction path instead of relying only on to_string.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: bfabbf43-503b-47fa-b0c1-0db367cce812
📒 Files selected for processing (11)
core-relations/src/action/mod.rscore-relations/src/free_join/mod.rsegglog-bridge/src/lib.rssrc/exec_state.rssrc/extract.rssrc/lib.mdsrc/lib.rssrc/prelude.rssrc/proofs/proof_extraction.rstests/api_query.rstests/integration_test.rs
…tractor # Conflicts: # src/extract.rs # src/proofs/proof_extraction.rs
oflatt
left a comment
oflatt
left a comment
There was a problem hiding this comment.
Looks good to me (PR descriptions very out of date)
|
One thing I'd love is to have extraction work inside a ReadState as well as on the EGraph. But not this PR's problem. |
| | Constraint::LtConst { .. } | ||
| | Constraint::GtConst { .. } | ||
| | Constraint::LeConst { .. } | ||
| | Constraint::GeConst { .. } => return true, |
There was a problem hiding this comment.
Should they be impossible cases?
| } | ||
|
|
||
| impl TreeCostModel<DefaultCost> for TreeAdditiveCostModel { | ||
| fn total_enode_cost( |
There was a problem hiding this comment.
I remember we discussed this and decided to keep the existing enode_cost? The original one is also more natural to me.
There was a problem hiding this comment.
The existing enode_cost has the problem where its only ever used to produce total cost with the fold, so it seemed like odd to keep it. Like the functions were ever only called changed together, with enode_cost feeding into the total call.
So that it returned a "Cost" type was also a bit weird, really it could return anything that the fold took in, like I had to return odd stuff from it from Python to basically just pass data between them and do all the computation in total_enode_cost.
There was a problem hiding this comment.
Did you pass odd stuff because there was no DAG cost model and extractor, or do you still need to do it even with the new DAG extractor?
If we use enode_cost here, TreeCostModel exposes a superset of cost functions of DAG cost model's, which is nice and matches our (my) intuition. My mental model of the tree cost model is that the term is annotated with cost tags and the cost of a term is just a fold over these cost tags. So, for example, the proposed cost model forbids you from doing it if you want to visualize an e-graph with per-node cost annotation, or serialize an e-graph with a custom cost model.
There was a problem hiding this comment.
As I understand it, we should have the cost trait reflect what the underlying extraction algorithm needs. The fact that you can split this up into a fold and an e-node cost is an implementation choice of a particular cost model, not a requirement of the extractor.
So for example, you could have a cost model for the tree extractor which says "on this particular e-node multiply the child costs by ten and on this other one multiply the child costs by twenty. In the other interface, you would have to smuggle the e-node ID through the cost output of enode_cost and then interpret it in fold.
If we use enode_cost here, TreeCostModel exposes a superset of cost functions of DAG cost model's, which is nice and matches our (my) intuition.
We can already use any dag cost model as a tree cost model, do you mean something else?
So, for example, the proposed cost model forbids you from doing it if you want to visualize an e-graph with per-node cost annotation, or serialize an e-graph with a custom cost model.
This is already true with fold, which is more general than what is allowed in the visualizer or in serialization. Both of those in fact do not currently support the set-cost even, so if we want to somehow make those features aware of this, we would have to change things.
There was a problem hiding this comment.
To me this is not an implementation choice, but the definition of the tree cost model.
The idea is that enode_cost returns all e-graph specific cost information, and fold is an e-graph--agnostic way to combine such information. This gives a clear description of the tree extraction problem, which can be specified as an e-graph with per-node cost information, and a generic fold function. I believe you cannot do this with total_node_cost.
"On this particular e-node multiply the child costs by ten and on this other one multiply the child costs by twenty" is a combine function we can define, while I think smuggling e-node ID is a bad idea. If you want to return odd stuff from enode_cost (e.g., the constant folded result of the children as a loop count estimate), the user can define the cost as a pair (ActualCost, Option) and ignore the second part for comparison, or better, we can tweak the egglog interface to support that.
We can already use any dag cost model as a tree cost model, do you mean something else?
I meant you could convert a tree cost model into a DAG one by disregarding combine.
Both of those in fact do not currently support the set-cost even
But we can implement this, right? Again, a serialized e-graph with node costs + an e-graph--agnostic fold function gives a complete specification of the extraction problem. But committing to total_enode_cost would eliminate this possibility.
Maybe another way to think about this is that TreeAdditiveCostModel and SetCostModel are essentially the same cost model, besides how they obtain the per-node cost, but the new interface loses this connection.
| &ch_costs, | ||
| self.cost_model.enode_cost(egraph, func, &enode), | ||
| )) | ||
| let cost_func = func |
There was a problem hiding this comment.
Could you explain what this does to me as someone who hasn't caught up with the proof development?
There was a problem hiding this comment.
In proof mode, view tables like AddView are used for querying and extraction, but the actual name of the function is still Add. The term_constructor attribute tells you the original name. Does that help?
It's annoying, but in proof mode everywhere we expose the API we need to keep in mind to use the "term_cosntructor" names
There was a problem hiding this comment.
Might be a better way to clean this up! Some sort of wrapper internally so we get the right names and right tables.
| /// subterm should always lead to a non-worse superterm, to guarantee the extracted term | ||
| /// being optimal under the given cost model. | ||
| /// If this is not followed, the extractor may panic on reconstruction | ||
| pub struct Extractor<C: Cost + Ord + Eq + Clone + Debug> { |
There was a problem hiding this comment.
Why is Extractor no longer public?
There was a problem hiding this comment.
We dont need it. Every use case of it just extracted a few particular nodes, so I cleaned up the interface to just expose that to keep the details more private.
There was a problem hiding this comment.
I thought part of the point of the extractor interface is to provide a zoo of different extractor implementations (like extraction-gym for egglog). It would be weird if someone implemented a faster extractor but found they couldn't get a handle on the plain Extractor for comparison. I'm also in favor of minimizing interface changes unless it's a strict improvement.
Another potential use case of the extractor is if the user wants to interactively extract a series of terms, without building the Extractor every time
There was a problem hiding this comment.
We don't have an extractor interface. We just have a tree extractor and a dag extractor, and they expose different methods on the e-graph. Without anything that calls this interface, I am not sure what it would be for?
You can of course compare against the main extractor, you just call the methods on the e-graph.
Another potential use case of the extractor is if the user wants to interactively extract a series of terms, without building the Extractor every time
Yeah I just thought since I hadn't seen any use cases in experimental and main that exercised this pattern, we could remove it. That also frees us up to change how the extractor performs in the future. Like now it does this search at a sort level of the e-graph to trim, and does all extractions for that. But we could change it to do a more precise traversal of the e-graph and only build extractions for those expressions, instead of all pieces. By keeping the interface smaller then that doesn't have to be a breaking change.
There was a problem hiding this comment.
We will want an extractor interface, right? There are many DAG extractor implementations (ILP, branch and bound, ASP, etc.), and there's the Dijkstra algorithm for tree extraction. Just like we have an interface for extensible schedulers, we should do the same for extractors. I'm all in for standardizing the interfaces around DAG and tree extractors, just like what we did in extraction-gym.
Not in experimental and main does not mean users won't have this pattern? A user could import egglog, build an e-graph, and interactively extract terms from the Rust side.
There was a problem hiding this comment.
Sure but would that interface be? We dont define it in this PR and I would opt to defer it.
If we define that interface, then we want a way to actually use that interface in main somehow, like being able to switch extractors.
A user could import egglog, build an e-graph, and interactively extract terms from the Rust side.
Yeah you can do that today with the methods on the e-graph.
There was a problem hiding this comment.
Basically I think there are two related points here:
- There is a question about having a re-usable extractor interface. I like this idea, but I didn't implement it in this PR. There was no previous extractor trait, just a concrete implementation of extractor. That extractor happened to work in a way that traverses first the e-graph at a sort level first, prepares all of those items, then allows extractions. It's not clear that we would want to use this as "the" interface, because for example, the DAG extractor does not traverse the whole e-graph by sort. It does a depth first traversal based on the actual nodes you want to extract. I would prefer not to standardize an extractor interface in this PR and defer that to later work. If we do have an interface, we should have a way to use that in the e-graph in some way.
- There is the loss of functionality with this changes around the default extractor. Previously, you could do the work of creating costs for a subset of the e-graph based on a list of sorts and all their possible children. I have shrunk the API to simply providing a list of expressions and getting their extractions out. I didn't see any uses for this more flexible API. I decided to shrink the exposed syntax to make it easier in the future if we want to change out default tree based extractor to use a different design that might not require traversing the e-graph by sort first. By keeping this public API it keeps us locked into that syntax, so further performance improvements would need to conform to it as well. If there are actual use cases today for this interface that would be helpful to understand why it's important to preserve.
| /// | ||
| /// This is the normal user extraction path: it respects `:unextractable` | ||
| /// and hidden internal functions. | ||
| pub fn extract_best<C: Cost, M: TreeCostModel<C> + 'static>( |
There was a problem hiding this comment.
They seem to overlap with extract_value and extract_value_with_cost_model. Do we need all of them?
There was a problem hiding this comment.
Yeah extact_value and extract_value_with_cost_model were previous helpers, I can remove them.
| impl Cost for $cost { | ||
| impl CommutativeMonoid for $cost { | ||
| fn identity() -> Self { 0 } | ||
| fn unit() -> Self { 1 } |
There was a problem hiding this comment.
Why do we no longer have unit() for a cost? This provides a default for e.g., base values.
There was a problem hiding this comment.
You dont need it. It was only used in the default trait implementation and not used at all in the actual extractor, it was just used in the deafult trait implementation, but that wasn't really needed. so it seems cleaner to remove it. Like there is no reason for a cost to require it.
There was a problem hiding this comment.
It provides a default head cost for functions and values. For example, in your implementation of TreeAdditiveCostModel and CustomCostModel, you use the magic number 1. It does not need to be magic if we have unit(). Alternatively, consider how you would make a generic AstSizeCostModel<C> where C: Cost if without unit.
There was a problem hiding this comment.
Yeah it provides a default cost, but its not clear to me its worth having there, because if you define your own cost model, its not needed. I.e. cost should be about what the extraction/cost model needs, and its not required, its optional basically.
Like in the current implementation, this is how we implement the cost model for u64:
impl CostModel<DefaultCost> for TreeAdditiveCostModel {
fn fold(
&self,
_head: &str,
children_cost: &[DefaultCost],
head_cost: DefaultCost,
) -> DefaultCost {
children_cost.iter().fold(head_cost, |s, c| s.combine(c))
}
fn enode_cost(&self, egraph: &EGraph, func: &Function, _enode: &Enode<'_>) -> DefaultCost {
func.extraction_head_cost(egraph)
}
}It isn't clear to me how this is better than doing:
impl CostModel<DefaultCost> for TreeAdditiveCostModel {
fn fold(
&self,
_head: &str,
children_cost: &[DefaultCost],
head_cost: DefaultCost,
) -> DefaultCost {
children_cost.iter().fold(head_cost, |s, c| s.combine(c))
}
fn enode_cost(&self, egraph: &EGraph, func: &Function, _enode: &Enode<'_>) -> DefaultCost {
func.extraction_head_cost(egraph)
}
fn base_value_cost(&self, egraph: &EGraph, sort: &ArcSort, value: Value) -> C {
1
}
}There was a problem hiding this comment.
I updated it to make TreeAdditiveCostModel generic, so that you can parameterize it with different unit costs for different cost types.
| } | ||
|
|
||
| /// Requirements for a type to be usable as a cost by a [`CostModel`]. | ||
| pub trait Cost { |
There was a problem hiding this comment.
Do we have to change the name?
There was a problem hiding this comment.
I can change it back
There was a problem hiding this comment.
Reverted, I think its clearer now
|
Small nit: it seems some relatively big files are checked into the git history. Maybe worth doing a squash merge at the end. |
4 participants
Extraction support APIs
This is the core half of the greedy-DAG extraction split. It does not add
:extractor greedy-dagto core egglog; that command syntax and the extractor implementation live in the downstream experimental PR:Related context:
greedy_dag_cost_modelegglog-python#387Changes
EGraph, returning named structs with a sharedTermDag.Nonein the batch result; strict convenience APIs and commands convert that back intoExtractErrorwhere appropriate.(extract ...),(output ...),print-function/function_to_dag, andextract_value*through the high-level extraction path.(output ...)validate the whole extraction batch before appending to disk.Public Interfaces Added Or Changed
Extraction module:
BaseCostModel<C>: base primitive/container-independent value cost hook.TreeCostModel<C>: replacesCostModel<C>for total tree costs withtotal_enode_costandtotal_container_cost.CommutativeMonoid: providesidentityandcombine.Cost: now the extraction-facing marker overCommutativeMonoid + Ord + Eq + Debug.ExtractedTerm<C>,ExtractedTerms<C>,ExtractedTermVariants<C>: named result types with sharedTermDagstorage.ExtractedTerms<C>::termsis nowVec<Option<ExtractedTerm<C>>>;Nonemeans the corresponding requested root is unextractable.Extractoris no longer public; ordinary callers should use the high-levelEGraphextraction APIs.EGraph:extract_best(roots, cost_model)extract_variants(roots, nvariants, cost_model)container_inner_values(sort, value)reconstruct_base_value(sort, value, termdag)reconstruct_container_value(sort, value, termdag, element_terms)extract_value_with_cost_modelnow takes aTreeCostModel<DefaultCost>and maps a missing single root toExtractError.Read/introspection helpers:
Read::enodes_for_eclass(name, eclass, callback): indexed lookup for rows in one constructor/relation table whose output eclass matcheseclass.Function::is_constructor(): declared constructor/relation table predicate.Function::is_unextractable()Backend/bridge:
core_relations::ExecutionState::for_each_matching_colegglog_bridge::TableAction::for_each_output_valueReview Notes
The normal
(extract ...)command remains tree extraction and still defaults to the existing tree behavior. Greedy-DAG extraction,:extractor greedy-dag, and the performance-sensitive secondary-map data structures live inegglog-experimental.After #941, proof extraction is root-directed and separate from the normal user extractor. This PR no longer changes that proof-extraction path.
This PR deliberately does not expose internal union-find canonicalization. The downstream greedy-DAG extractor works in normal mode on the
(sort, value)roots and constructor row outputs it is given; term/proof-encoding internals stay out of the custom extractor API for now.The bridge/core-relations additions intentionally expose only row iteration by an indexed column and output-value iteration for a
TableAction. Earlier arbitrary projection/window scan APIs were removed to keep the support surface focused on the read-state eclass lookup.The core integration tests cover the new custom tree-cost public surface with a non-primitive cost type, mixed optional extraction results, semantic round-tripping of extracted terms, and the indexed
Read::enodes_for_eclasslookup over merged/subsumed rows.Validation
cargo checkcargo test --test api_query enodes_for_eclasscargo test --test integration_test extractcargo test --test extraction_proof_modemake nitsgit diff --check