cleanup and split rules

Author: SaltyPeppermint

examples/blocking.rs

@@ -14,45 +14,30 @@ fn main() {
 
     let runner_1 = Runner::default()
         .with_expr(&mm)
-        // .with_iter_limit(6)
         .with_time_limit(Duration::from_secs(60))
-        .with_node_limit(1_000_000)
+        .with_node_limit(10_000_000)
         .with_scheduler(SimpleScheduler)
         .with_hook(hooks::targe_hook(split_guide.clone()))
-        .with_hook(hooks::printer_hook)
+        // .with_hook(hooks::printer_hook)
         .run(&rise::rules(Ruleset::Split));
 
-    println!("{}", runner_1.report());
+    // println!("{}\nSPLIT STEP DONE DONE\n-----------\n", runner_1.report());
     assert_eq!(
         runner_1.roots[0],
         runner_1.egraph.lookup_expr(&split_guide).unwrap()
     );
 
-    // let split_guide_sketch = rise::sketchify(&split_guide, &|_| false);
-    // let sketch_extracted_split_guide =
-    //     &sketch::eclass_extract(&split_guide_sketch, AstSize, &runner_1.egraph, root_mm)
-    //         .unwrap()
-    //         .1;
-
-    // // assert!(
-    // //     utils::find_diff(
-    // //         &rise::canon_nat(sketch_extracted_split_guide),
-    // //         &rise::canon_nat(&split_guide)
-    // //     )
-    // //     .is_none()
-    // // );
-
     let runner_2 = Runner::default()
         .with_expr(&split_guide)
-        // .with_iter_limit(10)
         .with_time_limit(Duration::from_secs(60))
-        .with_node_limit(1_000_000)
+        .with_node_limit(10_000_000)
+        .with_iter_limit(11)
         .with_scheduler(SimpleScheduler)
         .with_hook(hooks::targe_hook(blocking_goal.clone()))
         .with_hook(hooks::printer_hook)
         .run(&rise::rules(Ruleset::Reorder));
 
-    println!("{}", runner_2.report());
+    println!("{}\nREORDER STEP DONE\n-----------\n", runner_2.report());
 
     let root_guide = runner_2.egraph.find(runner_2.roots[0]);
     let blocking_goal_sketch = rise::sketchify(&blocking_goal, &|n| matches!(n, Rise::NatMul(_)));
@@ -62,8 +47,8 @@ fn main() {
             .1,
     );
     assert!(utils::find_diff(&sketch_extracted_blocking_goal, &blocking_goal).is_none());
-    // assert_eq!(
-    //     root_guide,
-    //     runner_2.egraph.lookup_expr(&blocking_goal).unwrap()
-    // );
+    assert_eq!(
+        runner_2.roots[0],
+        runner_2.egraph.lookup_expr(&blocking_goal).unwrap()
+    );
 }

src/rewrite_system/rise/analysis.rs

@@ -99,7 +99,7 @@ impl Analysis<Rise> for FreeBetaNatAnalysis {
         let beta_extract = if empty {
             RecExpr::default()
         } else {
-            enode.join_recexprs(|id| egraph[id].data.beta_extract.as_ref())
+            enode.join_recexprs(|id| &egraph[id].data.beta_extract)
         };
 
         let canon_nat_expr = if beta_extract.is_empty() {
@@ -119,14 +119,12 @@ impl Analysis<Rise> for FreeBetaNatAnalysis {
         if !egraph[id].data.canon_nat_expr.is_empty()
             && egraph[id].data.canon_nat_expr != egraph[id].data.beta_extract
         {
-            // Remove all other nodes, only the canonical one may remain.
-            egraph[id].nodes.clear();
             // Add the canonical expr
             let canon_nat = &egraph[id].data.canon_nat_expr;
             let added = egraph.add_expr(&canon_nat.clone());
             egraph.union(id, added);
 
-            // #[cfg(debug_assertions)]
+            #[cfg(debug_assertions)]
             egraph[id].assert_unique_leaves();
         }
     }

src/rewrite_system/rise/func.rs

@@ -88,11 +88,9 @@ impl<A: Applier<Rise, FreeBetaNatAnalysis>> Applier<Rise, FreeBetaNatAnalysis>
             let mut new_subst = subst.clone();
             let added_expr_id = egraph.add_expr(&new_expr);
             new_subst.insert(self.vectorized_var, added_expr_id);
-            let mut ids =
-                self.applier
-                    .apply_one(egraph, eclass, &new_subst, searcher_ast, rule_name);
-            ids.push(added_expr_id);
-            ids
+
+            self.applier
+                .apply_one(egraph, eclass, &new_subst, searcher_ast, rule_name)
         } else {
             Vec::new()
         }

src/rewrite_system/rise/nat/applier.rs

@@ -1,6 +1,6 @@
 use egg::{Applier, EGraph, Id, Pattern, PatternAst, Searcher, Subst, Symbol, Var};
 
-use super::{Rise, FreeBetaNatAnalysis};
+use super::{FreeBetaNatAnalysis, Rise};
 
 pub struct ComputeNat<A: Applier<Rise, FreeBetaNatAnalysis>> {
     var: Var,
@@ -36,11 +36,9 @@ impl<A: Applier<Rise, FreeBetaNatAnalysis>> Applier<Rise, FreeBetaNatAnalysis> f
         let mut new_subst = subst.clone();
         let added_expr_id = egraph.add_expr(&simplified_nat);
         new_subst.insert(self.var, added_expr_id);
-        let mut ids = self
-            .applier
-            .apply_one(egraph, eclass, &new_subst, searcher_ast, rule_name);
-        ids.push(added_expr_id);
-        ids
+
+        self.applier
+            .apply_one(egraph, eclass, &new_subst, searcher_ast, rule_name)
     }
 }
 
@@ -60,7 +58,9 @@ impl<A: Applier<Rise, FreeBetaNatAnalysis>> ComputeNatCheck<A> {
     }
 }
 
-impl<A: Applier<Rise, FreeBetaNatAnalysis>> Applier<Rise, FreeBetaNatAnalysis> for ComputeNatCheck<A> {
+impl<A: Applier<Rise, FreeBetaNatAnalysis>> Applier<Rise, FreeBetaNatAnalysis>
+    for ComputeNatCheck<A>
+{
     fn apply_one(
         &self,
         egraph: &mut EGraph<Rise, FreeBetaNatAnalysis>,