Global DAG extraction #21

oflatt · 2023-12-05T22:11:45Z

This PR adds another greedy DAG extractor which improves the performance of calculating a term's cost.
It does this by sharing subterms in a global DAG, and exiting early when doing set unions.

cumulative time for bottom-up: 2474ms
cumulative time for global-greedy-dag: 4239ms
cumulative time for greedy-dag:            35011ms
cumulative dag cost for global-greedy-dag: 76907
cumulative dag cost for greedy-dag:             76907

oflatt · 2023-12-05T22:12:23Z

plot.py

+
+    extractors = sorted(set(j["extractor"] for j in js))
+
+    for i in range(len(extractors)):


This PR also makes the plot output data for each combination of extractors.
This creates a lot of output- maybe we don't want this change, but I find it helpful.

ezrosent

Mostly minor comments, but want some clarification on a few points.

(let me know if getting this in is urgent and I can still approve and we can fix later).

src/extract/global_greedy_dag.rs

ezrosent · 2023-12-09T06:02:25Z

src/extract/global_greedy_dag.rs

+                size: 1,
+            });
+            self.hash_cons.insert(term, next_id);
+            Some(next_id)


optional:

I think when the if/else are this long it can help to unnest after the "easy case", namely:

if children.is_empty() { ... return Some(next_id); } // check if children contains this node for child in &children { ...

eh, I like nesting
return considered harmful (only half joking)

Up to you! I suggested this because there's already a good amount of early-return in this function (78, 92, 99, for example).

I personally think it is good sometimes, and not good other times. For code like this that feels pretty imperative either way I think it can make the code clearer. Feel free to keep as is though

Ah I see
re-examining my head it seems that early return from a big code block makes me sad

ezrosent · 2023-12-09T06:04:05Z

src/extract/global_greedy_dag.rs

+            self.hash_cons.insert(term, next_id);
+            Some(next_id)
+        } else {
+            // check if children contains this node


Could you explain a bit why cycle detection here is "sound": afaik the standard greedy-dag/bottom-up doesn't have this check (does it need it? was it added later?)

This cycle detection is sound because reachable is the set of reachable eclasses from this term. We won't pick any e-nodes that rely on extracting this e-class.
The greedy-dag algorithm does have cycle detection on line 37

ezrosent · 2023-12-09T06:05:12Z

src/extract/global_greedy_dag.rs

+                .unwrap();
+
+            let mut cost = node_cost + self.total_cost(children[biggest_child]);
+            let mut reachable = Box::new(self.info[children[biggest_child]].reachable.clone());


This is my hack to keep track of a persistent set which we are "mutating" during recursive calls. We can't mutate the container itself, so we need a wrapper as far as I know.
Is there a preferred solution in rust?

Alternatively, the recursive function could also return the new set each time.

I'm not against having subcalls return a new set.

I still don't understand why you need a box here. Why can't you pass a &mut Reachable and then reassign as you are doing now?

Wow TIL that &mut literally means pass by reference. I thought &mut was a mutable reference but you couldn't assign to it.

Updated the code

src/extract/global_greedy_dag.rs

ezrosent · 2023-12-09T06:08:45Z

src/extract/global_greedy_dag.rs

+    // Also return the cost of the new nodes.
+    fn get_cost(&self, shared: &mut Box<Reachable>, id: TermId) -> NotNan<f64> {
+        let eclass = self.info[id].eclass.clone();
+        if shared.contains(&eclass) {


I think this is the key "why" for how this is better than greedy-dag: instead of doing an $O(n)$ union operation when you merge reachable sets, we "stop early" based on the shared egraph-level structure: if two nodes share a child somewhere down we don't continue unioning because we know the sets are the same.

Is that right? If so, I think it's worth a comment :) (If not, I'd definitely appreciate a comment)

Exactly right- I left a comment
// This is the key to why this algorithm is faster than greedy_dag.
// While doing the set union between reachable sets, we can stop early
// if we find a shared term.
// Since the term with id is shared, the reachable set of id will already
// be in shared.

ezrosent

Thanks! Left some follow-ups but feel free to resolve as you see fit.

ezrosent · 2023-12-13T06:25:36Z

src/extract/global_greedy_dag.rs

+                size: 1,
+            });
+            self.hash_cons.insert(term, next_id);
+            Some(next_id)


Up to you! I suggested this because there's already a good amount of early-return in this function (78, 92, 99, for example).

I personally think it is good sometimes, and not good other times. For code like this that feels pretty imperative either way I think it can make the code clearer. Feel free to keep as is though

ezrosent · 2023-12-13T06:27:12Z

src/extract/global_greedy_dag.rs

+                .unwrap();
+
+            let mut cost = node_cost + self.total_cost(children[biggest_child]);
+            let mut reachable = Box::new(self.info[children[biggest_child]].reachable.clone());


I'm not against having subcalls return a new set.

I still don't understand why you need a box here. Why can't you pass a &mut Reachable and then reassign as you are doing now?

oflatt added 5 commits December 4, 2023 11:47

add fast greedy dag algorithm

c7a273f

make plot do all combinations

f46dd03

don't do each thing twice

2d11f70

much faster global greedy dag

d813f28

small optimization

ab61dfa

oflatt commented Dec 5, 2023

View reviewed changes

ezrosent suggested changes Dec 9, 2023

View reviewed changes

oflatt added 2 commits December 11, 2023 15:43

comments and cleanup- thanks @ezrosent

64d98df

box comment

3db7b43

oflatt requested a review from ezrosent December 11, 2023 23:45

ezrosent approved these changes Dec 13, 2023

View reviewed changes

wow &mut is literal pass by reference ok

c722bd3

oflatt merged commit 934bab7 into egraphs-good:main Dec 13, 2023
2 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Global DAG extraction #21

Global DAG extraction #21

oflatt commented Dec 5, 2023 •

edited

Loading

oflatt Dec 5, 2023

ezrosent left a comment

ezrosent Dec 9, 2023

oflatt Dec 11, 2023 •

edited

Loading

ezrosent Dec 13, 2023

oflatt Dec 13, 2023

ezrosent Dec 9, 2023

oflatt Dec 11, 2023

ezrosent Dec 9, 2023

oflatt Dec 11, 2023

ezrosent Dec 13, 2023

oflatt Dec 13, 2023

oflatt Dec 13, 2023

ezrosent Dec 9, 2023

oflatt Dec 11, 2023

ezrosent left a comment

ezrosent Dec 13, 2023

ezrosent Dec 13, 2023


		extractors = sorted(set(j["extractor"] for j in js))

		for i in range(len(extractors)):

Global DAG extraction #21

Global DAG extraction #21

Conversation

oflatt commented Dec 5, 2023 • edited Loading

Choose a reason for hiding this comment

ezrosent left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

oflatt Dec 11, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ezrosent left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

oflatt commented Dec 5, 2023 •

edited

Loading

oflatt Dec 11, 2023 •

edited

Loading