diff --git a/Cargo.lock b/Cargo.lock index 0876bad..9e01200 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -106,9 +106,9 @@ checksum = "e78d4f1cc4ae33bbfc157ed5d5a5ef3bc29227303d595861deb238fcec4e9457" [[package]] name = "getrandom" -version = "0.2.5" +version = "0.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d39cd93900197114fa1fcb7ae84ca742095eed9442088988ae74fa744e930e77" +checksum = "9be70c98951c83b8d2f8f60d7065fa6d5146873094452a1008da8c2f1e4205ad" dependencies = [ "cfg-if", "libc", @@ -147,15 +147,15 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.118" +version = "0.2.125" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "06e509672465a0504304aa87f9f176f2b2b716ed8fb105ebe5c02dc6dce96a94" +checksum = "5916d2ae698f6de9bfb891ad7a8d65c09d232dc58cc4ac433c7da3b2fd84bc2b" [[package]] name = "memchr" -version = "2.4.1" +version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "308cc39be01b73d0d18f82a0e7b2a3df85245f84af96fdddc5d202d27e47b86a" +checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d" [[package]] name = "ppv-lite86" @@ -195,9 +195,9 @@ dependencies = [ [[package]] name = "regex" -version = "1.5.4" +version = "1.5.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d07a8629359eb56f1e2fb1652bb04212c072a87ba68546a04065d525673ac461" +checksum = "1a11647b6b25ff05a515cb92c365cec08801e83423a235b51e231e1808747286" dependencies = [ "aho-corasick", "memchr", @@ -244,9 +244,9 @@ checksum = "73b4b750c782965c211b42f022f59af1fbceabdd026623714f104152f1ec149f" [[package]] name = "serde" -version = "1.0.136" +version = "1.0.137" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ce31e24b01e1e524df96f1c2fdd054405f8d7376249a5110886fb4b658484789" +checksum = "61ea8d54c77f8315140a05f4c7237403bf38b72704d031543aa1d16abbf517d1" [[package]] name = "strsim" diff --git a/src/bdd.rs b/src/bdd.rs index 2981d6d..06bd14b 100644 --- a/src/bdd.rs +++ b/src/bdd.rs @@ -1,7 +1,6 @@ use itertools::Itertools; -use rustc_hash::FxHashMap; +use rustc_hash::{FxHashMap, FxHasher}; use std::cell::RefCell; -use std::collections::hash_map::DefaultHasher; use std::fmt; use std::fmt::{Debug, Display}; use std::hash::{Hash, Hasher}; @@ -55,29 +54,40 @@ impl From for usize { } } -// todo: place bdd items in a collection (hashmap?) -// when constructing a new bdd, check if it already exists in the collection. -// if it does, return a reference to the existing bdd. -// otherwise, create a new bdd and return a reference to it. +#[derive(Debug, Clone, Eq, PartialEq)] +pub struct BDD { + cached_hash: Option, + pub node: BDDNode, +} #[derive(Debug, Clone, Eq, PartialEq, Hash)] -pub enum BDD { +pub enum BDDNode { False, True, // Choice (true-subtree, symbol, false-subtree) Choice(Rc>, Symbol, Rc>), } +impl Hash for BDD { + fn hash(&self, state: &mut H) { + if let Some(cached) = self.cached_hash { + cached.hash(state); + } else { + self.node.hash(state); + } + } +} + impl From> for BDD { fn from(bdd: BDD) -> BDD { - match bdd { - BDD::False => BDD::False, - BDD::True => BDD::True, - BDD::Choice(true_subtree, symbol, false_subtree) => BDD::Choice( + match bdd.node { + BDDNode::False => BDD::new(&BDDNode::False), + BDDNode::True => BDD::new(&BDDNode::True), + BDDNode::Choice(true_subtree, symbol, false_subtree) => BDD::new(&BDDNode::Choice( Rc::new(BDD::from(true_subtree.as_ref().clone())), symbol.into(), Rc::new(BDD::from(false_subtree.as_ref().clone())), - ), + )), } } } @@ -101,18 +111,44 @@ impl Display for TruthTableEntry { impl Default for BDD { fn default() -> Self { - BDD::False + BDD::new(&BDDNode::False) } } impl BDD { pub fn get_hash(&self) -> u64 { - let mut s = DefaultHasher::new(); + let mut s = FxHasher::default(); self.hash(&mut s); s.finish() } } +impl BDD { + pub fn new(node: &BDDNode) -> BDD { + let mut result = BDD { + cached_hash: None, + node: node.clone(), + }; + + result.populate_hash(); + + result + } + + pub fn new_unoptimized(node: &BDDNode) -> BDD { + BDD { + cached_hash: None, + node: node.clone(), + } + } + + pub fn populate_hash(&mut self) { + let mut hasher = FxHasher::default(); + self.hash(&mut hasher); + self.cached_hash = Some(hasher.finish()); + } +} + #[derive(Debug, Clone, PartialEq, Eq)] pub struct BDDEnv { pub nodes: RefCell, Rc>>>, @@ -132,8 +168,8 @@ impl BDDEnv { // clean tries to reduce all duplicate subtrees to single nodes in the lookup table // this function currently has no effect, might be removed later pub fn clean(&self, root: Rc>) -> Rc> { - match root.as_ref() { - &BDD::Choice(ref l, ref s, ref r) => { + match root.as_ref().node { + BDDNode::Choice(ref l, ref s, ref r) => { let _l = self.find(l); let _r = self.find(r); @@ -165,8 +201,8 @@ impl BDDEnv { } pub fn node_list(&self, root: Rc>) -> Vec>> { - match root.as_ref() { - &BDD::Choice(ref l, _, ref r) => { + match root.as_ref().node { + BDDNode::Choice(ref l, _, ref r) => { let l_nodes = self.node_list(Rc::clone(l)); let r_nodes = self.node_list(Rc::clone(r)); @@ -177,7 +213,7 @@ impl BDDEnv { .cloned() .collect() } - &BDD::True | &BDD::False => vec![Rc::clone(&root)], + BDDNode::True | BDDNode::False => vec![Rc::clone(&root)], } } @@ -190,7 +226,7 @@ impl BDDEnv { false_subtree: Rc>, ) -> Rc> { // early simplification step - let ins = self.simplify(&Rc::new(BDD::Choice(true_subtree, symbol, false_subtree))); + let ins = self.simplify(&Rc::new(BDD::new_unoptimized(&BDDNode::Choice(true_subtree, symbol, false_subtree)))); // pre-borrow the nodes as mutable let mut nodes_borrow = self.nodes.borrow_mut(); @@ -200,17 +236,23 @@ impl BDDEnv { Rc::clone(subtree) } else { // only insert if it is not already in the lookup table - nodes_borrow.insert(ins.as_ref().clone(), Rc::clone(&ins)); - Rc::clone(&ins) + // first pre-compute the hash + let mut ins_populated = ins.as_ref().clone(); + ins_populated.populate_hash(); + let ins_toinsert = Rc::new(ins_populated); + + nodes_borrow.insert(ins_toinsert.as_ref().clone(), Rc::clone(&ins_toinsert)); + Rc::clone(&ins_toinsert) } } // find the true or false node in the lookup table and return a reference to it pub fn mk_const(&self, v: bool) -> Rc> { if v { - Rc::clone(self.nodes.borrow().get(&BDD::True).unwrap()) + // todo: return unoptimized node + Rc::clone(self.nodes.borrow().get(&BDD::new(&BDDNode::True)).unwrap()) } else { - Rc::clone(self.nodes.borrow().get(&BDD::False).unwrap()) + Rc::clone(self.nodes.borrow().get(&BDD::new(&BDDNode::False)).unwrap()) } } @@ -222,8 +264,11 @@ impl BDDEnv { pub fn new() -> Self { let mut nodes = FxHashMap::default(); - nodes.insert(BDD::True, Rc::new(BDD::True)); - nodes.insert(BDD::False, Rc::new(BDD::False)); + let true_node = BDD::new(&BDDNode::True); + let false_node = BDD::new(&BDDNode::False); + + nodes.insert(true_node.clone(), Rc::new(true_node)); + nodes.insert(false_node.clone(), Rc::new(false_node)); BDDEnv { nodes: RefCell::new(nodes), @@ -232,23 +277,25 @@ impl BDDEnv { // conjunction pub fn and(&self, a: Rc>, b: Rc>) -> Rc> { - match (a.as_ref(), b.as_ref()) { - (&BDD::False, _) | (_, &BDD::False) => self.mk_const(false), - (&BDD::True, _) => Rc::clone(&b), - (_, &BDD::True) => Rc::clone(&a), - (&BDD::Choice(ref at, ref va, ref af), &BDD::Choice(_, ref vb, _)) if va < vb => self - .mk_choice( + match (&a.as_ref().node, &b.as_ref().node) { + (BDDNode::False, _) | (_, BDDNode::False) => self.mk_const(false), + (BDDNode::True, _) => Rc::clone(&b), + (_, BDDNode::True) => Rc::clone(&a), + (BDDNode::Choice(ref at, ref va, ref af), BDDNode::Choice(_, ref vb, _)) if va < vb => { + self.mk_choice( self.and(Rc::clone(at), Rc::clone(&b)), va.clone(), self.and(Rc::clone(af), Rc::clone(&b)), - ), - (&BDD::Choice(_, ref va, _), &BDD::Choice(ref bt, ref vb, ref bf)) if vb < va => self - .mk_choice( + ) + } + (BDDNode::Choice(_, ref va, _), BDDNode::Choice(ref bt, ref vb, ref bf)) if vb < va => { + self.mk_choice( self.and(Rc::clone(bt), Rc::clone(&a)), vb.clone(), self.and(Rc::clone(bf), Rc::clone(&a)), - ), - (&BDD::Choice(ref at, ref va, ref af), &BDD::Choice(ref bt, ref vb, ref bf)) + ) + } + (BDDNode::Choice(ref at, ref va, ref af), BDDNode::Choice(ref bt, ref vb, ref bf)) if va == vb => { self.mk_choice( @@ -262,10 +309,10 @@ impl BDDEnv { } pub fn not(&self, a: Rc>) -> Rc> { - match *a.as_ref() { - BDD::False => self.mk_const(true), - BDD::True => self.mk_const(false), - BDD::Choice(ref at, ref va, ref af) => { + match a.as_ref().node { + BDDNode::False => self.mk_const(true), + BDDNode::True => self.mk_const(false), + BDDNode::Choice(ref at, ref va, ref af) => { self.mk_choice(self.not(Rc::clone(at)), va.clone(), self.not(Rc::clone(af))) } } @@ -424,10 +471,10 @@ impl BDDEnv { // existential quantification pub fn exists_impl(&self, s: S, b: Rc>) -> Rc> { - match b.as_ref() { - &BDD::False | &BDD::True => b, - &BDD::Choice(ref t, ref v, ref f) if *v == s => self.or(Rc::clone(t), Rc::clone(f)), - &BDD::Choice(ref t, ref v, ref f) => self.mk_choice( + match b.as_ref().node { + BDDNode::False | BDDNode::True => b, + BDDNode::Choice(ref t, ref v, ref f) if *v == s => self.or(Rc::clone(t), Rc::clone(f)), + BDDNode::Choice(ref t, ref v, ref f) => self.mk_choice( self.exists_impl(s.clone(), Rc::clone(t)), v.clone(), self.exists_impl(s, Rc::clone(f)), @@ -457,8 +504,8 @@ impl BDDEnv { } pub fn model(&self, a: Rc>) -> Rc> { - match a.as_ref() { - &BDD::Choice(ref t, ref v, ref f) => { + match a.as_ref().node { + BDDNode::Choice(ref t, ref v, ref f) => { let lhs = self.model(Rc::clone(t)); let rhs = self.model(Rc::clone(f)); if lhs != self.mk_const(false) { @@ -469,7 +516,7 @@ impl BDDEnv { self.mk_const(false) } } - &BDD::True | &BDD::False => a, + BDDNode::True | BDDNode::False => a, } } @@ -478,17 +525,17 @@ impl BDDEnv { // the second item determines the truth value for b pub fn infer(&self, a: Rc>, b: S) -> (bool, bool) { let ff = self.implies(a, self.var(b)); - match ff.as_ref() { - BDD::Choice(_, _, _) => (false, false), - BDD::True => (true, true), - BDD::False => (true, false), + match ff.as_ref().node { + BDDNode::Choice(_, _, _) => (false, false), + BDDNode::True => (true, true), + BDDNode::False => (true, false), } } // simplify removes a choice node if both subtrees are equivalent pub fn simplify(&self, a: &Rc>) -> Rc> { - let result = match a.as_ref() { - &BDD::Choice(ref t, _, ref f) if t.as_ref() == f.as_ref() => t, + let result = match a.as_ref().node { + BDDNode::Choice(ref t, _, ref f) if t.as_ref() == f.as_ref() => t, _ => a, }; diff --git a/src/bdd_io.rs b/src/bdd_io.rs index 96425d6..d1a1aa2 100644 --- a/src/bdd_io.rs +++ b/src/bdd_io.rs @@ -34,20 +34,20 @@ impl<'a, S: BDDSymbol> dot::Labeller<'a, GraphNode, GraphEdge> for BDDGrap } fn node_id(&self, n: &GraphNode) -> dot::Id<'a> { - match n.as_ref() { + match n.as_ref().node { // use grep -v n_true or grep -v n_false to filter nodes adjacent to true or false - BDD::True => dot::Id::new("n_true".to_string()).unwrap(), - BDD::False => dot::Id::new("n_false".to_string()).unwrap(), + BDDNode::True => dot::Id::new("n_true".to_string()).unwrap(), + BDDNode::False => dot::Id::new("n_false".to_string()).unwrap(), _ => dot::Id::new(format!("n_{:p}", Rc::into_raw(n.clone()))).unwrap(), // _ => dot::Id::new(format!("n_{}", n.get_hash())).unwrap(), // use the hash for optimal sharing, use (above) pointers to test issue with duplicates } } fn node_label(&self, n: &GraphNode) -> dot::LabelText<'a> { - match n.as_ref() { - BDD::True => dot::LabelText::label("true"), - BDD::False => dot::LabelText::label("false"), - &BDD::Choice(_, ref v, _) => dot::LabelText::label(format!("{}", v)), + match n.as_ref().node { + BDDNode::True => dot::LabelText::label("true"), + BDDNode::False => dot::LabelText::label("false"), + BDDNode::Choice(_, ref v, _) => dot::LabelText::label(format!("{}", v)), } } @@ -80,8 +80,8 @@ impl<'a, S: BDDSymbol> dot::GraphWalk<'a, GraphNode, GraphEdge> for BDDGra impl<'a, S: BDDSymbol> BDDGraph { fn nodes_recursive(&self, root: Rc>) -> dot::Nodes<'a, GraphNode> { - match root.as_ref() { - &BDD::Choice(ref l, _, ref r) => { + match &root.as_ref().node { + BDDNode::Choice(ref l, _, ref r) => { let l_nodes = self.nodes_recursive(l.clone()); let r_nodes = self.nodes_recursive(r.clone()); @@ -94,8 +94,8 @@ impl<'a, S: BDDSymbol> BDDGraph { .collect() } c if (self.filter == TruthTableEntry::Any) - || (self.filter == TruthTableEntry::True && *c == BDD::True) - || (self.filter == TruthTableEntry::False && *c == BDD::False) => + || (self.filter == TruthTableEntry::True && *c == BDDNode::True) + || (self.filter == TruthTableEntry::False && *c == BDDNode::False) => { vec![root.clone()].into() } @@ -104,25 +104,25 @@ impl<'a, S: BDDSymbol> BDDGraph { } fn edges_recursive(&self, root: Rc>) -> dot::Edges<'a, GraphEdge> { - match root.as_ref() { - &BDD::Choice(ref l, _, ref r) => { + match root.as_ref().node { + BDDNode::Choice(ref l, _, ref r) => { let l_edges = self.edges_recursive(l.clone()); let r_edges = self.edges_recursive(r.clone()); let mut self_edges = Vec::with_capacity(2); if (self.filter == TruthTableEntry::Any) - || (l.as_ref() != &BDD::True && l.as_ref() != &BDD::False) - || (l.as_ref() == &BDD::True && self.filter == TruthTableEntry::True) - || (l.as_ref() == &BDD::False && self.filter == TruthTableEntry::False) + || (l.as_ref().node != BDDNode::True && l.as_ref().node != BDDNode::False) + || (l.as_ref().node == BDDNode::True && self.filter == TruthTableEntry::True) + || (l.as_ref().node == BDDNode::False && self.filter == TruthTableEntry::False) { self_edges.push((root.clone(), true, l.clone())); } if (self.filter == TruthTableEntry::Any) - || (r.as_ref() != &BDD::True && r.as_ref() != &BDD::False) - || (r.as_ref() == &BDD::True && self.filter == TruthTableEntry::True) - || (r.as_ref() == &BDD::False && self.filter == TruthTableEntry::False) + || (r.as_ref().node != BDDNode::True && r.as_ref().node != BDDNode::False) + || (r.as_ref().node == BDDNode::True && self.filter == TruthTableEntry::True) + || (r.as_ref().node == BDDNode::False && self.filter == TruthTableEntry::False) { self_edges.push((root.clone(), false, r.clone())); } diff --git a/src/main.rs b/src/main.rs index 1be5191..b723515 100644 --- a/src/main.rs +++ b/src/main.rs @@ -215,8 +215,8 @@ fn print_true_vars_recursive( vars: &[String], parsed: &ParsedFormula, ) { - match root.as_ref() { - BDD::Choice(ref l, s, ref r) => { + match &root.as_ref().node { + BDDNode::Choice(ref l, s, ref r) => { // first visit the false subtree let mut r_vals = values.clone(); r_vals[parsed.to_free_index(s)] = TruthTableEntry::False; @@ -227,7 +227,7 @@ fn print_true_vars_recursive( l_vals[parsed.to_free_index(s)] = TruthTableEntry::True; print_true_vars_recursive(l, l_vals, vars, parsed); } - BDD::True => { + BDDNode::True => { let mut vars_str = Vec::new(); for (i, v) in values.iter().enumerate() { if *v == TruthTableEntry::True { @@ -250,8 +250,8 @@ fn print_truth_table_recursive( parsed: &ParsedFormula, sizes: &[usize], ) { - match root.as_ref() { - BDD::Choice(ref l, s, ref r) => { + match &root.as_ref().node { + BDDNode::Choice(ref l, s, ref r) => { // first visit the false subtree let mut r_vars = vars.clone(); r_vars[parsed.to_free_index(s)] = TruthTableEntry::False; @@ -263,8 +263,8 @@ fn print_truth_table_recursive( print_truth_table_recursive(l, l_vars, filter, parsed, sizes); } c if (filter == TruthTableEntry::Any) - || (filter == TruthTableEntry::True && *c == BDD::True) - || (filter == TruthTableEntry::False && *c == BDD::False) => + || (filter == TruthTableEntry::True && *c == BDDNode::True) + || (filter == TruthTableEntry::False && *c == BDDNode::False) => { print!("|"); for (i, var) in vars.iter().enumerate() { @@ -273,8 +273,8 @@ fn print_truth_table_recursive( println!( " {:indent$} |", match c { - BDD::True => "True", - BDD::False => "False", + BDDNode::True => "True", + BDDNode::False => "False", _ => unreachable!(), }, indent = sizes[vars.len()] diff --git a/tests/hash.rs b/tests/hash.rs index c87aeb5..eb8157e 100644 --- a/tests/hash.rs +++ b/tests/hash.rs @@ -2,7 +2,9 @@ use itertools::Itertools; use rsbdd::bdd; use rsbdd::bdd::BDDEnv; -use std::collections::HashMap; +use rsbdd::bdd::BDDNode; +use rustc_hash::{FxHasher, FxHashMap}; +use std::hash::Hash; use std::rc::Rc; use std::vec::Vec; @@ -94,7 +96,7 @@ fn test_duplicates() { // b contains a small example with duplicate nodes - let mut hm: HashMap>> = HashMap::new(); + let mut hm: FxHashMap>> = FxHashMap::default(); let mut max_size: usize = 0; @@ -139,3 +141,21 @@ fn test_duplicates() { } } } + +#[test] +fn test_hash_populated_equals_unpopulated() { + let populated = BDD::new(&BDDNode::True); + let unpopulated = BDD::new_unoptimized(&BDDNode::True); + + assert_eq!(populated.get_hash(), unpopulated.get_hash()); +} + +#[test] +fn test_hash_objects_compute_same_hash() { + let object_to_hash: usize = 42; + + let mut hasher1 = FxHasher::default(); + let mut hasher2 = FxHasher::default(); + + assert_eq!(object_to_hash.hash(&mut hasher1), object_to_hash.hash(&mut hasher2)); +} \ No newline at end of file