Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Optimize hashes #35

Draft
wants to merge 5 commits into
base: master
Choose a base branch
from
Draft

Optimize hashes #35

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
ad6664c
remove todo
timbeurskens Apr 12, 2022
b557f13
cache hash values in BDD wrapper. Note: cached hash differs from comp…
timbeurskens Apr 16, 2022
81e2969
return optimized node to fix runtime issue
timbeurskens Apr 18, 2022
d56a9f2
add hash equivalence test
timbeurskens Apr 25, 2022
4de8533
update cargo lock file
timbeurskens May 1, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 10 additions & 10 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

155 changes: 101 additions & 54 deletions src/bdd.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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};
Expand Down Expand Up @@ -55,29 +54,40 @@ impl From<NamedSymbol> 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<S: BDDSymbol> {
cached_hash: Option<u64>,
pub node: BDDNode<S>,
}

#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub enum BDD<Symbol: BDDSymbol> {
pub enum BDDNode<Symbol: BDDSymbol> {
False,
True,
// Choice (true-subtree, symbol, false-subtree)
Choice(Rc<BDD<Symbol>>, Symbol, Rc<BDD<Symbol>>),
}

impl<S: BDDSymbol> Hash for BDD<S> {
fn hash<H: Hasher>(&self, state: &mut H) {
if let Some(cached) = self.cached_hash {
cached.hash(state);
} else {
self.node.hash(state);
}
}
}

impl From<BDD<NamedSymbol>> for BDD<usize> {
fn from(bdd: BDD<NamedSymbol>) -> BDD<usize> {
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())),
),
)),
}
}
}
Expand All @@ -101,18 +111,44 @@ impl Display for TruthTableEntry {

impl<S: BDDSymbol> Default for BDD<S> {
fn default() -> Self {
BDD::False
BDD::new(&BDDNode::False)
}
}

impl<S: BDDSymbol> BDD<S> {
pub fn get_hash(&self) -> u64 {
let mut s = DefaultHasher::new();
let mut s = FxHasher::default();
self.hash(&mut s);
s.finish()
}
}

impl<S: BDDSymbol> BDD<S> {
pub fn new(node: &BDDNode<S>) -> BDD<S> {
let mut result = BDD {
cached_hash: None,
node: node.clone(),
};

result.populate_hash();

result
}

pub fn new_unoptimized(node: &BDDNode<S>) -> BDD<S> {
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<Symbol: BDDSymbol> {
pub nodes: RefCell<FxHashMap<BDD<Symbol>, Rc<BDD<Symbol>>>>,
Expand All @@ -132,8 +168,8 @@ impl<S: BDDSymbol> BDDEnv<S> {
// 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<BDD<S>>) -> Rc<BDD<S>> {
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);

Expand Down Expand Up @@ -165,8 +201,8 @@ impl<S: BDDSymbol> BDDEnv<S> {
}

pub fn node_list(&self, root: Rc<BDD<S>>) -> Vec<Rc<BDD<S>>> {
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));

Expand All @@ -177,7 +213,7 @@ impl<S: BDDSymbol> BDDEnv<S> {
.cloned()
.collect()
}
&BDD::True | &BDD::False => vec![Rc::clone(&root)],
BDDNode::True | BDDNode::False => vec![Rc::clone(&root)],
}
}

Expand All @@ -190,7 +226,7 @@ impl<S: BDDSymbol> BDDEnv<S> {
false_subtree: Rc<BDD<S>>,
) -> Rc<BDD<S>> {
// 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();
Expand All @@ -200,17 +236,23 @@ impl<S: BDDSymbol> BDDEnv<S> {
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<BDD<S>> {
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())
}
}

Expand All @@ -222,8 +264,11 @@ impl<S: BDDSymbol> BDDEnv<S> {
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),
Expand All @@ -232,23 +277,25 @@ impl<S: BDDSymbol> BDDEnv<S> {

// conjunction
pub fn and(&self, a: Rc<BDD<S>>, b: Rc<BDD<S>>) -> Rc<BDD<S>> {
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(
Expand All @@ -262,10 +309,10 @@ impl<S: BDDSymbol> BDDEnv<S> {
}

pub fn not(&self, a: Rc<BDD<S>>) -> Rc<BDD<S>> {
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)))
}
}
Expand Down Expand Up @@ -424,10 +471,10 @@ impl<S: BDDSymbol> BDDEnv<S> {

// existential quantification
pub fn exists_impl(&self, s: S, b: Rc<BDD<S>>) -> Rc<BDD<S>> {
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)),
Expand Down Expand Up @@ -457,8 +504,8 @@ impl<S: BDDSymbol> BDDEnv<S> {
}

pub fn model(&self, a: Rc<BDD<S>>) -> Rc<BDD<S>> {
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) {
Expand All @@ -469,7 +516,7 @@ impl<S: BDDSymbol> BDDEnv<S> {
self.mk_const(false)
}
}
&BDD::True | &BDD::False => a,
BDDNode::True | BDDNode::False => a,
}
}

Expand All @@ -478,17 +525,17 @@ impl<S: BDDSymbol> BDDEnv<S> {
// the second item determines the truth value for b
pub fn infer(&self, a: Rc<BDD<S>>, 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<BDD<S>>) -> Rc<BDD<S>> {
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,
};

Expand Down
Loading