From 121d98a437ffe07283a864e7ab72bc2906b4d8d0 Mon Sep 17 00:00:00 2001 From: oflatt Date: Tue, 20 Aug 2024 14:36:23 -0600 Subject: [PATCH] remove existence explanations --- CHANGELOG.md | 1 + src/egraph.rs | 89 ++++--------------------------- src/explain.rs | 138 +------------------------------------------------ src/run.rs | 14 ----- 4 files changed, 13 insertions(+), 229 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2d27c937..d7b4774d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,7 @@ # Changes ## [Unreleased] - ReleaseDate +- Removed existence explanations from egg (the `explain_existance` function). This feature was buggy and not well supported. Supporting it fully required many changes, and it is incompatible with analysis. See #332 for more details. - Change the API of `make` to have mutable access to the e-graph for some [advanced uses cases](https://github.com/egraphs-good/egg/pull/277). - Fix an e-matching performance regression introduced in [this commit](https://github.com/egraphs-good/egg/commit/ae8af8815231e4aba1b78962f8c07ce837ee1c0e#diff-1d06da761111802c793c6e5ca704bfa0d6336d0becf87fddff02d81548a838ab). - Use `quanta` instead of `instant` crate to provide timing information. This can provide a huge speedup if you have lots of rules, since it avoids some syscalls. diff --git a/src/egraph.rs b/src/egraph.rs index b8688153..8b842bf5 100644 --- a/src/egraph.rs +++ b/src/egraph.rs @@ -493,43 +493,6 @@ impl> EGraph { } } - /// When explanations are enabled, this function - /// produces an [`Explanation`] describing how the given expression came - /// to be in the egraph. - /// - /// The [`Explanation`] begins with some expression that was added directly - /// into the egraph and ends with the given `expr`. - /// Note that this function can be called again to explain any intermediate terms - /// used in the output [`Explanation`]. - pub fn explain_existance(&mut self, expr: &RecExpr) -> Explanation { - let id = self.add_expr_uncanonical(expr); - self.explain_existance_id(id) - } - - /// Equivalent to calling [`explain_existance`](EGraph::explain_existance)`(`[`id_to_expr`](EGraph::id_to_expr)`(id))` - /// but more efficient - fn explain_existance_id(&mut self, id: Id) -> Explanation { - if let Some(explain) = &mut self.explain { - explain.with_nodes(&self.nodes).explain_existance(id) - } else { - panic!("Use runner.with_explanations_enabled() or egraph.with_explanations_enabled() before running to get explanations.") - } - } - - /// Return an [`Explanation`] for why a pattern appears in the egraph. - pub fn explain_existance_pattern( - &mut self, - pattern: &PatternAst, - subst: &Subst, - ) -> Explanation { - let id = self.add_instantiation_noncanonical(pattern, subst); - if let Some(explain) = &mut self.explain { - explain.with_nodes(&self.nodes).explain_existance(id) - } else { - panic!("Use runner.with_explanations_enabled() or egraph.with_explanations_enabled() before running to get explanations.") - } - } - /// Get an explanation for why an expression matches a pattern. pub fn explain_matches( &mut self, @@ -858,14 +821,6 @@ impl> EGraph { } else { new_node_q.push(false); } - if let Some(explain) = &mut self.explain { - node.for_each(|child| { - // Set the existance reason for new nodes to their parent node. - if new_node_q[usize::from(child)] { - explain.set_existance_reason(new_ids[usize::from(child)], next_id); - } - }); - } new_ids.push(next_id); } *new_ids.last().unwrap() @@ -905,13 +860,6 @@ impl> EGraph { new_node_q.push(false); } - if let Some(explain) = &mut self.explain { - node.for_each(|child| { - if new_node_q[usize::from(child)] { - explain.set_existance_reason(new_ids[usize::from(child)], next_id); - } - }); - } new_ids.push(next_id); } } @@ -1046,11 +994,11 @@ impl> EGraph { *existing_explain } else { let new_id = self.unionfind.make_set(); - explain.add(original.clone(), new_id, new_id); + explain.add(original.clone(), new_id); debug_assert_eq!(Id::from(self.nodes.len()), new_id); self.nodes.push(original); self.unionfind.union(id, new_id); - explain.union(existing_id, new_id, Justification::Congruence, true); + explain.union(existing_id, new_id, Justification::Congruence); new_id } } else { @@ -1059,7 +1007,7 @@ impl> EGraph { } else { let id = self.make_new_eclass(enode, original.clone()); if let Some(explain) = self.explain.as_mut() { - explain.add(original, id, id); + explain.add(original, id); } // now that we updated explanations, run the analysis for the new eclass @@ -1139,16 +1087,9 @@ impl> EGraph { rule_name: impl Into, ) -> (Id, bool) { let id1 = self.add_instantiation_noncanonical(from_pat, subst); - let size_before = self.unionfind.size(); let id2 = self.add_instantiation_noncanonical(to_pat, subst); - let rhs_new = self.unionfind.size() > size_before; - let did_union = self.perform_union( - id1, - id2, - Some(Justification::Rule(rule_name.into())), - rhs_new, - ); + let did_union = self.perform_union(id1, id2, Some(Justification::Rule(rule_name.into()))); (self.find(id1), did_union) } @@ -1158,7 +1099,7 @@ impl> EGraph { /// `Id`s returned by functions like [`add_uncanonical`](EGraph::add_uncanonical) is important /// to control explanations pub fn union_trusted(&mut self, from: Id, to: Id, reason: impl Into) -> bool { - self.perform_union(from, to, Some(Justification::Rule(reason.into())), false) + self.perform_union(from, to, Some(Justification::Rule(reason.into()))) } /// Unions two eclasses given their ids. @@ -1181,17 +1122,11 @@ impl> EGraph { let caller = std::panic::Location::caller(); self.union_trusted(id1, id2, caller.to_string()) } else { - self.perform_union(id1, id2, None, false) + self.perform_union(id1, id2, None) } } - fn perform_union( - &mut self, - enode_id1: Id, - enode_id2: Id, - rule: Option, - any_new_rhs: bool, - ) -> bool { + fn perform_union(&mut self, enode_id1: Id, enode_id2: Id, rule: Option) -> bool { N::pre_union(self, enode_id1, enode_id2, &rule); self.clean = false; @@ -1213,7 +1148,7 @@ impl> EGraph { } if let Some(explain) = &mut self.explain { - explain.union(enode_id1, enode_id2, rule.unwrap(), any_new_rhs); + explain.union(enode_id1, enode_id2, rule.unwrap()); } // make id1 the new root @@ -1388,12 +1323,8 @@ impl> EGraph { let mut node = self.nodes[usize::from(class)].clone(); node.update_children(|id| self.find_mut(id)); if let Some(memo_class) = self.memo.insert(node, class) { - let did_something = self.perform_union( - memo_class, - class, - Some(Justification::Congruence), - false, - ); + let did_something = + self.perform_union(memo_class, class, Some(Justification::Congruence)); n_unions += did_something as usize; } } diff --git a/src/explain.rs b/src/explain.rs index 84fdb42b..05bcae8c 100644 --- a/src/explain.rs +++ b/src/explain.rs @@ -46,12 +46,6 @@ struct ExplainNode { // neighbors includes parent connections neighbors: Vec, parent_connection: Connection, - // it was inserted because of: - // 1) it's parent is inserted (points to parent enode) - // 2) a rewrite instantiated it (points to adjacent enode) - // 3) it was inserted directly (points to itself) - // if 1 is true but it's also adjacent (2) then either works and it picks 2 - existance_node: Id, } #[derive(Debug, Clone)] @@ -916,11 +910,7 @@ impl Explain { } } - pub(crate) fn set_existance_reason(&mut self, node: Id, existance_node: Id) { - self.explainfind[usize::from(node)].existance_node = existance_node; - } - - pub(crate) fn add(&mut self, node: L, set: Id, existance_node: Id) -> Id { + pub(crate) fn add(&mut self, node: L, set: Id) -> Id { assert_eq!(self.explainfind.len(), usize::from(set)); self.uncanon_memo.insert(node, set); self.explainfind.push(ExplainNode { @@ -931,7 +921,6 @@ impl Explain { next: set, current: set, }, - existance_node, }); set } @@ -988,19 +977,10 @@ impl Explain { .insert((node2, node1), (BigUint::one(), node1)); } - pub(crate) fn union( - &mut self, - node1: Id, - node2: Id, - justification: Justification, - new_rhs: bool, - ) { + pub(crate) fn union(&mut self, node1: Id, node2: Id, justification: Justification) { if let Justification::Congruence = justification { // assert!(self.node(node1).matches(self.node(node2))); } - if new_rhs { - self.set_existance_reason(node2, node1) - } self.make_leader(node1); self.explainfind[usize::from(node1)].parent_connection.next = node2; @@ -1105,21 +1085,6 @@ impl<'x, L: Language> ExplainNodes<'x, L> { for i in 0..self.explainfind.len() { let explain_node = &self.explainfind[i]; - // check that explanation reasons never form a cycle - let mut existance = i; - let mut seen_existance: HashSet = Default::default(); - loop { - seen_existance.insert(existance); - let next = usize::from(self.explainfind[existance].existance_node); - if existance == next { - break; - } - existance = next; - if seen_existance.contains(&existance) { - panic!("Cycle in existance!"); - } - } - if explain_node.parent_connection.next != Id::from(i) { let mut current_explanation = self.node_to_flat_explanation(Id::from(i)); let mut next_explanation = @@ -1161,17 +1126,6 @@ impl<'x, L: Language> ExplainNodes<'x, L> { Explanation::new(self.explain_enodes(left, right, &mut cache, &mut enode_cache, false)) } - pub(crate) fn explain_existance(&mut self, left: Id) -> Explanation { - let mut cache = Default::default(); - let mut enode_cache = Default::default(); - Explanation::new(self.explain_enode_existance( - left, - self.node_to_explanation(left, &mut enode_cache), - &mut cache, - &mut enode_cache, - )) - } - fn common_ancestor(&self, mut left: Id, mut right: Id) -> Id { let mut seen_left: HashSet = Default::default(); let mut seen_right: HashSet = Default::default(); @@ -1257,62 +1211,6 @@ impl<'x, L: Language> ExplainNodes<'x, L> { (left_connections, right_connections) } - fn explain_enode_existance( - &self, - node: Id, - rest_of_proof: Rc>, - cache: &mut ExplainCache, - enode_cache: &mut NodeExplanationCache, - ) -> TreeExplanation { - let graphnode = &self.explainfind[usize::from(node)]; - let existance = graphnode.existance_node; - let existance_node = &self.explainfind[usize::from(existance)]; - // case 1) - if existance == node { - return vec![self.node_to_explanation(node, enode_cache), rest_of_proof]; - } - - // case 2) - if graphnode.parent_connection.next == existance - || existance_node.parent_connection.next == node - { - let mut connection = if graphnode.parent_connection.next == existance { - graphnode.parent_connection.clone() - } else { - existance_node.parent_connection.clone() - }; - - if graphnode.parent_connection.next == existance { - connection.is_rewrite_forward = !connection.is_rewrite_forward; - std::mem::swap(&mut connection.next, &mut connection.current); - } - - let adj = self.explain_adjacent(connection, cache, enode_cache, false); - let mut exp = self.explain_enode_existance(existance, adj, cache, enode_cache); - exp.push(rest_of_proof); - return exp; - } - - // case 3) - let mut new_rest_of_proof = (*self.node_to_explanation(existance, enode_cache)).clone(); - let mut index_of_child = 0; - let mut found = false; - self.node(existance).for_each(|child| { - if found { - return; - } - if child == node { - found = true; - } else { - index_of_child += 1; - } - }); - assert!(found); - new_rest_of_proof.child_proofs[index_of_child].push(rest_of_proof); - - self.explain_enode_existance(existance, Rc::new(new_rest_of_proof), cache, enode_cache) - } - fn explain_enodes( &self, left: Id, @@ -2050,38 +1948,6 @@ mod tests { egraph.dot().to_dot("target/foo.dot").unwrap(); } - - #[test] - fn simple_explain_exists() { - //! Same as previous test, but now I want to make a rewrite add some term and see it exists in - //! more then one step - use crate::SymbolLang; - init_logger(); - - let rws: Vec> = - [rewrite!("makeb"; "a" => "b"), rewrite!("makec"; "b" => "c")] - .iter() - .cloned() - .collect(); - let mut egraph = Runner::default() - .with_explanations_enabled() - .without_explanation_length_optimization() - .with_expr(&"a".parse().unwrap()) - .run(&rws) - .egraph; - egraph.rebuild(); - let a: Symbol = "a".parse().unwrap(); - let b: Symbol = "b".parse().unwrap(); - let c: Symbol = "c".parse().unwrap(); - let mut exp = egraph.explain_existance(&"c".parse().unwrap()); - println!("{:?}", exp.make_flat_explanation()); - assert_eq!( - exp.make_flat_explanation().len(), - 3, - "Expected 3 steps, got {:?}", - exp.make_flat_explanation() - ); - } } #[test] diff --git a/src/run.rs b/src/run.rs index ae78d84e..5dd80e4b 100644 --- a/src/run.rs +++ b/src/run.rs @@ -462,20 +462,6 @@ where self.egraph.explain_equivalence(left, right) } - /// Calls [`EGraph::explain_existance`](EGraph::explain_existance()). - pub fn explain_existance(&mut self, expr: &RecExpr) -> Explanation { - self.egraph.explain_existance(expr) - } - - /// Calls [EGraph::explain_existance_pattern`](EGraph::explain_existance_pattern()). - pub fn explain_existance_pattern( - &mut self, - pattern: &PatternAst, - subst: &Subst, - ) -> Explanation { - self.egraph.explain_existance_pattern(pattern, subst) - } - /// Get an explanation for why an expression matches a pattern. pub fn explain_matches( &mut self,