Skip to content

Commit

Permalink
Merge pull request #63 from ninehusky/ninehusky-improve-logs
Browse files Browse the repository at this point in the history 
Improve logs to have rule search/apply duration
  • Loading branch information
@ninehusky
ninehusky authored Jan 20, 2025
2 parents d6b9436 + b7d4f03 commit cd9f425
Show file tree
Hide file tree
Showing 3 changed files with 254 additions and 9 deletions.
217 changes: 217 additions & 0 deletions rules.txt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,217 @@

running 1 test
Value: (Const -1 )
Value: (Const 0 )
Value: (Const 1 )
Predicate: (Neq (Const -1 ) (Const -1 ) )
Predicate: (Neq (Const -1 ) (Const 0 ) )
Predicate: (Neq (Const -1 ) (Const 1 ) )
Predicate: (Neq (Const -1 ) (Var a ) )
Predicate: (Neq (Const -1 ) (Var b ) )
Predicate: (Neq (Const -1 ) (Var c ) )
Predicate: (Neq (Const -1 ) (Var d ) )
Predicate: (Neq (Const 0 ) (Const -1 ) )
Predicate: (Neq (Const 0 ) (Const 0 ) )
Predicate: (Neq (Const 0 ) (Const 1 ) )
Predicate: (Neq (Const 0 ) (Var a ) )
Predicate: (Neq (Const 0 ) (Var b ) )
Predicate: (Neq (Const 0 ) (Var c ) )
Predicate: (Neq (Const 0 ) (Var d ) )
Predicate: (Neq (Const 1 ) (Const -1 ) )
Predicate: (Neq (Const 1 ) (Const 0 ) )
Predicate: (Neq (Const 1 ) (Const 1 ) )
Predicate: (Neq (Const 1 ) (Var a ) )
Predicate: (Neq (Const 1 ) (Var b ) )
Predicate: (Neq (Const 1 ) (Var c ) )
Predicate: (Neq (Const 1 ) (Var d ) )
Predicate: (Neq (Var a ) (Const -1 ) )
Predicate: (Neq (Var a ) (Const 0 ) )
Predicate: (Neq (Var a ) (Const 1 ) )
Predicate: (Neq (Var a ) (Var a ) )
Predicate: (Neq (Var a ) (Var b ) )
Predicate: (Neq (Var a ) (Var c ) )
Predicate: (Neq (Var a ) (Var d ) )
Predicate: (Neq (Var b ) (Const -1 ) )
Predicate: (Neq (Var b ) (Const 0 ) )
Predicate: (Neq (Var b ) (Const 1 ) )
Predicate: (Neq (Var b ) (Var a ) )
Predicate: (Neq (Var b ) (Var b ) )
Predicate: (Neq (Var b ) (Var c ) )
Predicate: (Neq (Var b ) (Var d ) )
Predicate: (Neq (Var c ) (Const -1 ) )
Predicate: (Neq (Var c ) (Const 0 ) )
Predicate: (Neq (Var c ) (Const 1 ) )
Predicate: (Neq (Var c ) (Var a ) )
Predicate: (Neq (Var c ) (Var b ) )
Predicate: (Neq (Var c ) (Var c ) )
Predicate: (Neq (Var c ) (Var d ) )
Predicate: (Neq (Var d ) (Const -1 ) )
Predicate: (Neq (Var d ) (Const 0 ) )
Predicate: (Neq (Var d ) (Const 1 ) )
Predicate: (Neq (Var d ) (Var a ) )
Predicate: (Neq (Var d ) (Var b ) )
Predicate: (Neq (Var d ) (Var c ) )
Predicate: (Neq (Var d ) (Var d ) )
Predicate: (Gt (Const -1 ) (Const -1 ) )
Predicate: (Gt (Const -1 ) (Const 0 ) )
Predicate: (Gt (Const -1 ) (Const 1 ) )
Predicate: (Gt (Const -1 ) (Var a ) )
Predicate: (Gt (Const -1 ) (Var b ) )
Predicate: (Gt (Const -1 ) (Var c ) )
Predicate: (Gt (Const -1 ) (Var d ) )
Predicate: (Gt (Const 0 ) (Const -1 ) )
Predicate: (Gt (Const 0 ) (Const 0 ) )
Predicate: (Gt (Const 0 ) (Const 1 ) )
Predicate: (Gt (Const 0 ) (Var a ) )
Predicate: (Gt (Const 0 ) (Var b ) )
Predicate: (Gt (Const 0 ) (Var c ) )
Predicate: (Gt (Const 0 ) (Var d ) )
Predicate: (Gt (Const 1 ) (Const -1 ) )
Predicate: (Gt (Const 1 ) (Const 0 ) )
Predicate: (Gt (Const 1 ) (Const 1 ) )
Predicate: (Gt (Const 1 ) (Var a ) )
Predicate: (Gt (Const 1 ) (Var b ) )
Predicate: (Gt (Const 1 ) (Var c ) )
Predicate: (Gt (Const 1 ) (Var d ) )
Predicate: (Gt (Var a ) (Const -1 ) )
Predicate: (Gt (Var a ) (Const 0 ) )
Predicate: (Gt (Var a ) (Const 1 ) )
Predicate: (Gt (Var a ) (Var a ) )
Predicate: (Gt (Var a ) (Var b ) )
Predicate: (Gt (Var a ) (Var c ) )
Predicate: (Gt (Var a ) (Var d ) )
Predicate: (Gt (Var b ) (Const -1 ) )
Predicate: (Gt (Var b ) (Const 0 ) )
Predicate: (Gt (Var b ) (Const 1 ) )
Predicate: (Gt (Var b ) (Var a ) )
Predicate: (Gt (Var b ) (Var b ) )
Predicate: (Gt (Var b ) (Var c ) )
Predicate: (Gt (Var b ) (Var d ) )
Predicate: (Gt (Var c ) (Const -1 ) )
Predicate: (Gt (Var c ) (Const 0 ) )
Predicate: (Gt (Var c ) (Const 1 ) )
Predicate: (Gt (Var c ) (Var a ) )
Predicate: (Gt (Var c ) (Var b ) )
Predicate: (Gt (Var c ) (Var c ) )
Predicate: (Gt (Var c ) (Var d ) )
Predicate: (Gt (Var d ) (Const -1 ) )
Predicate: (Gt (Var d ) (Const 0 ) )
Predicate: (Gt (Var d ) (Const 1 ) )
Predicate: (Gt (Var d ) (Var a ) )
Predicate: (Gt (Var d ) (Var b ) )
Predicate: (Gt (Var d ) (Var c ) )
Predicate: (Gt (Var d ) (Var d ) )
size: 1
workload len: 7
running rewrites...
i'm done running rewrites
size: 2
workload len: 7
running rewrites...
i'm done running rewrites
size: 3
workload len: 21
running rewrites...
i'm done running rewrites
rule: if (Gt (Const -1 ) ?a ) then (Neg ?a ) ~> (Abs ?a )
rule: if (Gt ?a (Const -1 ) ) then (Abs ?a ) ~> ?a
running rewrites...
i'm done running rewrites
size: 4
workload len: 35
running rewrites...
i'm done running rewrites
rule: if (Gt ?a (Const -1 ) ) then (Neg (Neg ?a ) ) ~> (Abs (Abs ?a ) )
rule: if (Gt (Const -1 ) ?a ) then (Neg (Neg ?a ) ) ~> (Neg (Abs ?a ) )
rule: if (Gt (Const -1 ) ?a ) then (Neg (Abs ?a ) ) ~> ?a
rule: if (Gt ?a (Const -1 ) ) then (Neg (Abs ?a ) ) ~> (Neg ?a )
rule: if (Gt ?a (Const -1 ) ) then (Abs (Neg ?a ) ) ~> ?a
running rewrites...
i'm done running rewrites
size: 5
workload len: 357
running rewrites...
i'm done running rewrites
rule: (Sub ?a (Const 1 ) ) ~> (Add (Const -1 ) ?a )
rule: (Add ?a (Const -1 ) ) ~> (Sub ?a (Const 1 ) )
rule: (Mul ?a (Const 0 ) ) ~> (Neq (Const 1 ) (Const 1 ) )
rule: (Neq ?a ?a ) ~> (Neq (Const 1 ) (Const 1 ) )
rule: if (Gt ?a (Const -1 ) ) then (Gt (Const -1 ) ?a ) ~> (Neq (Const 1 ) (Const 1 ) )
rule: if (Gt ?a (Const -1 ) ) then (Gt (Const 0 ) ?a ) ~> (Neq (Const 1 ) (Const 1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt ?a (Const 1 ) ) ~> (Neq (Const 1 ) (Const 1 ) )
rule: if (Gt ?a (Const 0 ) ) then (Gt (Const 1 ) ?a ) ~> (Neq (Const 1 ) (Const 1 ) )
rule: (Sub ?a ?a ) ~> (Neq (Const 1 ) (Const 1 ) )
rule: (Gt ?a ?a ) ~> (Neq (Const 1 ) (Const 1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt ?a (Const -1 ) ) ~> (Neq (Const 1 ) (Const 1 ) )
rule: (Mul (Const 0 ) ?a ) ~> (Neq (Const 1 ) (Const 1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt ?a (Const 0 ) ) ~> (Neq (Const 1 ) (Const 1 ) )
rule: (Mul ?a (Const 0 ) ) ~> (Div (Const 0 ) (Const -1 ) )
rule: (Mul ?a (Const 0 ) ) ~> (Add (Const 0 ) (Const 0 ) )
rule: (Mul ?a (Const 0 ) ) ~> (Div (Const 0 ) (Const 1 ) )
rule: (Mul ?a (Const 0 ) ) ~> (Add (Const -1 ) (Const 1 ) )
rule: (Mul ?a (Const 0 ) ) ~> (Const 0 )
rule: (Div ?a (Const -1 ) ) ~> (Neg ?a )
rule: (Div ?a (Const -1 ) ) ~> (Sub (Const 0 ) ?a )
rule: (Mul (Const -1 ) ?a ) ~> (Div ?a (Const -1 ) )
rule: (Neq ?a ?a ) ~> (Add (Const 0 ) (Const 0 ) )
rule: (Neq ?a ?a ) ~> (Div (Const 0 ) (Const 1 ) )
rule: (Neq ?a ?a ) ~> (Add (Const -1 ) (Const 1 ) )
rule: (Neq ?a ?a ) ~> (Const 0 )
rule: (Neg ?a ) ~> (Sub (Const 0 ) ?a )
rule: if (Gt (Const -1 ) ?a ) then (Sub (Const 0 ) ?a ) ~> (Abs (Abs ?a ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Div (Const -1 ) (Const -1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Neq ?a (Const -1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Const 1 )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Neq (Const 0 ) (Const -1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Neq (Const 1 ) (Const -1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Div ?a ?a )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Mul (Const 1 ) (Const 1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Neq ?a (Const 0 ) )
rule: if (Gt ?a (Const 1 ) ) then (Gt (Const -1 ) ?a ) ~> (Div (Const 1 ) ?a )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Neq (Const -1 ) (Const 0 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Gt (Const 0 ) (Const -1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Add (Const 1 ) (Const 0 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Gt (Const 1 ) (Const -1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Neq (Const 1 ) (Const 0 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Div (Const 1 ) (Const 1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Neq (Const -1 ) ?a )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Neq (Const 0 ) ?a )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Neq (Const 1 ) ?a )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Neq ?a (Const 1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Add (Const 0 ) (Const 1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Neq (Const -1 ) (Const 1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Sub (Const 1 ) (Const 0 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Abs (Const -1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Neq (Const 0 ) (Const 1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Gt (Const -1 ) ?a ) ~> (Gt (Const 1 ) (Const 0 ) )
rule: if (Gt (Const -1 ) ?a ) then (Abs (Abs (Neg ?a ) ) ) ~> (Mul ?a (Const -1 ) )
rule: if (Gt (Const -1 ) ?a ) then (Mul (Const 1 ) ?a ) ~> (Neg (Abs (Abs ?a ) ) )
rule: (Mul (Const 1 ) ?a ) ~> (Add (Const 0 ) ?a )
rule: (Mul (Const 1 ) ?a ) ~> (Sub ?a (Const 0 ) )
rule: (Add ?a ?b ) ~> (Add ?b ?a )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Div (Const -1 ) (Const -1 ) )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Neq (Const -1 ) ?a )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Neq ?a (Const -1 ) )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Neq (Const 0 ) ?a )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Const 1 )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Neq (Const 0 ) (Const -1 ) )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Neq (Const 1 ) (Const -1 ) )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Mul (Const 1 ) (Const 1 ) )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Neq ?a (Const 0 ) )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Neq (Const -1 ) (Const 0 ) )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Gt (Const 0 ) (Const -1 ) )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Gt (Const 1 ) (Const -1 ) )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Neq (Const 1 ) (Const 0 ) )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Div (Const 1 ) (Const 1 ) )
rule: if (Neq (Const 1 ) ?a ) then (Gt ?a (Const 1 ) ) ~> (Gt ?a (Const 0 ) )
rule: if (Gt ?a (Const 1 ) ) then (Gt ?a (Const 1 ) ) ~> (Div ?a ?a )
test math::tests::check_math_rules ... FAILED

failures:

failures:
math::tests::check_math_rules

test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 0 filtered out; finished in 11.80s

writing flamegraph to "flamegraph.svg"
44 changes: 36 additions & 8 deletions src/chomper.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,13 +70,14 @@ pub trait Chomper {
/// Adds the given term to the e-graph.
/// Optionally, sets the eclass id of the term to the given id.
fn add_term(&self, term: &Sexp, egraph: &mut EGraph, eclass_id: Option<usize>) {
info!("adding term: {}", term);
let term = format_sexp(term);
let prog = format!("({} {})", UNIVERSAL_RELATION, term);
egraph.parse_and_run_program(None, &prog).unwrap();
if let Some(id) = eclass_id {
egraph
.parse_and_run_program(None, format!("(set (eclass {term}) {id})").as_str())
.unwrap();
let prog = format!("(set (eclass {term}) {id})", term = term, id = id);
info!("running program: {}", prog);
egraph.parse_and_run_program(None, &prog).unwrap();
}
}

Expand All @@ -102,7 +103,13 @@ pub trait Chomper {
"#
.to_string()
};
egraph.parse_and_run_program(None, &prog).unwrap();

let prog = format!("{prog}\n(print-stats)\n");

info!("running rewrites: {}", prog);

let results = egraph.parse_and_run_program(None, &prog).unwrap();
log_rewrite_stats(results);
}

/// Returns a map from e-class id to a candidate term in the e-class.
Expand Down Expand Up @@ -306,13 +313,13 @@ pub trait Chomper {
let mut old_workload = atoms.clone();
let mut max_eclass_id: usize = 1;
for size in 1..=max_size {
println!("size: {}", size);
info!("CONSIDERING PROGRAMS OF SIZE {}:", size);
let new_workload = atoms.clone().append(
language
.produce(&old_workload.clone())
.filter(Filter::MetricEq(Metric::Atoms, size)),
);
println!("workload len: {}", new_workload.force().len());
info!("workload len: {}", new_workload.force().len());
for term in &new_workload.force() {
self.add_term(term, &mut egraph, Some(max_eclass_id));
max_eclass_id += 1;
Expand All @@ -325,9 +332,9 @@ pub trait Chomper {
}
let mut seen_rules: HashSet<String> = Default::default();
loop {
println!("running rewrites...");
info!("trying to merge new terms using existing rewrites...");
self.run_rewrites(&mut egraph, None);
println!("i'm done running rewrites");
info!("i'm done running rewrites");

let candidates = self
.cvec_match(&mut egraph, &pvecs, &env)
Expand Down Expand Up @@ -355,6 +362,7 @@ pub trait Chomper {
info!("is derivable? {}", if derivable { "yes" } else { "no" });
if valid == ValidationResult::Valid && !derivable {
let rule = language.generalize_rule(&rule.clone());
info!("rule: {}", rule);
println!("rule: {}", rule);
rules.push(rule.clone());
self.add_rewrite(&mut egraph, &rule);
Expand Down Expand Up @@ -470,6 +478,26 @@ pub fn all_variables_bound(rule: &Rule) -> bool {
.all(|var| lhs_vars.contains(var))
}

fn log_rewrite_stats(outputs: Vec<String>) {
fn chop_off_seconds(s: &str) -> f64 {
s.split('s').next().unwrap().parse().unwrap()
}

let long_time = 0.0001;
let last_two = outputs.iter().rev().take(2).collect::<Vec<&String>>();
for line in last_two.iter().rev() {
// the last, third to last, and fifth to last tokens are the relevant ones.
let tokens = line.split_whitespace().collect::<Vec<&str>>();
let rebuild_time = chop_off_seconds(tokens.last().unwrap());
let apply_time = chop_off_seconds(tokens[tokens.len() - 3]);
let search_time = chop_off_seconds(tokens[tokens.len() - 5]);
if search_time > long_time || apply_time > long_time || rebuild_time > long_time {
info!("Running rewrites took a long time!");
info!("Egglog output:");
info!("{}", line);
}
}
}
/// A sample implementation of the Chomper trait for the MathLang language.
pub struct MathChomper;

Expand Down
2 changes: 1 addition & 1 deletion tests/math/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ pub mod tests {

#[test]
fn check_math_rules() {
env_logger::init();
let chomper = MathChomper;
let predicates = chomper.get_language().get_predicates();
let values = chomper.get_language().get_vals();
Expand Down Expand Up @@ -40,4 +41,3 @@ pub mod tests {
);
}
}

0 comments on commit cd9f425

Please sign in to comment.