From 509375472624817c75cc95dbcb4baea6bf8905b9 Mon Sep 17 00:00:00 2001 From: oflatt Date: Tue, 20 Aug 2024 10:42:09 -0600 Subject: [PATCH] debugging problem --- src/egraph.rs | 18 +++++++++++------- src/explain.rs | 3 +++ src/multipattern.rs | 1 + src/pattern.rs | 43 ++++++++++++++++++++----------------------- src/rewrite.rs | 28 +++++++++++++++------------- src/run.rs | 12 ++++-------- 6 files changed, 54 insertions(+), 51 deletions(-) diff --git a/src/egraph.rs b/src/egraph.rs index 81cbbaa2..4856d981 100644 --- a/src/egraph.rs +++ b/src/egraph.rs @@ -857,7 +857,6 @@ impl> EGraph { let mut new_ids = Vec::with_capacity(nodes.len()); for node in nodes { let new_node = node.clone().map_children(|i| new_ids[usize::from(i)]); - let size_before = self.unionfind.size(); let next_id = self.add_uncanonical_with_reason(new_node, Some(ExistanceReason::Direct)); if let Some(explain) = &mut self.explain { node.for_each(|child| { @@ -911,7 +910,7 @@ impl> EGraph { // When existance is Some, the new node is first added with `Unset` existance reason. let next_id = self.add_uncanonical_with_reason( new_node, - existance.as_ref().map(|e| ExistanceReason::Unset), + existance.as_ref().map(|_e| ExistanceReason::Unset), ); if self.unionfind.size() > size_before { new_node_q.push(true); @@ -938,7 +937,7 @@ impl> EGraph { if let (Some(explain), Some(existance_reason)) = (&mut self.explain, existance) { // Finally, set the top-level existance reason correctly - explain.set_existance_reason(new_ids.last().unwrap().clone(), existance_reason); + explain.set_existance_reason(*new_ids.last().unwrap(), existance_reason); } // All children have existance and so does the top-level term, therefore nothing is still [`ExistanceReason::Unset`] @@ -1093,6 +1092,8 @@ impl> EGraph { ); debug_assert_eq!(Id::from(self.nodes.len()), new_id); self.nodes.push(original); + // careful to make the old id the leader! + // otherwise, the hash-cons may become out-of-date while adding `lhs_terms` self.unionfind.union(id, new_id); explain.union(existing_id, new_id, Justification::Congruence); new_id @@ -1204,18 +1205,21 @@ impl> EGraph { /// This makes existance explanations more precise after matching a pattern. pub(crate) fn union_matched_rule( &mut self, - from_term: &Id, + from_term: Id, to_pat: &PatternAst, subst: &Subst, rule_name: impl Into, ) -> (Id, bool) { // the rhs is added due to the rule - let id2 = - self.add_instantiation_noncanonical(to_pat, subst, Some(ExistanceReason::EqualTo(id1))); + let id2 = self.add_instantiation_noncanonical( + to_pat, + subst, + Some(ExistanceReason::EqualTo(from_term)), + ); let did_union = self.perform_union(from_term, id2, Some(Justification::Rule(rule_name.into()))); - (self.find(id1), did_union) + (self.find(from_term), did_union) } /// Unions two e-classes, using a given reason to justify it. diff --git a/src/explain.rs b/src/explain.rs index ccdd2949..1ac143fb 100644 --- a/src/explain.rs +++ b/src/explain.rs @@ -1144,6 +1144,9 @@ impl<'x, L: Language> ExplainNodes<'x, L> { &next_explanation, rule, ) { + eprintln!("{:?}", current_explanation); + eprintln!("{:?}", rule.name); + eprintln!("{:?}", next_explanation); return false; } } diff --git a/src/multipattern.rs b/src/multipattern.rs index 4a13a170..d6e59ba2 100644 --- a/src/multipattern.rs +++ b/src/multipattern.rs @@ -124,6 +124,7 @@ impl> Searcher for MultiPattern { } else { Some(SearchMatches { eclass, + lhs_terms: None, substs, ast: None, }) diff --git a/src/pattern.rs b/src/pattern.rs index 30902e06..1ff98012 100644 --- a/src/pattern.rs +++ b/src/pattern.rs @@ -276,7 +276,7 @@ pub struct SearchMatches<'a, L: Language> { pub eclass: Id, /// The substitutions for each match. pub substs: Vec, - /// The particular terms for each substitution. + /// The particular matched terms for each substitution. /// This is [`None`] unless explanations are enabled. pub lhs_terms: Option>, /// Optionally, an ast for the matches used in proof production. @@ -355,27 +355,23 @@ where let ast = self.ast.as_ref(); let mut id_buf = vec![0.into(); ast.len()]; for mat in matches { - let sast = mat.ast.as_ref().map(|cow| cow.as_ref()); - for subst in &mat.substs { - let did_something; - let id; - if egraph.are_explanations_enabled() { - let (id_temp, did_something_temp) = egraph - .union_instantiations_guaranteed_match( - sast.unwrap(), - &self.ast, - subst, - rule_name, - ); - did_something = did_something_temp; - id = id_temp; - } else { - id = apply_pat(&mut id_buf, ast, egraph, subst); - did_something = egraph.union(id, mat.eclass); + if egraph.are_explanations_enabled() { + for (subst, lhs_term) in mat.substs.iter().zip(mat.lhs_terms.as_ref().unwrap()) { + let (id, did_something) = + egraph.union_matched_rule(*lhs_term, &self.ast, subst, rule_name); + + if did_something { + added.push(id) + } } + } else { + for subst in &mat.substs { + let id = apply_pat(&mut id_buf, ast, egraph, subst); + let did_something = egraph.union(id, mat.eclass); - if did_something { - added.push(id) + if did_something { + added.push(id) + } } } } @@ -387,15 +383,16 @@ where egraph: &mut EGraph, lhs_term: Id, subst: &Subst, - searcher_ast: Option<&PatternAst>, + _searcher_ast: Option<&PatternAst>, rule_name: Symbol, ) -> Vec { let ast = self.ast.as_ref(); let mut id_buf = vec![0.into(); ast.len()]; let id = apply_pat(&mut id_buf, ast, egraph, subst); - if let Some(ast) = searcher_ast { - let (from, did_something) = egraph.union_matched_rule(ast, &self.ast, subst, rule_name); + if egraph.are_explanations_enabled() { + let (from, did_something) = + egraph.union_matched_rule(lhs_term, &self.ast, subst, rule_name); if did_something { vec![from] } else { diff --git a/src/rewrite.rs b/src/rewrite.rs index b1db4c43..fee43caa 100644 --- a/src/rewrite.rs +++ b/src/rewrite.rs @@ -338,16 +338,18 @@ where ) -> Vec { let mut added = vec![]; - if egraph.are_explanations_enabled() { - let ast = mat.ast.as_ref().map(|cow| cow.as_ref()); - for (subst, lhs_term) in mat.substs.iter().zip(mat.lhs_terms.unwrap().iter()) { - let ids = self.apply_one(egraph, mat.eclass, subst, None, rule_name); - added.extend(ids) - } - } else { - for subst in &mat.substs { - let ids = self.apply_one(egraph, mat.eclass, subst, None, rule_name); - added.extend(ids) + for mat in matches { + if egraph.are_explanations_enabled() { + let sast = mat.ast.as_ref().map(|cow| cow.as_ref()); + for (subst, lhs_term) in mat.substs.iter().zip(mat.lhs_terms.as_ref().unwrap().iter()) { + let ids = self.apply_one(egraph, *lhs_term, subst, sast, rule_name); + added.extend(ids) + } + } else { + for subst in &mat.substs { + let ids = self.apply_one(egraph, mat.eclass, subst, None, rule_name); + added.extend(ids) + } } } @@ -429,14 +431,14 @@ where fn apply_one( &self, egraph: &mut EGraph, - eclass: Id, + lhs_term: Id, subst: &Subst, searcher_ast: Option<&PatternAst>, rule_name: Symbol, ) -> Vec { - if self.condition.check(egraph, eclass, subst) { + if self.condition.check(egraph, lhs_term, subst) { self.applier - .apply_one(egraph, eclass, subst, searcher_ast, rule_name) + .apply_one(egraph, lhs_term, subst, searcher_ast, rule_name) } else { vec![] } diff --git a/src/run.rs b/src/run.rs index 13be4260..2897607b 100644 --- a/src/run.rs +++ b/src/run.rs @@ -554,20 +554,16 @@ where // when proofs are enabled, first add all LHS of terms to the egraph if self.egraph.are_explanations_enabled() { result = result.and_then(|_| { - rules.iter().zip(&mut matches).try_for_each(|(rw, ms)| { - assert_eq!(ms.lhs_terms, None); - + matches.iter_mut().try_for_each(|ms| { for rule_match in ms { + let sast = rule_match.ast.as_ref().expect("Expected all rewrites to have an AST for the lhs when explanations are enabled"); + assert_eq!(rule_match.lhs_terms, None); let mut new_terms = vec![]; for subst in &rule_match.substs { - // get the pattern of the lhs of the rule - let lhs_pattern = rw.searcher.get_pattern_ast().expect("Expected all rewrites to have an AST for the lhs when explanations are enabled"); - // now instantiate the pattern with the substitution, getting the new term's id - let lhs_term = self.egraph.add_instantiation_noncanonical(lhs_pattern, subst, None); + let lhs_term = self.egraph.add_instantiation_noncanonical(sast, subst, None); new_terms.push(lhs_term); - } rule_match.lhs_terms = Some(new_terms); }