[NEVER EVER EVER MERGE THIS]

Cargo.toml

@@ -8,8 +8,8 @@ edition = "2018"
 
 [dependencies]
 # egg = { git = "https://github.com/caviar-trs/egg", branch = "check_equivalence_iteration_level" }
-egg = { git = "https://github.com/caviar-trs/egg", branch = "fail_fast" }
-# egg = { path="../egg" }
+# egg = { git = "https://github.com/caviar-trs/egg", branch = "fail_fast" }
+egg = "0.10.0"
 
 ordered-float = "1"
 env_logger = "0.8.2"

src/dataset/mod.rs

@@ -99,7 +99,7 @@ pub fn minimal_set_to_prove(
         ruleset_copy_names = ruleset_minimal
             .clone()
             .into_iter()
-            .map(|rule| rule.name().to_string())
+            .map(|rule| rule.name.to_string())
             .rev()
             .collect();
         data_object = object! {
@@ -113,9 +113,7 @@ pub fn minimal_set_to_prove(
         println!(
             "{0} rules are needed to prove: {1}",
             format!("{0}", ruleset_minimal.len()).red().bold(),
-            expression.0.to_string()
-                .bright_green()
-                .bold(),
+            expression.0.to_string().bright_green().bold(),
         );
         // for r in ruleset_minimal{
         //     println!(
@@ -180,7 +178,8 @@ pub fn minimal_set_to_prove_0_1(
     let goals = [end_0.clone(), end_1.clone()];
     let mut proved_goal = "0/1".to_string();
     let ruleset = Ruleset::from(ruleset_id);
-    let result = crate::trs::prove(-1, expression, &ruleset, params, true, false);
+    let (result, _) =
+        crate::trs::prove_with_explanation(-1, expression, &ruleset, params, true, false);
     if result.result {
         let mut runner;
         let mut id;
@@ -193,7 +192,7 @@ pub fn minimal_set_to_prove_0_1(
         ruleset.shuffle(&mut rng);
         let mut ruleset_copy: Vec<egg::Rewrite<Math, ConstantFold>>;
         let mut ruleset_minimal: Vec<egg::Rewrite<Math, ConstantFold>>;
-        
+
         counter = 0;
         ruleset_minimal = ruleset.clone();
         while counter < reorder_count {
@@ -210,7 +209,8 @@ pub fn minimal_set_to_prove_0_1(
                     .with_expr(&start);
 
                 if use_iteration_check {
-                    runner = runner.run_check_iteration(ruleset_copy.iter(), &goals);
+                    panic!("You are on the branch with new egg, `run_check_iteration` is not available.");
+                    // runner = runner.run_check_iteration(ruleset_copy.iter(), &goals);
                 } else {
                     runner = runner.run(ruleset_copy.iter());
                 }
@@ -235,7 +235,7 @@ pub fn minimal_set_to_prove_0_1(
         let ruleset_copy_names: Vec<String> = ruleset_minimal
             .clone()
             .into_iter()
-            .map(|rule| rule.name().to_string())
+            .map(|rule| rule.name.to_string())
             .rev()
             .collect();
         data_object = object! {

src/lib.rs

@@ -11,7 +11,8 @@ pub mod structs;
 pub mod trs;
 
 use trs::{
-    prove, prove_expression_with_file_classes, prove_npp, prove_pulses, prove_pulses_npp, simplify,
+    prove_expression_with_file_classes, prove_npp, prove_pulses, prove_pulses_npp,
+    prove_with_explanation, simplify,
 };
 
 /// Runs Simple Caviar to prove the expressions passed as vector using the different params passed. #[allow(dead_code)]
@@ -30,7 +31,7 @@ pub fn prove_expressions(
     //For each expression try to prove it then push the results into the results vector.
     for expression in exprs_vect.iter() {
         println!("Starting Expression: {}", expression.index);
-        let mut res = prove(
+        let (mut res, explanation) = prove_with_explanation(
             expression.index,
             &expression.expression,
             ruleset,
@@ -39,6 +40,7 @@ pub fn prove_expressions(
             report,
         );
         res.add_halide(expression.halide_result.clone(), expression.halide_time);
+        println!("explanation: {:?}", explanation);
         println!("result: {:?}", res.stop_reason);
         results.push(res);
     }

src/main.rs

@@ -71,9 +71,8 @@ fn main() {
             // Prove expressions using Caviar with/without ILC
             "prove" => {
                 let expression_vect = read_expressions(&expressions_file).unwrap();
-                // hacky
-
-                let results = prove_expressions(&expression_vect, &ruleset, params, true, false);
+                // use_iteration_check must be false on this branch
+                let results = prove_expressions(&expression_vect, &ruleset, params, false, false);
                 write_results("tmp/results_prove.csv", &results).unwrap();
             }
             // Prove expressions using Caviar with pulses and with/without ILC.