From 9d0845c740bc61ed4791aded202758e85a05e2a8 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler <71695780+ellmau@users.noreply.github.com> Date: Wed, 15 Jun 2022 17:34:59 +0200 Subject: [PATCH 01/51] Add NoGood and NoGoodStore (#65) * Add NoGood and NoGoodStore with basic functionality --- Cargo.lock | 24 +++ lib/Cargo.toml | 1 + lib/src/lib.rs | 1 + lib/src/nogoods.rs | 448 +++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 474 insertions(+) create mode 100644 lib/src/nogoods.rs diff --git a/Cargo.lock b/Cargo.lock index f913116..de0527c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -14,6 +14,7 @@ dependencies = [ "nom", "quickcheck", "quickcheck_macros", + "roaring", "serde", "serde_json", "test-log", @@ -147,6 +148,12 @@ dependencies = [ "regex-automata", ] +[[package]] +name = "bytemuck" +version = "1.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cdead85bdec19c194affaeeb670c0e41fe23de31459efd1c174d049269cf02cc" + [[package]] name = "byteorder" version = "1.4.3" @@ -718,6 +725,23 @@ dependencies = [ "winapi", ] +[[package]] +name = "retain_mut" +version = "0.1.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4389f1d5789befaf6029ebd9f7dac4af7f7e3d61b69d4f30e2ac02b57e7712b0" + +[[package]] +name = "roaring" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dd539cab4e32019956fe7e0cf160bb6d4802f4be2b52c4253d76d3bb0f85a5f7" +dependencies = [ + "bytemuck", + "byteorder", + "retain_mut", +] + [[package]] name = "ryu" version = "1.0.9" diff --git a/lib/Cargo.toml b/lib/Cargo.toml index a4209be..82cae2c 100644 --- a/lib/Cargo.toml +++ b/lib/Cargo.toml @@ -30,6 +30,7 @@ serde = { version = "1.0", features = ["derive","rc"] } serde_json = "1.0" biodivine-lib-bdd = "0.4.0" derivative = "2.2.0" +roaring = "0.9.0" [dev-dependencies] test-log = "0.2" diff --git a/lib/src/lib.rs b/lib/src/lib.rs index f50c4df..6bb39b7 100644 --- a/lib/src/lib.rs +++ b/lib/src/lib.rs @@ -182,6 +182,7 @@ pub mod adfbiodivine; pub mod datatypes; pub mod obdd; pub mod parser; +pub mod nogoods; #[cfg(test)] mod test; //pub mod obdd2; diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs new file mode 100644 index 0000000..003aa2d --- /dev/null +++ b/lib/src/nogoods.rs @@ -0,0 +1,448 @@ +//! Collection of all nogood-related structures. + +use std::{ + borrow::Borrow, + ops::{BitAnd, BitOr, BitXor}, +}; + +use crate::datatypes::Term; +use roaring::RoaringBitmap; + +/// Representation of a nogood by a pair of [Bitmaps][RoaringBitmap] +#[derive(Debug, Default, Clone)] +pub struct NoGood { + active: RoaringBitmap, + value: RoaringBitmap, +} + +impl Eq for NoGood {} +impl PartialEq for NoGood { + fn eq(&self, other: &Self) -> bool { + self.active + .borrow() + .bitxor(other.active.borrow()) + .is_empty() + && self.value.borrow().bitxor(other.value.borrow()).is_empty() + } +} + +impl NoGood { + /// Creates a [NoGood] from a given Vector of [Terms][Term]. + pub fn from_term_vec(term_vec: &[Term]) -> NoGood { + let mut result = Self::default(); + term_vec.iter().enumerate().for_each(|(idx, val)| { + let idx:u32 = idx.try_into().expect("no-good learner implementation is based on the assumption that only u32::MAX-many variables are in place"); + if val.is_truth_value() { + result.active.insert(idx); + if val.is_true() { + result.value.insert(idx); + } + } + }); + result + } + + /// Returns [None] if the pair contains inconsistent pairs. + /// Otherwise it returns a [NoGood] which represents the set values. + pub fn try_from_pair_iter( + pair_iter: &mut impl Iterator, + ) -> Option { + let mut result = Self::default(); + let mut visit = false; + for (idx, val) in pair_iter { + visit = true; + let idx:u32 = idx.try_into().expect("no-good learner implementation is based on the assumption that only u32::MAX-many variables are in place"); + let is_new = result.active.insert(idx); + let upd = if val { + result.value.insert(idx) + } else { + result.value.remove(idx) + }; + // if the state is not new and the value is changed + if !is_new && upd { + return None; + } + } + if visit { + Some(result) + } else { + None + } + } + + /// Creates an updated [Vec], based on the given [&[Term]] and the [NoGood]. + pub fn update_term_vec(&self, term_vec: &[Term]) -> Vec { + term_vec.iter().enumerate().map(|(idx,val)|{ + let idx:u32 = idx.try_into().expect("no-good learner implementation is based on the assumption that only u32::MAX-many variables are in place"); + if self.active.contains(idx){ + if self.value.contains(idx){ + Term::TOP + }else{ + Term::BOT + } + }else{ + *val + } + }).collect() + } + + /// Given a [NoGood] and another one, conclude a non-conflicting value which can be concluded on basis of the given one. + pub fn conclude(&self, other: &NoGood) -> Option<(usize, bool)> { + log::debug!("conclude: {:?} other {:?}", self, other); + let implication = self + .active + .borrow() + .bitxor(other.active.borrow()) + .bitand(self.active.borrow()); + if implication.len() == 1 { + let pos = implication + .min() + .expect("just checked that there is one element to be found"); + Some((pos as usize, !self.value.contains(pos))) + } else { + None + } + } + + /// Updates the [NoGood] and a second one in a disjunctive (bitor) manner. + pub fn disjunction(&mut self, other: &NoGood) { + self.active = self.active.borrow().bitor(&other.active); + self.value = self.value.borrow().bitor(&other.value); + } + + /// Returns [true] if the other [NoGood] matches with all the assignments of the current [NoGood]. + pub fn is_violating(&self, other: &NoGood) -> bool { + let active = self.active.borrow().bitand(other.active.borrow()); + if self.active.len() == active.len() { + let lhs = active.borrow().bitand(self.value.borrow()); + let rhs = active.borrow().bitand(other.value.borrow()); + if lhs.bitxor(rhs).is_empty() { + return true; + } + } + false + } + + /// Returns the number of set (i.e. active) bits. + pub fn len(&self) -> usize { + self.active + .len() + .try_into() + .expect("expecting to be on a 64 bit system") + } + + #[must_use] + /// Returns [true] if the [NoGood] does not set any value. + pub fn is_empty(&self) -> bool { + self.len() == 0 + } +} + +impl From<&[Term]> for NoGood { + fn from(term_vec: &[Term]) -> Self { + Self::from_term_vec(term_vec) + } +} + +/// A structure to store [NoGoods][NoGood] and offer operations and deductions based on them. +// TODO:make struct crate-private +#[derive(Debug)] +pub struct NoGoodStore { + store: Vec>, + duplicates: DuplicateElemination, +} + +impl NoGoodStore { + /// Creates a new [NoGoodStore] and assumes a size compatible with the underlying [NoGood] implementation. + pub fn new(size: u32) -> NoGoodStore { + Self { + store: vec![Vec::new(); size as usize], + duplicates: DuplicateElemination::Equiv, + } + } + + /// Tries to create a new [NoGoodStore]. + /// Does not succeed if the size is too big for the underlying [NoGood] implementation. + pub fn try_new(size: usize) -> Option { + match TryInto::::try_into(size) { + Ok(val) => Some(Self::new(val)), + Err(_) => None, + } + } + + /// Sets the behaviour when managing duplicates. + pub fn set_dup_elem(&mut self, mode: DuplicateElemination) { + self.duplicates = mode; + } + + /// Adds a given [NoGood] + pub fn add_ng(&mut self, nogood: NoGood) { + let mut idx = nogood.len(); + if idx > 0 { + idx -= 1; + if match self.duplicates { + DuplicateElemination::None => true, + DuplicateElemination::Equiv => !self.store[idx].contains(&nogood), + DuplicateElemination::Subsume => { + self.store + .iter_mut() + .enumerate() + .for_each(|(cur_idx, ng_vec)| { + if idx >= cur_idx { + ng_vec.retain(|ng| !ng.is_violating(&nogood)); + } + }); + true + } + } { + self.store[idx].push(nogood); + } + } + } + + /// Draws a (Conclusion)[NoGood], based on the [NoGoodstore] and the given [NoGood]. + pub fn conclusions(&self, nogood: &NoGood) -> Option { + let mut result = NoGood::default(); + self.store + .iter() + .enumerate() + .filter(|(len, _vec)| *len <= nogood.len()) + .filter_map(|(_len, val)| { + NoGood::try_from_pair_iter(&mut val.iter().filter_map(|ng| ng.conclude(nogood))) + }) + .try_fold(&mut result, |acc, ng| { + if ng.is_violating(acc) { + None + } else { + acc.disjunction(&ng); + Some(acc) + } + })?; + if self + .store + .iter() + .enumerate() + .filter(|(len, _vec)| *len <= nogood.len()) + .any(|(_, vec)| vec.iter().any(|elem| result.is_violating(elem))) + { + return None; + } + Some(result) + } +} + +/// Allows to define how costly the DuplicateElemination is done. +#[derive(Debug, Copy, Clone)] +pub enum DuplicateElemination { + /// No Duplicate Detection + None, + /// Only check weak equivalence + Equiv, + /// Check for subsumptions + Subsume, +} + +#[cfg(test)] +mod test { + use super::*; + use test_log::test; + + #[test] + fn create_ng() { + let terms = vec![Term::TOP, Term(22), Term(13232), Term::BOT, Term::TOP]; + let ng = NoGood::from_term_vec(&terms); + + assert_eq!(ng.active.len(), 3); + assert_eq!(ng.value.len(), 2); + assert!(ng.active.contains(0)); + assert!(!ng.active.contains(1)); + assert!(!ng.active.contains(2)); + assert!(ng.active.contains(3)); + assert!(ng.active.contains(4)); + + assert!(ng.value.contains(0)); + assert!(!ng.value.contains(1)); + assert!(!ng.value.contains(2)); + assert!(!ng.value.contains(3)); + assert!(ng.value.contains(4)); + } + + #[test] + fn conclude() { + let ng1 = NoGood::from_term_vec(&[Term::TOP, Term(22), Term::TOP, Term::BOT, Term::TOP]); + let ng2 = NoGood::from_term_vec(&[Term::TOP, Term(22), Term(13232), Term::BOT, Term::TOP]); + let ng3 = NoGood::from_term_vec(&[ + Term::TOP, + Term(22), + Term(13232), + Term::BOT, + Term::TOP, + Term::BOT, + ]); + + assert_eq!(ng1.conclude(&ng2), Some((2, false))); + assert_eq!(ng1.conclude(&ng1), None); + assert_eq!(ng2.conclude(&ng1), None); + assert_eq!(ng1.conclude(&ng3), Some((2, false))); + assert_eq!(ng3.conclude(&ng1), Some((5, true))); + assert_eq!(ng3.conclude(&ng2), Some((5, true))); + + // conclusions on empty knowledge + let ng4 = NoGood::from_term_vec(&[Term::TOP]); + let ng5 = NoGood::from_term_vec(&[Term::BOT]); + let ng6 = NoGood::from_term_vec(&[]); + + assert_eq!(ng4.conclude(&ng6), Some((0, false))); + assert_eq!(ng5.conclude(&ng6), Some((0, true))); + assert_eq!(ng6.conclude(&ng5), None); + assert_eq!(ng4.conclude(&ng5), None); + + let ng_a = NoGood::from_term_vec(&[Term::BOT, Term(22)]); + let ng_b = NoGood::from_term_vec(&[Term(22), Term::TOP]); + + assert_eq!(ng_a.conclude(&ng_b), Some((0, true))); + } + + #[test] + fn violate() { + let ng1 = NoGood::from_term_vec(&[Term::TOP, Term(22), Term::TOP, Term::BOT, Term::TOP]); + let ng2 = NoGood::from_term_vec(&[Term::TOP, Term(22), Term(13232), Term::BOT, Term::TOP]); + let ng3 = NoGood::from_term_vec(&[ + Term::TOP, + Term(22), + Term(13232), + Term::BOT, + Term::TOP, + Term::BOT, + ]); + let ng4 = NoGood::from_term_vec(&[Term::TOP]); + + assert!(ng4.is_violating(&ng1)); + assert!(!ng1.is_violating(&ng4)); + assert!(ng2.is_violating(&ng3)); + assert!(!ng3.is_violating(&ng2)); + } + + #[test] + fn add_ng() { + let mut ngs = NoGoodStore::new(5); + let ng1 = NoGood::from_term_vec(&[Term::TOP]); + let ng2 = NoGood::from_term_vec(&[Term(22), Term::TOP]); + let ng3 = NoGood::from_term_vec(&[Term(22), Term(22), Term::TOP]); + let ng4 = NoGood::from_term_vec(&[Term(22), Term(22), Term(22), Term::TOP]); + let ng5 = NoGood::from_term_vec(&[Term::BOT]); + + assert!(!ng1.is_violating(&ng5)); + assert!(ng1.is_violating(&ng1)); + + ngs.add_ng(ng1.clone()); + ngs.add_ng(ng2.clone()); + ngs.add_ng(ng3.clone()); + ngs.add_ng(ng4.clone()); + ngs.add_ng(ng5.clone()); + + assert_eq!( + ngs.store + .iter() + .fold(0, |acc, ng_vec| { acc + ng_vec.len() }), + 5 + ); + + ngs.set_dup_elem(DuplicateElemination::Equiv); + + ngs.add_ng(ng1.clone()); + ngs.add_ng(ng2.clone()); + ngs.add_ng(ng3.clone()); + ngs.add_ng(ng4.clone()); + ngs.add_ng(ng5.clone()); + + assert_eq!( + ngs.store + .iter() + .fold(0, |acc, ng_vec| { acc + ng_vec.len() }), + 5 + ); + ngs.set_dup_elem(DuplicateElemination::Subsume); + ngs.add_ng(ng1); + ngs.add_ng(ng2); + ngs.add_ng(ng3); + ngs.add_ng(ng4); + ngs.add_ng(ng5); + + assert_eq!( + ngs.store + .iter() + .fold(0, |acc, ng_vec| { acc + ng_vec.len() }), + 5 + ); + + ngs.add_ng(NoGood::from_term_vec(&[Term(22), Term::BOT, Term(22)])); + + assert_eq!( + ngs.store + .iter() + .fold(0, |acc, ng_vec| { acc + ng_vec.len() }), + 6 + ); + + ngs.add_ng(NoGood::from_term_vec(&[Term(22), Term::BOT, Term::BOT])); + + assert_eq!( + ngs.store + .iter() + .fold(0, |acc, ng_vec| { acc + ng_vec.len() }), + 6 + ); + + assert!(NoGood::from_term_vec(&[Term(22), Term::BOT, Term(22)]) + .is_violating(&NoGood::from_term_vec(&[Term(22), Term::BOT, Term::BOT]))); + } + + #[test] + fn ng_store_conclusions() { + let mut ngs = NoGoodStore::new(5); + + let ng1 = NoGood::from_term_vec(&[Term::BOT]); + + ngs.add_ng(ng1.clone()); + assert_eq!(ng1.conclude(&ng1), None); + assert_eq!( + ng1.conclude(&NoGood::from_term_vec(&[Term(33)])), + Some((0, true)) + ); + assert_eq!(ngs.conclusions(&ng1), None); + assert_ne!(ngs.conclusions(&NoGood::from_term_vec(&[Term(33)])), None); + assert_eq!( + ngs.conclusions(&NoGood::from_term_vec(&[Term(33)])) + .expect("just checked with prev assertion") + .update_term_vec(&[Term(33)]), + vec![Term::TOP] + ); + + let ng2 = NoGood::from_term_vec(&[Term(123), Term::TOP, Term(234), Term(345)]); + let ng3 = NoGood::from_term_vec(&[Term::TOP, Term::BOT, Term::TOP, Term(345)]); + + ngs.add_ng(ng2); + ngs.add_ng(ng3); + + log::debug!("issues start here"); + assert!(ngs + .conclusions(&NoGood::from_term_vec(&[Term::TOP])) + .is_some()); + assert_eq!( + ngs.conclusions(&[Term::TOP].as_slice().into()) + .expect("just checked with prev assertion") + .update_term_vec(&[Term::TOP, Term(4), Term(5), Term(6), Term(7)]), + vec![Term::TOP, Term::BOT, Term(5), Term(6), Term(7)] + ); + assert!(ngs + .conclusions(&NoGood::from_term_vec(&[ + Term::TOP, + Term::BOT, + Term(5), + Term(6), + Term(7) + ])) + .is_some()); + } +} From 795d8ab4e63d5a80c6f28e10d000557f9f82bb0d Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Wed, 15 Jun 2022 17:43:40 +0200 Subject: [PATCH 02/51] Fix issue with nogoods module definition in lib --- lib/src/lib.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/lib/src/lib.rs b/lib/src/lib.rs index 6bb39b7..5fba465 100644 --- a/lib/src/lib.rs +++ b/lib/src/lib.rs @@ -180,9 +180,8 @@ for model in adf.complete() { pub mod adf; pub mod adfbiodivine; pub mod datatypes; +pub mod nogoods; pub mod obdd; pub mod parser; -pub mod nogoods; #[cfg(test)] mod test; -//pub mod obdd2; From 4eb54e79d9bb80c8149d083cfcc50b8c94a217b2 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Thu, 16 Jun 2022 16:18:34 +0200 Subject: [PATCH 03/51] Fix issues with inconsistencies --- lib/src/nogoods.rs | 150 +++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 145 insertions(+), 5 deletions(-) diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs index 003aa2d..d14b332 100644 --- a/lib/src/nogoods.rs +++ b/lib/src/nogoods.rs @@ -71,10 +71,14 @@ impl NoGood { } /// Creates an updated [Vec], based on the given [&[Term]] and the [NoGood]. - pub fn update_term_vec(&self, term_vec: &[Term]) -> Vec { + pub fn update_term_vec(&self, term_vec: &[Term], update: &mut bool) -> Vec { + *update = false; term_vec.iter().enumerate().map(|(idx,val)|{ let idx:u32 = idx.try_into().expect("no-good learner implementation is based on the assumption that only u32::MAX-many variables are in place"); if self.active.contains(idx){ + if !val.is_truth_value() { + *update = true; + } if self.value.contains(idx){ Term::TOP }else{ @@ -202,7 +206,7 @@ impl NoGoodStore { /// Draws a (Conclusion)[NoGood], based on the [NoGoodstore] and the given [NoGood]. pub fn conclusions(&self, nogood: &NoGood) -> Option { - let mut result = NoGood::default(); + let mut result = nogood.clone(); self.store .iter() .enumerate() @@ -223,7 +227,10 @@ impl NoGoodStore { .iter() .enumerate() .filter(|(len, _vec)| *len <= nogood.len()) - .any(|(_, vec)| vec.iter().any(|elem| result.is_violating(elem))) + .any(|(_, vec)| { + vec.iter() + .any(|elem| result.is_violating(elem) || elem.is_violating(nogood)) + }) { return None; } @@ -415,7 +422,7 @@ mod test { assert_eq!( ngs.conclusions(&NoGood::from_term_vec(&[Term(33)])) .expect("just checked with prev assertion") - .update_term_vec(&[Term(33)]), + .update_term_vec(&[Term(33)], &mut false), vec![Term::TOP] ); @@ -432,7 +439,7 @@ mod test { assert_eq!( ngs.conclusions(&[Term::TOP].as_slice().into()) .expect("just checked with prev assertion") - .update_term_vec(&[Term::TOP, Term(4), Term(5), Term(6), Term(7)]), + .update_term_vec(&[Term::TOP, Term(4), Term(5), Term(6), Term(7)], &mut false), vec![Term::TOP, Term::BOT, Term(5), Term(6), Term(7)] ); assert!(ngs @@ -444,5 +451,138 @@ mod test { Term(7) ])) .is_some()); + + ngs = NoGoodStore::new(10); + ngs.add_ng([Term::BOT].as_slice().into()); + ngs.add_ng( + [Term::TOP, Term::BOT, Term(33), Term::TOP] + .as_slice() + .into(), + ); + ngs.add_ng( + [Term::TOP, Term::BOT, Term(33), Term(33), Term::BOT] + .as_slice() + .into(), + ); + ngs.add_ng([Term::TOP, Term::TOP].as_slice().into()); + + let interpr: Vec = vec![ + Term(123), + Term(233), + Term(345), + Term(456), + Term(567), + Term(678), + Term(789), + Term(899), + Term(999), + Term(1000), + ]; + let concl = ngs.conclusions(&interpr.as_slice().into()); + assert_eq!(concl, Some(NoGood::from_term_vec(&[Term::TOP]))); + let mut update = false; + let new_interpr = concl + .expect("just tested in assert") + .update_term_vec(&interpr, &mut update); + assert_eq!( + new_interpr, + vec![ + Term::TOP, + Term(233), + Term(345), + Term(456), + Term(567), + Term(678), + Term(789), + Term(899), + Term(999), + Term(1000) + ] + ); + assert!(update); + + let new_int_2 = ngs + .conclusions(&new_interpr.as_slice().into()) + .map(|val| val.update_term_vec(&new_interpr, &mut update)) + .expect("Should return a value"); + assert_eq!( + new_int_2, + vec![ + Term::TOP, + Term::BOT, + Term(345), + Term(456), + Term(567), + Term(678), + Term(789), + Term(899), + Term(999), + Term(1000) + ] + ); + assert!(update); + + let new_int_3 = ngs + .conclusions(&new_int_2.as_slice().into()) + .map(|val| val.update_term_vec(&new_int_2, &mut update)) + .expect("Should return a value"); + + assert_eq!( + new_int_3, + vec![ + Term::TOP, + Term::BOT, + Term(345), + Term::BOT, + Term::TOP, + Term(678), + Term(789), + Term(899), + Term(999), + Term(1000) + ] + ); + assert!(update); + + let concl4 = ngs.conclusions(&new_int_3.as_slice().into()); + assert_ne!(concl4, None); + + let new_int_4 = ngs + .conclusions(&new_int_3.as_slice().into()) + .map(|val| val.update_term_vec(&new_int_3, &mut update)) + .expect("Should return a value"); + + assert_eq!( + new_int_4, + vec![ + Term::TOP, + Term::BOT, + Term(345), + Term::BOT, + Term::TOP, + Term(678), + Term(789), + Term(899), + Term(999), + Term(1000) + ] + ); + assert!(!update); + + // inconsistence + let interpr = vec![ + Term::TOP, + Term::TOP, + Term::BOT, + Term::BOT, + Term(111), + Term(678), + Term(789), + Term(899), + Term(999), + Term(1000), + ]; + + assert_eq!(ngs.conclusions(&interpr.as_slice().into()), None); } } From 8059590fc0bb88bf8fe83b1ca31209ed11abdd7e Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Fri, 17 Jun 2022 13:43:35 +0200 Subject: [PATCH 04/51] Add closure of conclusions of an interpretation and a NoGoodStore --- lib/src/nogoods.rs | 133 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 133 insertions(+) diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs index d14b332..e884b4c 100644 --- a/lib/src/nogoods.rs +++ b/lib/src/nogoods.rs @@ -71,6 +71,7 @@ impl NoGood { } /// Creates an updated [Vec], based on the given [&[Term]] and the [NoGood]. + /// The parameter _update_ is set to [`true`] if there has been an update and to [`false`] otherwise pub fn update_term_vec(&self, term_vec: &[Term], update: &mut bool) -> Vec { *update = false; term_vec.iter().enumerate().map(|(idx,val)|{ @@ -205,6 +206,7 @@ impl NoGoodStore { } /// Draws a (Conclusion)[NoGood], based on the [NoGoodstore] and the given [NoGood]. + /// *Returns* [None] if there is a conflict pub fn conclusions(&self, nogood: &NoGood) -> Option { let mut result = nogood.clone(); self.store @@ -236,6 +238,25 @@ impl NoGoodStore { } Some(result) } + + /// Constructs the Closure of the conclusions drawn by the nogoods with respect to the given `interpretation` + pub(crate) fn conclusion_closure(&self, interpretation: &[Term]) -> ClosureResult { + let mut update = true; + let mut result = match self.conclusions(&interpretation.into()) { + Some(val) => val.update_term_vec(interpretation, &mut update), + None => return ClosureResult::Inconsistent, + }; + if !update { + return ClosureResult::NoUpdate; + } + while update { + match self.conclusions(&result.as_slice().into()) { + Some(val) => result = val.update_term_vec(&result, &mut update), + None => return ClosureResult::Inconsistent, + } + } + ClosureResult::Update(result) + } } /// Allows to define how costly the DuplicateElemination is done. @@ -249,6 +270,40 @@ pub enum DuplicateElemination { Subsume, } +/// If the closure had some issues, it is represented with this enum +#[derive(Debug, PartialEq, Eq)] +pub(crate) enum ClosureResult { + Update(Vec), + NoUpdate, + Inconsistent, +} + +impl ClosureResult { + pub fn is_update(&self) -> bool { + matches!(self, Self::Update(_)) + } + + pub fn is_no_update(&self) -> bool { + matches!(self, Self::NoUpdate) + } + + pub fn is_inconsistent(&self) -> bool { + matches!(self, Self::Inconsistent) + } +} + +impl TryInto> for ClosureResult { + type Error = &'static str; + + fn try_into(self) -> Result, Self::Error> { + match self { + ClosureResult::Update(val) => Ok(val), + ClosureResult::NoUpdate => Err("No update occurred, use the old value instead"), + ClosureResult::Inconsistent => Err("Inconsistency occurred"), + } + } +} + #[cfg(test)] mod test { use super::*; @@ -585,4 +640,82 @@ mod test { assert_eq!(ngs.conclusions(&interpr.as_slice().into()), None); } + + #[test] + fn conclusion_closure() { + let mut ngs = NoGoodStore::new(10); + ngs.add_ng([Term::BOT].as_slice().into()); + ngs.add_ng( + [Term::TOP, Term::BOT, Term(33), Term::TOP] + .as_slice() + .into(), + ); + ngs.add_ng( + [Term::TOP, Term::BOT, Term(33), Term(33), Term::BOT] + .as_slice() + .into(), + ); + ngs.add_ng([Term::TOP, Term::TOP].as_slice().into()); + + let interpr: Vec = vec![ + Term(123), + Term(233), + Term(345), + Term(456), + Term(567), + Term(678), + Term(789), + Term(899), + Term(999), + Term(1000), + ]; + + let result = ngs.conclusion_closure(&interpr); + assert!(result.is_update()); + let resultint: Vec = result.try_into().expect("just checked conversion"); + assert_eq!( + resultint, + vec![ + Term::TOP, + Term::BOT, + Term(345), + Term::BOT, + Term::TOP, + Term(678), + Term(789), + Term(899), + Term(999), + Term(1000) + ] + ); + let result_no_upd = ngs.conclusion_closure(&resultint); + + assert!(result_no_upd.is_no_update()); + assert_eq!( + >>::try_into(result_no_upd) + .expect_err("just checked that it is an error"), + "No update occurred, use the old value instead" + ); + + let inconsistent_interpr = vec![ + Term::TOP, + Term::TOP, + Term::BOT, + Term::BOT, + Term(111), + Term(678), + Term(789), + Term(899), + Term(999), + Term(1000), + ]; + let result_inconsistent = ngs.conclusion_closure(&inconsistent_interpr); + + assert!(result_inconsistent.is_inconsistent()); + assert_eq!( + >>::try_into(result_inconsistent) + .expect_err("just checked that it is an error"), + "Inconsistency occurred" + ); + } } From ced0b3aea34bbf87b1d0e348aa31b425fac15038 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Fri, 17 Jun 2022 14:14:31 +0200 Subject: [PATCH 05/51] flake.lock: Update MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Flake lock file updates: • Updated input 'flake-utils': 'github:numtide/flake-utils/04c1b180862888302ddfb2e3ad9eaa63afc60cf8' (2022-05-17) → 'github:numtide/flake-utils/1ed9fb1935d260de5fe1c2f7ee0ebaae17ed2fa1' (2022-05-30) • Updated input 'nixpkgs-unstable': 'github:NixOS/nixpkgs/dfd82985c273aac6eced03625f454b334daae2e8' (2022-05-20) → 'github:NixOS/nixpkgs/b1957596ff1c7aa8c55c4512b7ad1c9672502e8e' (2022-06-15) • Updated input 'rust-overlay': 'github:oxalica/rust-overlay/c5486f823e4af2c0dfb5b2673002d5c973ef5209' (2022-05-24) → 'github:oxalica/rust-overlay/9eea93067eff400846c36f57b7499df9ef428ba0' (2022-06-17) --- flake.lock | 82 +++++++++++++----------------------------------------- 1 file changed, 19 insertions(+), 63 deletions(-) diff --git a/flake.lock b/flake.lock index 014657e..ff4fe4a 100644 --- a/flake.lock +++ b/flake.lock @@ -1,43 +1,12 @@ { "nodes": { - "flake-compat": { - "flake": false, - "locked": { - "lastModified": 1650374568, - "narHash": "sha256-Z+s0J8/r907g149rllvwhb4pKi8Wam5ij0st8PwAh+E=", - "owner": "edolstra", - "repo": "flake-compat", - "rev": "b4a34015c698c7793d592d66adbab377907a2be8", - "type": "github" - }, - "original": { - "owner": "edolstra", - "repo": "flake-compat", - "type": "github" - } - }, "flake-utils": { "locked": { - "lastModified": 1652776076, - "narHash": "sha256-gzTw/v1vj4dOVbpBSJX4J0DwUR6LIyXo7/SuuTJp1kM=", - "owner": "numtide", - "repo": "flake-utils", - "rev": "04c1b180862888302ddfb2e3ad9eaa63afc60cf8", - "type": "github" - }, - "original": { - "owner": "numtide", - "repo": "flake-utils", - "type": "github" - } - }, - "flake-utils_2": { - "locked": { - "lastModified": 1637014545, - "narHash": "sha256-26IZAc5yzlD9FlDT54io1oqG/bBoyka+FJk5guaX4x4=", + "lastModified": 1653893745, + "narHash": "sha256-0jntwV3Z8//YwuOjzhV2sgJJPt+HY6KhU7VZUL0fKZQ=", "owner": "numtide", "repo": "flake-utils", - "rev": "bba5dcc8e0b20ab664967ad83d24d64cb64ec4f4", + "rev": "1ed9fb1935d260de5fe1c2f7ee0ebaae17ed2fa1", "type": "github" }, "original": { @@ -64,27 +33,27 @@ }, "nixpkgs": { "locked": { - "lastModified": 1653087707, - "narHash": "sha256-zfno3snrzZTWQ2B7K53QHrGZwrjnJLTRPalymrSsziU=", + "lastModified": 1655278232, + "narHash": "sha256-H6s7tnHYiDKFCcLADS4sl1sUq0dDJuRQXCieguk/6SA=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "cbd40c72b2603ab54e7208f99f9b35fc158bc009", + "rev": "8b538fcb329a7bc3d153962f17c509ee49166973", "type": "github" }, "original": { "owner": "NixOS", - "ref": "nixos-21.11", + "ref": "nixos-22.05", "repo": "nixpkgs", "type": "github" } }, "nixpkgs-unstable": { "locked": { - "lastModified": 1653060744, - "narHash": "sha256-kfRusllRumpt33J1hPV+CeCCylCXEU7e0gn2/cIM7cY=", + "lastModified": 1655306633, + "narHash": "sha256-nv4FfWWV/dEelByjXJtJkoDPOHIsKfLq50RN3Hqq5Yk=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "dfd82985c273aac6eced03625f454b334daae2e8", + "rev": "b1957596ff1c7aa8c55c4512b7ad1c9672502e8e", "type": "github" }, "original": { @@ -94,25 +63,8 @@ "type": "github" } }, - "nixpkgs_2": { - "locked": { - "lastModified": 1637453606, - "narHash": "sha256-Gy6cwUswft9xqsjWxFYEnx/63/qzaFUwatcbV5GF/GQ=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "8afc4e543663ca0a6a4f496262cd05233737e732", - "type": "github" - }, - "original": { - "owner": "NixOS", - "ref": "nixpkgs-unstable", - "repo": "nixpkgs", - "type": "github" - } - }, "root": { "inputs": { - "flake-compat": "flake-compat", "flake-utils": "flake-utils", "gitignoresrc": "gitignoresrc", "nixpkgs": "nixpkgs", @@ -122,15 +74,19 @@ }, "rust-overlay": { "inputs": { - "flake-utils": "flake-utils_2", - "nixpkgs": "nixpkgs_2" + "flake-utils": [ + "flake-utils" + ], + "nixpkgs": [ + "nixpkgs" + ] }, "locked": { - "lastModified": 1653360353, - "narHash": "sha256-WA1eevoRzs3LfTA+XWNj29thaoh4wN8HJSRs48Q2ICU=", + "lastModified": 1655434021, + "narHash": "sha256-lfioRPXTsDXk0OIApyvCtiVQDdqUs19iCi+aWkijcm0=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "c5486f823e4af2c0dfb5b2673002d5c973ef5209", + "rev": "9eea93067eff400846c36f57b7499df9ef428ba0", "type": "github" }, "original": { From 670a604fc443a16bf193d3a1cb18e38df8c0c0de Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Fri, 17 Jun 2022 14:14:53 +0200 Subject: [PATCH 06/51] Update Flake to nix 22.05 --- flake.nix | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/flake.nix b/flake.nix index f95d1a0..4c888ed 100644 --- a/flake.nix +++ b/flake.nix @@ -2,21 +2,23 @@ description = "basic rust flake"; inputs = { - nixpkgs.url = "github:NixOS/nixpkgs/nixos-21.11"; + nixpkgs.url = "github:NixOS/nixpkgs/nixos-22.05"; nixpkgs-unstable.url = "github:NixOS/nixpkgs/nixos-unstable"; - rust-overlay.url = "github:oxalica/rust-overlay"; - flake-utils.url = "github:numtide/flake-utils"; - flake-compat = { - url = "github:edolstra/flake-compat"; - flake = false; + rust-overlay = { + url = "github:oxalica/rust-overlay"; + inputs = { + nixpkgs.follows = "nixpkgs"; + flake-utils.follows = "flake-utils"; + }; }; + flake-utils.url = "github:numtide/flake-utils"; gitignoresrc = { url = "github:hercules-ci/gitignore.nix"; flake = false; }; }; - outputs = { self, nixpkgs, nixpkgs-unstable, flake-utils, flake-compat, gitignoresrc, rust-overlay, ... }@inputs: + outputs = { self, nixpkgs, nixpkgs-unstable, flake-utils, gitignoresrc, rust-overlay, ... }@inputs: { #overlay = import ./nix { inherit gitignoresrc; }; } // (flake-utils.lib.eachDefaultSystem (system: @@ -35,11 +37,13 @@ buildInputs = [ pkgs.rust-bin.nightly.latest.rustfmt pkgs.rust-bin.stable.latest.default - unstable.rust-analyzer + pkgs.rust-analyzer pkgs.cargo-audit pkgs.cargo-license pkgs.cargo-tarpaulin pkgs.cargo-kcov + pkgs.valgrind + pkgs.gnuplot pkgs.kcov ]; }; From 3ce1b54c0b6a750b31706b493fe3e096393b87f4 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Mon, 20 Jun 2022 18:05:08 +0200 Subject: [PATCH 07/51] Add nogood-algorithm to the ADF add additional test cases, fixed a bug in the ng-learner module --- lib/src/adf.rs | 147 +++++++++++++++++++++++++++++++++++++++++++++ lib/src/nogoods.rs | 62 ++++++++++++++++++- 2 files changed, 208 insertions(+), 1 deletion(-) diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 03ebffc..fa714cc 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -5,6 +5,10 @@ This module describes the abstract dialectical framework. - computing fixpoints */ +pub mod heuristics; + +use std::cmp::Ordering; + use serde::{Deserialize, Serialize}; use crate::{ @@ -15,6 +19,7 @@ use crate::{ }, FacetCounts, ModelCounts, Term, Var, }, + nogoods::{NoGood, NoGoodStore}, obdd::Bdd, parser::{AdfParser, Formula}, }; @@ -405,6 +410,10 @@ impl Adf { true } + fn is_two_valued(&self, interpretation: &[Term]) -> bool { + interpretation.iter().all(|t| t.is_truth_value()) + } + fn two_val_model_counts(&mut self, interpr: &[Term], heuristic: H) -> Vec> where H: Fn(&Self, (Var, Term), (Var, Term), &[Term]) -> std::cmp::Ordering + Copy, @@ -590,6 +599,26 @@ impl Adf { } } + /// Constructs the fixpoint of the given interpretation with respect to the ADF. + /// sets _update_ to [`true`] if the value has been updated and to [`false`] otherwise. + fn update_interpretation_fixpoint_upd( + &mut self, + interpretation: &[Term], + update: &mut bool, + ) -> Vec { + let mut cur_int = interpretation.to_vec(); + *update = false; + loop { + let new_int = self.update_interpretation(interpretation); + if cur_int == new_int { + return cur_int; + } else { + cur_int = new_int; + *update = true; + } + } + } + fn update_interpretation(&mut self, interpretation: &[Term]) -> Vec { self.apply_interpretation(interpretation, interpretation) } @@ -697,6 +726,101 @@ impl Adf { }) .collect::>() } + + fn stable_nogood(&mut self, interpretation: &[Term], heuristic: H) -> Vec> + where + H: Fn(&Self, &[Term]) -> Option<(Var, Term)>, + { + let mut result = Vec::new(); + let mut cur_interpr = interpretation.to_vec(); + let mut ng_store = NoGoodStore::new( + self.ac + .len() + .try_into() + .expect("Expecting only u32 many statements"), + ); + 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_fp = false; + let mut choice = false; + + log::debug!("start learning loop"); + loop { + log::trace!("interpr: {:?}", cur_interpr); + log::trace!("choice: {}", choice); + if choice { + choice = false; + if let Some((var, term)) = heuristic(&*self, &cur_interpr) { + log::trace!("choose {}->{}", var, term.is_true()); + interpr_history.push(cur_interpr.to_vec()); + cur_interpr[var.value()] = term; + stack.push((true, cur_interpr.as_slice().into())); + } else { + backtrack = true; + } + } + update_ng = true; + log::trace!("backtrack: {}", backtrack); + if backtrack { + backtrack = false; + if stack.is_empty() { + break; + } + while let Some((choice, ng)) = stack.pop() { + log::trace!("adding ng: {:?}", ng); + ng_store.add_ng(ng); + + if choice { + cur_interpr = interpr_history.pop().expect("both stacks (interpr_history and `stack`) should always be synchronous"); + log::trace!( + "choice found, reverting interpretation to {:?}", + cur_interpr + ); + break; + } + } + } + match ng_store.conclusion_closure(&cur_interpr) { + crate::nogoods::ClosureResult::Update(new_int) => { + cur_interpr = new_int; + log::trace!("ng update: {:?}", cur_interpr); + stack.push((false, cur_interpr.as_slice().into())); + } + crate::nogoods::ClosureResult::NoUpdate => { + log::trace!("no update"); + update_ng = false; + } + crate::nogoods::ClosureResult::Inconsistent => { + log::trace!("inconsistency"); + backtrack = true; + continue; + } + } + + cur_interpr = self.update_interpretation_fixpoint_upd(&cur_interpr, &mut update_fp); + if update_fp { + log::trace!("fixpount updated"); + stack.push((false, cur_interpr.as_slice().into())); + } else if !update_ng { + // No updates done this loop + if !self.is_two_valued(&cur_interpr) { + choice = true; + } else if self.stability_check(&cur_interpr) { + // stable model found + stack.push((false, cur_interpr.as_slice().into())); + result.push(cur_interpr.clone()); + backtrack = true; + } else { + // not stable + stack.push((false, cur_interpr.as_slice().into())); + backtrack = true; + } + } + } + result + } } #[cfg(test)] @@ -882,6 +1006,29 @@ mod test { assert_eq!(adf.stable_count_optimisation_heu_b().next(), None); } + #[test] + fn stable_nogood() { + let parser = AdfParser::default(); + parser.parse()("s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,b).ac(c,and(a,b)).ac(d,neg(b)).\ns(e).ac(e,and(b,or(neg(b),c(f)))).s(f).\n\nac(f,xor(a,e)).") + .unwrap(); + let mut adf = Adf::from_parser(&parser); + + let grounded = adf.grounded(); + let stable = adf.stable_nogood(&grounded, crate::adf::heuristics::heu_simple); + + assert_eq!( + stable, + vec![vec![ + Term::TOP, + Term::BOT, + Term::BOT, + Term::TOP, + Term::BOT, + Term::TOP + ]] + ); + } + #[test] fn complete() { let parser = AdfParser::default(); diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs index e884b4c..ed197ee 100644 --- a/lib/src/nogoods.rs +++ b/lib/src/nogoods.rs @@ -42,6 +42,17 @@ impl NoGood { result } + /// Creates a [NoGood] representing an atomic assignment. + pub fn new_single_nogood(pos: usize, val: bool) -> NoGood { + let mut result = Self::default(); + let pos:u32 = pos.try_into().expect("nog-good learner implementation is based on the assumption that only u32::MAX-many variables are in place"); + result.active.insert(pos); + if val { + result.value.insert(pos); + } + result + } + /// Returns [None] if the pair contains inconsistent pairs. /// Otherwise it returns a [NoGood] which represents the set values. pub fn try_from_pair_iter( @@ -231,7 +242,7 @@ impl NoGoodStore { .filter(|(len, _vec)| *len <= nogood.len()) .any(|(_, vec)| { vec.iter() - .any(|elem| result.is_violating(elem) || elem.is_violating(nogood)) + .any(|elem| elem.is_violating(&result) || elem.is_violating(nogood)) }) { return None; @@ -383,6 +394,8 @@ mod test { assert!(!ng1.is_violating(&ng4)); assert!(ng2.is_violating(&ng3)); assert!(!ng3.is_violating(&ng2)); + + assert_eq!(ng4, NoGood::new_single_nogood(0, true)); } #[test] @@ -639,6 +652,35 @@ mod test { ]; assert_eq!(ngs.conclusions(&interpr.as_slice().into()), None); + + ngs = NoGoodStore::new(6); + ngs.add_ng( + [Term(1), Term(1), Term(1), Term(0), Term(0), Term(1)] + .as_slice() + .into(), + ); + ngs.add_ng( + [Term(1), Term(1), Term(8), Term(0), Term(0), Term(11)] + .as_slice() + .into(), + ); + ngs.add_ng([Term(22), Term(1)].as_slice().into()); + + assert_eq!( + ngs.conclusions( + &[Term(1), Term(3), Term(3), Term(9), Term(0), Term(1)] + .as_slice() + .into(), + ), + Some(NoGood::from_term_vec(&[ + Term(1), + Term(0), + Term(3), + Term(9), + Term(0), + Term(1) + ])) + ); } #[test] @@ -717,5 +759,23 @@ mod test { .expect_err("just checked that it is an error"), "Inconsistency occurred" ); + + ngs = NoGoodStore::new(6); + ngs.add_ng( + [Term(1), Term(1), Term(1), Term(0), Term(0), Term(1)] + .as_slice() + .into(), + ); + ngs.add_ng( + [Term(1), Term(1), Term(8), Term(0), Term(0), Term(11)] + .as_slice() + .into(), + ); + ngs.add_ng([Term(22), Term(1)].as_slice().into()); + + assert_eq!( + ngs.conclusion_closure(&[Term(1), Term(3), Term(3), Term(9), Term(0), Term(1)]), + ClosureResult::Update(vec![Term(1), Term(0), Term(0), Term(1), Term(0), Term(1)]) + ); } } From f6f922d5e93120672ddca8ad22d67e43fb26bbf3 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 21 Jun 2022 10:47:58 +0200 Subject: [PATCH 08/51] Fix typo in Readme --- README.md | 2 +- bin/README.md | 2 +- lib/README.md | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 358a464..4211dc6 100644 --- a/README.md +++ b/README.md @@ -139,7 +139,7 @@ the Bundesministerium für Bildung und Forschung (BMBF, Federal Ministry of Educ and by the [Center for Advancing Electronics Dresden](https://cfaed.tu-dresden.de) (cfaed). # Affiliation -This work has been party developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). +This work has been partly developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). # Disclaimer Hosting content here does not establish any formal or legal relation to TU Dresden diff --git a/bin/README.md b/bin/README.md index 21d9770..0dcfd6e 100644 --- a/bin/README.md +++ b/bin/README.md @@ -121,7 +121,7 @@ the Bundesministerium für Bildung und Forschung (BMBF, Federal Ministry of Educ and by the [Center for Advancing Electronics Dresden](https://cfaed.tu-dresden.de) (cfaed). # Affiliation -This work has been party developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). +This work has been partly developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). # Disclaimer Hosting content here does not establish any formal or legal relation to TU Dresden diff --git a/lib/README.md b/lib/README.md index 51657ab..ff2af33 100644 --- a/lib/README.md +++ b/lib/README.md @@ -129,7 +129,7 @@ the Bundesministerium für Bildung und Forschung (BMBF, Federal Ministry of Educ and by the [Center for Advancing Electronics Dresden](https://cfaed.tu-dresden.de) (cfaed). # Affiliation -This work has been party developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). +This work has been partly developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). # Disclaimer Hosting content here does not establish any formal or legal relation to TU Dresden From fa9e622db9f8244fb73671f202f50ec3ca17c363 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 21 Jun 2022 16:07:03 +0200 Subject: [PATCH 09/51] Add public api for the nogood-learner Increment of the patch-version of the crate Add public enum to comfortably choose a heuristics function --- Cargo.lock | 22 ++++++++++----------- lib/Cargo.toml | 2 +- lib/src/adf.rs | 49 +++++++++++++++++++++++++++++++++++++++++----- lib/src/nogoods.rs | 8 ++++++-- 4 files changed, 62 insertions(+), 19 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index de0527c..c7931f7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -5,41 +5,41 @@ version = 3 [[package]] name = "adf_bdd" version = "0.2.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e781519ea5434514f014476c02ccee777b28e600ad58fadca195715acb194c69" dependencies = [ - "biodivine-lib-bdd 0.4.0", + "biodivine-lib-bdd 0.3.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" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e781519ea5434514f014476c02ccee777b28e600ad58fadca195715acb194c69" +version = "0.2.5" dependencies = [ - "biodivine-lib-bdd 0.3.0", + "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) } From dece879b279cbae6440aaf898a9f051ee11d9912 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 21 Jun 2022 16:10:26 +0200 Subject: [PATCH 10/51] Add missing heuristics module to git --- lib/src/adf/heuristics.rs | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 lib/src/adf/heuristics.rs diff --git a/lib/src/adf/heuristics.rs b/lib/src/adf/heuristics.rs new file mode 100644 index 0000000..301dc3d --- /dev/null +++ b/lib/src/adf/heuristics.rs @@ -0,0 +1,34 @@ +/*! +This module contains all the crate-wide defined heuristic functions. +In addition there is the public enum [Heuristic], which allows to set a heuristic function with the public API. + */ +use super::Adf; +use crate::datatypes::{Term, Var}; + +pub(crate) fn heu_simple(_adf: &Adf, interpr: &[Term]) -> Option<(Var, Term)> { + for (idx, term) in interpr.iter().enumerate() { + if !term.is_truth_value() { + return Some((Var(idx), Term::TOP)); + } + } + None +} + +type RetVal = Option<(Var, Term)>; + +/// Enumeration of all currently implemented heuristics. +/// It represents a public view on the crate-view implementations of heuristics. +#[derive(Debug, Clone, Copy)] +pub enum Heuristic { + /// Implementation of a simple heuristic. + /// This will just take the first not decided variable and maps it value to (`true`)[Term::TOP]. + Simple, +} + +impl Heuristic { + pub(crate) fn get_heuristic(&self) -> Box RetVal> { + match self { + Heuristic::Simple => Box::new(heu_simple), + } + } +} From 57cdb469a0bd47033e2390796f285178a5cfe676 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 21 Jun 2022 16:11:30 +0200 Subject: [PATCH 11/51] Fix rustfmt --- lib/src/adfbiodivine.rs | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/lib/src/adfbiodivine.rs b/lib/src/adfbiodivine.rs index 6d57370..43228e9 100644 --- a/lib/src/adfbiodivine.rs +++ b/lib/src/adfbiodivine.rs @@ -326,17 +326,15 @@ impl Adf { &biodivine_lib_bdd::boolean_expression::BooleanExpression::Const(true), ), |acc, (idx, formula)| { - acc.and( - &formula.iff( - &self.varset.eval_expression( - &biodivine_lib_bdd::boolean_expression::BooleanExpression::Variable( - self.ordering - .name(crate::datatypes::Var(idx)) - .expect("Variable should exist"), - ), + acc.and(&formula.iff( + &self.varset.eval_expression( + &biodivine_lib_bdd::boolean_expression::BooleanExpression::Variable( + self.ordering + .name(crate::datatypes::Var(idx)) + .expect("Variable should exist"), ), ), - ) + )) }, ) } From 273973f378bfcf25910ba45f66326d180a3da3dd Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 21 Jun 2022 16:17:36 +0200 Subject: [PATCH 12/51] Update to trigger a new rustfmt The rustfmt issue on the CI is not reproducable --- lib/src/adfbiodivine.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/lib/src/adfbiodivine.rs b/lib/src/adfbiodivine.rs index 43228e9..a1eebe9 100644 --- a/lib/src/adfbiodivine.rs +++ b/lib/src/adfbiodivine.rs @@ -319,6 +319,7 @@ impl Adf { .collect::>>() } + /// compute the stable representation fn stable_representation(&self) -> Bdd { log::debug!("[Start] stable representation rewriting"); self.ac.iter().enumerate().fold( From f99d6171e9483737f2c558bdcf7197b5264586be Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 21 Jun 2022 16:21:07 +0200 Subject: [PATCH 13/51] Updated rustfmt to match the version on the server-CI --- flake.nix | 2 +- lib/src/adfbiodivine.rs | 16 +++++++++------- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/flake.nix b/flake.nix index 4c888ed..29c6635 100644 --- a/flake.nix +++ b/flake.nix @@ -35,7 +35,7 @@ RUST_LOG = "debug"; RUST_BACKTRACE = 1; buildInputs = [ - pkgs.rust-bin.nightly.latest.rustfmt + pkgs.rust-bin.stable.latest.rustfmt pkgs.rust-bin.stable.latest.default pkgs.rust-analyzer pkgs.cargo-audit diff --git a/lib/src/adfbiodivine.rs b/lib/src/adfbiodivine.rs index a1eebe9..c5d94d1 100644 --- a/lib/src/adfbiodivine.rs +++ b/lib/src/adfbiodivine.rs @@ -327,15 +327,17 @@ impl Adf { &biodivine_lib_bdd::boolean_expression::BooleanExpression::Const(true), ), |acc, (idx, formula)| { - acc.and(&formula.iff( - &self.varset.eval_expression( - &biodivine_lib_bdd::boolean_expression::BooleanExpression::Variable( - self.ordering - .name(crate::datatypes::Var(idx)) - .expect("Variable should exist"), + acc.and( + &formula.iff( + &self.varset.eval_expression( + &biodivine_lib_bdd::boolean_expression::BooleanExpression::Variable( + self.ordering + .name(crate::datatypes::Var(idx)) + .expect("Variable should exist"), + ), ), ), - )) + ) }, ) } From e78cd57210691c3ece2fe429dc9799b65f915189 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler <71695780+ellmau@users.noreply.github.com> Date: Tue, 21 Jun 2022 18:15:44 +0200 Subject: [PATCH 14/51] Update lib/src/nogoods.rs Co-authored-by: Maximilian Marx --- lib/src/nogoods.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs index daa407f..27ad71d 100644 --- a/lib/src/nogoods.rs +++ b/lib/src/nogoods.rs @@ -86,7 +86,10 @@ impl NoGood { pub fn update_term_vec(&self, term_vec: &[Term], update: &mut bool) -> Vec { *update = false; term_vec.iter().enumerate().map(|(idx,val)|{ - let idx:u32 = idx.try_into().expect("no-good learner implementation is based on the assumption that only u32::MAX-many variables are in place"); + let idx: u32 = idx.try_into().expect( + "no-good learner implementation is based on the assumption \ + that only u32::MAX-many variables are in place", + ); if self.active.contains(idx){ if !val.is_truth_value() { *update = true; From e7f38c100bdbac51f649e0f23ddb04f6462a1d12 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 21 Jun 2022 18:16:13 +0200 Subject: [PATCH 15/51] Fix rustfmt --- lib/src/nogoods.rs | 32 ++++++++++++++++++-------------- 1 file changed, 18 insertions(+), 14 deletions(-) diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs index 27ad71d..155e4cf 100644 --- a/lib/src/nogoods.rs +++ b/lib/src/nogoods.rs @@ -85,24 +85,28 @@ impl NoGood { /// The parameter _update_ is set to [`true`] if there has been an update and to [`false`] otherwise pub fn update_term_vec(&self, term_vec: &[Term], update: &mut bool) -> Vec { *update = false; - term_vec.iter().enumerate().map(|(idx,val)|{ + term_vec + .iter() + .enumerate() + .map(|(idx, val)| { let idx: u32 = idx.try_into().expect( "no-good learner implementation is based on the assumption \ that only u32::MAX-many variables are in place", ); - if self.active.contains(idx){ - if !val.is_truth_value() { - *update = true; - } - if self.value.contains(idx){ - Term::TOP - }else{ - Term::BOT - } - }else{ - *val - } - }).collect() + if self.active.contains(idx) { + if !val.is_truth_value() { + *update = true; + } + if self.value.contains(idx) { + Term::TOP + } else { + Term::BOT + } + } else { + *val + } + }) + .collect() } /// Given a [NoGood] and another one, conclude a non-conflicting value which can be concluded on basis of the given one. From e7d92918d9845dc7f182929fb1f849c32d11e4a1 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 21 Jun 2022 18:34:31 +0200 Subject: [PATCH 16/51] Add direnv to gitignore --- .gitignore | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.gitignore b/.gitignore index 0e650ce..0d56a6f 100644 --- a/.gitignore +++ b/.gitignore @@ -21,3 +21,6 @@ tramp *_flymake* /tests/out/ + +# Ignore direnv data +/.direnv/ \ No newline at end of file From d68d6cca1cf94bfd2710adb5cba2d8e7a61f9a61 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 21 Jun 2022 18:35:25 +0200 Subject: [PATCH 17/51] Ignore perf data (gitignore) --- .gitignore | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 0d56a6f..e20f82e 100644 --- a/.gitignore +++ b/.gitignore @@ -23,4 +23,7 @@ tramp /tests/out/ # Ignore direnv data -/.direnv/ \ No newline at end of file +/.direnv/ + +# ignore perfdata +perf.data \ No newline at end of file From 5da2c2cf62c90262089f2dab9f05bc83b2041826 Mon Sep 17 00:00:00 2001 From: Maximilian Marx Date: Tue, 21 Jun 2022 19:45:36 +0200 Subject: [PATCH 18/51] Avoid a Box, support custom heuristics functions --- lib/src/adf.rs | 13 +++++++++++++ lib/src/adf/heuristics.rs | 26 ++++++++++++++++++++------ 2 files changed, 33 insertions(+), 6 deletions(-) diff --git a/lib/src/adf.rs b/lib/src/adf.rs index dec54b0..e51c274 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -1066,6 +1066,19 @@ mod test { stable.collect::>(), vec![vec![Term(1), Term(0)], vec![Term(0), Term(1)]] ); + + let stable = adf.stable_nogood(Heuristic::Custom(&|_adf, interpr| { + for (idx, term) in interpr.iter().enumerate() { + if !term.is_truth_value() { + return Some((Var(idx), Term::BOT)); + } + } + None + })); + assert_eq!( + stable.collect::>(), + vec![vec![Term(0), Term(1)], vec![Term(1), Term(0)]] + ); } #[test] diff --git a/lib/src/adf/heuristics.rs b/lib/src/adf/heuristics.rs index 301dc3d..ccfc642 100644 --- a/lib/src/adf/heuristics.rs +++ b/lib/src/adf/heuristics.rs @@ -14,21 +14,35 @@ pub(crate) fn heu_simple(_adf: &Adf, interpr: &[Term]) -> Option<(Var, Term)> { None } -type RetVal = Option<(Var, Term)>; +/// Return value for heuristics. +pub type RetVal = Option<(Var, Term)>; +/// Signature for heuristics functions. +pub type HeuristicFn = dyn Fn(&Adf, &[Term]) -> RetVal; /// Enumeration of all currently implemented heuristics. /// It represents a public view on the crate-view implementations of heuristics. -#[derive(Debug, Clone, Copy)] -pub enum Heuristic { +pub enum Heuristic<'a> { /// Implementation of a simple heuristic. /// This will just take the first not decided variable and maps it value to (`true`)[Term::TOP]. Simple, + /// Allow passing in an externally-defined custom heuristic. + Custom(&'a HeuristicFn), } -impl Heuristic { - pub(crate) fn get_heuristic(&self) -> Box RetVal> { +impl std::fmt::Debug for Heuristic<'_> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { - Heuristic::Simple => Box::new(heu_simple), + Self::Simple => write!(f, "Simple"), + Self::Custom(_) => f.debug_tuple("Custom function").finish(), + } + } +} + +impl Heuristic<'_> { + pub(crate) fn get_heuristic(&self) -> &(dyn Fn(&Adf, &[Term]) -> RetVal + '_) { + match self { + Heuristic::Simple => &heu_simple, + Self::Custom(f) => f, } } } From 86084d722173bb2fe59ace77cf8b87ca86c2e1d6 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Wed, 22 Jun 2022 17:15:51 +0200 Subject: [PATCH 19/51] Add ng option with heu to binary Fix various bugs with the nogood learner --- Cargo.lock | 79 +++++++++++++++++++++------------------ bin/Cargo.toml | 7 ++-- bin/src/main.rs | 15 +++++++- lib/Cargo.toml | 1 + lib/src/adf.rs | 3 +- lib/src/adf/heuristics.rs | 65 ++++++++++++++++++++++++++++++-- lib/src/datatypes/bdd.rs | 10 +++++ lib/src/nogoods.rs | 39 +++++++++++++++++-- 8 files changed, 169 insertions(+), 50 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index c7931f7..43e85e4 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,26 +2,11 @@ # It is not intended for manual editing. version = 3 -[[package]] -name = "adf_bdd" -version = "0.2.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e781519ea5434514f014476c02ccee777b28e600ad58fadca195715acb194c69" -dependencies = [ - "biodivine-lib-bdd 0.3.0", - "derivative", - "lexical-sort", - "log", - "nom", - "serde", - "serde_json", -] - [[package]] name = "adf_bdd" version = "0.2.5" dependencies = [ - "biodivine-lib-bdd 0.4.0", + "biodivine-lib-bdd", "derivative", "env_logger 0.9.0", "lexical-sort", @@ -32,14 +17,15 @@ dependencies = [ "roaring", "serde", "serde_json", + "strum", "test-log", ] [[package]] name = "adf_bdd-solver" -version = "0.2.4" +version = "0.2.5" dependencies = [ - "adf_bdd 0.2.4", + "adf_bdd", "assert_cmd", "assert_fs", "clap", @@ -48,6 +34,7 @@ dependencies = [ "predicates", "serde", "serde_json", + "strum", ] [[package]] @@ -110,16 +97,6 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" -[[package]] -name = "biodivine-lib-bdd" -version = "0.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bddcfb460c1131729ec8d797ce0be49ec102506e764ce62f20a40056516851c5" -dependencies = [ - "fxhash", - "rand 0.7.3", -] - [[package]] name = "biodivine-lib-bdd" version = "0.4.0" @@ -168,16 +145,16 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "3.1.18" +version = "3.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d2dbdf4bdacb33466e854ce889eee8dfd5729abf7ccd7664d0a2d60cd384440b" +checksum = "9f1fe12880bae935d142c8702d500c63a4e8634b6c3c57ad72bf978fc7b6249a" dependencies = [ "atty", "bitflags", "clap_derive", "clap_lex", "indexmap", - "lazy_static", + "once_cell", "strsim", "termcolor", "textwrap", @@ -185,9 +162,9 @@ dependencies = [ [[package]] name = "clap_derive" -version = "3.1.18" +version = "3.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "25320346e922cffe59c0bbc5410c8d8784509efb321488971081313cb1e1a33c" +checksum = "ed6db9e867166a43a53f7199b5e4d1f522a1e5bd626654be263c999ce59df39a" dependencies = [ "heck", "proc-macro-error", @@ -198,9 +175,9 @@ dependencies = [ [[package]] name = "clap_lex" -version = "0.2.0" +version = "0.2.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a37c35f1112dad5e6e0b1adaff798507497a18fceeb30cceb3bae7d1427b9213" +checksum = "87eba3c8c7f42ef17f6c659fc7416d0f4758cd3e58861ee63c5fa4a4dde649e4" dependencies = [ "os_str_bytes", ] @@ -515,9 +492,9 @@ dependencies = [ [[package]] name = "once_cell" -version = "1.9.0" +version = "1.12.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da32515d9f6e6e489d7bc9d84c71b060db7247dc035bbe44eac88cf87486d8d5" +checksum = "7709cef83f0c1f58f666e746a08b21e0085f7440fa6a29cc194d68aac97a4225" [[package]] name = "os_str_bytes" @@ -742,6 +719,12 @@ dependencies = [ "retain_mut", ] +[[package]] +name = "rustversion" +version = "1.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a0a5f7c728f5d284929a1cccb5bc19884422bfe6ef4d6c409da2c41838983fcf" + [[package]] name = "ryu" version = "1.0.9" @@ -794,6 +777,28 @@ version = "0.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623" +[[package]] +name = "strum" +version = "0.24.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "063e6045c0e62079840579a7e47a355ae92f60eb74daaf156fb1e84ba164e63f" +dependencies = [ + "strum_macros", +] + +[[package]] +name = "strum_macros" +version = "0.24.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6878079b17446e4d3eba6192bb0a2950d5b14f0ed8424b852310e5a94345d0ef" +dependencies = [ + "heck", + "proc-macro2", + "quote", + "rustversion", + "syn", +] + [[package]] name = "syn" version = "1.0.92" diff --git a/bin/Cargo.toml b/bin/Cargo.toml index 79cef0e..33a8cb0 100644 --- a/bin/Cargo.toml +++ b/bin/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "adf_bdd-solver" -version = "0.2.4" +version = "0.2.5" authors = ["Stefan Ellmauthaler "] edition = "2021" license = "MIT" @@ -14,12 +14,13 @@ name = "adf-bdd" path = "src/main.rs" [dependencies] -adf_bdd = { version="0.2.4", default-features = false } -clap = {version = "3.1.18", features = [ "derive", "cargo", "env" ]} +adf_bdd = { version="0.2.5", path="../lib", default-features = false } +clap = {version = "3.2.6", features = [ "derive", "cargo", "env" ]} log = { version = "0.4", features = [ "max_level_trace", "release_max_level_info" ] } serde = { version = "1.0", features = ["derive","rc"] } serde_json = "1.0" env_logger = "0.9" +strum = { version = "0.24" } [dev-dependencies] assert_cmd = "2.0" diff --git a/bin/src/main.rs b/bin/src/main.rs index 13fb052..5bac810 100644 --- a/bin/src/main.rs +++ b/bin/src/main.rs @@ -74,6 +74,7 @@ use adf_bdd::adfbiodivine::Adf as BdAdf; use adf_bdd::parser::AdfParser; use clap::Parser; +use strum::VariantNames; #[derive(Parser, Debug)] #[clap(author, version, about)] @@ -84,7 +85,7 @@ struct App { /// Sets the verbosity to 'warn', 'info', 'debug' or 'trace' if -v and -q are not use #[clap(long = "rust_log", env)] rust_log: Option, - /// choose the bdd implementation of either 'biodivine', 'naive', or hybrid + /// Choose the bdd implementation of either 'biodivine', 'naive', or hybrid #[clap(long = "lib", default_value = "hybrid")] implementation: String, /// Sets log verbosity (multiple times means more verbose) @@ -120,6 +121,12 @@ struct App { /// Compute the stable models with a single-formula rewriting on internal representation(only hybrid lib-mode) #[clap(long = "stmrew2")] stable_rew2: bool, + /// Compute the stable models with the nogood-learning based approach + #[clap(long = "stmng")] + stable_ng: bool, + /// Choose which heuristics shall be used by the nogood-learning approach + #[clap(long, possible_values = adf_bdd::adf::heuristics::Heuristic::VARIANTS.iter().filter(|&v| v != &"Custom"))] + heu: Option>, /// Compute the complete models #[clap(long = "com")] complete: bool, @@ -244,6 +251,12 @@ impl App { print!("{}", printer.print_interpretation(&model)); } } + + if self.stable_ng { + for model in naive_adf.stable_nogood(self.heu.unwrap_or_default()) { + print!("{}", printer.print_interpretation(&model)); + } + } } "biodivine" => { if self.counter.is_some() { diff --git a/lib/Cargo.toml b/lib/Cargo.toml index c5a39e2..98a8007 100644 --- a/lib/Cargo.toml +++ b/lib/Cargo.toml @@ -31,6 +31,7 @@ serde_json = "1.0" biodivine-lib-bdd = "0.4.0" derivative = "2.2.0" roaring = "0.9.0" +strum = { version = "0.24", features = ["derive"] } [dev-dependencies] test-log = "0.2" diff --git a/lib/src/adf.rs b/lib/src/adf.rs index e51c274..9106951 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -815,7 +815,7 @@ impl Adf { cur_interpr = self.update_interpretation_fixpoint_upd(&cur_interpr, &mut update_fp); if update_fp { log::trace!("fixpount updated"); - stack.push((false, cur_interpr.as_slice().into())); + //stack.push((false, cur_interpr.as_slice().into())); } else if !update_ng { // No updates done this loop if !self.is_two_valued(&cur_interpr) { @@ -832,6 +832,7 @@ impl Adf { } } } + log::info!("{ng_store}"); result } } diff --git a/lib/src/adf/heuristics.rs b/lib/src/adf/heuristics.rs index ccfc642..7e7eb23 100644 --- a/lib/src/adf/heuristics.rs +++ b/lib/src/adf/heuristics.rs @@ -5,6 +5,13 @@ In addition there is the public enum [Heuristic], which allows to set a heuristi use super::Adf; use crate::datatypes::{Term, Var}; +use strum::{EnumString, EnumVariantNames}; + +/// Return value for heuristics. +pub type RetVal = Option<(Var, Term)>; +/// Signature for heuristics functions. +pub type HeuristicFn = dyn Fn(&Adf, &[Term]) -> RetVal; + pub(crate) fn heu_simple(_adf: &Adf, interpr: &[Term]) -> Option<(Var, Term)> { for (idx, term) in interpr.iter().enumerate() { if !term.is_truth_value() { @@ -14,25 +21,59 @@ pub(crate) fn heu_simple(_adf: &Adf, interpr: &[Term]) -> Option<(Var, Term)> { None } -/// Return value for heuristics. -pub type RetVal = Option<(Var, Term)>; -/// Signature for heuristics functions. -pub type HeuristicFn = dyn Fn(&Adf, &[Term]) -> RetVal; +pub(crate) fn heu_mc_minpaths_maxvarimp(adf: &Adf, interpr: &[Term]) -> Option<(Var, Term)> { + interpr + .iter() + .enumerate() + .filter(|(_var, term)| !term.is_truth_value()) + .min_by(|(vara, &terma), (varb, &termb)| { + match adf + .bdd + .paths(terma, true) + .minimum() + .cmp(&adf.bdd.paths(termb, true).minimum()) + { + std::cmp::Ordering::Equal => adf + .bdd + .passive_var_impact(Var::from(*vara), interpr) + .cmp(&adf.bdd.passive_var_impact(Var::from(*varb), interpr)), + value => value, + } + }) + .map(|(var, term)| { + ( + Var::from(var), + (!adf.bdd.paths(*term, true).more_models()).into(), + ) + }) +} /// Enumeration of all currently implemented heuristics. /// It represents a public view on the crate-view implementations of heuristics. +#[derive(EnumString, EnumVariantNames, Copy, Clone)] pub enum Heuristic<'a> { /// Implementation of a simple heuristic. /// This will just take the first not decided variable and maps it value to (`true`)[Term::TOP]. Simple, + /// Implementation of a heuristic, which which uses minimal number of [paths][crate::obdd::Bdd::paths] and maximal [variable-impact][crate::obdd::Bdd::passive_var_impact to identify the variable to be set. + /// As the value of the variable value with the minimal model-path is chosen. + MinModMinPathsMaxVarImp, /// Allow passing in an externally-defined custom heuristic. + #[strum(disabled)] Custom(&'a HeuristicFn), } +impl Default for Heuristic<'_> { + fn default() -> Self { + Self::Simple + } +} + impl std::fmt::Debug for Heuristic<'_> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { Self::Simple => write!(f, "Simple"), + Self::MinModMinPathsMaxVarImp => write!(f, "Minimal model count as value and minimum paths with maximal variable impact as variable choice"), Self::Custom(_) => f.debug_tuple("Custom function").finish(), } } @@ -42,7 +83,23 @@ impl Heuristic<'_> { pub(crate) fn get_heuristic(&self) -> &(dyn Fn(&Adf, &[Term]) -> RetVal + '_) { match self { Heuristic::Simple => &heu_simple, + Heuristic::MinModMinPathsMaxVarImp => &heu_mc_minpaths_maxvarimp, Self::Custom(f) => f, } } } + +// impl FromStr for Heuristic<'_> { +// type Err = (); + +// fn from_str(s: &str) -> Result { +// match s { +// "simple" => Ok(Self::Simple), +// "MinmcMinpathsMaxvarimp" => Ok(Self::MinModMinPathsMaxVarImp), +// _ => { +// log::info!("Unknown heuristic {s}"); +// Err(()) +// } +// } +// } +// } diff --git a/lib/src/datatypes/bdd.rs b/lib/src/datatypes/bdd.rs index b1c2975..5324b03 100644 --- a/lib/src/datatypes/bdd.rs +++ b/lib/src/datatypes/bdd.rs @@ -25,6 +25,16 @@ impl From for Term { } } +impl From for Term { + fn from(val: bool) -> Self { + if val { + Self::TOP + } else { + Self::BOT + } + } +} + impl From<&biodivine_lib_bdd::Bdd> for Term { fn from(val: &biodivine_lib_bdd::Bdd) -> Self { if val.is_true() { diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs index 155e4cf..07e15c1 100644 --- a/lib/src/nogoods.rs +++ b/lib/src/nogoods.rs @@ -2,7 +2,8 @@ use std::{ borrow::Borrow, - ops::{BitAnd, BitOr, BitXor}, + fmt::Display, + ops::{BitAnd, BitOr, BitXor, BitXorAssign}, }; use crate::datatypes::Term; @@ -117,12 +118,22 @@ impl NoGood { .borrow() .bitxor(other.active.borrow()) .bitand(self.active.borrow()); - if implication.len() == 1 { + + let bothactive = self.active.borrow().bitand(other.active.borrow()); + let mut no_matches = bothactive.borrow().bitand(other.value.borrow()); + no_matches.bitxor_assign(bothactive.bitand(self.value.borrow())); + + if implication.len() == 1 && no_matches.is_empty() { let pos = implication .min() .expect("just checked that there is one element to be found"); + log::trace!( + "Conclude {:?}", + Some((pos as usize, !self.value.contains(pos))) + ); Some((pos as usize, !self.value.contains(pos))) } else { + log::trace!("Nothing to Conclude"); None } } @@ -175,6 +186,16 @@ pub struct NoGoodStore { duplicates: DuplicateElemination, } +impl Display for NoGoodStore { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + writeln!(f, "NoGoodStats: [")?; + for (arity, vec) in self.store.iter().enumerate() { + writeln!(f, "{arity}: {}", vec.len())?; + } + write!(f, "]") + } +} + impl NoGoodStore { /// Creates a new [NoGoodStore] and assumes a size compatible with the underlying [NoGood] implementation. pub fn new(size: u32) -> NoGoodStore { @@ -227,6 +248,7 @@ impl NoGoodStore { /// *Returns* [None] if there is a conflict pub fn conclusions(&self, nogood: &NoGood) -> Option { let mut result = nogood.clone(); + log::trace!("ng-store: {:?}", self.store); self.store .iter() .enumerate() @@ -236,6 +258,7 @@ impl NoGoodStore { }) .try_fold(&mut result, |acc, ng| { if ng.is_violating(acc) { + log::trace!("ng conclusion violating"); None } else { acc.disjunction(&ng); @@ -261,7 +284,15 @@ impl NoGoodStore { pub(crate) fn conclusion_closure(&self, interpretation: &[Term]) -> ClosureResult { let mut update = true; let mut result = match self.conclusions(&interpretation.into()) { - Some(val) => val.update_term_vec(interpretation, &mut update), + Some(val) => { + log::trace!( + "conclusion-closure step 1: val:{:?} -> {:?}", + val, + val.update_term_vec(interpretation, &mut update) + ); + val.update_term_vec(interpretation, &mut update) + } + None => return ClosureResult::Inconsistent, }; if !update { @@ -786,7 +817,7 @@ mod test { assert_eq!( ngs.conclusion_closure(&[Term(1), Term(3), Term(3), Term(9), Term(0), Term(1)]), - ClosureResult::Update(vec![Term(1), Term(0), Term(0), Term(1), Term(0), Term(1)]) + ClosureResult::Update(vec![Term(1), Term(0), Term(3), Term(9), Term(0), Term(1)]) ); } } From 4eabf1692ba8b10759c119aa42ba70c96d0957b5 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Thu, 23 Jun 2022 12:36:20 +0200 Subject: [PATCH 20/51] Optimise ng learner further on and fix a verification bug Introduce a new flag to handle big instances (modelcount vs adhoccount) --- bin/Cargo.toml | 1 + lib/Cargo.toml | 3 ++- lib/src/adf.rs | 22 ++++++++++++++++++++++ lib/src/nogoods.rs | 3 ++- lib/src/obdd.rs | 7 +++++-- 5 files changed, 32 insertions(+), 4 deletions(-) diff --git a/bin/Cargo.toml b/bin/Cargo.toml index 33a8cb0..bac2933 100644 --- a/bin/Cargo.toml +++ b/bin/Cargo.toml @@ -33,3 +33,4 @@ adhoccounting = ["adf_bdd/adhoccounting"] # count models ad-hoc - disable if importexport = ["adf_bdd/importexport"] variablelist = [ "HashSet", "adf_bdd/variablelist" ] HashSet = ["adf_bdd/HashSet"] +adhoccountmodels = ["adf_bdd/adhoccountmodels"] \ No newline at end of file diff --git a/lib/Cargo.toml b/lib/Cargo.toml index 98a8007..3123fa6 100644 --- a/lib/Cargo.toml +++ b/lib/Cargo.toml @@ -41,7 +41,8 @@ quickcheck_macros = "1" [features] default = ["adhoccounting", "variablelist" ] -adhoccounting = [] # count models ad-hoc - disable if counting is not needed +adhoccounting = [] # count paths ad-hoc - disable if counting is not needed importexport = [] variablelist = [ "HashSet" ] HashSet = [] +adhoccountmodels = [ "adhoccounting" ] # count models as well as paths ad-hoc diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 9106951..1df4f1c 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -136,6 +136,8 @@ impl Adf { } } }); + log::trace!("ordering: {:?}", result.ordering); + log::trace!("adf {:?} instantiated with bdd {}", result.ac, result.bdd); result } @@ -812,6 +814,24 @@ impl Adf { } } + let ac_consistent_interpr = self.apply_interpretation(&self.ac.clone(), &cur_interpr); + log::trace!( + "checking consistency of {:?} against {:?}", + ac_consistent_interpr, + cur_interpr + ); + if cur_interpr + .iter() + .zip(ac_consistent_interpr.iter()) + .any(|(cur, ac)| { + cur.is_truth_value() && ac.is_truth_value() && cur.is_true() != ac.is_true() + }) + { + log::trace!("ac_inconsistency"); + backtrack = true; + continue; + } + cur_interpr = self.update_interpretation_fixpoint_upd(&cur_interpr, &mut update_fp); if update_fp { log::trace!("fixpount updated"); @@ -827,12 +847,14 @@ impl Adf { backtrack = true; } else { // not stable + log::trace!("2 val not stable"); stack.push((false, cur_interpr.as_slice().into())); backtrack = true; } } } log::info!("{ng_store}"); + log::debug!("{:?}", ng_store); result } } diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs index 07e15c1..133db5f 100644 --- a/lib/src/nogoods.rs +++ b/lib/src/nogoods.rs @@ -2,7 +2,7 @@ use std::{ borrow::Borrow, - fmt::Display, + fmt::{Debug, Display}, ops::{BitAnd, BitOr, BitXor, BitXorAssign}, }; @@ -191,6 +191,7 @@ impl Display for NoGoodStore { writeln!(f, "NoGoodStats: [")?; for (arity, vec) in self.store.iter().enumerate() { writeln!(f, "{arity}: {}", vec.len())?; + log::debug!("Nogoods:\n {:?}", vec); } write!(f, "]") } diff --git a/lib/src/obdd.rs b/lib/src/obdd.rs index 97f9268..f361d66 100644 --- a/lib/src/obdd.rs +++ b/lib/src/obdd.rs @@ -277,11 +277,14 @@ impl Bdd { hi_paths.models, hidepth ); + #[cfg(feature = "adhoccountmodels")] let (lo_exp, hi_exp) = if lodepth > hidepth { (1, 2usize.pow((lodepth - hidepth) as u32)) } else { (2usize.pow((hidepth - lodepth) as u32), 1) }; + #[cfg(not(feature = "adhoccountmodels"))] + let (lo_exp, hi_exp) = (0, 0); log::debug!("lo_exp {}, hi_exp {}", lo_exp, hi_exp); count_cache.insert( new_term, @@ -310,11 +313,11 @@ impl Bdd { /// /// Use the flag `_memoization` to choose between using the memoization approach or not. (This flag does nothing, if the feature `adhoccounting` is used) pub fn models(&self, term: Term, _memoization: bool) -> ModelCounts { - #[cfg(feature = "adhoccounting")] + #[cfg(feature = "adhoccountmodels")] { return self.count_cache.borrow().get(&term).expect("The term should be originating from this bdd, otherwise the result would be inconsistent anyways").0; } - #[cfg(not(feature = "adhoccounting"))] + #[cfg(not(feature = "adhoccountmodels"))] if _memoization { self.modelcount_memoization(term).0 } else { From 0dc35d39d5579c5d451228182cacd5c5bed67dd5 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Thu, 23 Jun 2022 14:02:53 +0200 Subject: [PATCH 21/51] Fix tests, which are changed due to the new feature flag --- lib/Cargo.toml | 2 +- lib/src/adf.rs | 3 +- lib/src/obdd.rs | 87 ++++++++++++++++++++++++++----------------------- 3 files changed, 50 insertions(+), 42 deletions(-) diff --git a/lib/Cargo.toml b/lib/Cargo.toml index 3123fa6..d13c6cb 100644 --- a/lib/Cargo.toml +++ b/lib/Cargo.toml @@ -45,4 +45,4 @@ adhoccounting = [] # count paths ad-hoc - disable if counting is not needed importexport = [] variablelist = [ "HashSet" ] HashSet = [] -adhoccountmodels = [ "adhoccounting" ] # count models as well as paths ad-hoc +adhoccountmodels = [ "adhoccounting" ] # count models as well as paths ad-hoc note that facet methods will need this feature too diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 1df4f1c..837910c 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -1146,6 +1146,7 @@ mod test { } } + #[cfg(feature = "adhoccountmodels")] #[test] fn formulacounts() { let parser = AdfParser::default(); @@ -1160,7 +1161,7 @@ mod test { fn adf_default() { let _adf = Adf::default(); } - + #[cfg(feature = "adhoccountmodels")] #[test] fn facet_counts() { let parser = AdfParser::default(); diff --git a/lib/src/obdd.rs b/lib/src/obdd.rs index f361d66..0a653c4 100644 --- a/lib/src/obdd.rs +++ b/lib/src/obdd.rs @@ -645,6 +645,7 @@ mod test { let formula3 = bdd.xor(v1, v2); let formula4 = bdd.and(v3, formula2); + #[cfg(feature = "adhoccountmodels")] assert_eq!(bdd.models(v1, false), (1, 1).into()); let mut x = bdd.count_cache.get_mut().iter().collect::>(); x.sort(); @@ -653,20 +654,23 @@ mod test { log::debug!("{:?}", x); } log::debug!("{:?}", x); - assert_eq!(bdd.models(formula1, false), (3, 1).into()); - assert_eq!(bdd.models(formula2, false), (1, 3).into()); - assert_eq!(bdd.models(formula3, false), (2, 2).into()); - assert_eq!(bdd.models(formula4, false), (5, 3).into()); - assert_eq!(bdd.models(Term::TOP, false), (0, 1).into()); - assert_eq!(bdd.models(Term::BOT, false), (1, 0).into()); - - assert_eq!(bdd.models(v1, true), (1, 1).into()); - assert_eq!(bdd.models(formula1, true), (3, 1).into()); - assert_eq!(bdd.models(formula2, true), (1, 3).into()); - assert_eq!(bdd.models(formula3, true), (2, 2).into()); - assert_eq!(bdd.models(formula4, true), (5, 3).into()); - assert_eq!(bdd.models(Term::TOP, true), (0, 1).into()); - assert_eq!(bdd.models(Term::BOT, true), (1, 0).into()); + #[cfg(feature = "adhoccountmodels")] + { + assert_eq!(bdd.models(formula1, false), (3, 1).into()); + assert_eq!(bdd.models(formula2, false), (1, 3).into()); + assert_eq!(bdd.models(formula3, false), (2, 2).into()); + assert_eq!(bdd.models(formula4, false), (5, 3).into()); + assert_eq!(bdd.models(Term::TOP, false), (0, 1).into()); + assert_eq!(bdd.models(Term::BOT, false), (1, 0).into()); + + assert_eq!(bdd.models(v1, true), (1, 1).into()); + assert_eq!(bdd.models(formula1, true), (3, 1).into()); + assert_eq!(bdd.models(formula2, true), (1, 3).into()); + assert_eq!(bdd.models(formula3, true), (2, 2).into()); + assert_eq!(bdd.models(formula4, true), (5, 3).into()); + assert_eq!(bdd.models(Term::TOP, true), (0, 1).into()); + assert_eq!(bdd.models(Term::BOT, true), (1, 0).into()); + } assert_eq!(bdd.paths(formula1, false), (2, 1).into()); assert_eq!(bdd.paths(formula2, false), (1, 2).into()); @@ -709,32 +713,35 @@ mod test { ((1, 0).into(), (1, 0).into(), 0) ); - assert_eq!( - bdd.modelcount_naive(formula4), - bdd.modelcount_memoization(formula4) - ); - - assert_eq!(bdd.modelcount_naive(v1), bdd.modelcount_memoization(v1)); - assert_eq!( - bdd.modelcount_naive(formula1), - bdd.modelcount_memoization(formula1) - ); - assert_eq!( - bdd.modelcount_naive(formula2), - bdd.modelcount_memoization(formula2) - ); - assert_eq!( - bdd.modelcount_naive(formula3), - bdd.modelcount_memoization(formula3) - ); - assert_eq!( - bdd.modelcount_naive(Term::TOP), - bdd.modelcount_memoization(Term::TOP) - ); - assert_eq!( - bdd.modelcount_naive(Term::BOT), - bdd.modelcount_memoization(Term::BOT) - ); + #[cfg(feature = "adhoccountmodels")] + { + assert_eq!( + bdd.modelcount_naive(formula4), + bdd.modelcount_memoization(formula4) + ); + + assert_eq!(bdd.modelcount_naive(v1), bdd.modelcount_memoization(v1)); + assert_eq!( + bdd.modelcount_naive(formula1), + bdd.modelcount_memoization(formula1) + ); + assert_eq!( + bdd.modelcount_naive(formula2), + bdd.modelcount_memoization(formula2) + ); + assert_eq!( + bdd.modelcount_naive(formula3), + bdd.modelcount_memoization(formula3) + ); + assert_eq!( + bdd.modelcount_naive(Term::TOP), + bdd.modelcount_memoization(Term::TOP) + ); + assert_eq!( + bdd.modelcount_naive(Term::BOT), + bdd.modelcount_memoization(Term::BOT) + ); + } assert_eq!(bdd.max_depth(Term::BOT), 0); assert_eq!(bdd.max_depth(v1), 1); From 55e6c30472e81eb4f66245d612f9a41907f172ad Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Fri, 24 Jun 2022 16:02:44 +0200 Subject: [PATCH 22/51] Add new heuristic maxvarimp_minpaths has been implemented --- lib/src/adf/heuristics.rs | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/lib/src/adf/heuristics.rs b/lib/src/adf/heuristics.rs index 7e7eb23..e28f56b 100644 --- a/lib/src/adf/heuristics.rs +++ b/lib/src/adf/heuristics.rs @@ -48,6 +48,34 @@ pub(crate) fn heu_mc_minpaths_maxvarimp(adf: &Adf, interpr: &[Term]) -> Option<( }) } +pub(crate) fn heu_mc_maxvarimp_minpaths(adf: &Adf, interpr: &[Term]) -> Option<(Var, Term)> { + interpr + .iter() + .enumerate() + .filter(|(_var, term)| !term.is_truth_value()) + .min_by(|(vara, &terma), (varb, &termb)| { + match adf + .bdd + .passive_var_impact(Var::from(*vara), interpr) + .cmp(&adf.bdd.passive_var_impact(Var::from(*varb), interpr)) + { + std::cmp::Ordering::Equal => adf + .bdd + .paths(terma, true) + .minimum() + .cmp(&adf.bdd.paths(termb, true).minimum()), + + value => value, + } + }) + .map(|(var, term)| { + ( + Var::from(var), + (!adf.bdd.paths(*term, true).more_models()).into(), + ) + }) +} + /// Enumeration of all currently implemented heuristics. /// It represents a public view on the crate-view implementations of heuristics. #[derive(EnumString, EnumVariantNames, Copy, Clone)] @@ -58,6 +86,9 @@ pub enum Heuristic<'a> { /// Implementation of a heuristic, which which uses minimal number of [paths][crate::obdd::Bdd::paths] and maximal [variable-impact][crate::obdd::Bdd::passive_var_impact to identify the variable to be set. /// As the value of the variable value with the minimal model-path is chosen. MinModMinPathsMaxVarImp, + /// Implementation of a heuristic, which which uses maximal [variable-impact][crate::obdd::Bdd::passive_var_impact] and minimal number of [paths][crate::obdd::Bdd::paths] to identify the variable to be set. + /// As the value of the variable value with the minimal model-path is chosen. + MinModMaxVarImpMinPaths, /// Allow passing in an externally-defined custom heuristic. #[strum(disabled)] Custom(&'a HeuristicFn), @@ -74,6 +105,7 @@ impl std::fmt::Debug for Heuristic<'_> { match self { Self::Simple => write!(f, "Simple"), Self::MinModMinPathsMaxVarImp => write!(f, "Minimal model count as value and minimum paths with maximal variable impact as variable choice"), + Self::MinModMaxVarImpMinPaths => write!(f, "Minimal model count as value and maximal variable impact with minimum paths as variable choice"), Self::Custom(_) => f.debug_tuple("Custom function").finish(), } } @@ -84,6 +116,7 @@ impl Heuristic<'_> { match self { Heuristic::Simple => &heu_simple, Heuristic::MinModMinPathsMaxVarImp => &heu_mc_minpaths_maxvarimp, + Heuristic::MinModMaxVarImpMinPaths => &heu_mc_maxvarimp_minpaths, Self::Custom(f) => f, } } From 83b403baf24fd1ec003a97ba02461d8198239766 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Fri, 24 Jun 2022 16:06:51 +0200 Subject: [PATCH 23/51] Modified heuristics --- lib/src/adf/heuristics.rs | 27 ++++++--------------------- 1 file changed, 6 insertions(+), 21 deletions(-) diff --git a/lib/src/adf/heuristics.rs b/lib/src/adf/heuristics.rs index e28f56b..e649714 100644 --- a/lib/src/adf/heuristics.rs +++ b/lib/src/adf/heuristics.rs @@ -43,7 +43,7 @@ pub(crate) fn heu_mc_minpaths_maxvarimp(adf: &Adf, interpr: &[Term]) -> Option<( .map(|(var, term)| { ( Var::from(var), - (!adf.bdd.paths(*term, true).more_models()).into(), + adf.bdd.paths(*term, true).more_models().into(), ) }) } @@ -71,7 +71,7 @@ pub(crate) fn heu_mc_maxvarimp_minpaths(adf: &Adf, interpr: &[Term]) -> Option<( .map(|(var, term)| { ( Var::from(var), - (!adf.bdd.paths(*term, true).more_models()).into(), + adf.bdd.paths(*term, true).more_models().into(), ) }) } @@ -84,10 +84,10 @@ pub enum Heuristic<'a> { /// This will just take the first not decided variable and maps it value to (`true`)[Term::TOP]. Simple, /// Implementation of a heuristic, which which uses minimal number of [paths][crate::obdd::Bdd::paths] and maximal [variable-impact][crate::obdd::Bdd::passive_var_impact to identify the variable to be set. - /// As the value of the variable value with the minimal model-path is chosen. + /// As the value of the variable value with the maximal model-path is chosen. MinModMinPathsMaxVarImp, /// Implementation of a heuristic, which which uses maximal [variable-impact][crate::obdd::Bdd::passive_var_impact] and minimal number of [paths][crate::obdd::Bdd::paths] to identify the variable to be set. - /// As the value of the variable value with the minimal model-path is chosen. + /// As the value of the variable value with the maximal model-path is chosen. MinModMaxVarImpMinPaths, /// Allow passing in an externally-defined custom heuristic. #[strum(disabled)] @@ -104,8 +104,8 @@ impl std::fmt::Debug for Heuristic<'_> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { Self::Simple => write!(f, "Simple"), - Self::MinModMinPathsMaxVarImp => write!(f, "Minimal model count as value and minimum paths with maximal variable impact as variable choice"), - Self::MinModMaxVarImpMinPaths => write!(f, "Minimal model count as value and maximal variable impact with minimum paths as variable choice"), + Self::MinModMinPathsMaxVarImp => write!(f, "Maximal model-path count as value and minimum paths with maximal variable impact as variable choice"), + Self::MinModMaxVarImpMinPaths => write!(f, "Maximal model-path count as value and maximal variable impact with minimum paths as variable choice"), Self::Custom(_) => f.debug_tuple("Custom function").finish(), } } @@ -121,18 +121,3 @@ impl Heuristic<'_> { } } } - -// impl FromStr for Heuristic<'_> { -// type Err = (); - -// fn from_str(s: &str) -> Result { -// match s { -// "simple" => Ok(Self::Simple), -// "MinmcMinpathsMaxvarimp" => Ok(Self::MinModMinPathsMaxVarImp), -// _ => { -// log::info!("Unknown heuristic {s}"); -// Err(()) -// } -// } -// } -// } From c6f112b4ed207c90201904c2d1741e5db3602f5b Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 26 Jul 2022 10:55:05 +0200 Subject: [PATCH 24/51] Add crossbeam-channel to represent an output-stream of stable models Uses a crossbeam-channel to fill a Queue, which can be used safely from outside the function. This rework is done to also allow ad-hoc output of results in a potentially multi-threaded setup. --- Cargo.lock | 11 +++++++++ lib/Cargo.toml | 1 + lib/src/adf.rs | 66 ++++++++++++++++++++++++++++++++++++++++---------- 3 files changed, 65 insertions(+), 13 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index de26c5e..9e7db04 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -7,6 +7,7 @@ name = "adf_bdd" version = "0.2.5" dependencies = [ "biodivine-lib-bdd", + "crossbeam-channel", "derivative", "env_logger 0.9.0", "lexical-sort", @@ -182,6 +183,16 @@ dependencies = [ "os_str_bytes", ] +[[package]] +name = "crossbeam-channel" +version = "0.5.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c2dd04ddaf88237dc3b8d8f9a3c1004b506b54b3313403944054d23c0870c521" +dependencies = [ + "cfg-if", + "crossbeam-utils", +] + [[package]] name = "crossbeam-utils" version = "0.8.7" diff --git a/lib/Cargo.toml b/lib/Cargo.toml index d13c6cb..ad05d20 100644 --- a/lib/Cargo.toml +++ b/lib/Cargo.toml @@ -32,6 +32,7 @@ biodivine-lib-bdd = "0.4.0" derivative = "2.2.0" roaring = "0.9.0" strum = { version = "0.24", features = ["derive"] } +crossbeam-channel = "0.5" [dev-dependencies] test-log = "0.2" diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 837910c..c466709 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -6,9 +6,6 @@ This module describes the abstract dialectical framework. */ pub mod heuristics; - -use serde::{Deserialize, Serialize}; - use crate::{ datatypes::{ adf::{ @@ -21,6 +18,7 @@ use crate::{ obdd::Bdd, parser::{AdfParser, Formula}, }; +use serde::{Deserialize, Serialize}; use self::heuristics::Heuristic; @@ -729,7 +727,7 @@ impl Adf { .collect::>() } - /// Computes the stable extensions of a given [`Adf`], using the [`NoGood`]-learner + /// Computes the stable extensions of a given [`Adf`], using the [`NoGood`]-learner. pub fn stable_nogood<'a, 'c>( &'a mut self, heuristic: Heuristic, @@ -739,14 +737,43 @@ impl Adf { { let grounded = self.grounded(); let heu = heuristic.get_heuristic(); - self.stable_nogood_internal(&grounded, heu).into_iter() + let (s, r) = crossbeam_channel::unbounded::>(); + self.stable_nogood_get_vec(&grounded, heu, s, r).into_iter() + } + + /// Computes the stable extension of a given [`Adf`], using the [`NoGood`]-learner. + /// Needs a [`Sender`][crossbeam_channel::Sender>] where the results of the computation can be put to. + pub fn stable_nogood_channel( + &mut self, + heuristic: Heuristic, + sender: crossbeam_channel::Sender>, + ) { + let grounded = self.grounded(); + self.stable_nogood_internal(&grounded, heuristic.get_heuristic(), sender); } - fn stable_nogood_internal(&mut self, interpretation: &[Term], heuristic: H) -> Vec> + fn stable_nogood_get_vec( + &mut self, + interpretation: &[Term], + heuristic: H, + s: crossbeam_channel::Sender>, + r: crossbeam_channel::Receiver>, + ) -> Vec> where H: Fn(&Self, &[Term]) -> Option<(Var, Term)>, { - let mut result = Vec::new(); + self.stable_nogood_internal(interpretation, heuristic, s); + r.iter().collect() + } + + fn stable_nogood_internal( + &mut self, + interpretation: &[Term], + heuristic: H, + s: crossbeam_channel::Sender>, + ) where + H: Fn(&Self, &[Term]) -> Option<(Var, Term)>, + { let mut cur_interpr = interpretation.to_vec(); let mut ng_store = NoGoodStore::new( self.ac @@ -843,7 +870,8 @@ impl Adf { } else if self.stability_check(&cur_interpr) { // stable model found stack.push((false, cur_interpr.as_slice().into())); - result.push(cur_interpr.clone()); + s.send(cur_interpr.clone()) + .expect("Sender should accept results"); backtrack = true; } else { // not stable @@ -855,13 +883,13 @@ impl Adf { } log::info!("{ng_store}"); log::debug!("{:?}", ng_store); - result } } #[cfg(test)] mod test { use super::*; + use crossbeam_channel::unbounded; use test_log::test; #[test] @@ -1050,10 +1078,11 @@ mod test { let mut adf = Adf::from_parser(&parser); let grounded = adf.grounded(); - let stable = adf.stable_nogood_internal(&grounded, crate::adf::heuristics::heu_simple); + let (s, r) = unbounded(); + adf.stable_nogood_internal(&grounded, crate::adf::heuristics::heu_simple, s); assert_eq!( - stable, + r.iter().collect::>(), vec![vec![ Term::TOP, Term::BOT, @@ -1081,8 +1110,13 @@ mod test { 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 (s, r) = unbounded(); + adf.stable_nogood_internal(&grounded, crate::adf::heuristics::heu_simple, s.clone()); + let stable_result = r.try_iter().collect::>(); + assert_eq!( + stable_result, + vec![vec![Term(1), Term(0)], vec![Term(0), Term(1)]] + ); let stable = adf.stable_nogood(Heuristic::Simple); assert_eq!( @@ -1102,6 +1136,12 @@ mod test { stable.collect::>(), vec![vec![Term(0), Term(1)], vec![Term(1), Term(0)]] ); + + adf.stable_nogood_channel(Heuristic::Simple, s); + assert_eq!( + r.iter().collect::>(), + vec![vec![Term(1), Term(0)], vec![Term(0), Term(1)]] + ); } #[test] From 80e1ca998d6f89fc7a95241390e9075f0f22abb3 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 26 Jul 2022 11:34:16 +0200 Subject: [PATCH 25/51] Add test-case to show multi-threaded use of the ng solver Added a bit of documentation on this new feature on the module-page --- lib/src/adf.rs | 38 ++++++++++++++++++++++++++++++++++++++ lib/src/lib.rs | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 71 insertions(+) diff --git a/lib/src/adf.rs b/lib/src/adf.rs index c466709..3678f0d 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -1142,6 +1142,44 @@ mod test { r.iter().collect::>(), vec![vec![Term(1), Term(0)], vec![Term(0), Term(1)]] ); + + // multi-threaded usage + let (s, r) = unbounded(); + let solving = std::thread::spawn(move || { + let parser = AdfParser::default(); + parser.parse()("s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,b).ac(c,and(a,b)).ac(d,neg(b)).\ns(e).ac(e,and(b,or(neg(b),c(f)))).s(f).\n\nac(f,xor(a,e)).") + .unwrap(); + let mut adf = Adf::from_parser(&parser); + adf.stable_nogood_channel(Heuristic::MinModMaxVarImpMinPaths, s.clone()); + adf.stable_nogood_channel(Heuristic::MinModMinPathsMaxVarImp, s); + }); + + let mut result_vec = Vec::new(); + while let Ok(result) = r.recv() { + result_vec.push(result); + } + assert_eq!( + result_vec, + vec![ + vec![ + Term::TOP, + Term::BOT, + Term::BOT, + Term::TOP, + Term::BOT, + Term::TOP + ], + vec![ + Term::TOP, + Term::BOT, + Term::BOT, + Term::TOP, + Term::BOT, + Term::TOP + ] + ] + ); + solving.join().unwrap(); } #[test] diff --git a/lib/src/lib.rs b/lib/src/lib.rs index 5fba465..f826d7c 100644 --- a/lib/src/lib.rs +++ b/lib/src/lib.rs @@ -159,6 +159,39 @@ let printer = adf.print_dictionary(); for model in adf.complete() { print!("{}", printer.print_interpretation(&model)); } +``` + +### Using the [`NoGood`]-learner approach, together with the [`crossbeam-channel`] implementation +This can be used to have a worker and a consumer thread to print the results as they are computed. +Please note that the [`NoGood`]-learner needs a heuristics function to work. +The enum [`Heuristic`][adf_bdd::adf::heuristics::Heuristic] allows one to choose a pre-defined heuristic, or implement a `Custom` one. +```rust +use adf_bdd::parser::AdfParser; +use adf_bdd::adf::Adf; +use adf_bdd::adf::heuristics::Heuristic; +use adf_bdd::datatypes::Term; +// create a channel +let (s, r) = crossbeam_channel::unbounded(); +// spawn a solver thread +let solving = std::thread::spawn(move || { + // use the above example as input + let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d)."; + let parser = AdfParser::default(); + parser.parse()(&input).expect("parsing worked well"); + // use hybrid approach + let mut adf = adf_bdd::adfbiodivine::Adf::from_parser(&parser).hybrid_step(); + // compute stable with the simple heuristic + adf.stable_nogood_channel(Heuristic::Simple, s); +}); + +// print results as they are computed +while let Ok(result) = r.recv() { + println!("stable model: {:?}", result); +# assert_eq!(result, vec![Term(1),Term(1),Term(0),Term(0)]); +} +// waiting for the other thread to close +solving.join().unwrap(); + ``` */ #![deny( From 6215573925c0a5d47c6c339a1b8031bc58f0ba55 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 26 Jul 2022 11:47:51 +0200 Subject: [PATCH 26/51] Add better test coverage --- lib/src/adf.rs | 2 +- lib/src/adf/heuristics.rs | 16 ++++++++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 3678f0d..48e7082 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -1137,7 +1137,7 @@ mod test { vec![vec![Term(0), Term(1)], vec![Term(1), Term(0)]] ); - adf.stable_nogood_channel(Heuristic::Simple, s); + adf.stable_nogood_channel(Heuristic::default(), s); assert_eq!( r.iter().collect::>(), vec![vec![Term(1), Term(0)], vec![Term(0), Term(1)]] diff --git a/lib/src/adf/heuristics.rs b/lib/src/adf/heuristics.rs index e649714..2cbb9f6 100644 --- a/lib/src/adf/heuristics.rs +++ b/lib/src/adf/heuristics.rs @@ -121,3 +121,19 @@ impl Heuristic<'_> { } } } +#[cfg(test)] +mod test { + use super::*; + use crate::datatypes::Term; + use crate::datatypes::Var; + + #[test] + fn debug_out() { + dbg!(Heuristic::Simple); + dbg!(Heuristic::MinModMaxVarImpMinPaths); + dbg!(Heuristic::MinModMinPathsMaxVarImp); + dbg!(Heuristic::Custom(&|_adf: &Adf, + _int: &[Term]| + -> Option<(Var, Term)> { None })); + } +} From ea1043620ad76c4b6e80d69033189560988a5be3 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 26 Jul 2022 11:56:51 +0200 Subject: [PATCH 27/51] Fix broken links in rust-doc --- lib/src/lib.rs | 6 +++--- lib/src/nogoods.rs | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/src/lib.rs b/lib/src/lib.rs index f826d7c..f15c7eb 100644 --- a/lib/src/lib.rs +++ b/lib/src/lib.rs @@ -161,10 +161,10 @@ for model in adf.complete() { } ``` -### Using the [`NoGood`]-learner approach, together with the [`crossbeam-channel`] implementation +### Using the [`NoGood`][crate::nogoods::NoGood]-learner approach, together with the [`crossbeam-channel`] implementation This can be used to have a worker and a consumer thread to print the results as they are computed. -Please note that the [`NoGood`]-learner needs a heuristics function to work. -The enum [`Heuristic`][adf_bdd::adf::heuristics::Heuristic] allows one to choose a pre-defined heuristic, or implement a `Custom` one. +Please note that the [`NoGood`][crate::nogoods::NoGood]-learner needs a heuristics function to work. +The enum [`Heuristic`][crate::adf::heuristics::Heuristic] allows one to choose a pre-defined heuristic, or implement a `Custom` one. ```rust use adf_bdd::parser::AdfParser; use adf_bdd::adf::Adf; diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs index 133db5f..ef117e5 100644 --- a/lib/src/nogoods.rs +++ b/lib/src/nogoods.rs @@ -245,7 +245,7 @@ impl NoGoodStore { } } - /// Draws a (Conclusion)[NoGood], based on the [NoGoodstore] and the given [NoGood]. + /// Draws a (Conclusion)[NoGood], based on the [NoGoodStore] and the given [NoGood]. /// *Returns* [None] if there is a conflict pub fn conclusions(&self, nogood: &NoGood) -> Option { let mut result = nogood.clone(); From 1163f305fc74d2c12c54502ef7b4a37bd4e103f5 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 26 Jul 2022 12:03:38 +0200 Subject: [PATCH 28/51] Update Readme for lib to reflect the new NoGood API --- lib/README.md | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/lib/README.md b/lib/README.md index ff2af33..fd652d0 100644 --- a/lib/README.md +++ b/lib/README.md @@ -122,6 +122,34 @@ for model in adf.complete() { } ``` +use the new `NoGood`-based algorithm and utilise the new interface with channels: +```rust +use adf_bdd::parser::AdfParser; +use adf_bdd::adf::Adf; +use adf_bdd::adf::heuristics::Heuristic; +use adf_bdd::datatypes::Term; +// create a channel +let (s, r) = crossbeam_channel::unbounded(); +// spawn a solver thread +let solving = std::thread::spawn(move || { + // use the above example as input + let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d)."; + let parser = AdfParser::default(); + parser.parse()(&input).expect("parsing worked well"); + // use hybrid approach + let mut adf = adf_bdd::adfbiodivine::Adf::from_parser(&parser).hybrid_step(); + // compute stable with the simple heuristic + adf.stable_nogood_channel(Heuristic::Simple, s); +}); + +// print results as they are computed +while let Ok(result) = r.recv() { + println!("stable model: {:?}", result); +} +// waiting for the other thread to close +solving.join().unwrap(); +``` + # Acknowledgements This work is partly supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) in projects number 389792660 (TRR 248, [Center for Perspicuous Systems](https://www.perspicuous-computing.science/)), the Bundesministerium für Bildung und Forschung (BMBF, Federal Ministry of Education and Research) in the From e1b9eeb3b28f50f2a2364110a30bb98110759fe8 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 26 Jul 2022 12:19:00 +0200 Subject: [PATCH 29/51] Add metadata to bin/Cargo.toml, add features added a benchmark feature, to easily compile benchmark-releases --- bin/Cargo.toml | 7 +++++-- lib/Cargo.toml | 1 + 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/bin/Cargo.toml b/bin/Cargo.toml index 5374876..6a5ccaf 100644 --- a/bin/Cargo.toml +++ b/bin/Cargo.toml @@ -3,8 +3,10 @@ name = "adf_bdd-solver" version = "0.2.5" authors = ["Stefan Ellmauthaler "] edition = "2021" +homepage = "https://ellmau.github.io/adf-obdd" +repository = "https://github.com/ellmau/adf-obdd" license = "MIT" -exclude = ["res/", "./flake*", "*.nix", ".envrc", "_config.yml"] +exclude = ["res/", "./flake*", "*.nix", ".envrc", "_config.yml", "tarpaulin-report.*", "*~"] description = "Solver for ADFs grounded, complete, and stable semantics by utilising OBDDs - ordered binary decision diagrams" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html @@ -33,4 +35,5 @@ adhoccounting = ["adf_bdd/adhoccounting"] # count models ad-hoc - disable if importexport = ["adf_bdd/importexport"] variablelist = [ "HashSet", "adf_bdd/variablelist" ] HashSet = ["adf_bdd/HashSet"] -adhoccountmodels = ["adf_bdd/adhoccountmodels"] \ No newline at end of file +adhoccountmodels = ["adf_bdd/adhoccountmodels"] +benchmark = ["adf_bdd/benchmark"] \ No newline at end of file diff --git a/lib/Cargo.toml b/lib/Cargo.toml index ad05d20..33b761b 100644 --- a/lib/Cargo.toml +++ b/lib/Cargo.toml @@ -47,3 +47,4 @@ importexport = [] variablelist = [ "HashSet" ] HashSet = [] adhoccountmodels = [ "adhoccounting" ] # count models as well as paths ad-hoc note that facet methods will need this feature too +benchmark = ["adhoccounting", "variablelist"] # set of features for speed benchmarks From 00674f7c5ea4ecc00a603cfef02c460ec629da6e Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 26 Jul 2022 14:42:27 +0200 Subject: [PATCH 30/51] Fix facet count tests --- lib/src/adf.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 48e7082..4d812a4 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -710,7 +710,7 @@ impl Adf { interpretation .iter() .map(|t| { - let mcs = self.bdd.models(*t, true); + let mcs = self.bdd.models(*t, false); let n_vdps = { |t| self.bdd.var_dependencies(t).len() }; @@ -1239,7 +1239,7 @@ mod test { fn adf_default() { let _adf = Adf::default(); } - #[cfg(feature = "adhoccountmodels")] + //#[cfg(feature = "adhoccountmodels")] #[test] fn facet_counts() { let parser = AdfParser::default(); From 84aa627159d86c5485f1c29ece7473eeafe28d6e Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Wed, 27 Jul 2022 11:50:14 +0200 Subject: [PATCH 31/51] Add multithread-safe functionality for the dictionary/ordering * Streamline a couple of API calls * Expose more structs and methods to the public API * Breaking some API (though nothing which is currently used in the binary) --- lib/src/adf.rs | 44 +++++++++++----------- lib/src/adfbiodivine.rs | 16 ++++---- lib/src/datatypes/adf.rs | 62 ++++++++++++++++++------------ lib/src/lib.rs | 11 ++++-- lib/src/parser.rs | 81 +++++++++++++++++++++++++++++----------- 5 files changed, 135 insertions(+), 79 deletions(-) diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 4d812a4..6063bac 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -47,19 +47,14 @@ impl Adf { pub fn from_parser(parser: &AdfParser) -> Self { log::info!("[Start] instantiating BDD"); let mut result = Self { - ordering: VarContainer::from_parser( - parser.namelist_rc_refcell(), - parser.dict_rc_refcell(), - ), + ordering: parser.var_container(), bdd: Bdd::new(), - ac: vec![Term(0); parser.namelist_rc_refcell().as_ref().borrow().len()], + ac: vec![Term(0); parser.dict_size()], }; - (0..parser.namelist_rc_refcell().borrow().len()) - .into_iter() - .for_each(|value| { - log::trace!("adding variable {}", Var(value)); - result.bdd.variable(Var(value)); - }); + (0..parser.dict_size()).into_iter().for_each(|value| { + log::trace!("adding variable {}", Var(value)); + result.bdd.variable(Var(value)); + }); log::debug!("[Start] adding acs"); parser .formula_order() @@ -87,7 +82,7 @@ impl Adf { bio_ac: &[biodivine_lib_bdd::Bdd], ) -> Self { let mut result = Self { - ordering: VarContainer::copy(ordering), + ordering: ordering.clone(), bdd: Bdd::new(), ac: vec![Term(0); bio_ac.len()], }; @@ -900,11 +895,16 @@ mod test { parser.parse()(input).unwrap(); let adf = Adf::from_parser(&parser); - assert_eq!(adf.ordering.names().as_ref().borrow()[0], "a"); - assert_eq!(adf.ordering.names().as_ref().borrow()[1], "c"); - assert_eq!(adf.ordering.names().as_ref().borrow()[2], "b"); - assert_eq!(adf.ordering.names().as_ref().borrow()[3], "e"); - assert_eq!(adf.ordering.names().as_ref().borrow()[4], "d"); + assert_eq!(adf.ordering.name(Var(0)), Some("a".to_string())); + assert_eq!(adf.ordering.names().read().unwrap()[0], "a"); + assert_eq!(adf.ordering.name(Var(1)), Some("c".to_string())); + assert_eq!(adf.ordering.names().read().unwrap()[1], "c"); + assert_eq!(adf.ordering.name(Var(2)), Some("b".to_string())); + assert_eq!(adf.ordering.names().read().unwrap()[2], "b"); + assert_eq!(adf.ordering.name(Var(3)), Some("e".to_string())); + assert_eq!(adf.ordering.names().read().unwrap()[3], "e"); + assert_eq!(adf.ordering.name(Var(4)), Some("d".to_string())); + assert_eq!(adf.ordering.names().read().unwrap()[4], "d"); assert_eq!(adf.ac, vec![Term(4), Term(2), Term(7), Term(15), Term(12)]); @@ -915,11 +915,11 @@ mod test { parser.varsort_alphanum(); let adf = Adf::from_parser(&parser); - assert_eq!(adf.ordering.names().as_ref().borrow()[0], "a"); - assert_eq!(adf.ordering.names().as_ref().borrow()[1], "b"); - assert_eq!(adf.ordering.names().as_ref().borrow()[2], "c"); - assert_eq!(adf.ordering.names().as_ref().borrow()[3], "d"); - assert_eq!(adf.ordering.names().as_ref().borrow()[4], "e"); + assert_eq!(adf.ordering.names().read().unwrap()[0], "a"); + assert_eq!(adf.ordering.names().read().unwrap()[1], "b"); + assert_eq!(adf.ordering.names().read().unwrap()[2], "c"); + assert_eq!(adf.ordering.names().read().unwrap()[3], "d"); + assert_eq!(adf.ordering.names().read().unwrap()[4], "e"); assert_eq!(adf.ac, vec![Term(3), Term(7), Term(2), Term(11), Term(13)]); } diff --git a/lib/src/adfbiodivine.rs b/lib/src/adfbiodivine.rs index c5d94d1..c5d76df 100644 --- a/lib/src/adfbiodivine.rs +++ b/lib/src/adfbiodivine.rs @@ -40,19 +40,17 @@ impl Adf { pub fn from_parser(parser: &AdfParser) -> Self { log::info!("[Start] instantiating BDD"); let mut bdd_var_builder = biodivine_lib_bdd::BddVariableSetBuilder::new(); - let namelist = parser.namelist_rc_refcell().as_ref().borrow().clone(); + let namelist = parser + .namelist() + .read() + .expect("ReadLock on namelist failed") + .clone(); let slice_vec: Vec<&str> = namelist.iter().map(<_>::as_ref).collect(); bdd_var_builder.make_variables(&slice_vec); let bdd_variables = bdd_var_builder.build(); let mut result = Self { - ordering: VarContainer::from_parser( - parser.namelist_rc_refcell(), - parser.dict_rc_refcell(), - ), - ac: vec![ - bdd_variables.mk_false(); - parser.namelist_rc_refcell().as_ref().borrow().len() - ], + ordering: parser.var_container(), + ac: vec![bdd_variables.mk_false(); parser.dict_size()], vars: bdd_variables.variables(), varset: bdd_variables, rewrite: None, diff --git a/lib/src/datatypes/adf.rs b/lib/src/datatypes/adf.rs index 2716d4f..c4db79d 100644 --- a/lib/src/datatypes/adf.rs +++ b/lib/src/datatypes/adf.rs @@ -2,49 +2,63 @@ use super::{Term, Var}; use serde::{Deserialize, Serialize}; -use std::{cell::RefCell, collections::HashMap, fmt::Display, rc::Rc}; - -#[derive(Serialize, Deserialize, Debug)] -pub(crate) struct VarContainer { - names: Rc>>, - mapping: Rc>>, +use std::{collections::HashMap, fmt::Display, sync::Arc, sync::RwLock}; + +/// A container which acts as a dictionary as well as an ordering of variables. +/// *names* is a list of variable-names and the sequence of the values is inducing the order of variables. +/// *mapping* allows to search for a variable name and to receive the corresponding position in the variable list (`names`). +#[derive(Serialize, Deserialize, Debug, Clone)] +pub struct VarContainer { + names: Arc>>, + mapping: Arc>>, } impl Default for VarContainer { fn default() -> Self { VarContainer { - names: Rc::new(RefCell::new(Vec::new())), - mapping: Rc::new(RefCell::new(HashMap::new())), + names: Arc::new(RwLock::new(Vec::new())), + mapping: Arc::new(RwLock::new(HashMap::new())), } } } impl VarContainer { - pub fn from_parser( - names: Rc>>, - mapping: Rc>>, + pub(crate) fn from_parser( + names: Arc>>, + mapping: Arc>>, ) -> VarContainer { VarContainer { names, mapping } } - pub fn copy(from: &Self) -> Self { - VarContainer { - names: from.names.clone(), - mapping: from.mapping.clone(), - } - } - + /// Get the [Var] used by the `Bdd` which corresponds to the given [&str]. + /// Returns [None] if no matching value is found. pub fn variable(&self, name: &str) -> Option { - self.mapping.borrow().get(name).map(|val| Var(*val)) + self.mapping + .read() + .ok() + .and_then(|map| map.get(name).map(|val| Var(*val))) } + /// Get the name which corresponds to the given [Var]. + /// Returns [None] if no matching value is found. pub fn name(&self, var: Var) -> Option { - self.names.borrow().get(var.value()).cloned() + self.names + .read() + .ok() + .and_then(|name| name.get(var.value()).cloned()) + } + + pub(crate) fn names(&self) -> Arc>> { + Arc::clone(&self.names) + } + + pub(crate) fn mappings(&self) -> Arc>> { + Arc::clone(&self.mapping) } - #[allow(dead_code)] - pub fn names(&self) -> Rc>> { - Rc::clone(&self.names) + /// Creates a [PrintDictionary] for output purposes. + pub fn print_dictionary(&self) -> PrintDictionary { + PrintDictionary::new(self) } } /// A struct which holds the dictionary to print interpretations and allows to instantiate printable interpretations. @@ -56,7 +70,7 @@ pub struct PrintDictionary { impl PrintDictionary { pub(crate) fn new(order: &VarContainer) -> Self { Self { - ordering: VarContainer::copy(order), + ordering: order.clone(), } } /// creates a [PrintableInterpretation] for output purposes diff --git a/lib/src/lib.rs b/lib/src/lib.rs index f15c7eb..3709699 100644 --- a/lib/src/lib.rs +++ b/lib/src/lib.rs @@ -169,14 +169,16 @@ The enum [`Heuristic`][crate::adf::heuristics::Heuristic] allows one to choose a use adf_bdd::parser::AdfParser; use adf_bdd::adf::Adf; use adf_bdd::adf::heuristics::Heuristic; -use adf_bdd::datatypes::Term; +use adf_bdd::datatypes::{Term, adf::VarContainer}; // create a channel let (s, r) = crossbeam_channel::unbounded(); +let variables = VarContainer::default(); +let variables_worker = variables.clone(); // spawn a solver thread let solving = std::thread::spawn(move || { // use the above example as input let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d)."; - let parser = AdfParser::default(); + let parser = AdfParser::with_var_container(variables_worker); parser.parse()(&input).expect("parsing worked well"); // use hybrid approach let mut adf = adf_bdd::adfbiodivine::Adf::from_parser(&parser).hybrid_step(); @@ -184,9 +186,12 @@ let solving = std::thread::spawn(move || { adf.stable_nogood_channel(Heuristic::Simple, s); }); +let printer = variables.print_dictionary(); // print results as they are computed while let Ok(result) = r.recv() { - println!("stable model: {:?}", result); + print!("stable model: {:?} \n", result); + // use dictionary + print!("stable model with variable names: {}", printer.print_interpretation(&result)); # assert_eq!(result, vec![Term(1),Term(1),Term(0),Term(0)]); } // waiting for the other thread to close diff --git a/lib/src/parser.rs b/lib/src/parser.rs index acac346..2603e5a 100644 --- a/lib/src/parser.rs +++ b/lib/src/parser.rs @@ -10,7 +10,13 @@ use nom::{ sequence::{delimited, preceded, separated_pair, terminated}, IResult, }; -use std::{cell::RefCell, collections::HashMap, rc::Rc}; +use std::collections::HashMap; +use std::{ + cell::RefCell, + sync::{Arc, RwLock}, +}; + +use crate::datatypes::adf::VarContainer; /// A representation of a formula, still using the strings from the input. #[derive(Clone, PartialEq, Eq)] @@ -127,8 +133,8 @@ impl std::fmt::Debug for Formula<'_> { /// Note that the parser can be utilised by an [ADF][`crate::adf::Adf`] to initialise it with minimal overhead. #[derive(Debug)] pub struct AdfParser<'a> { - namelist: Rc>>, - dict: Rc>>, + namelist: Arc>>, + dict: Arc>>, formulae: RefCell>>, formulaname: RefCell>, } @@ -136,8 +142,8 @@ pub struct AdfParser<'a> { impl Default for AdfParser<'_> { fn default() -> Self { AdfParser { - namelist: Rc::new(RefCell::new(Vec::new())), - dict: Rc::new(RefCell::new(HashMap::new())), + namelist: Arc::new(RwLock::new(Vec::new())), + dict: Arc::new(RwLock::new(HashMap::new())), formulae: RefCell::new(Vec::new()), formulaname: RefCell::new(Vec::new()), } @@ -176,8 +182,14 @@ where fn parse_statement(&'a self) -> impl FnMut(&'a str) -> IResult<&'a str, ()> { |input| { - let mut dict = self.dict.borrow_mut(); - let mut namelist = self.namelist.borrow_mut(); + let mut dict = self + .dict + .write() + .expect("RwLock of dict could not get write access"); + let mut namelist = self + .namelist + .write() + .expect("RwLock of namelist could not get write access"); let (remain, statement) = terminated(AdfParser::statement, terminated(tag("."), multispace0))(input)?; if !dict.contains_key(statement) { @@ -200,16 +212,31 @@ where } } +impl<'a> AdfParser<'a> { + /// Creates a new parser, utilising the already existing [VarContainer] + pub fn with_var_container(var_container: VarContainer) -> AdfParser<'a> { + AdfParser { + namelist: var_container.names(), + dict: var_container.mappings(), + formulae: RefCell::new(Vec::new()), + formulaname: RefCell::new(Vec::new()), + } + } +} + impl AdfParser<'_> { /// after an update to the namelist, all indizes are updated fn regenerate_indizes(&self) { self.namelist - .as_ref() - .borrow() + .read() + .expect("ReadLock on namelist failed") .iter() .enumerate() .for_each(|(i, elem)| { - self.dict.as_ref().borrow_mut().insert(elem.clone(), i); + self.dict + .write() + .expect("WriteLock on dict failed") + .insert(elem.clone(), i); }); } @@ -217,7 +244,10 @@ impl AdfParser<'_> { /// Results, which got used before might become corrupted. /// Ensure that all used data is physically copied. pub fn varsort_lexi(&self) -> &Self { - self.namelist.as_ref().borrow_mut().sort_unstable(); + self.namelist + .write() + .expect("WriteLock on namelist failed") + .sort_unstable(); self.regenerate_indizes(); self } @@ -227,8 +257,8 @@ impl AdfParser<'_> { /// Ensure that all used data is physically copied. pub fn varsort_alphanum(&self) -> &Self { self.namelist - .as_ref() - .borrow_mut() + .write() + .expect("WriteLock on namelist failed") .string_sort_unstable(natural_lexical_cmp); self.regenerate_indizes(); self @@ -343,14 +373,18 @@ impl AdfParser<'_> { /// Allows insight of the number of parsed statements. pub fn dict_size(&self) -> usize { //self.dict.borrow().len() - self.dict.as_ref().borrow().len() + self.dict.read().expect("ReadLock on dict failed").len() } /// Returns the number-representation and position of a given statement in string-representation. /// /// Will return [None] if the string does no occur in the dictionary. pub fn dict_value(&self, value: &str) -> Option { - self.dict.as_ref().borrow().get(value).copied() + self.dict + .read() + .expect("ReadLock on dict failed") + .get(value) + .copied() } /// Returns the acceptance condition of a statement at the given position. @@ -360,12 +394,17 @@ impl AdfParser<'_> { self.formulae.borrow().get(idx).cloned() } - pub(crate) fn dict_rc_refcell(&self) -> Rc>> { - Rc::clone(&self.dict) + pub(crate) fn dict(&self) -> Arc>> { + Arc::clone(&self.dict) + } + + pub(crate) fn namelist(&self) -> Arc>> { + Arc::clone(&self.namelist) } - pub(crate) fn namelist_rc_refcell(&self) -> Rc>> { - Rc::clone(&self.namelist) + /// Returns a [`VarContainer`][crate::datatypes::adf::VarContainer] which allows to access the variable information gathered by the parser + pub fn var_container(&self) -> VarContainer { + VarContainer::from_parser(self.namelist(), self.dict()) } pub(crate) fn formula_count(&self) -> usize { @@ -379,8 +418,8 @@ impl AdfParser<'_> { .map(|name| { *self .dict - .as_ref() - .borrow() + .read() + .expect("ReadLock on dict failed") .get(name) .expect("Dictionary should contain all the used formulanames") }) From c531413192e8f945ada7b08c63806f9849e6c88a Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Wed, 27 Jul 2022 12:38:47 +0200 Subject: [PATCH 32/51] Add first documentation structure --- gh-pages/_config.yml | 10 ++ gh-pages/_data/navigation.yaml | 7 ++ gh-pages/adf-bdd.md | 122 ++++++++++++++++++++++++ gh-pages/adf_bdd.md | 164 +++++++++++++++++++++++++++++++++ gh-pages/index.md | 54 +++++++++++ 5 files changed, 357 insertions(+) create mode 100644 gh-pages/_config.yml create mode 100644 gh-pages/_data/navigation.yaml create mode 100644 gh-pages/adf-bdd.md create mode 100644 gh-pages/adf_bdd.md create mode 100644 gh-pages/index.md diff --git a/gh-pages/_config.yml b/gh-pages/_config.yml new file mode 100644 index 0000000..db849c7 --- /dev/null +++ b/gh-pages/_config.yml @@ -0,0 +1,10 @@ +theme: jekyll-theme-architect +show_downloads: false +markdown: kramdown +defaults: + - scope: + path = "" + type = docs + values: + sidebar: + nav: docs diff --git a/gh-pages/_data/navigation.yaml b/gh-pages/_data/navigation.yaml new file mode 100644 index 0000000..0b7de83 --- /dev/null +++ b/gh-pages/_data/navigation.yaml @@ -0,0 +1,7 @@ +docs: + - title: "Getting started" + url: index.md + - title: "Binary" + url: adf-bdd.md + - title: "Library" + url: adf_bdd.md diff --git a/gh-pages/adf-bdd.md b/gh-pages/adf-bdd.md new file mode 100644 index 0000000..4163b4b --- /dev/null +++ b/gh-pages/adf-bdd.md @@ -0,0 +1,122 @@ +![GitHub Workflow Status](https://img.shields.io/github/workflow/status/ellmau/adf-obdd/Code%20coverage%20with%20tarpaulin) [![Coveralls](https://img.shields.io/coveralls/github/ellmau/adf-obdd)](https://coveralls.io/github/ellmau/adf-obdd) ![GitHub release (latest by date including pre-releases)](https://img.shields.io/github/v/release/ellmau/adf-obdd?include_prereleases) ![GitHub (Pre-)Release Date](https://img.shields.io/github/release-date-pre/ellmau/adf-obdd?label=release%20from) ![GitHub top language](https://img.shields.io/github/languages/top/ellmau/adf-obdd) [![GitHub all releases](https://img.shields.io/github/downloads/ellmau/adf-obdd/total)](https://github.com/ellmau/adf-obdd/releases) [![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd)](https://github.com/ellmau/adf-obdd/discussions) ![rust-edition](https://img.shields.io/badge/Rust--edition-2021-blue?logo=rust) + +# Abstract Dialectical Frameworks solved by Binary Decision Diagrams; developed in Dresden (ADF-BDD) +This is the readme for the executable solver. + +## Usage +``` +USAGE: + adf_bdd [OPTIONS] + +ARGS: + Input filename + +OPTIONS: + --an Sorts variables in an alphanumeric manner + --com Compute the complete models + --counter Set if the (counter-)models shall be computed and printed, + possible values are 'nai' and 'mem' for naive and memoization + repectively (only works in hybrid and naive mode) + --export Export the adf-bdd state after parsing and BDD instantiation to + the given filename + --grd Compute the grounded model + -h, --help Print help information + --import Import an adf- bdd state instead of an adf + --lib choose the bdd implementation of either 'biodivine', 'naive', or + hybrid [default: hybrid] + --lx Sorts variables in an lexicographic manner + -q Sets log verbosity to only errors + --rust_log Sets the verbosity to 'warn', 'info', 'debug' or 'trace' if -v and + -q are not use [env: RUST_LOG=debug] + --stm Compute the stable models + --stmca Compute the stable models with the help of modelcounting using + heuristics a + --stmcb Compute the stable models with the help of modelcounting using + heuristics b + --stmpre Compute the stable models with a pre-filter (only hybrid lib-mode) + --stmrew Compute the stable models with a single-formula rewriting (only + hybrid lib-mode) + --stmrew2 Compute the stable models with a single-formula rewriting on + internal representation(only hybrid lib-mode) + -v Sets log verbosity (multiple times means more verbose) + -V, --version Print version information +``` + +Note that import and export only works if the naive library is chosen + +Right now there is no additional information to the computed models, so if you use --com --grd --stm the borders between the results are not obviously communicated. +They can be easily identified though: +- The computation is always in the same order + - grd + - com + - stm +- We know that there is always exactly one grounded model +- We know that there always exist at least one complete model (i.e. the grounded one) +- We know that there does not need to exist a stable model +- We know that every stable model is a complete model too + + +## Input-file format: +Each statement is defined by an ASP-style unary predicate s, where the enclosed term represents the label of the statement. +The binary predicate ac relates each statement to one propositional formula in prefix notation, with the logical operations and constants as follows: +- and(x,y): conjunction +- or(x,y): disjunctin +- iff(x,Y): if and only if +- xor(x,y): exclusive or +- neg(x): classical negation +- c(v): constant symbol "verum" - tautology/top +- c(f): constant symbol "falsum" - inconsistency/bot + +# Development notes +To build the binary, you need to run +```bash +$> cargo build --workspace --release +``` + +To build the binary with debug-symbols, run +```bash +$> cargo build --workspace +``` + +To run all the tests placed in the submodule you need to run +```bash +$> git submodule init +``` +at the first time. +Afterwards you need to update the content of the submodule to be on the currently used revision by +```bash +$> git submodule update +``` + +The tests can be started by using the test-framework of cargo, i.e. +```bash +$> cargo test +``` +Note that some of the instances are quite big and it might take some time to finish all the tests. +If you do not initialise the submodule, tests will "only" run on the other unit-tests and (possibly forthcoming) other integration tests. +Due to the way of the generated test-modules you need to call +```bash +$> cargo clean +``` +if you change some of your test-cases. + +To remove the tests just type +```bash +$> git submodule deinit res/adf-instances +``` +or +```bash +$> git submodule deinit --all +``` + +# Acknowledgements +This work is partly supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) in projects number 389792660 (TRR 248, [Center for Perspicuous Systems](https://www.perspicuous-computing.science/)), +the Bundesministerium für Bildung und Forschung (BMBF, Federal Ministry of Education and Research) in the +[Center for Scalable Data Analytics and Artificial Intelligence](https://www.scads.de) (ScaDS.AI), +and by the [Center for Advancing Electronics Dresden](https://cfaed.tu-dresden.de) (cfaed). + +# Affiliation +This work has been partly developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). + +# Disclaimer +Hosting content here does not establish any formal or legal relation to TU Dresden diff --git a/gh-pages/adf_bdd.md b/gh-pages/adf_bdd.md new file mode 100644 index 0000000..47af6fa --- /dev/null +++ b/gh-pages/adf_bdd.md @@ -0,0 +1,164 @@ +[![Crates.io](https://img.shields.io/crates/v/adf_bdd)](https://crates.io/crates/adf_bdd) +[![docs.rs](https://img.shields.io/docsrs/adf_bdd?label=docs.rs)](https://docs.rs/adf_bdd/latest/adf_bdd/) +![GitHub Workflow Status](https://img.shields.io/github/workflow/status/ellmau/adf-obdd/Code%20coverage%20with%20tarpaulin) +[![Coveralls](https://img.shields.io/coveralls/github/ellmau/adf-obdd)](https://coveralls.io/github/ellmau/adf-obdd) +![GitHub release (latest by date including pre-releases)](https://img.shields.io/github/v/release/ellmau/adf-obdd?include_prereleases) +![GitHub (Pre-)Release Date](https://img.shields.io/github/release-date-pre/ellmau/adf-obdd?label=release%20from) ![GitHub top language](https://img.shields.io/github/languages/top/ellmau/adf-obdd) +[![GitHub all releases](https://img.shields.io/github/downloads/ellmau/adf-obdd/total)](https://github.com/ellmau/adf-obdd/releases) +![Crates.io](https://img.shields.io/crates/l/adf_bdd) +[![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd)](https://github.com/ellmau/adf-obdd/discussions) ![rust-edition](https://img.shields.io/badge/Rust--edition-2021-blue?logo=rust) + +# Abstract Dialectical Frameworks solved by Binary Decision Diagrams; developed in Dresden (ADF_BDD) +This library contains an efficient representation of Abstract Dialectical Frameworks (ADf) by utilising an implementation of Ordered Binary Decision Diagrams (OBDD) + +## Noteworthy relations between ADF semantics + +They can be easily identified though: + +* The computation is always in the same order + * grd + * com + * stm +* We know that there is always exactly one grounded model +* We know that there always exist at least one complete model (i.e. the grounded one) +* We know that there does not need to exist a stable model +* We know that every stable model is a complete model too + + +## Ordered Binary Decision Diagram + +An ordered binary decision diagram is a normalised representation of binary functions, where satisfiability- and validity checks can be done relatively cheap. + +Note that one advantage of this implementation is that only one oBDD is used for all acceptance conditions. This can be done because all of them have the identical signature (i.e. the set of all statements + top and bottom concepts). Due to this uniform representation reductions on subformulae which are shared by two or more statements only need to be computed once and is already cached in the data structure for further applications. + +The used algorithm to create a BDD, based on a given formula does not perform well on bigger formulae, therefore it is possible to use a state-of-the art library to instantiate the BDD (https://github.com/sybila/biodivine-lib-bdd). It is possible to either stay with the biodivine library or switch back to the variant implemented by adf-bdd. The variant implemented in this library offers reuse of already done reductions and memoisation techniques, which are not offered by biodivine. In addition some further features, like counter-model counting is not supported by biodivine. + +Note that import and export only works if the naive library is chosen + +## Input-file format: + +Each statement is defined by an ASP-style unary predicate s, where the enclosed term represents the label of the statement. The binary predicate ac relates each statement to one propositional formula in prefix notation, with the logical operations and constants as follows: +```plain +and(x,y): conjunction +or(x,y): disjunctin +iff(x,Y): if and only if +xor(x,y): exclusive or +neg(x): classical negation +c(v): constant symbol “verum” - tautology/top +c(f): constant symbol “falsum” - inconsistency/bot +``` + +### Example input file: +```plain +s(a). +s(b). +s(c). +s(d). + +ac(a,c(v)). +ac(b,or(a,b)). +ac(c,neg(b)). +ac(d,d). +``` + +## Usage examples + +First parse a given ADF and sort the statements, if needed. + +```rust +use adf_bdd::parser::AdfParser; +use adf_bdd::adf::Adf; +// use the above example as input +let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d)."; +let parser = AdfParser::default(); +match parser.parse()(&input) { + Ok(_) => log::info!("[Done] parsing"), + Err(e) => { + log::error!( + "Error during parsing:\n{} \n\n cannot continue, panic!", + e + ); + panic!("Parsing failed, see log for further details") + } +} +// sort lexicographic +parser.varsort_lexi(); +``` +use the naive/in-crate implementation + +```rust +// create Adf +let mut adf = Adf::from_parser(&parser); +// compute and print the complete models +let printer = adf.print_dictionary(); +for model in adf.complete() { + print!("{}", printer.print_interpretation(&model)); +} +``` +use the biodivine implementation +```rust +// create Adf +let adf = adf_bdd::adfbiodivine::Adf::from_parser(&parser); +// compute and print the complete models +let printer = adf.print_dictionary(); +for model in adf.complete() { + print!("{}", printer.print_interpretation(&model)); +} +``` +use the hybrid approach implementation +```rust +// create biodivine Adf +let badf = adf_bdd::adfbiodivine::Adf::from_parser(&parser); +// instantiate the internally used adf after the reduction done by biodivine +let mut adf = badf.hybrid_step(); +// compute and print the complete models +let printer = adf.print_dictionary(); +for model in adf.complete() { + print!("{}", printer.print_interpretation(&model)); +} +``` + +use the new `NoGood`-based algorithm and utilise the new interface with channels: +```rust +use adf_bdd::parser::AdfParser; +use adf_bdd::adf::Adf; +use adf_bdd::adf::heuristics::Heuristic; +use adf_bdd::datatypes::{Term, adf::VarContainer}; +// create a channel +let (s, r) = crossbeam_channel::unbounded(); +let variables = VarContainer::default(); +let variables_worker = variables.clone(); +// spawn a solver thread +let solving = std::thread::spawn(move || { + // use the above example as input + let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d)."; + let parser = AdfParser::with_var_container(variables_worker); + parser.parse()(&input).expect("parsing worked well"); + // use hybrid approach + let mut adf = adf_bdd::adfbiodivine::Adf::from_parser(&parser).hybrid_step(); + // compute stable with the simple heuristic + adf.stable_nogood_channel(Heuristic::Simple, s); +}); + +let printer = variables.print_dictionary(); +// print results as they are computed +while let Ok(result) = r.recv() { + print!("stable model: {:?} \n", result); + // use dictionary + print!("stable model with variable names: {}", printer.print_interpretation(&result)); +} +// waiting for the other thread to close +solving.join().unwrap(); +``` + +# Acknowledgements +This work is partly supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) in projects number 389792660 (TRR 248, [Center for Perspicuous Systems](https://www.perspicuous-computing.science/)), +the Bundesministerium für Bildung und Forschung (BMBF, Federal Ministry of Education and Research) in the +[Center for Scalable Data Analytics and Artificial Intelligence](https://www.scads.de) (ScaDS.AI), +and by the [Center for Advancing Electronics Dresden](https://cfaed.tu-dresden.de) (cfaed). + +# Affiliation +This work has been partly developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). + +# Disclaimer +Hosting content here does not establish any formal or legal relation to TU Dresden diff --git a/gh-pages/index.md b/gh-pages/index.md new file mode 100644 index 0000000..2bc2828 --- /dev/null +++ b/gh-pages/index.md @@ -0,0 +1,54 @@ +[![Crates.io](https://img.shields.io/crates/v/adf_bdd)](https://crates.io/crates/adf_bdd) +[![docs.rs](https://img.shields.io/docsrs/adf_bdd?label=docs.rs)](https://docs.rs/adf_bdd/latest/adf_bdd/) +![GitHub Workflow Status](https://img.shields.io/github/workflow/status/ellmau/adf-obdd/Code%20coverage%20with%20tarpaulin) +[![Coveralls](https://img.shields.io/coveralls/github/ellmau/adf-obdd)](https://coveralls.io/github/ellmau/adf-obdd) +![GitHub release (latest by date including pre-releases)](https://img.shields.io/github/v/release/ellmau/adf-obdd?include_prereleases) +![GitHub (Pre-)Release Date](https://img.shields.io/github/release-date-pre/ellmau/adf-obdd?label=release%20from) ![GitHub top language](https://img.shields.io/github/languages/top/ellmau/adf-obdd) +[![GitHub all releases](https://img.shields.io/github/downloads/ellmau/adf-obdd/total)](https://github.com/ellmau/adf-obdd/releases) +![Crates.io](https://img.shields.io/crates/l/adf_bdd) +[![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd)](https://github.com/ellmau/adf-obdd/discussions) ![rust-edition](https://img.shields.io/badge/Rust--edition-2021-blue?logo=rust) + +# Abstract Dialectical Frameworks solved by (ordered) Binary Decision Diagrams; developed in Dresden (ADF-oBDD project) + +This project is currently split into two parts: +- a [binary (adf-bdd)](adf-bdd.md), which allows one to easily answer semantics questions on abstract dialectical frameworks +- a [library (adf_bdd)](adf_bdd.md), which contains all the necessary algorithms and an open API which compute the answers to the semantics questions + + +## Abstract Dialectical Frameworks +An abstract dialectical framework (ADF) consists of abstract statements. Each statement has an unique label and might be related to other statements (s) in the ADF. This relation is defined by a so-called acceptance condition (ac), which intuitively is a propositional formula, where the variable symbols are the labels of the statements. An interpretation is a three valued function which maps to each statement a truth value (true, false, undecided). We call such an interpretation a model, if each acceptance condition agrees to the interpration. +## Ordered Binary Decision Diagram +An ordered binary decision diagram is a normalised representation of binary functions, where satisfiability- and validity checks can be done relatively cheap. + +## Input-file format: +Each statement is defined by an ASP-style unary predicate s, where the enclosed term represents the label of the statement. +The binary predicate ac relates each statement to one propositional formula in prefix notation, with the logical operations and constants as follows: +- and(x,y): conjunction +- or(x,y): disjunctin +- iff(x,Y): if and only if +- xor(x,y): exclusive or +- neg(x): classical negation +- c(v): constant symbol "verum" - tautology/top +- c(f): constant symbol "falsum" - inconsistency/bot + +# Features + +- `adhoccounting` will cache the modelcount on-the-fly during the construction of the BDD +- `adhoccountmodels` allows in addition to compute the models ad-hoc too. Note that the memoization approach for modelcounting does not work correctly if `adhoccounting` is set and `adhoccountmodels` is not. + +# Development notes +Additional information for contribution, testing, and development in general can be found here. +## Contributing to the project +You want to help and contribute to the project? That is great. Please see the [contributing guidelines](https://github.com/ellmau/adf-obdd/blob/main/.github/CONTRIBUTING.md) first. + +# Acknowledgements +This work is partly supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) in projects number 389792660 (TRR 248, [Center for Perspicuous Systems](https://www.perspicuous-computing.science/)), +the Bundesministerium für Bildung und Forschung (BMBF, Federal Ministry of Education and Research) in the +[Center for Scalable Data Analytics and Artificial Intelligence](https://www.scads.de) (ScaDS.AI), +and by the [Center for Advancing Electronics Dresden](https://cfaed.tu-dresden.de) (cfaed). + +# Affiliation +This work has been partly developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). + +# Disclaimer +Hosting content here does not establish any formal or legal relation to TU Dresden From 65de1298a64d119c5353b031edd3a0343ab888f9 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Wed, 27 Jul 2022 12:40:18 +0200 Subject: [PATCH 33/51] mv gh-pages to docs --- {gh-pages => docs}/_config.yml | 0 {gh-pages => docs}/_data/navigation.yaml | 0 {gh-pages => docs}/adf-bdd.md | 0 {gh-pages => docs}/adf_bdd.md | 0 {gh-pages => docs}/index.md | 0 5 files changed, 0 insertions(+), 0 deletions(-) rename {gh-pages => docs}/_config.yml (100%) rename {gh-pages => docs}/_data/navigation.yaml (100%) rename {gh-pages => docs}/adf-bdd.md (100%) rename {gh-pages => docs}/adf_bdd.md (100%) rename {gh-pages => docs}/index.md (100%) diff --git a/gh-pages/_config.yml b/docs/_config.yml similarity index 100% rename from gh-pages/_config.yml rename to docs/_config.yml diff --git a/gh-pages/_data/navigation.yaml b/docs/_data/navigation.yaml similarity index 100% rename from gh-pages/_data/navigation.yaml rename to docs/_data/navigation.yaml diff --git a/gh-pages/adf-bdd.md b/docs/adf-bdd.md similarity index 100% rename from gh-pages/adf-bdd.md rename to docs/adf-bdd.md diff --git a/gh-pages/adf_bdd.md b/docs/adf_bdd.md similarity index 100% rename from gh-pages/adf_bdd.md rename to docs/adf_bdd.md diff --git a/gh-pages/index.md b/docs/index.md similarity index 100% rename from gh-pages/index.md rename to docs/index.md From b38c64ab5f8fcc174402857b2e92221ac688f06c Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Wed, 27 Jul 2022 12:42:41 +0200 Subject: [PATCH 34/51] Fix docs string --- docs/_config.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/_config.yml b/docs/_config.yml index db849c7..f0f8d0f 100644 --- a/docs/_config.yml +++ b/docs/_config.yml @@ -7,4 +7,4 @@ defaults: type = docs values: sidebar: - nav: docs + nav: "docs" From d4465feea22d3a91acce27d08109a9b3886b3694 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Wed, 27 Jul 2022 12:44:30 +0200 Subject: [PATCH 35/51] Simple version of gh pages --- docs/_config.yml | 7 ------- docs/_data/navigation.yaml | 7 ------- 2 files changed, 14 deletions(-) delete mode 100644 docs/_data/navigation.yaml diff --git a/docs/_config.yml b/docs/_config.yml index f0f8d0f..1d7a267 100644 --- a/docs/_config.yml +++ b/docs/_config.yml @@ -1,10 +1,3 @@ theme: jekyll-theme-architect show_downloads: false markdown: kramdown -defaults: - - scope: - path = "" - type = docs - values: - sidebar: - nav: "docs" diff --git a/docs/_data/navigation.yaml b/docs/_data/navigation.yaml deleted file mode 100644 index 0b7de83..0000000 --- a/docs/_data/navigation.yaml +++ /dev/null @@ -1,7 +0,0 @@ -docs: - - title: "Getting started" - url: index.md - - title: "Binary" - url: adf-bdd.md - - title: "Library" - url: adf_bdd.md From 2b86e745b2dcd949408cae693d621ded40728ee1 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Wed, 27 Jul 2022 12:50:04 +0200 Subject: [PATCH 36/51] Fix some style issues --- README.md | 2 +- bin/README.md | 2 +- docs/adf-bdd.md | 2 +- docs/adf_bdd.md | 2 +- docs/index.md | 2 +- lib/README.md | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 4211dc6..b6dbbf1 100644 --- a/README.md +++ b/README.md @@ -142,4 +142,4 @@ and by the [Center for Advancing Electronics Dresden](https://cfaed.tu-dresden.d This work has been partly developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). # Disclaimer -Hosting content here does not establish any formal or legal relation to TU Dresden +Hosting content here does not establish any formal or legal relation to TU Dresden. diff --git a/bin/README.md b/bin/README.md index 0dcfd6e..3cc03ab 100644 --- a/bin/README.md +++ b/bin/README.md @@ -124,4 +124,4 @@ and by the [Center for Advancing Electronics Dresden](https://cfaed.tu-dresden.d This work has been partly developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). # Disclaimer -Hosting content here does not establish any formal or legal relation to TU Dresden +Hosting content here does not establish any formal or legal relation to TU Dresden. diff --git a/docs/adf-bdd.md b/docs/adf-bdd.md index 4163b4b..0e8853a 100644 --- a/docs/adf-bdd.md +++ b/docs/adf-bdd.md @@ -119,4 +119,4 @@ and by the [Center for Advancing Electronics Dresden](https://cfaed.tu-dresden.d This work has been partly developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). # Disclaimer -Hosting content here does not establish any formal or legal relation to TU Dresden +Hosting content here does not establish any formal or legal relation to TU Dresden. diff --git a/docs/adf_bdd.md b/docs/adf_bdd.md index 47af6fa..605898e 100644 --- a/docs/adf_bdd.md +++ b/docs/adf_bdd.md @@ -161,4 +161,4 @@ and by the [Center for Advancing Electronics Dresden](https://cfaed.tu-dresden.d This work has been partly developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). # Disclaimer -Hosting content here does not establish any formal or legal relation to TU Dresden +Hosting content here does not establish any formal or legal relation to TU Dresden. diff --git a/docs/index.md b/docs/index.md index 2bc2828..64a6501 100644 --- a/docs/index.md +++ b/docs/index.md @@ -51,4 +51,4 @@ and by the [Center for Advancing Electronics Dresden](https://cfaed.tu-dresden.d This work has been partly developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). # Disclaimer -Hosting content here does not establish any formal or legal relation to TU Dresden +Hosting content here does not establish any formal or legal relation to TU Dresden. diff --git a/lib/README.md b/lib/README.md index fd652d0..5c87cfc 100644 --- a/lib/README.md +++ b/lib/README.md @@ -160,4 +160,4 @@ and by the [Center for Advancing Electronics Dresden](https://cfaed.tu-dresden.d This work has been partly developed by the [Knowledge-Based Systems Group](http://kbs.inf.tu-dresden.de/), [Faculty of Computer Science](https://tu-dresden.de/ing/informatik) of [TU Dresden](https://tu-dresden.de). # Disclaimer -Hosting content here does not establish any formal or legal relation to TU Dresden +Hosting content here does not establish any formal or legal relation to TU Dresden. From fa52a02de085410b9562e532daa149959bf73af7 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Wed, 27 Jul 2022 12:53:41 +0200 Subject: [PATCH 37/51] Added more links and information to the landing page --- docs/index.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/docs/index.md b/docs/index.md index 64a6501..4c2f6dc 100644 --- a/docs/index.md +++ b/docs/index.md @@ -14,6 +14,11 @@ This project is currently split into two parts: - a [binary (adf-bdd)](adf-bdd.md), which allows one to easily answer semantics questions on abstract dialectical frameworks - a [library (adf_bdd)](adf_bdd.md), which contains all the necessary algorithms and an open API which compute the answers to the semantics questions +Latest documentation of the API can be found [here](https://docs.rs/adf_bdd/latest/adf_bdd/). +The current version of the binary can be downloaded [here](https://github.com/ellmau/adf-obdd/releases). + +Do not hesitate to report bugs or ask about features in the [issues-section](https://github.com/ellmau/adf-obdd/issues) or have a conversation about anything of the project in the [discussion space](https://github.com/ellmau/adf-obdd/discussions) + ## Abstract Dialectical Frameworks An abstract dialectical framework (ADF) consists of abstract statements. Each statement has an unique label and might be related to other statements (s) in the ADF. This relation is defined by a so-called acceptance condition (ac), which intuitively is a propositional formula, where the variable symbols are the labels of the statements. An interpretation is a three valued function which maps to each statement a truth value (true, false, undecided). We call such an interpretation a model, if each acceptance condition agrees to the interpration. From 30c0ca6c30113732be3e9cb3333346ab711a3d3b Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Wed, 27 Jul 2022 12:57:04 +0200 Subject: [PATCH 38/51] Fix badges in the app-doc --- docs/adf-bdd.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/docs/adf-bdd.md b/docs/adf-bdd.md index 0e8853a..5771a5d 100644 --- a/docs/adf-bdd.md +++ b/docs/adf-bdd.md @@ -1,4 +1,12 @@ -![GitHub Workflow Status](https://img.shields.io/github/workflow/status/ellmau/adf-obdd/Code%20coverage%20with%20tarpaulin) [![Coveralls](https://img.shields.io/coveralls/github/ellmau/adf-obdd)](https://coveralls.io/github/ellmau/adf-obdd) ![GitHub release (latest by date including pre-releases)](https://img.shields.io/github/v/release/ellmau/adf-obdd?include_prereleases) ![GitHub (Pre-)Release Date](https://img.shields.io/github/release-date-pre/ellmau/adf-obdd?label=release%20from) ![GitHub top language](https://img.shields.io/github/languages/top/ellmau/adf-obdd) [![GitHub all releases](https://img.shields.io/github/downloads/ellmau/adf-obdd/total)](https://github.com/ellmau/adf-obdd/releases) [![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd)](https://github.com/ellmau/adf-obdd/discussions) ![rust-edition](https://img.shields.io/badge/Rust--edition-2021-blue?logo=rust) +[![Crates.io](https://img.shields.io/crates/v/adf_bdd)](https://crates.io/crates/adf_bdd) +[![docs.rs](https://img.shields.io/docsrs/adf_bdd?label=docs.rs)](https://docs.rs/adf_bdd/latest/adf_bdd/) +![GitHub Workflow Status](https://img.shields.io/github/workflow/status/ellmau/adf-obdd/Code%20coverage%20with%20tarpaulin) +[![Coveralls](https://img.shields.io/coveralls/github/ellmau/adf-obdd)](https://coveralls.io/github/ellmau/adf-obdd) +![GitHub release (latest by date including pre-releases)](https://img.shields.io/github/v/release/ellmau/adf-obdd?include_prereleases) +![GitHub (Pre-)Release Date](https://img.shields.io/github/release-date-pre/ellmau/adf-obdd?label=release%20from) ![GitHub top language](https://img.shields.io/github/languages/top/ellmau/adf-obdd) +[![GitHub all releases](https://img.shields.io/github/downloads/ellmau/adf-obdd/total)](https://github.com/ellmau/adf-obdd/releases) +![Crates.io](https://img.shields.io/crates/l/adf_bdd) +[![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd)](https://github.com/ellmau/adf-obdd/discussions) ![rust-edition](https://img.shields.io/badge/Rust--edition-2021-blue?logo=rust) # Abstract Dialectical Frameworks solved by Binary Decision Diagrams; developed in Dresden (ADF-BDD) This is the readme for the executable solver. From 44d41ec00167b6ac404e9bf90fb8b27186bf4586 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Thu, 28 Jul 2022 14:24:44 +0200 Subject: [PATCH 39/51] Add two valued interpretation Parameterised the stable-nogood algorithm to allow a variable stability check function. --- lib/src/adf.rs | 66 ++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 58 insertions(+), 8 deletions(-) diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 6063bac..8413e45 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -744,7 +744,28 @@ impl Adf { sender: crossbeam_channel::Sender>, ) { let grounded = self.grounded(); - self.stable_nogood_internal(&grounded, heuristic.get_heuristic(), sender); + self.stable_nogood_internal( + &grounded, + heuristic.get_heuristic(), + Self::stability_check, + sender, + ); + } + + /// Computes the two valued extension of a given [`Adf`], using the [`NoGood`]-learner. + /// Needs a [`Sender`][crossbeam_channel::Sender>] where the results of the computation can be put to. + pub fn two_val_nogood_channel( + &mut self, + heuristic: Heuristic, + sender: crossbeam_channel::Sender>, + ) { + let grounded = self.grounded(); + self.stable_nogood_internal( + &grounded, + heuristic.get_heuristic(), + |_self: &mut Self, _int: &[Term]| true, + sender, + ) } fn stable_nogood_get_vec( @@ -757,17 +778,19 @@ impl Adf { where H: Fn(&Self, &[Term]) -> Option<(Var, Term)>, { - self.stable_nogood_internal(interpretation, heuristic, s); + self.stable_nogood_internal(interpretation, heuristic, Self::stability_check, s); r.iter().collect() } - fn stable_nogood_internal( + fn stable_nogood_internal( &mut self, interpretation: &[Term], heuristic: H, + stability_check: I, s: crossbeam_channel::Sender>, ) where H: Fn(&Self, &[Term]) -> Option<(Var, Term)>, + I: Fn(&mut Self, &[Term]) -> bool, { let mut cur_interpr = interpretation.to_vec(); let mut ng_store = NoGoodStore::new( @@ -862,7 +885,7 @@ impl Adf { // No updates done this loop if !self.is_two_valued(&cur_interpr) { choice = true; - } else if self.stability_check(&cur_interpr) { + } else if stability_check(self, &cur_interpr) { // stable model found stack.push((false, cur_interpr.as_slice().into())); s.send(cur_interpr.clone()) @@ -1079,7 +1102,12 @@ mod test { let grounded = adf.grounded(); let (s, r) = unbounded(); - adf.stable_nogood_internal(&grounded, crate::adf::heuristics::heu_simple, s); + adf.stable_nogood_internal( + &grounded, + crate::adf::heuristics::heu_simple, + crate::adf::Adf::stability_check, + s, + ); assert_eq!( r.iter().collect::>(), @@ -1111,7 +1139,12 @@ mod test { let mut adf = Adf::from_parser(&parser); let grounded = adf.grounded(); let (s, r) = unbounded(); - adf.stable_nogood_internal(&grounded, crate::adf::heuristics::heu_simple, s.clone()); + adf.stable_nogood_internal( + &grounded, + crate::adf::heuristics::heu_simple, + crate::adf::Adf::stability_check, + s.clone(), + ); let stable_result = r.try_iter().collect::>(); assert_eq!( stable_result, @@ -1151,7 +1184,8 @@ mod test { .unwrap(); let mut adf = Adf::from_parser(&parser); adf.stable_nogood_channel(Heuristic::MinModMaxVarImpMinPaths, s.clone()); - adf.stable_nogood_channel(Heuristic::MinModMinPathsMaxVarImp, s); + adf.stable_nogood_channel(Heuristic::MinModMinPathsMaxVarImp, s.clone()); + adf.two_val_nogood_channel(Heuristic::Simple, s) }); let mut result_vec = Vec::new(); @@ -1176,7 +1210,23 @@ mod test { Term::TOP, Term::BOT, Term::TOP - ] + ], + vec![ + Term::TOP, + Term::TOP, + Term::TOP, + Term::BOT, + Term::BOT, + Term::TOP + ], + vec![ + Term::TOP, + Term::BOT, + Term::BOT, + Term::TOP, + Term::BOT, + Term::TOP + ], ] ); solving.join().unwrap(); From e2e77ea03498b9eed97349fc5875413405286a43 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Thu, 28 Jul 2022 14:27:49 +0200 Subject: [PATCH 40/51] Refactor nogood-algorithm name --- lib/src/adf.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 8413e45..7bb8247 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -744,7 +744,7 @@ impl Adf { sender: crossbeam_channel::Sender>, ) { let grounded = self.grounded(); - self.stable_nogood_internal( + self.nogood_internal( &grounded, heuristic.get_heuristic(), Self::stability_check, @@ -760,7 +760,7 @@ impl Adf { sender: crossbeam_channel::Sender>, ) { let grounded = self.grounded(); - self.stable_nogood_internal( + self.nogood_internal( &grounded, heuristic.get_heuristic(), |_self: &mut Self, _int: &[Term]| true, @@ -778,11 +778,11 @@ impl Adf { where H: Fn(&Self, &[Term]) -> Option<(Var, Term)>, { - self.stable_nogood_internal(interpretation, heuristic, Self::stability_check, s); + self.nogood_internal(interpretation, heuristic, Self::stability_check, s); r.iter().collect() } - fn stable_nogood_internal( + fn nogood_internal( &mut self, interpretation: &[Term], heuristic: H, @@ -1102,7 +1102,7 @@ mod test { let grounded = adf.grounded(); let (s, r) = unbounded(); - adf.stable_nogood_internal( + adf.nogood_internal( &grounded, crate::adf::heuristics::heu_simple, crate::adf::Adf::stability_check, @@ -1139,7 +1139,7 @@ mod test { let mut adf = Adf::from_parser(&parser); let grounded = adf.grounded(); let (s, r) = unbounded(); - adf.stable_nogood_internal( + adf.nogood_internal( &grounded, crate::adf::heuristics::heu_simple, crate::adf::Adf::stability_check, From ab515e6f7a6083da3ee7cd0ddce065dc2df1b082 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Thu, 28 Jul 2022 14:33:41 +0200 Subject: [PATCH 41/51] Update README.md `README.md` on the `/` level is now presenting the same information which is provided in `docs/index.md` --- README.md | 110 ++++++------------------------------------------------ 1 file changed, 12 insertions(+), 98 deletions(-) diff --git a/README.md b/README.md index b6dbbf1..4f915a2 100644 --- a/README.md +++ b/README.md @@ -8,7 +8,16 @@ ![Crates.io](https://img.shields.io/crates/l/adf_bdd) [![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd)](https://github.com/ellmau/adf-obdd/discussions) ![rust-edition](https://img.shields.io/badge/Rust--edition-2021-blue?logo=rust) -# Abstract Dialectical Frameworks solved by Binary Decision Diagrams; developed in Dresden (ADF-BDD) +# Abstract Dialectical Frameworks solved by (ordered) Binary Decision Diagrams; developed in Dresden (ADF-oBDD project) + +This project is currently split into two parts: +- a [binary (adf-bdd)](bin/README.md), which allows one to easily answer semantics questions on abstract dialectical frameworks +- a [library (adf_bdd)](lib/README.md), which contains all the necessary algorithms and an open API which compute the answers to the semantics questions + +Latest documentation of the API can be found [here](https://docs.rs/adf_bdd/latest/adf_bdd/). +The current version of the binary can be downloaded [here](https://github.com/ellmau/adf-obdd/releases). + +Do not hesitate to report bugs or ask about features in the [issues-section](https://github.com/ellmau/adf-obdd/issues) or have a conversation about anything of the project in the [discussion space](https://github.com/ellmau/adf-obdd/discussions) ## Abstract Dialectical Frameworks @@ -16,59 +25,6 @@ An abstract dialectical framework (ADF) consists of abstract statements. Each st ## Ordered Binary Decision Diagram An ordered binary decision diagram is a normalised representation of binary functions, where satisfiability- and validity checks can be done relatively cheap. -## Usage of the binary -``` -USAGE: - adf_bdd [OPTIONS] - -ARGS: - Input filename - -OPTIONS: - --an Sorts variables in an alphanumeric manner - --com Compute the complete models - --counter Set if the (counter-)models shall be computed and printed, - possible values are 'nai' and 'mem' for naive and memoization - repectively (only works in hybrid and naive mode) - --export Export the adf-bdd state after parsing and BDD instantiation to - the given filename - --grd Compute the grounded model - -h, --help Print help information - --import Import an adf- bdd state instead of an adf - --lib choose the bdd implementation of either 'biodivine', 'naive', or - hybrid [default: hybrid] - --lx Sorts variables in an lexicographic manner - -q Sets log verbosity to only errors - --rust_log Sets the verbosity to 'warn', 'info', 'debug' or 'trace' if -v and - -q are not use [env: RUST_LOG=debug] - --stm Compute the stable models - --stmca Compute the stable models with the help of modelcounting using - heuristics a - --stmcb Compute the stable models with the help of modelcounting using - heuristics b - --stmpre Compute the stable models with a pre-filter (only hybrid lib-mode) - --stmrew Compute the stable models with a single-formula rewriting (only - hybrid lib-mode) - --stmrew2 Compute the stable models with a single-formula rewriting on - internal representation(only hybrid lib-mode) - -v Sets log verbosity (multiple times means more verbose) - -V, --version Print version information -``` - -Note that import and export only works if the naive library is chosen - -Right now there is no additional information to the computed models, so if you use `--com --grd --stm` as the command line arguments the borders between the results are not obviously communicated. -They can be easily identified though: -- The computation is always in the same order - - grd - - com - - stm -- We know that there is always exactly one grounded model -- We know that there always exist at least one complete model (i.e. the grounded one) -- We know that there does not need to exist a stable model -- We know that every stable model is a complete model too - - ## Input-file format: Each statement is defined by an ASP-style unary predicate s, where the enclosed term represents the label of the statement. The binary predicate ac relates each statement to one propositional formula in prefix notation, with the logical operations and constants as follows: @@ -82,56 +38,14 @@ The binary predicate ac relates each statement to one propositional formula in p # Features -`adhoccounting` will cache the modelcount on-the-fly during the construction of the BDD +- `adhoccounting` will cache the modelcount on-the-fly during the construction of the BDD +- `adhoccountmodels` allows in addition to compute the models ad-hoc too. Note that the memoization approach for modelcounting does not work correctly if `adhoccounting` is set and `adhoccountmodels` is not. # Development notes Additional information for contribution, testing, and development in general can be found here. ## Contributing to the project You want to help and contribute to the project? That is great. Please see the [contributing guidelines](https://github.com/ellmau/adf-obdd/blob/main/.github/CONTRIBUTING.md) first. -## Building the binary: -To build the binary, you need to run -```bash -$> cargo build --workspace --release -``` - -To build the binary with debug-symbols, run -```bash -$> cargo build --workspace -``` - -## Testing with the `res` folder: -To run all the tests placed in the submodule you need to run -```bash -$> git submodule init -``` -at the first time. -Afterwards you need to update the content of the submodule to be on the currently used revision by -```bash -$> git submodule update -``` - -The tests can be started by using the test-framework of cargo, i.e. -```bash -$> cargo test -``` -Note that some of the instances are quite big and it might take some time to finish all the tests. -If you do not initialise the submodule, tests will "only" run on the other unit-tests and (possibly forthcoming) other integration tests. -Due to the way of the generated test-modules you need to call -```bash -$> cargo clean -``` -if you change some of your test-cases. - -To remove the tests just type -```bash -$> git submodule deinit res/adf-instances -``` -or -```bash -$> git submodule deinit --all -``` - # Acknowledgements This work is partly supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) in projects number 389792660 (TRR 248, [Center for Perspicuous Systems](https://www.perspicuous-computing.science/)), the Bundesministerium für Bildung und Forschung (BMBF, Federal Ministry of Education and Research) in the From 5fc720d5f54fda7aa6f3771dc5b7ab6c5daaa265 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler <71695780+ellmau@users.noreply.github.com> Date: Thu, 28 Jul 2022 14:43:04 +0200 Subject: [PATCH 42/51] Fix link to binary and library subfolder --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 4f915a2..886ef96 100644 --- a/README.md +++ b/README.md @@ -11,8 +11,8 @@ # Abstract Dialectical Frameworks solved by (ordered) Binary Decision Diagrams; developed in Dresden (ADF-oBDD project) This project is currently split into two parts: -- a [binary (adf-bdd)](bin/README.md), which allows one to easily answer semantics questions on abstract dialectical frameworks -- a [library (adf_bdd)](lib/README.md), which contains all the necessary algorithms and an open API which compute the answers to the semantics questions +- a [binary (adf-bdd)](bin), which allows one to easily answer semantics questions on abstract dialectical frameworks +- a [library (adf_bdd)](lib), which contains all the necessary algorithms and an open API which compute the answers to the semantics questions Latest documentation of the API can be found [here](https://docs.rs/adf_bdd/latest/adf_bdd/). The current version of the binary can be downloaded [here](https://github.com/ellmau/adf-obdd/releases). From 20131d7b8963d52c68b33ea2c2e7d10100791d86 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Thu, 28 Jul 2022 15:24:41 +0200 Subject: [PATCH 43/51] Update main - Update main functionality - Update naming - Update README/Documentation --- Cargo.lock | 31 ++++++++++++++++--------------- bin/Cargo.toml | 3 ++- bin/README.md | 10 ++++++++-- bin/src/main.rs | 27 ++++++++++++++++++++++++--- docs/adf-bdd.md | 10 ++++++++-- 5 files changed, 58 insertions(+), 23 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 9e7db04..182222d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -3,39 +3,40 @@ version = 3 [[package]] -name = "adf_bdd" +name = "adf-bdd-solver" version = "0.2.5" dependencies = [ - "biodivine-lib-bdd", + "adf_bdd", + "assert_cmd", + "assert_fs", + "clap", "crossbeam-channel", - "derivative", "env_logger 0.9.0", - "lexical-sort", "log", - "nom", - "quickcheck", - "quickcheck_macros", - "roaring", + "predicates", "serde", "serde_json", "strum", - "test-log", ] [[package]] -name = "adf_bdd-solver" +name = "adf_bdd" version = "0.2.5" dependencies = [ - "adf_bdd", - "assert_cmd", - "assert_fs", - "clap", + "biodivine-lib-bdd", + "crossbeam-channel", + "derivative", "env_logger 0.9.0", + "lexical-sort", "log", - "predicates", + "nom", + "quickcheck", + "quickcheck_macros", + "roaring", "serde", "serde_json", "strum", + "test-log", ] [[package]] diff --git a/bin/Cargo.toml b/bin/Cargo.toml index 6a5ccaf..46ce01d 100644 --- a/bin/Cargo.toml +++ b/bin/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "adf_bdd-solver" +name = "adf-bdd-solver" version = "0.2.5" authors = ["Stefan Ellmauthaler "] edition = "2021" @@ -23,6 +23,7 @@ serde = { version = "1.0", features = ["derive","rc"] } serde_json = "1.0" env_logger = "0.9" strum = { version = "0.24" } +crossbeam-channel = "0.5" [dev-dependencies] assert_cmd = "2.0" diff --git a/bin/README.md b/bin/README.md index 3cc03ab..6b34e8e 100644 --- a/bin/README.md +++ b/bin/README.md @@ -11,7 +11,7 @@ An ordered binary decision diagram is a normalised representation of binary func ## Usage ``` USAGE: - adf_bdd [OPTIONS] + adf-bdd [OPTIONS] ARGS: Input filename @@ -26,8 +26,11 @@ OPTIONS: the given filename --grd Compute the grounded model -h, --help Print help information + --heu Choose which heuristics shall be used by the nogood-learning + approach [possible values: Simple, MinModMinPathsMaxVarImp, + MinModMaxVarImpMinPaths] --import Import an adf- bdd state instead of an adf - --lib choose the bdd implementation of either 'biodivine', 'naive', or + --lib Choose the bdd implementation of either 'biodivine', 'naive', or hybrid [default: hybrid] --lx Sorts variables in an lexicographic manner -q Sets log verbosity to only errors @@ -38,11 +41,14 @@ OPTIONS: heuristics a --stmcb Compute the stable models with the help of modelcounting using heuristics b + --stmng Compute the stable models with the nogood-learning based approach --stmpre Compute the stable models with a pre-filter (only hybrid lib-mode) --stmrew Compute the stable models with a single-formula rewriting (only hybrid lib-mode) --stmrew2 Compute the stable models with a single-formula rewriting on internal representation(only hybrid lib-mode) + --twoval Compute the two valued models with the nogood-learning based + approach -v Sets log verbosity (multiple times means more verbose) -V, --version Print version information ``` diff --git a/bin/src/main.rs b/bin/src/main.rs index 5bac810..949200f 100644 --- a/bin/src/main.rs +++ b/bin/src/main.rs @@ -17,7 +17,7 @@ In addition some further features, like counter-model counting is not supported # Usage ```plain USAGE: - adf_bdd [OPTIONS] + adf-bdd [OPTIONS] ARGS: Input filename @@ -32,20 +32,29 @@ OPTIONS: the given filename --grd Compute the grounded model -h, --help Print help information + --heu Choose which heuristics shall be used by the nogood-learning + approach [possible values: Simple, MinModMinPathsMaxVarImp, + MinModMaxVarImpMinPaths] --import Import an adf- bdd state instead of an adf - --lib choose the bdd implementation of either 'biodivine', 'naive', or + --lib Choose the bdd implementation of either 'biodivine', 'naive', or hybrid [default: hybrid] --lx Sorts variables in an lexicographic manner -q Sets log verbosity to only errors --rust_log Sets the verbosity to 'warn', 'info', 'debug' or 'trace' if -v and -q are not use [env: RUST_LOG=debug] --stm Compute the stable models - --stmc Compute the stable models with the help of modelcounting + --stmca Compute the stable models with the help of modelcounting using + heuristics a + --stmcb Compute the stable models with the help of modelcounting using + heuristics b + --stmng Compute the stable models with the nogood-learning based approach --stmpre Compute the stable models with a pre-filter (only hybrid lib-mode) --stmrew Compute the stable models with a single-formula rewriting (only hybrid lib-mode) --stmrew2 Compute the stable models with a single-formula rewriting on internal representation(only hybrid lib-mode) + --twoval Compute the two valued models with the nogood-learning based + approach -v Sets log verbosity (multiple times means more verbose) -V, --version Print version information ``` @@ -74,6 +83,7 @@ use adf_bdd::adfbiodivine::Adf as BdAdf; use adf_bdd::parser::AdfParser; use clap::Parser; +use crossbeam_channel::unbounded; use strum::VariantNames; #[derive(Parser, Debug)] @@ -127,6 +137,9 @@ struct App { /// Choose which heuristics shall be used by the nogood-learning approach #[clap(long, possible_values = adf_bdd::adf::heuristics::Heuristic::VARIANTS.iter().filter(|&v| v != &"Custom"))] heu: Option>, + /// Compute the two valued models with the nogood-learning based approach + #[clap(long = "twoval")] + two_val: bool, /// Compute the complete models #[clap(long = "com")] complete: bool, @@ -222,6 +235,14 @@ impl App { } } + if self.two_val { + let (sender, receiver) = unbounded(); + naive_adf.two_val_nogood_channel(self.heu.unwrap_or_default(), sender); + for model in receiver.into_iter() { + print!("{}", printer.print_interpretation(&model)); + } + } + if self.stable { for model in naive_adf.stable() { print!("{}", printer.print_interpretation(&model)); diff --git a/docs/adf-bdd.md b/docs/adf-bdd.md index 5771a5d..bb9ed08 100644 --- a/docs/adf-bdd.md +++ b/docs/adf-bdd.md @@ -14,7 +14,7 @@ This is the readme for the executable solver. ## Usage ``` USAGE: - adf_bdd [OPTIONS] + adf-bdd [OPTIONS] ARGS: Input filename @@ -29,8 +29,11 @@ OPTIONS: the given filename --grd Compute the grounded model -h, --help Print help information + --heu Choose which heuristics shall be used by the nogood-learning + approach [possible values: Simple, MinModMinPathsMaxVarImp, + MinModMaxVarImpMinPaths] --import Import an adf- bdd state instead of an adf - --lib choose the bdd implementation of either 'biodivine', 'naive', or + --lib Choose the bdd implementation of either 'biodivine', 'naive', or hybrid [default: hybrid] --lx Sorts variables in an lexicographic manner -q Sets log verbosity to only errors @@ -41,11 +44,14 @@ OPTIONS: heuristics a --stmcb Compute the stable models with the help of modelcounting using heuristics b + --stmng Compute the stable models with the nogood-learning based approach --stmpre Compute the stable models with a pre-filter (only hybrid lib-mode) --stmrew Compute the stable models with a single-formula rewriting (only hybrid lib-mode) --stmrew2 Compute the stable models with a single-formula rewriting on internal representation(only hybrid lib-mode) + --twoval Compute the two valued models with the nogood-learning based + approach -v Sets log verbosity (multiple times means more verbose) -V, --version Print version information ``` From c234bd436a34067dfb0312bbfe43489ced43ad25 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Thu, 28 Jul 2022 16:35:20 +0200 Subject: [PATCH 44/51] Fix cli-test Update name in cli test for the testing of the binary --- bin/tests/cli.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bin/tests/cli.rs b/bin/tests/cli.rs index 8460b1e..7ca6bfc 100644 --- a/bin/tests/cli.rs +++ b/bin/tests/cli.rs @@ -27,7 +27,7 @@ fn arguments() -> Result<(), Box> { cmd.arg("--version"); cmd.assert() .success() - .stdout(predicate::str::contains("adf_bdd-solver ")); + .stdout(predicate::str::contains("adf-bdd-solver ")); Ok(()) } From deb7282b6f1df6f53fdcf98f10871707f1287ffb Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler <71695780+ellmau@users.noreply.github.com> Date: Fri, 29 Jul 2022 09:16:47 +0200 Subject: [PATCH 45/51] Update lib/README to match lib-documentation --- lib/README.md | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/lib/README.md b/lib/README.md index 5c87cfc..8d364b2 100644 --- a/lib/README.md +++ b/lib/README.md @@ -127,24 +127,29 @@ use the new `NoGood`-based algorithm and utilise the new interface with channels use adf_bdd::parser::AdfParser; use adf_bdd::adf::Adf; use adf_bdd::adf::heuristics::Heuristic; -use adf_bdd::datatypes::Term; +use adf_bdd::datatypes::{Term, adf::VarContainer}; // create a channel let (s, r) = crossbeam_channel::unbounded(); +let variables = VarContainer::default(); +let variables_worker = variables.clone(); // spawn a solver thread let solving = std::thread::spawn(move || { // use the above example as input let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d)."; - let parser = AdfParser::default(); + let parser = AdfParser::with_var_container(variables_worker); parser.parse()(&input).expect("parsing worked well"); // use hybrid approach let mut adf = adf_bdd::adfbiodivine::Adf::from_parser(&parser).hybrid_step(); // compute stable with the simple heuristic adf.stable_nogood_channel(Heuristic::Simple, s); }); - +let printer = variables.print_dictionary(); // print results as they are computed while let Ok(result) = r.recv() { - println!("stable model: {:?}", result); + print!("stable model: {:?} \n", result); + // use dictionary + print!("stable model with variable names: {}", printer.print_interpretation(&result)); +# assert_eq!(result, vec![Term(1),Term(1),Term(0),Term(0)]); } // waiting for the other thread to close solving.join().unwrap(); From e70d55f79286bced4dcc2edc2c8348058109186d Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Fri, 29 Jul 2022 09:19:50 +0200 Subject: [PATCH 46/51] Update Version to 0.3.0 Due to braking API changes and reaching a milestone, the version is incremented to 0.3.0 (beta) --- Cargo.lock | 4 ++-- bin/Cargo.toml | 4 ++-- lib/Cargo.toml | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 182222d..1f44795 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4,7 +4,7 @@ version = 3 [[package]] name = "adf-bdd-solver" -version = "0.2.5" +version = "0.3.0" dependencies = [ "adf_bdd", "assert_cmd", @@ -21,7 +21,7 @@ dependencies = [ [[package]] name = "adf_bdd" -version = "0.2.5" +version = "0.3.0" dependencies = [ "biodivine-lib-bdd", "crossbeam-channel", diff --git a/bin/Cargo.toml b/bin/Cargo.toml index 46ce01d..4779075 100644 --- a/bin/Cargo.toml +++ b/bin/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "adf-bdd-solver" -version = "0.2.5" +version = "0.3.0" authors = ["Stefan Ellmauthaler "] edition = "2021" homepage = "https://ellmau.github.io/adf-obdd" @@ -16,7 +16,7 @@ name = "adf-bdd" path = "src/main.rs" [dependencies] -adf_bdd = { version="0.2.5", path="../lib", default-features = false } +adf_bdd = { version="0.3.0", path="../lib", default-features = false } clap = {version = "3.2.12", features = [ "derive", "cargo", "env" ]} log = { version = "0.4", features = [ "max_level_trace", "release_max_level_info" ] } serde = { version = "1.0", features = ["derive","rc"] } diff --git a/lib/Cargo.toml b/lib/Cargo.toml index 33b761b..2a9599b 100644 --- a/lib/Cargo.toml +++ b/lib/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "adf_bdd" -version = "0.2.5" +version = "0.3.0" authors = ["Stefan Ellmauthaler "] edition = "2021" homepage = "https://ellmau.github.io/adf-obdd/" From e4c5718ab6d7cc1ef5d863b82aebb5457672070c Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler <71695780+ellmau@users.noreply.github.com> Date: Fri, 29 Jul 2022 13:10:15 +0200 Subject: [PATCH 47/51] Update Documentation navigation (#81) * Update index.md * Update adf_bdd.md * Update adf-bdd.md --- docs/adf-bdd.md | 3 +++ docs/adf_bdd.md | 3 +++ docs/index.md | 3 +++ 3 files changed, 9 insertions(+) diff --git a/docs/adf-bdd.md b/docs/adf-bdd.md index bb9ed08..e76c6ca 100644 --- a/docs/adf-bdd.md +++ b/docs/adf-bdd.md @@ -8,6 +8,9 @@ ![Crates.io](https://img.shields.io/crates/l/adf_bdd) [![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd)](https://github.com/ellmau/adf-obdd/discussions) ![rust-edition](https://img.shields.io/badge/Rust--edition-2021-blue?logo=rust) +| [Home](index.md) | [Binary](adf-bdd.md) | [Library](adf_bdd.md)| [Repository](https://github.com/ellmau/adf-obdd) | +|--- | --- | --- | --- | + # Abstract Dialectical Frameworks solved by Binary Decision Diagrams; developed in Dresden (ADF-BDD) This is the readme for the executable solver. diff --git a/docs/adf_bdd.md b/docs/adf_bdd.md index 605898e..1dcc0c3 100644 --- a/docs/adf_bdd.md +++ b/docs/adf_bdd.md @@ -8,6 +8,9 @@ ![Crates.io](https://img.shields.io/crates/l/adf_bdd) [![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd)](https://github.com/ellmau/adf-obdd/discussions) ![rust-edition](https://img.shields.io/badge/Rust--edition-2021-blue?logo=rust) +| [Home](index.md) | [Binary](adf-bdd.md) | [Library](adf_bdd.md)| [Repository](https://github.com/ellmau/adf-obdd) | +|--- | --- | --- | --- | + # Abstract Dialectical Frameworks solved by Binary Decision Diagrams; developed in Dresden (ADF_BDD) This library contains an efficient representation of Abstract Dialectical Frameworks (ADf) by utilising an implementation of Ordered Binary Decision Diagrams (OBDD) diff --git a/docs/index.md b/docs/index.md index 4c2f6dc..e0eed26 100644 --- a/docs/index.md +++ b/docs/index.md @@ -8,6 +8,9 @@ ![Crates.io](https://img.shields.io/crates/l/adf_bdd) [![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd)](https://github.com/ellmau/adf-obdd/discussions) ![rust-edition](https://img.shields.io/badge/Rust--edition-2021-blue?logo=rust) +| [Home](index.md) | [Binary](adf-bdd.md) | [Library](adf_bdd.md)| [Repository](https://github.com/ellmau/adf-obdd) | +|--- | --- | --- | --- | + # Abstract Dialectical Frameworks solved by (ordered) Binary Decision Diagrams; developed in Dresden (ADF-oBDD project) This project is currently split into two parts: From fac10ddb3c066cc1acb286e6e5a6b38cce16a8d0 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 2 Aug 2022 09:54:39 +0200 Subject: [PATCH 48/51] flake.lock: Update MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Flake lock file updates: • Updated input 'flake-utils': 'github:numtide/flake-utils/1ed9fb1935d260de5fe1c2f7ee0ebaae17ed2fa1' (2022-05-30) → 'github:numtide/flake-utils/7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249' (2022-07-04) • Updated input 'gitignoresrc': 'github:hercules-ci/gitignore.nix/bff2832ec341cf30acb3a4d3e2e7f1f7b590116a' (2022-03-05) → 'github:hercules-ci/gitignore.nix/f2ea0f8ff1bce948ccb6b893d15d5ea3efaf1364' (2022-07-21) • Updated input 'nixpkgs': 'github:NixOS/nixpkgs/8b538fcb329a7bc3d153962f17c509ee49166973' (2022-06-15) → 'github:NixOS/nixpkgs/e43cf1748462c81202a32b26294e9f8eefcc3462' (2022-08-01) • Updated input 'nixpkgs-unstable': 'github:NixOS/nixpkgs/b1957596ff1c7aa8c55c4512b7ad1c9672502e8e' (2022-06-15) → 'github:NixOS/nixpkgs/7b9be38c7250b22d829ab6effdee90d5e40c6e5c' (2022-07-30) • Updated input 'rust-overlay': 'github:oxalica/rust-overlay/9eea93067eff400846c36f57b7499df9ef428ba0' (2022-06-17) → 'github:oxalica/rust-overlay/9055cb4f33f062c0dd33aa7e3c89140da8f70057' (2022-08-02) --- flake.lock | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/flake.lock b/flake.lock index ff4fe4a..4159f04 100644 --- a/flake.lock +++ b/flake.lock @@ -2,11 +2,11 @@ "nodes": { "flake-utils": { "locked": { - "lastModified": 1653893745, - "narHash": "sha256-0jntwV3Z8//YwuOjzhV2sgJJPt+HY6KhU7VZUL0fKZQ=", + "lastModified": 1656928814, + "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=", "owner": "numtide", "repo": "flake-utils", - "rev": "1ed9fb1935d260de5fe1c2f7ee0ebaae17ed2fa1", + "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249", "type": "github" }, "original": { @@ -18,11 +18,11 @@ "gitignoresrc": { "flake": false, "locked": { - "lastModified": 1646480205, - "narHash": "sha256-kekOlTlu45vuK2L9nq8iVN17V3sB0WWPqTTW3a2SQG0=", + "lastModified": 1658402513, + "narHash": "sha256-wk38v/mbLsOo6+IDmmH1H0ADR87iq9QTTD1BP9X2Ags=", "owner": "hercules-ci", "repo": "gitignore.nix", - "rev": "bff2832ec341cf30acb3a4d3e2e7f1f7b590116a", + "rev": "f2ea0f8ff1bce948ccb6b893d15d5ea3efaf1364", "type": "github" }, "original": { @@ -33,11 +33,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1655278232, - "narHash": "sha256-H6s7tnHYiDKFCcLADS4sl1sUq0dDJuRQXCieguk/6SA=", + "lastModified": 1659342832, + "narHash": "sha256-ePnxG4hacRd6oZMk+YeCSYMNUnHCe+qPLI0/+VaTu48=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "8b538fcb329a7bc3d153962f17c509ee49166973", + "rev": "e43cf1748462c81202a32b26294e9f8eefcc3462", "type": "github" }, "original": { @@ -49,11 +49,11 @@ }, "nixpkgs-unstable": { "locked": { - "lastModified": 1655306633, - "narHash": "sha256-nv4FfWWV/dEelByjXJtJkoDPOHIsKfLq50RN3Hqq5Yk=", + "lastModified": 1659219666, + "narHash": "sha256-pzYr5fokQPHv7CmUXioOhhzDy/XyWOIXP4LZvv/T7Mk=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "b1957596ff1c7aa8c55c4512b7ad1c9672502e8e", + "rev": "7b9be38c7250b22d829ab6effdee90d5e40c6e5c", "type": "github" }, "original": { @@ -82,11 +82,11 @@ ] }, "locked": { - "lastModified": 1655434021, - "narHash": "sha256-lfioRPXTsDXk0OIApyvCtiVQDdqUs19iCi+aWkijcm0=", + "lastModified": 1659409092, + "narHash": "sha256-OBY2RCYZeeOA3FTYUb86BPMUBEyKEwpwhpU2QKboRJQ=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "9eea93067eff400846c36f57b7499df9ef428ba0", + "rev": "9055cb4f33f062c0dd33aa7e3c89140da8f70057", "type": "github" }, "original": { From b3b2632d8cd16ff4dbbf0b416871477069a33df1 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 2 Aug 2022 10:04:48 +0200 Subject: [PATCH 49/51] Add type alias for NoGood Add a type alias `Interpretation` for NoGood to reflect the duality where an Interpretation might become a NoGood. --- lib/src/nogoods.rs | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs index ef117e5..6a53faf 100644 --- a/lib/src/nogoods.rs +++ b/lib/src/nogoods.rs @@ -9,6 +9,10 @@ use std::{ use crate::datatypes::Term; use roaring::RoaringBitmap; +/// A [NoGood] and an [Interpretation] can be represented by the same structure. +/// Moreover this duality (i.e. an [Interpretation] becomes a [NoGood] is reflected by this type alias. +pub type Interpretation = NoGood; + /// Representation of a nogood by a pair of [Bitmaps][RoaringBitmap] #[derive(Debug, Default, Clone)] pub struct NoGood { @@ -28,8 +32,8 @@ impl PartialEq for NoGood { } impl NoGood { - /// Creates a [NoGood] from a given Vector of [Terms][Term]. - pub fn from_term_vec(term_vec: &[Term]) -> NoGood { + /// Creates an [Interpretation] from a given Vector of [Terms][Term]. + pub fn from_term_vec(term_vec: &[Term]) -> Interpretation { let mut result = Self::default(); term_vec.iter().enumerate().for_each(|(idx, val)| { let idx:u32 = idx.try_into().expect("no-good learner implementation is based on the assumption that only u32::MAX-many variables are in place"); @@ -55,10 +59,10 @@ impl NoGood { } /// Returns [None] if the pair contains inconsistent pairs. - /// Otherwise it returns a [NoGood] which represents the set values. + /// Otherwise it returns an [Interpretation] which represents the set values. pub fn try_from_pair_iter( pair_iter: &mut impl Iterator, - ) -> Option { + ) -> Option { let mut result = Self::default(); let mut visit = false; for (idx, val) in pair_iter { @@ -144,8 +148,8 @@ impl NoGood { self.value = self.value.borrow().bitor(&other.value); } - /// Returns [true] if the other [NoGood] matches with all the assignments of the current [NoGood]. - pub fn is_violating(&self, other: &NoGood) -> bool { + /// Returns [true] if the other [Interpretation] matches with all the assignments of the current [NoGood]. + pub fn is_violating(&self, other: &Interpretation) -> bool { let active = self.active.borrow().bitand(other.active.borrow()); if self.active.len() == active.len() { let lhs = active.borrow().bitand(self.value.borrow()); @@ -179,7 +183,6 @@ impl From<&[Term]> for NoGood { } /// A structure to store [NoGoods][NoGood] and offer operations and deductions based on them. -// TODO:make struct crate-private #[derive(Debug)] pub struct NoGoodStore { store: Vec>, From 154b975287dc94c2441bc38aa6bab8bb6dd4e5f2 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 2 Aug 2022 10:24:56 +0200 Subject: [PATCH 50/51] Apply review comments --- lib/src/adf.rs | 2 +- lib/src/nogoods.rs | 11 ++--------- 2 files changed, 3 insertions(+), 10 deletions(-) diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 7bb8247..f8822dd 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -1289,7 +1289,7 @@ mod test { fn adf_default() { let _adf = Adf::default(); } - //#[cfg(feature = "adhoccountmodels")] + #[test] fn facet_counts() { let parser = AdfParser::default(); diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs index 6a53faf..de25bbe 100644 --- a/lib/src/nogoods.rs +++ b/lib/src/nogoods.rs @@ -79,11 +79,7 @@ impl NoGood { return None; } } - if visit { - Some(result) - } else { - None - } + visit.then_some(result) } /// Creates an updated [Vec], based on the given [&[Term]] and the [NoGood]. @@ -212,10 +208,7 @@ impl NoGoodStore { /// Tries to create a new [NoGoodStore]. /// Does not succeed if the size is too big for the underlying [NoGood] implementation. pub fn try_new(size: usize) -> Option { - match TryInto::::try_into(size) { - Ok(val) => Some(Self::new(val)), - Err(_) => None, - } + Some(Self::new(size.try_into().ok()?)) } /// Sets the behaviour when managing duplicates. From 5bada6fd951a15ab0311b4164625038527ae1b86 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 2 Aug 2022 10:33:01 +0200 Subject: [PATCH 51/51] Add documentation information about later revisions on VarContainer --- lib/src/datatypes/adf.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/lib/src/datatypes/adf.rs b/lib/src/datatypes/adf.rs index c4db79d..555fb43 100644 --- a/lib/src/datatypes/adf.rs +++ b/lib/src/datatypes/adf.rs @@ -7,6 +7,9 @@ use std::{collections::HashMap, fmt::Display, sync::Arc, sync::RwLock}; /// A container which acts as a dictionary as well as an ordering of variables. /// *names* is a list of variable-names and the sequence of the values is inducing the order of variables. /// *mapping* allows to search for a variable name and to receive the corresponding position in the variable list (`names`). +/// +/// # Important note +/// If one [VarContainer] is used to instantiate an [Adf][crate::adf::Adf] (resp. [Biodivine Adf][crate::adfbiodivine::Adf]) a revision (other than adding more information) might result in wrong variable-name mapping when trying to print the output using the [PrintDictionary]. #[derive(Serialize, Deserialize, Debug, Clone)] pub struct VarContainer { names: Arc>>,