diff --git a/Cargo.lock b/Cargo.lock index de0527c..c7931f7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,24 +2,6 @@ # It is not intended for manual editing. version = 3 -[[package]] -name = "adf_bdd" -version = "0.2.4" -dependencies = [ - "biodivine-lib-bdd 0.4.0", - "derivative", - "env_logger 0.9.0", - "lexical-sort", - "log", - "nom", - "quickcheck", - "quickcheck_macros", - "roaring", - "serde", - "serde_json", - "test-log", -] - [[package]] name = "adf_bdd" version = "0.2.4" @@ -35,11 +17,29 @@ dependencies = [ "serde_json", ] +[[package]] +name = "adf_bdd" +version = "0.2.5" +dependencies = [ + "biodivine-lib-bdd 0.4.0", + "derivative", + "env_logger 0.9.0", + "lexical-sort", + "log", + "nom", + "quickcheck", + "quickcheck_macros", + "roaring", + "serde", + "serde_json", + "test-log", +] + [[package]] name = "adf_bdd-solver" version = "0.2.4" dependencies = [ - "adf_bdd 0.2.4 (registry+https://github.com/rust-lang/crates.io-index)", + "adf_bdd 0.2.4", "assert_cmd", "assert_fs", "clap", diff --git a/lib/Cargo.toml b/lib/Cargo.toml index 82cae2c..c5a39e2 100644 --- a/lib/Cargo.toml +++ b/lib/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "adf_bdd" -version = "0.2.4" +version = "0.2.5" authors = ["Stefan Ellmauthaler "] edition = "2021" homepage = "https://ellmau.github.io/adf-obdd/" diff --git a/lib/src/adf.rs b/lib/src/adf.rs index fa714cc..dec54b0 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -7,8 +7,6 @@ This module describes the abstract dialectical framework. pub mod heuristics; -use std::cmp::Ordering; - use serde::{Deserialize, Serialize}; use crate::{ @@ -24,6 +22,8 @@ use crate::{ parser::{AdfParser, Formula}, }; +use self::heuristics::Heuristic; + #[derive(Serialize, Deserialize, Debug)] /// Representation of an ADF, with an ordering and dictionary which relates statements to numbers, a binary decision diagram, and a list of acceptance conditions in [`Term`][crate::datatypes::Term] representation. /// @@ -727,7 +727,20 @@ impl Adf { .collect::>() } - fn stable_nogood(&mut self, interpretation: &[Term], heuristic: H) -> Vec> + /// Computes the stable extensions of a given [`Adf`], using the [`NoGood`]-learner + pub fn stable_nogood<'a, 'c>( + &'a mut self, + heuristic: Heuristic, + ) -> impl Iterator> + 'c + where + 'a: 'c, + { + let grounded = self.grounded(); + let heu = heuristic.get_heuristic(); + self.stable_nogood_internal(&grounded, heu).into_iter() + } + + fn stable_nogood_internal(&mut self, interpretation: &[Term], heuristic: H) -> Vec> where H: Fn(&Self, &[Term]) -> Option<(Var, Term)>, { @@ -742,7 +755,7 @@ impl Adf { let mut stack: Vec<(bool, NoGood)> = Vec::new(); let mut interpr_history: Vec> = Vec::new(); let mut backtrack = false; - let mut update_ng = true; + let mut update_ng; let mut update_fp = false; let mut choice = false; @@ -1014,7 +1027,7 @@ mod test { let mut adf = Adf::from_parser(&parser); let grounded = adf.grounded(); - let stable = adf.stable_nogood(&grounded, crate::adf::heuristics::heu_simple); + let stable = adf.stable_nogood_internal(&grounded, crate::adf::heuristics::heu_simple); assert_eq!( stable, @@ -1027,6 +1040,32 @@ mod test { Term::TOP ]] ); + let mut stable_iter = adf.stable_nogood(Heuristic::Simple); + assert_eq!( + stable_iter.next(), + Some(vec![ + Term::TOP, + Term::BOT, + Term::BOT, + Term::TOP, + Term::BOT, + Term::TOP + ]) + ); + + assert_eq!(stable_iter.next(), None); + let parser = AdfParser::default(); + parser.parse()("s(a).s(b).ac(a,neg(b)).ac(b,neg(a)).").unwrap(); + let mut adf = Adf::from_parser(&parser); + let grounded = adf.grounded(); + let stable = adf.stable_nogood_internal(&grounded, crate::adf::heuristics::heu_simple); + assert_eq!(stable, vec![vec![Term(1), Term(0)], vec![Term(0), Term(1)]]); + + let stable = adf.stable_nogood(Heuristic::Simple); + assert_eq!( + stable.collect::>(), + vec![vec![Term(1), Term(0)], vec![Term(0), Term(1)]] + ); } #[test] diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs index ed197ee..daa407f 100644 --- a/lib/src/nogoods.rs +++ b/lib/src/nogoods.rs @@ -290,14 +290,18 @@ pub(crate) enum ClosureResult { } impl ClosureResult { + /// Dead_code due to (currently) unused utility function for the [ClosureResult] enum. + #[allow(dead_code)] pub fn is_update(&self) -> bool { matches!(self, Self::Update(_)) } - + /// Dead_code due to (currently) unused utility function for the [ClosureResult] enum. + #[allow(dead_code)] pub fn is_no_update(&self) -> bool { matches!(self, Self::NoUpdate) } - + /// Dead_code due to (currently) unused utility function for the [ClosureResult] enum. + #[allow(dead_code)] pub fn is_inconsistent(&self) -> bool { matches!(self, Self::Inconsistent) }