Log and report egraph size for egg.

Cargo.toml

@@ -10,6 +10,7 @@ criterion = "0.5.1"
 egg = "0.9.5"
 log = "0.4.21"
 rand = "0.8.5"
+env_logger = "0.10"
 
 [[bench]]
 name = "benchmarks"

Makefile

@@ -12,10 +12,11 @@ mt-bench:
 	$(HOME)/.julia/bin/benchpkg Metatheory \
 		-r $(BRANCH1),$(BRANCH2) \
 		--bench-on=$(BRANCH1) \
-		--output-dir=$(MT_RESULTS_DIR)
+		--output-dir=$(MT_RESULTS_DIR) \
+		2>&1 | tee "$(MT_RESULTS_DIR)/mt-log.txt"
 
 egg-bench:
-	cargo bench
+	cargo bench 2>&1 | tee ./target/egg-log.txt
 
 results-table:
 	# TODO: don't cut off long table header names

benches/benchmarks.rs

@@ -1,10 +1,27 @@
-use criterion::criterion_main;
+use criterion::{criterion_main, criterion_group, Criterion};
+use log::{LevelFilter};
+use env_logger;
 
 mod symbollang;
 mod customlang;
 mod egraph;
 
+
+fn init_logger() {
+    env_logger::Builder::new()
+        .filter_level(LevelFilter::Warn) // use warning level to skip all infos logged by egg
+        .init();
+}
+
+// Function to execute all benchmarks
+fn init_benchmarks(_c: &mut Criterion) {
+    init_logger(); // Initialize the logger
+}
+
+criterion_group!(benches, init_benchmarks);
+
 criterion_main! {
+    benches,
     symbollang::basic_maths::benches,
     symbollang::calc_logic::benches,
     symbollang::prop_logic::benches,

benches/customlang/basic_maths.rs

@@ -1,6 +1,7 @@
 use criterion::{black_box, criterion_group, criterion_main, Criterion};
 use egg::*;
-use egg_benchmark::simplify;
+use egg_benchmark::{simplify, EGraphSize};
+use log::{warn};
 
 define_language! {
     pub enum BasicMath {
@@ -50,16 +51,16 @@ pub fn basic_maths_rules() -> Vec<Rewrite<BasicMath, ()>> {
         rewrite!("power-distr-1"; "(^ (* ?x ?y) ?z)" => "(* (^ ?x ?z) (^ ?y ?z))"),
         rewrite!("power-distr-2"; "(* (^ ?x ?z) (^ ?y ?z))" => "(^ (* ?x ?y) ?z)"),
         //(x^p)^q == x^(p * q)
-        rewrite!("power-power-1"; "(^ (^ ?x ?p) ?q)" => "(^ ?x (+ ?p ?q))"),
-        rewrite!("power-power-2"; "(^ ?x (+ ?p ?q))" => "(^ (^ ?x ?p) ?q)"),
+        rewrite!("power-power-1"; "(^ (^ ?x ?p) ?q)" => "(^ ?x (* ?p ?q))"),
+        rewrite!("power-power-2"; "(^ ?x (* ?p ?q))" => "(^ (^ ?x ?p) ?q)"),
         //x^0 --> 1
         rewrite!("power-x0"; "(^ ?x 0)" => "1"),
         //0^x --> 0
         rewrite!("power-0x"; "(^ 0 ?x)" => "0"),
         //1^x --> 1
         rewrite!("power-1x"; "(^ 1 ?x)" => "1"),
         //x^1 --> x
-        rewrite!("power-x1"; "(^ 1 ?x)" => "?x"),
+        rewrite!("power-x1"; "(^ ?x 1)" => "?x"),
         //inv(x) == x^(-1)
         rewrite!("power-inv"; "(inv ?x)" => "(^ ?x (- 1))")
     ]
@@ -70,21 +71,31 @@ pub fn basic_maths_rules() -> Vec<Rewrite<BasicMath, ()>> {
 pub fn basic_maths_benchmark(c: &mut Criterion) {
     c.bench_function(
         "customlang/basic_maths/simpl1",
-        |b| b.iter(|| {
+        |b| {
+            let mut size = EGraphSize{num_classes:0, num_nodes:0, num_memo:0};
+            b.iter(|| {
             let expr: RecExpr<BasicMath> = "(+ a (+ b (+ (* 0 c) d)))".parse().unwrap();
 
-            simplify(black_box(&expr), black_box(&basic_maths_rules()), 8);
+            let (_result,itersize) = simplify(black_box(&expr), black_box(&basic_maths_rules()), 8);
+            size=itersize;
             //assert_eq!(result, "(+ d (+ b a))");
-        })
+            });
+            warn!("customlang/basic_maths/simpl1 {}", size);
+        }
     );
 
     c.bench_function(
         "customlang/basic_maths/simpl2",
-        |b| b.iter(|| {
-            let expr = "(+ (+ (+ 0 (* (* 1 foo) 0)) (* a 0)) a)".parse().unwrap();
-            let result =  simplify(black_box(&expr), black_box(&basic_maths_rules()), 8);
-            assert_eq!(result, "a".parse().unwrap());
-        })
+        |b| {
+            let mut size = EGraphSize{num_classes:0, num_nodes:0, num_memo:0};
+            b.iter(|| {
+                let expr = "(+ (+ (+ 0 (* (* 1 foo) 0)) (* a 0)) a)".parse().unwrap();
+                let (result,itersize) =  simplify(black_box(&expr), black_box(&basic_maths_rules()), 8);
+                size=itersize;
+                assert_eq!(result, "a".parse().unwrap());
+            });
+            warn!("customlang/basic_maths/simpl2 {}", size);
+        }
     );
 }
 

benches/customlang/calc_logic.rs

@@ -1,6 +1,7 @@
 use criterion::{black_box, criterion_group, criterion_main, Criterion};
 use egg::*;
 use egg_benchmark::*;
+use log::{warn};
 
 // ## Theory of Calculational Logic
 // https://www.cs.cornell.edu/gries/Logic/Axioms.html
@@ -80,20 +81,26 @@ pub fn calc_logic_benchmark(c: &mut Criterion) {
 
     let demorgan: RecExpr<CalcLogic> = "(== (!! (|| p q)) (&& (!! p) (!! q)))".parse().unwrap();
     c.bench_function("customlang/calc_logic/demorgan", |b| {
+        let mut size = EGraphSize{num_classes:0, num_nodes:0, num_memo:0};
         b.iter(|| {
-            let res = prove(black_box(&demorgan), black_box(&rules), 1, 10, &tru);
+            let (res,itersize) = prove(black_box(&demorgan), black_box(&rules), 1, 10, &tru);
+            size = itersize;
             assert!(tru.eq(&res))
-        })
+        });
+        warn!("customlang/calc_logic/demorgan {}", size);
     });
 
     let frege: RecExpr<CalcLogic> = "(=> (=> p (=> q r)) (=> (=> p q) (=> p r)))"
         .parse()
         .unwrap();
     c.bench_function("customlang/calc_logic/freges_theorem", |b| {
+        let mut size = EGraphSize{num_classes:0, num_nodes:0, num_memo:0};
         b.iter(|| {
-            let res = prove(black_box(&frege), black_box(&rules), 2, 10, &tru);
+            let (res,itersize) = prove(black_box(&frege), black_box(&rules), 2, 10, &tru);
+            size = itersize;
             assert!(tru.eq(&res))
-        })
+        });
+        warn!("customlang/calc_logic/freges_theorem {}", size);
     });
 }
 

benches/customlang/prop_logic.rs

@@ -1,6 +1,7 @@
 use criterion::{black_box, criterion_group, criterion_main, Criterion};
 use egg::{*, rewrite as rw};
 use egg_benchmark::{*};
+use log::{warn};
 
 define_language! {
     pub enum PropositionalLogic {
@@ -90,32 +91,47 @@ pub fn propositional_logic_benchmark(c: &mut Criterion) {
         .parse().unwrap();
     c.bench_function(
         "customlang/prop_logic/prove1",
-        |b| b.iter(|| {
-            let result = prove(black_box(&ex_logic), black_box(&rules), 2, 6, &tru);
-            assert_eq!(result, tru)
-        })
+        |b| {
+            let mut size = EGraphSize{num_classes:0, num_nodes:0, num_memo:0};
+            b.iter(|| {
+                let (result,itersize) = prove(black_box(&ex_logic), black_box(&rules), 2, 6, &tru);
+                size = itersize;
+                assert_eq!(result, tru)
+            });
+            warn!("customlang/prop_logic/prove1 {}", size);
+        }
     );
 
     let demorgan: RecExpr<PropositionalLogic>
         = "(== (!! (|| p q)) (&& (!! p) (!! q)))"
         .parse().unwrap();
     c.bench_function(
         "customlang/prop_logic/demorgan",
-        |b| b.iter(|| {
-            let result = prove(black_box(&demorgan), black_box(&rules), 1, 10, &tru);
-            assert_eq!(result, tru)
-        })
+        |b| {
+            let mut size = EGraphSize{num_classes:0, num_nodes:0, num_memo:0};
+            b.iter(|| {
+                let (result,itersize) = prove(black_box(&demorgan), black_box(&rules), 1, 10, &tru);
+                size = itersize;
+                assert_eq!(result, tru)
+            });
+            warn!("customlang/prop_logic/demorgan {}", size);
+        }
     );
 
     let frege: RecExpr<PropositionalLogic>
         = "(=> (=> p (=> q r)) (=> (=> p q) (=> p r)))"
         .parse().unwrap();
     c.bench_function(
         "customlang/prop_logic/freges_theorem",
-        |b| b.iter(|| {
-            let result = prove(black_box(&frege), black_box(&rules), 1, 10, &tru);
-            assert_eq!(result, tru)
-        })
+        |b| {
+            let mut size = EGraphSize{num_classes:0, num_nodes:0, num_memo:0};
+            b.iter(|| {
+                let (result,itersize) = prove(black_box(&frege), black_box(&rules), 1, 10, &tru);
+                size = itersize;
+                assert_eq!(result, tru)
+            });
+            warn!("customlang/prop_logic/freges_theorem {}", size);
+        }
     );
 }
 

benches/egraph.rs

@@ -15,7 +15,8 @@ use rand::Rng;
 use std::char;
 use criterion::{black_box, criterion_group, criterion_main, Criterion};
 use egg::{*};
-
+use egg_benchmark::*;
+use log::{warn};
 
 define_language! {
     pub enum BasicMath {
@@ -59,10 +60,17 @@ pub fn egraph_benchmark(c: &mut Criterion) {
 
     let expr: RecExpr<BasicMath> = nested_expr(2000).parse().unwrap();
     c.bench_function( "egraph/addexpr",
-        |b| b.iter(|| {
-            let runner: Runner<BasicMath,()> = Runner::default().with_expr(black_box(&expr));
-            runner
-        })
+        |b| {
+            let mut size = EGraphSize{num_classes:0, num_nodes:0, num_memo:0};
+            b.iter(|| {
+                let runner: Runner<BasicMath,()> = Runner::default().with_expr(black_box(&expr));
+                size.num_classes = runner.egraph.classes().count();
+                size.num_memo = runner.egraph.total_size();
+                size.num_nodes = runner.egraph.total_number_of_nodes();
+                runner
+            });
+            warn!("egraph/addexpr {}", size);
+        }
     );
 }
 

benches/symbollang/basic_maths.rs

@@ -1,6 +1,7 @@
 use criterion::{black_box, criterion_group, criterion_main, Criterion};
 use egg::*;
-use egg_benchmark::simplify;
+use egg_benchmark::{simplify, EGraphSize};
+use log::{warn};
 
 define_language! {
     pub enum BasicMath {
@@ -50,16 +51,16 @@ pub fn basic_maths_rules() -> Vec<Rewrite<SymbolLang, ()>> {
         rewrite!("power-distr-1"; "(^ (* ?x ?y) ?z)" => "(* (^ ?x ?z) (^ ?y ?z))"),
         rewrite!("power-distr-2"; "(* (^ ?x ?z) (^ ?y ?z))" => "(^ (* ?x ?y) ?z)"),
         //(x^p)^q == x^(p * q)
-        rewrite!("power-power-1"; "(^ (^ ?x ?p) ?q)" => "(^ ?x (+ ?p ?q))"),
-        rewrite!("power-power-2"; "(^ ?x (+ ?p ?q))" => "(^ (^ ?x ?p) ?q)"),
+        rewrite!("power-power-1"; "(^ (^ ?x ?p) ?q)" => "(^ ?x (* ?p ?q))"),
+        rewrite!("power-power-2"; "(^ ?x (* ?p ?q))" => "(^ (^ ?x ?p) ?q)"),
         //x^0 --> 1
         rewrite!("power-x0"; "(^ ?x 0)" => "1"),
         //0^x --> 0
         rewrite!("power-0x"; "(^ 0 ?x)" => "0"),
         //1^x --> 1
         rewrite!("power-1x"; "(^ 1 ?x)" => "1"),
         //x^1 --> x
-        rewrite!("power-x1"; "(^ 1 ?x)" => "?x"),
+        rewrite!("power-x1"; "(^ ?x 1)" => "?x"),
         //inv(x) == x^(-1)
         rewrite!("power-inv"; "(inv ?x)" => "(^ ?x (- 1))")
     ]
@@ -69,21 +70,33 @@ pub fn basic_maths_rules() -> Vec<Rewrite<SymbolLang, ()>> {
 pub fn basic_maths_benchmark(c: &mut Criterion) {
     let rules = basic_maths_rules();
     let expr = "(+ a (+ b (+ (* 0 c) d)))".parse().unwrap();
+
     c.bench_function(
         "basic_maths/simpl1",
-        |b| b.iter(|| {
-            simplify(black_box(&expr), black_box(&rules), 8);
-            //assert_eq!(result, "(+ d (+ b a))");
-        })
+        |b| {
+            let mut size = EGraphSize{num_classes:0, num_nodes:0, num_memo:0};
+            b.iter(|| {
+                let (result,itersize) = simplify(black_box(&expr), black_box(&rules), 8);
+                size=itersize;
+                result
+                //assert_eq!(result, "(+ d (+ b a))");
+            });
+            warn!("basic_maths/simpl1 {}", size);
+        }
     );
 
     let expr = "(+ (+ (+ 0 (* (* 1 foo) 0)) (* a 0)) a)".parse().unwrap();
     c.bench_function(
         "basic_maths/simpl2",
-        |b| b.iter(|| {
-            let result =  simplify(black_box(&expr), black_box(&rules), 8);
-            assert_eq!(result, "a".parse().unwrap());
-        })
+        |b| {
+            let mut size = EGraphSize{num_classes:0, num_nodes:0, num_memo:0};
+            b.iter(|| {
+                let (result,itersize) = simplify(black_box(&expr), black_box(&rules), 8);
+                size=itersize;
+                assert_eq!(result, "a".parse().unwrap());
+            });
+            warn!("basic_maths/simpl2 {}", size);
+        }
     );
 }
 

benches/symbollang/calc_logic.rs

@@ -1,6 +1,7 @@
 use criterion::{black_box, criterion_group, criterion_main, Criterion};
 use egg::*;
 use egg_benchmark::*;
+use log::{warn};
 
 // ## Theory of Calculational Logic
 // https://www.cs.cornell.edu/gries/Logic/Axioms.html
@@ -80,20 +81,26 @@ pub fn calc_logic_benchmark(c: &mut Criterion) {
 
     let demorgan: RecExpr<SymbolLang> = "(== (!! (|| p q)) (&& (!! p) (!! q)))".parse().unwrap();
     c.bench_function("calc_logic/demorgan", |b| {
+        let mut size = EGraphSize{num_classes:0, num_nodes:0, num_memo:0};
         b.iter(|| {
-            let res = prove(black_box(&demorgan), black_box(&rules), 1, 10, &tru);
+            let (res,itersize) = prove(black_box(&demorgan), black_box(&rules), 1, 10, &tru);
+            size = itersize;
             assert!(tru.eq(&res))
-        })
+        });
+        warn!("calc_logic/demorgan {}", size);
     });
 
     let frege: RecExpr<SymbolLang> = "(=> (=> p (=> q r)) (=> (=> p q) (=> p r)))"
         .parse()
         .unwrap();
     c.bench_function("calc_logic/freges_theorem", |b| {
+        let mut size = EGraphSize{num_classes:0, num_nodes:0, num_memo:0};
         b.iter(|| {
-            let res = prove(black_box(&frege), black_box(&rules), 2, 10, &tru);
+            let (res,itersize) = prove(black_box(&frege), black_box(&rules), 2, 10, &tru);
+            size = itersize;
             assert!(tru.eq(&res))
-        })
+        });
+        warn!("calc_logic/freges_theorem {}", size);
     });
 }