Extract dijkstras #6
Conversation
FTRobbin
left a comment
FTRobbin
left a comment
There was a problem hiding this comment.
This cannot be a drop-in replacement for the existing extractor, as it does not handle containers correctly. But we can delay the support for it in Poach.
Besides, the implementation makes two copies of the db(!) and can use some further optimizations. However, we can first test how far this version goes in terms of performance and come back to further optimizations later.
src/extract.rs
Outdated
| self.cost_model.enode_cost( | ||
| egraph, | ||
| func, | ||
| &egglog_bridge::FunctionRow { |
There was a problem hiding this comment.
Why do we need to create a new FunctionRow here?
src/extract.rs
Outdated
| //log::debug!("compute_cost_hyperedge head {} sorts {:?}", head, sorts); | ||
| // Relying on .zip to truncate the values | ||
| for (value, sort) in row.iter().zip(sorts.iter()) { | ||
| if let Some(c) = self.compute_cost_node(egraph, *value, sort) { |
There was a problem hiding this comment.
The complexity here is not quite right in the case of a container.
src/extract.rs
Outdated
| if row.subsumed { | ||
| return; | ||
| } | ||
| id2enode.insert(next_id, (func.clone(), row.vals.to_vec())); |
There was a problem hiding this comment.
Should just be id2enode.push(...) instead of insert
There was a problem hiding this comment.
Furthermore, this makes copies of entire tables, which is not good for performance.
| for (i, eclass) in row.vals.iter().take(row.vals.len() - 1).enumerate() { | ||
| let sort = &func_schema.input[i]; | ||
| if sort.is_eq_sort() || sort.is_container_sort() { | ||
| eclass2parents |
There was a problem hiding this comment.
This almost copies the entire db a second time.
| next_id += 1; | ||
| }, | ||
| ); | ||
| } |
There was a problem hiding this comment.
Since we are making copies of the db, you can actually filter out the rows that correspond to the eclasses we are interested in, instead of just looking at the tables we are interested in.
src/extract.rs
Outdated
|
|
||
| for &parent_id in eclass2parents.entry(*eclass).or_default().iter() { | ||
| remaining_children[parent_id] -= 1; | ||
| if remaining_children[parent_id] == 0 { |
There was a problem hiding this comment.
We can ignore eclasses that already have a lower cost here.
| } | ||
| } | ||
| } | ||
| } |
There was a problem hiding this comment.
I'm not sure this code handles containers correctly. Have you tested it?
There was a problem hiding this comment.
Specifically, containers do not correspond to rows in the tables, so id2enode won't have them, and the costs of containers are never computed.
Implement an egraph extractor using Knuth's algorithm to replace Bellman-Ford.