diff --git a/bin/src/main.rs b/bin/src/main.rs index 949200f..0b1e7c3 100644 --- a/bin/src/main.rs +++ b/bin/src/main.rs @@ -414,6 +414,13 @@ impl App { 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)); + } + } } } } diff --git a/lib/src/obdd.rs b/lib/src/obdd.rs index d349202..a54cb70 100644 --- a/lib/src/obdd.rs +++ b/lib/src/obdd.rs @@ -217,7 +217,9 @@ impl Bdd { } else if node.var() < var { let lonode = self.restrict(node.lo(), 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 { if 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)) { *result } else { + log::trace!("if_then_else: i {i} t {t} e {e} not found"); let minvar = Var(min( self.nodes[i.value()].var().value(), min( @@ -298,7 +301,7 @@ impl Bdd { var_set.insert(var); self.var_deps.push(var_set); } - log::debug!("newterm: {} as {:?}", new_term, node); + log::trace!("newterm: {} as {:?}", new_term, node); #[cfg(feature = "adhoccounting")] { let mut count_cache = self.count_cache.borrow_mut(); diff --git a/lib/tests/test_template b/lib/tests/test_template index fc3275a..419bd05 100644 --- a/lib/tests/test_template +++ b/lib/tests/test_template @@ -1,5 +1,5 @@ #[test] -fn {name}() {{ +fn {name}_biodivine() {{ let resource = "{path}"; log::debug!("resource: {{}}", resource); 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()) + ); +}} +