Starting to add support for multipattern. Need to change existance\un…

…ion to multiple reasons and update apply_matches

Cargo.toml

@@ -36,6 +36,7 @@ serde_json = { version = "1.0.81", optional = true }
 saturating = "0.1.0"
 rayon = { version = "1.10.0", optional = true }
 crossbeam = { version = "0.8.4", optional = true, features = ["crossbeam-channel"] }
+itertools = "0.13.0"
 
 [dev-dependencies]
 ordered-float = "3.0.0"
@@ -55,6 +56,7 @@ serde-1 = [
 ]
 wasm-bindgen = []
 parallel = ["rayon", "crossbeam"]
+check_proof = []
 
 # private features for testing
 test-explanations = []

src/egraph.rs

@@ -854,9 +854,10 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
         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(new_node);
+            let next_id = self.add_uncanonical(new_node.clone());
             if self.unionfind.size() > size_before {
                 new_node_q.push(true);
+                println!("Pushed new node {new_node} to egraph");
             } else {
                 new_node_q.push(false);
             }
@@ -1144,7 +1145,6 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
         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,
@@ -1492,6 +1492,7 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
         n_unions
     }
 
+    #[cfg(feature = "check_proof")]
     pub(crate) fn check_each_explain(&mut self, rules: &[&Rewrite<L, N>]) -> bool {
         if let Some(explain) = &mut self.explain {
             explain.with_nodes(&self.nodes).check_each_explain(rules)