ellmau/adf-obdd
1
0
Fork 0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-19 09:29:36 +01:00
Code Issues Projects Releases Wiki Activity

Optimise caching further

Browse Source
This commit is contained in:
Stefan Ellmauthaler 2022-10-19 15:23:52 +02:00
parent 3541afe4b8
commit d61f5fcb95
Failed to extract signature
1 changed files with 17 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
lib/src/obdd.rs
View File

@ -34,6 +34,8 @@ pub struct Bdd {
ite_cache: HashMap<(Term, Term, Term), Term>, ite_cache: HashMap<(Term, Term, Term), Term>,
#[serde(skip)] #[serde(skip)]
restrict_cache: HashMap<(Term, Var, bool), Term>, restrict_cache: HashMap<(Term, Var, bool), Term>,
#[serde(skip)]
restrict_cache2: HashMap<(Term, Vec<(Var, bool)>), Term>,
} }
impl Display for Bdd { impl Display for Bdd {
@ -70,6 +72,7 @@ impl Bdd {
receiver: None, receiver: None,
ite_cache: HashMap::new(), ite_cache: HashMap::new(),
restrict_cache: HashMap::new(), restrict_cache: HashMap::new(),
restrict_cache2: HashMap::new(),
} }
} }
#[cfg(feature = "adhoccounting")] #[cfg(feature = "adhoccounting")]
@ -86,6 +89,7 @@ impl Bdd {
receiver: None, receiver: None,
ite_cache: HashMap::new(), ite_cache: HashMap::new(),
restrict_cache: HashMap::new(), restrict_cache: HashMap::new(),
restrict_cache2: HashMap::new(),
}; };
result result
.count_cache .count_cache
@ -202,10 +206,13 @@ impl Bdd {
} }
/// Restrict the bdd to the given list of [variables][crate::datatypes::Var] and [values][bool]. /// Restrict the bdd to the given list of [variables][crate::datatypes::Var] and [values][bool].
///
/// # Caution
/// `restrict_list` only works as described if the `list` follows the variable ordering.
pub fn restrict_list(&mut self, tree: Term, list: &[(Var, bool)]) -> Term { pub fn restrict_list(&mut self, tree: Term, list: &[(Var, bool)]) -> Term {
if let Some(&(var, val)) = list.first() { if let Some(&(var, val)) = list.first() {
if let Some(result) = self.restrict_cache.get(&(tree, var, val)) { if let Some(result) = self.restrict_cache2.get(&(tree, list.to_vec())) {
self.restrict_list(*result, &list[1..]) *result
} else { } else {
let node = self.nodes[tree.value()]; let node = self.nodes[tree.value()];
#[cfg(feature = "variablelist")] #[cfg(feature = "variablelist")]
@ -221,12 +228,15 @@ impl Bdd {
} else if node.var() < var { } else if node.var() < var {
let lonode = self.restrict_list(node.lo(), list); let lonode = self.restrict_list(node.lo(), list);
let hinode = self.restrict_list(node.hi(), list); let hinode = self.restrict_list(node.hi(), list);
let result = self.node(node.var(), lonode, hinode); let mut result = self.node(node.var(), lonode, hinode);
self.restrict_list(result, &list[1..]) result = self.restrict_list(result, &list[1..]);
self.restrict_cache2.insert((tree, list.into()), result);
result
} else { } else {
let result = if val { node.hi() } else { node.lo() }; let result =
self.restrict_cache.insert((tree, var, val), result); self.restrict_list(if val { node.hi() } else { node.lo() }, &list[1..]);
self.restrict_list(result, &list[1..]) self.restrict_cache2.insert((tree, list.into()), result);
result
} }
} }
} else { } else {