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

Fix/restrict slow (#103)

Browse Source 
* Fix missing cache usage in restrict algorithm
This commit is contained in:
Stefan Ellmauthaler 2022-08-23 15:17:51 +02:00 committed by GitHub
parent bc21ecabc7
commit 17a57938c7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 33 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
bin/src/main.rs
View File

@ -414,6 +414,13 @@ impl App {
print!("{}", printer.print_interpretation(&model)); print!("{}", printer.print_interpretation(&model));
} }
} }
if self.stable_ng {
let printer = adf.print_dictionary();
for model in adf.stable_nogood(self.heu.unwrap_or_default()) {
print!("{}", printer.print_interpretation(&model));
}
}
} }
} }
} }

7
lib/src/obdd.rs
View File

@ -217,7 +217,9 @@ impl Bdd {
} else if node.var() < var { } else if node.var() < var {
let lonode = self.restrict(node.lo(), var, val); let lonode = self.restrict(node.lo(), var, val);
let hinode = self.restrict(node.hi(), var, val); let hinode = self.restrict(node.hi(), var, val);
self.node(node.var(), lonode, hinode) let result = self.node(node.var(), lonode, hinode);
self.restrict_cache.insert((tree, var, val), result);
result
} else { } else {
if val { if val {
let result = self.restrict(node.hi(), var, val); let result = self.restrict(node.hi(), var, val);
@ -245,6 +247,7 @@ impl Bdd {
} else if let Some(result) = self.ite_cache.get(&(i, t, e)) { } else if let Some(result) = self.ite_cache.get(&(i, t, e)) {
*result *result
} else { } else {
log::trace!("if_then_else: i {i} t {t} e {e} not found");
let minvar = Var(min( let minvar = Var(min(
self.nodes[i.value()].var().value(), self.nodes[i.value()].var().value(),
min( min(
@ -298,7 +301,7 @@ impl Bdd {
var_set.insert(var); var_set.insert(var);
self.var_deps.push(var_set); self.var_deps.push(var_set);
} }
log::debug!("newterm: {} as {:?}", new_term, node); log::trace!("newterm: {} as {:?}", new_term, node);
#[cfg(feature = "adhoccounting")] #[cfg(feature = "adhoccounting")]
{ {
let mut count_cache = self.count_cache.borrow_mut(); let mut count_cache = self.count_cache.borrow_mut();

22
lib/tests/test_template
View File

@ -1,5 +1,5 @@
#[test] #[test]
fn {name}() {{ fn {name}_biodivine() {{
let resource = "{path}"; let resource = "{path}";
log::debug!("resource: {{}}", resource); log::debug!("resource: {{}}", resource);
let grounded = "{grounded}"; let grounded = "{grounded}";
@ -18,3 +18,23 @@ fn {name}() {{
); );
}} }}
#[test]
fn {name}_naive() {{
let resource = "{path}";
log::debug!("resource: {{}}", resource);
let grounded = "{grounded}";
log::debug!("Grounded: {{}}", grounded);
let parser = AdfParser::default();
let expected_result = std::fs::read_to_string(grounded);
assert!(expected_result.is_ok());
let input = std::fs::read_to_string(resource).unwrap();
parser.parse()(&input).unwrap();
parser.varsort_alphanum();
let mut adf = adf_bdd::adf::Adf::from_parser(&parser);
let grounded = adf.grounded();
assert_eq!(
format!("{{}}", adf.print_interpretation(&grounded)),
format!("{{}}\n",expected_result.unwrap())
);
}}