diff --git a/Cargo.toml b/Cargo.toml index 20562ba..40fe10d 100644 --- a/Cargo.toml +++ b/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" diff --git a/Makefile b/Makefile index 95aecda..c37fcc3 100644 --- a/Makefile +++ b/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 diff --git a/benches/benchmarks.rs b/benches/benchmarks.rs index eea4564..8d1bf5d 100644 --- a/benches/benchmarks.rs +++ b/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, diff --git a/benches/customlang/basic_maths.rs b/benches/customlang/basic_maths.rs index cfc0f17..881bd55 100644 --- a/benches/customlang/basic_maths.rs +++ b/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,8 +51,8 @@ pub fn basic_maths_rules() -> Vec> { 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 @@ -59,7 +60,7 @@ pub fn basic_maths_rules() -> Vec> { //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> { 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 = "(+ 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); + } ); } diff --git a/benches/customlang/calc_logic.rs b/benches/customlang/calc_logic.rs index 5d4de94..532b0bf 100644 --- a/benches/customlang/calc_logic.rs +++ b/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 = "(== (!! (|| 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 = "(=> (=> 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); }); } diff --git a/benches/customlang/prop_logic.rs b/benches/customlang/prop_logic.rs index b569db1..429ff84 100644 --- a/benches/customlang/prop_logic.rs +++ b/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,10 +91,15 @@ 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 @@ -101,10 +107,15 @@ pub fn propositional_logic_benchmark(c: &mut Criterion) { .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 @@ -112,10 +123,15 @@ pub fn propositional_logic_benchmark(c: &mut Criterion) { .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); + } ); } diff --git a/benches/egraph.rs b/benches/egraph.rs index e046d06..1d4c8fe 100644 --- a/benches/egraph.rs +++ b/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 = nested_expr(2000).parse().unwrap(); c.bench_function( "egraph/addexpr", - |b| b.iter(|| { - let runner: Runner = 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 = 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); + } ); } diff --git a/benches/symbollang/basic_maths.rs b/benches/symbollang/basic_maths.rs index bf1235a..1e5b232 100644 --- a/benches/symbollang/basic_maths.rs +++ b/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,8 +51,8 @@ pub fn basic_maths_rules() -> Vec> { 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 @@ -59,7 +60,7 @@ pub fn basic_maths_rules() -> Vec> { //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> { 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); + } ); } diff --git a/benches/symbollang/calc_logic.rs b/benches/symbollang/calc_logic.rs index e706488..5f2efd5 100644 --- a/benches/symbollang/calc_logic.rs +++ b/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 = "(== (!! (|| 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 = "(=> (=> 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); }); } diff --git a/benches/symbollang/prop_logic.rs b/benches/symbollang/prop_logic.rs index eb6c83d..c356953 100644 --- a/benches/symbollang/prop_logic.rs +++ b/benches/symbollang/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 { @@ -89,20 +90,30 @@ pub fn propositional_logic_benchmark(c: &mut Criterion) { = "(|| (!! (&& (|| (!! p) q) (&& (|| (!! r) s) (|| p r)))) (|| q s))" .parse().unwrap(); c.bench_function( "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); + assert_eq!(result, tru); + size = itersize; + }); + warn!("prop_logic/prove1 {}", size); + } ); let demorgan: RecExpr = "(== (!! (|| p q)) (&& (!! p) (!! q)))" .parse().unwrap(); c.bench_function( "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!("prop_logic/demorgan {}", size); + } ); let frege: RecExpr @@ -110,10 +121,15 @@ pub fn propositional_logic_benchmark(c: &mut Criterion) { .parse().unwrap(); c.bench_function( "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!("prop_logic/freges_theorem {}", size); + } ); } diff --git a/scripts/load_results.jl b/scripts/load_results.jl index 8d79e75..c38bdfa 100644 --- a/scripts/load_results.jl +++ b/scripts/load_results.jl @@ -42,11 +42,12 @@ function load_results(path::String) benchpaths = map(d -> joinpath(path, d, "new", "estimates.json"), dirs) crit_results = OrderedDict(bench => JSON.parsefile(path) for (bench, path) in zip(dirs, benchpaths)) + z75 = 1.15 z95 = 1.96 # output point estimates - OrderedDict( + od = OrderedDict( bench => Dict( "median"=> d["median"]["point_estimate"], "mean" => d["mean"]["point_estimate"], @@ -56,6 +57,61 @@ function load_results(path::String) ) for (bench, d) in crit_results ) + + + # parse egraph size from logs + pat = r"\[[^\]]+] (?.+) n_classes: (?\d+), n_nodes: (?\d+), n_memo: (?\d+)" + open("./target/egg-log.txt", "r") do io + d = Dict() + for line in eachline(io) + m = match(pat, line) + !isnothing(m) || continue + bench = replace(m["bench"], "/" => "_") + n_classes = parse(Int,m["n_classes"]) + n_nodes = parse(Int, m["n_nodes"]) + n_memo = parse(Int, m["n_memo"]) + + (v1,v2,v3) = get!(d, bench, (UInt64[],UInt64[],UInt64[])) + push!(v1, n_classes); push!(v2, n_nodes); push!(v3, n_memo) + end + + avg(xs) = sum(xs) / length(xs) + for (bench, vectors) in d + push!(od[bench], "n_classes_avg" => avg(vectors[1])) + push!(od[bench], "n_nodes_avg" => avg(vectors[2])) + push!(od[bench], "n_memo_avg" => avg(vectors[3])) + end + end + od +end + +function load_size_results!(od) + # parse egraph size from logs + pat1 = r".*Info.*Running benchmarks for [^@]+@(?[^:]+):" + # [ Info: Running benchmarks for Metatheory@31db7e8: + pat2 = r"(?.+) n_classes: (?\d+), n_nodes: (?\d+), n_memo: (?\d+)" + open("./target/mt_results/mt-log.txt", "r") do io + curbranch = "" + avg(xs) = sum(xs) / length(xs) + for line in eachline(io) + m1 = match(pat1, line) + !isnothing(m1) && (curbranch = m1["branch"]) + + m2 = match(pat2, line) + !isnothing(m2) || continue + + bench = m2["bench"] + n_classes = parse(Int,m2["n_classes"]) + n_nodes = parse(Int, m2["n_nodes"]) + n_memo = parse(Int, m2["n_memo"]) + + push!(od[curbranch][bench], "n_classes_avg" => n_classes) + push!(od[curbranch][bench], "n_nodes_avg" => n_nodes) + push!(od[curbranch][bench], "n_memo_avg" => n_memo) + end + + end + od end function format_val(val::Dict; confidence_interval=true) @@ -70,21 +126,38 @@ function format_val(val::Dict; confidence_interval=true) elseif haskey(val, "median") unit, unit_name = val["median"]>1e6 ? (1e-6, "ms") : (1e-3, "μs") @sprintf("%.3g %s", val["median"] * unit, unit_name) + elseif haskey(val, "median ratio") + @sprintf("%.3f", val["median ratio"]) else - @sprintf("%.3g", val["speedup"]) + "" end end format_val(::Missing; kw...) = @sprintf("") -function ratio_column!(combined_results, c1, c2, key="median") + +function format_size(val::Dict) + if haskey(val, "n_classes_avg") + @sprintf("%i %i %i", val["n_classes_avg"], val["n_nodes_avg"], val["n_memo_avg"]) + elseif haskey(val, "n_classes_avg ratio") + @sprintf("%.3f %.3f", val["n_classes_avg ratio"], val["n_nodes_avg ratio"]) + else + "" + end +end +format_size(::Missing; kw...) = @sprintf("") + +function ratio_column!(combined_results, c1, c2, ratiokeys...) all_keys = combined_results[c1] |> keys col = OrderedDict{String,Dict}() for row in all_keys if haskey(combined_results[c2], row) - a = combined_results[c1][row][key] - b = combined_results[c2][row][key] - ratio = a/b - col[row] = Dict("speedup"=>a/b) + for rkey in ratiokeys + a = get(combined_results[c1][row], rkey, nothing) + b = get(combined_results[c2][row], rkey, nothing) + !isnothing(a) && !isnothing(b) || continue + + get!(col, row, Dict())["$rkey ratio"] = a/b + end end end @@ -97,12 +170,13 @@ air = AirspeedVelocity.load_results( "Metatheory", BRANCHES, input_dir=MT_RESULTS_DIR ) +load_size_results!(air) egg = load_results(EGG_RESULTS_DIR) egg_customlang = Dict(k=>v for (k,v) in egg if occursin("customlang", k)) egg_symbollang = Dict(k=>v for (k,v) in egg if k ∉ keys(egg_customlang)) -egg_customlang = Dict(replace(k, "customlang_"=>"")=>v for (k,v) in egg_customlang) +egg_customlang = Dict(replace(k, "customlang_" => "")=>v for (k,v) in egg_customlang) results = OrderedDict( "egg-sym" => egg_symbollang, "egg-cust" => egg_customlang, @@ -114,16 +188,16 @@ end new_res = OrderedDict( rev => OrderedDict( - replace(k, "/"=>"_") => v for (k,v) in d + replace(k, "/" => "_") => v for (k,v) in d ) for (rev, d) in results ) - -ratio_column!(new_res, "egg-sym", "MT@$(BRANCHES[1])") -ratio_column!(new_res, "egg-cust", "MT@$(BRANCHES[1])") +ratiokeys = ("median", "n_classes_avg", "n_nodes_avg") +ratio_column!(new_res, "egg-sym", "MT@$(BRANCHES[1])", ratiokeys...) +ratio_column!(new_res, "egg-cust", "MT@$(BRANCHES[1])", ratiokeys...) for b2 in BRANCHES[2:end] - ratio_column!(new_res, "MT@$b2", "MT@$(BRANCHES[1])") + ratio_column!(new_res, "MT@$b2", "MT@$(BRANCHES[1])", ratiokeys...) end table = AirspeedVelocity.create_table( new_res, @@ -136,4 +210,19 @@ if !isnothing(OUTPUT) write(io, table) end end -print(table) +println(table) + +# append another table with size information +table = AirspeedVelocity.create_table( + new_res, + formatter=v->format_size(v) +) + +if !isnothing(OUTPUT) + @info "Saving table at $(OUTPUT)" + open(OUTPUT, "a") do io + println(io) + write(io, table) + end +end +println(table) diff --git a/src/lib.rs b/src/lib.rs index d33b057..82e4db3 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,10 +1,25 @@ use egg::*; +pub struct EGraphSize { + pub num_classes: usize, + pub num_memo: usize, + pub num_nodes: usize +} + +use std::fmt; + +impl fmt::Display for EGraphSize { + fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result { + write!(fmt, "n_classes: {}, n_nodes: {}, n_memo: {}", self.num_classes, self.num_nodes, self.num_memo) + } +} + + pub fn simplify( expr: &RecExpr, rules: &Vec>, timeout: usize, -) -> RecExpr { +) -> (RecExpr, EGraphSize) { // run rules let scheduler = BackoffScheduler::default(); let runner = Runner::default() @@ -17,7 +32,11 @@ pub fn simplify( // extract shortest expression let extractor = Extractor::new(&runner.egraph, AstSize); let (_, best) = extractor.find_best(runner.roots[0]); - best + let size = EGraphSize { + num_classes: runner.egraph.classes().count(), + num_memo: runner.egraph.total_size(), + num_nodes: runner.egraph.total_number_of_nodes() }; + (best, size) } pub fn prove( @@ -26,7 +45,12 @@ pub fn prove( steps: usize, timeout: usize, tru: &RecExpr, -) -> RecExpr { +) -> (RecExpr, EGraphSize) { + let mut n_classes = 0; + let mut n_memo = 0; + let mut n_nodes = 0; + // We start with the provided expr and in the following iterations start with the expr returned by the previous iteration. + // As soon as expr == true all subsequent calls of .run() will return immediately because of the hook. let out: RecExpr = (0..steps).fold(expr.clone(), |expr, _| { let scheduler = BackoffScheduler::default() .with_initial_match_limit(6000) @@ -51,7 +75,12 @@ pub fn prove( let root = runner.roots[0]; let extractor = Extractor::new(&runner.egraph, AstSize); let (_, best) = extractor.find_best(root); + n_classes += runner.egraph.classes().count(); + n_memo += runner.egraph.total_size(); + n_nodes += runner.egraph.total_number_of_nodes(); best }); - out + let size = EGraphSize { num_classes: n_classes, num_memo: n_memo, num_nodes: n_nodes }; + + (out, size) } diff --git a/src/main.rs b/src/main.rs index 499671e..2b4d931 100644 --- a/src/main.rs +++ b/src/main.rs @@ -91,7 +91,8 @@ pub fn main() { // demorgan let ex_demorgan: RecExpr = "(== (!! (|| p q)) (&& (!! p) (!! q)))" .parse().unwrap(); - println!("demorgan: {}", prove(&ex_demorgan, &rules, 1, 10, &tru)); + let (res, size) = prove(&ex_demorgan, &rules, 1, 10, &tru); + println!("demorgan: {} {}", res, size); println!("simplification time {}", apply_time.elapsed().as_secs_f64()); @@ -102,7 +103,8 @@ pub fn main() { // frege let ex_frege: RecExpr = "(=> (=> p (=> q r)) (=> (=> p q) (=> p r)))" .parse().unwrap(); - println!("frege: {}", prove(&ex_frege, &rules, 1, 10, &tru)); + let (res, size) = prove(&ex_frege, &rules, 1, 10, &tru); + println!("frege: {} {}", res, size); println!("simplification time {}", apply_time.elapsed().as_secs_f64()); @@ -117,8 +119,8 @@ pub fn main() { // let ex_logic = "(== p p)"; let ex_logic: RecExpr = s.parse().unwrap(); - let expr = prove(&ex_logic, &rules, 2, 6, &tru); - println!("logic: {}", tru.eq(&expr)); + let (expr, size) = prove(&ex_logic, &rules, 2, 6, &tru); + println!("logic: {} {}", tru.eq(&expr), size); println!("simplification time {}", apply_time.elapsed().as_secs_f64()); }