debugging problem

src/egraph.rs

@@ -857,7 +857,6 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
         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<L: Language, N: Analysis<L>> EGraph<L, N> {
                     // 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<L: Language, N: Analysis<L>> EGraph<L, N> {
 
         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<L: Language, N: Analysis<L>> EGraph<L, N> {
                     );
                     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<L: Language, N: Analysis<L>> EGraph<L, N> {
     /// 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<L>,
         subst: &Subst,
         rule_name: impl Into<Symbol>,
     ) -> (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.

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;
                         }
                     }

src/multipattern.rs

@@ -124,6 +124,7 @@ impl<L: Language, A: Analysis<L>> Searcher<L, A> for MultiPattern<L> {
         } else {
             Some(SearchMatches {
                 eclass,
+                lhs_terms: None,
                 substs,
                 ast: None,
             })

src/pattern.rs

@@ -276,7 +276,7 @@ pub struct SearchMatches<'a, L: Language> {
     pub eclass: Id,
     /// The substitutions for each match.
     pub substs: Vec<Subst>,
-    /// The particular terms for each substitution.
+    /// The particular matched terms for each substitution.
     /// This is [`None`] unless explanations are enabled.
     pub lhs_terms: Option<Vec<Id>>,
     /// 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<L, A>,
         lhs_term: Id,
         subst: &Subst,
-        searcher_ast: Option<&PatternAst<L>>,
+        _searcher_ast: Option<&PatternAst<L>>,
         rule_name: Symbol,
     ) -> Vec<Id> {
         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 {

src/rewrite.rs

@@ -338,16 +338,18 @@ where
     ) -> Vec<Id> {
         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<L, N>,
-        eclass: Id,
+        lhs_term: Id,
         subst: &Subst,
         searcher_ast: Option<&PatternAst<L>>,
         rule_name: Symbol,
     ) -> Vec<Id> {
-        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![]
         }

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);
                     }