Skip to content

Commit

Permalink
nits
Browse files Browse the repository at this point in the history
  • Loading branch information
eytans committed Jun 22, 2024
1 parent 462a06c commit 70a6908
Showing 1 changed file with 19 additions and 13 deletions.
32 changes: 19 additions & 13 deletions src/explain.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@ use num_bigint::BigUint;
use num_traits::identities::{One, Zero};
use symbolic_expressions::Sexp;

use crate::Symbol;
use crate::{
Analysis, EClass, ENodeOrVar, FromOp, HashMap, HashSet, Id, Language, PatternAst,
RecExpr, Rewrite, UnionFind, util::pretty_print, Var,
util::pretty_print, Analysis, EClass, ENodeOrVar, FromOp, HashMap, HashSet, Id, Language,
PatternAst, RecExpr, Rewrite, UnionFind, Var,
};
use crate::Symbol;

type ProofCost = BigUint;

Expand Down Expand Up @@ -1287,12 +1287,7 @@ impl<'x, L: Language> ExplainNodes<'x, L> {
}

let adj = self.explain_adjacent(connection, cache, enode_cache, false);
let mut exp = self.explain_enode_existance(
existance,
adj,
cache,
enode_cache,
);
let mut exp = self.explain_enode_existance(existance, adj, cache, enode_cache);
exp.push(rest_of_proof);
return exp;
}
Expand Down Expand Up @@ -2063,18 +2058,29 @@ mod tests {
use crate::SymbolLang;
init_logger();

let rws: Vec<Rewrite<SymbolLang, ()>> = [rewrite!("makeb"; "a" => "b"), rewrite!("makec"; "b" => "c")].iter().cloned().collect();
let mut egraph = Runner::default().with_explanations_enabled()
let rws: Vec<Rewrite<SymbolLang, ()>> =
[rewrite!("makeb"; "a" => "b"), rewrite!("makec"; "b" => "c")]
.iter()
.cloned()
.collect();
let mut egraph = Runner::default()
.with_explanations_enabled()
.without_explanation_length_optimization()
.with_expr(&"a".parse().unwrap())
.run(&rws).egraph;
.run(&rws)
.egraph;
egraph.rebuild();
let a: Symbol = "a".parse().unwrap();
let b: Symbol = "b".parse().unwrap();
let c: Symbol = "c".parse().unwrap();
let mut exp = egraph.explain_existance(&"c".parse().unwrap());
println!("{:?}", exp.make_flat_explanation());
assert_eq!(exp.make_flat_explanation().len(), 3, "Expected 3 steps, got {:?}", exp.make_flat_explanation());
assert_eq!(
exp.make_flat_explanation().len(),
3,
"Expected 3 steps, got {:?}",
exp.make_flat_explanation()
);
}
}

Expand Down

0 comments on commit 70a6908

Please sign in to comment.