From 308a39b435a38c7f7c41f6cd27c60c7f3d29d9e8 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Wed, 12 Jan 2022 14:27:00 +0100 Subject: [PATCH] Implements complete models in a dual manner to stable models Signed-off-by: Stefan Ellmauthaler --- Cargo.toml | 2 +- flake.nix | 2 +- src/adf.rs | 80 +++++++++++++++++++- src/datatypes/adf.rs | 168 ++++++++++++++++++++++++++++++++++++++++++ src/main.rs | 13 +++- src/obdd.rs | 39 +++------- src/obdd/vectorize.rs | 27 +++++++ tests/cli.rs | 24 ++++-- 8 files changed, 316 insertions(+), 39 deletions(-) create mode 100644 src/obdd/vectorize.rs diff --git a/Cargo.toml b/Cargo.toml index 5f294ef..a6cd49e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "adf_bdd" -version = "0.1.3" +version = "0.1.4" authors = ["Stefan Ellmauthaler "] edition = "2021" repository = "https://github.com/ellmau/adf-obdd/" diff --git a/flake.nix b/flake.nix index 668ef00..2033a51 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "basic rust flake"; inputs = { - nixpkgs.url = "github:NixOS/nixpkgs/nixos-21.05"; + nixpkgs.url = "github:NixOS/nixpkgs/nixos-21.11"; rust-overlay.url = "github:oxalica/rust-overlay"; flake-utils.url = "github:numtide/flake-utils"; flake-compat = { diff --git a/src/adf.rs b/src/adf.rs index ba82584..dd5334b 100644 --- a/src/adf.rs +++ b/src/adf.rs @@ -9,7 +9,10 @@ use serde::{Deserialize, Serialize}; use crate::{ datatypes::{ - adf::{PrintableInterpretation, TwoValuedInterpretationsIterator, VarContainer}, + adf::{ + PrintableInterpretation, ThreeValuedInterpretationsIterator, + TwoValuedInterpretationsIterator, VarContainer, + }, Term, Var, }, obdd::Bdd, @@ -206,6 +209,49 @@ impl Adf { .map(|(int, _grd)| int) } + /// Computes the first `max_values` stable models + /// if max_values is 0, then all will be computed + pub fn complete(&mut self, max_values: usize) -> Vec> { + let grounded = self.grounded(); + if max_values == 0 { + self.complete_iter(&grounded).collect() + } else { + self.complete_iter(&grounded) + .enumerate() + .take_while(|(idx, _elem)| *idx < max_values) + .map(|(_, elem)| elem) + .collect() + } + } + + /// Computes the complete models + /// Returns an Iterator which contains all complete models + fn complete_iter<'a, 'b, 'c>( + &'a mut self, + grounded: &'b [Term], + ) -> impl Iterator> + 'c + where + 'a: 'c, + 'b: 'c, + { + ThreeValuedInterpretationsIterator::new(grounded).filter(|interpretation| { + interpretation.iter().all(|ac| { + ac.compare_inf( + &interpretation + .iter() + .enumerate() + .fold(*ac, |acc, (var, term)| { + if term.is_truth_value() { + self.bdd.restrict(acc, Var(var), term.is_true()) + } else { + acc + } + }), + ) + }) + }) + } + /// creates a [PrintableInterpretation] for output purposes pub fn print_interpretation<'a, 'b>( &'a self, @@ -360,4 +406,36 @@ mod test { assert_eq!(adf.stable(0), empty); assert_eq!(adf.stable(99999), empty); } + + #[test] + fn complete() { + 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); + + assert_eq!( + adf.complete(1), + vec![vec![Term(1), Term(3), Term(3), Term(9), Term(0), Term(1)]] + ); + + assert_eq!( + adf.complete(0), + vec![ + vec![Term(1), Term(3), Term(3), Term(9), Term(0), Term(1)], + vec![Term(1), Term(3), Term(3), Term(1), Term(0), Term(1)], + vec![Term(1), Term(3), Term(3), Term(0), Term(0), Term(1)], + vec![Term(1), Term(3), Term(1), Term(9), Term(0), Term(1)], + vec![Term(1), Term(3), Term(1), Term(1), Term(0), Term(1)], + vec![Term(1), Term(3), Term(1), Term(0), Term(0), Term(1)], + vec![Term(1), Term(3), Term(0), Term(0), Term(0), Term(1)], + vec![Term(1), Term(1), Term(1), Term(1), Term(0), Term(1)], + vec![Term(1), Term(1), Term(1), Term(0), Term(0), Term(1)], + vec![Term(1), Term(1), Term(0), Term(0), Term(0), Term(1)], + vec![Term(1), Term(0), Term(0), Term(0), Term(0), Term(1)], + vec![Term(1), Term(0), Term(1), Term(1), Term(0), Term(1)], + vec![Term(1), Term(0), Term(1), Term(0), Term(0), Term(1)] + ] + ); + } } diff --git a/src/datatypes/adf.rs b/src/datatypes/adf.rs index eb67006..c3b73b0 100644 --- a/src/datatypes/adf.rs +++ b/src/datatypes/adf.rs @@ -142,9 +142,98 @@ impl Iterator for TwoValuedInterpretationsIterator { } } +/// Provides an Iterator, which contains all three valued Interpretations, with respect to the given +/// 3-valued interpretation. + +#[derive(Debug)] +pub struct ThreeValuedInterpretationsIterator { + original: Vec, + indexes: Vec, + current: Option>, + started: bool, + last_iteration: bool, +} + +impl ThreeValuedInterpretationsIterator { + /// Creates a new iterable structure, which represents all three-valued interpretations wrt. the given 3-valued interpretation + pub fn new(term: &[Term]) -> Self { + let indexes = term + .iter() + .enumerate() + .filter_map(|(idx, &v)| (!v.is_truth_value()).then(|| idx)) + .rev() + .collect::>(); + let current = vec![2; indexes.len()]; + + Self { + indexes, + started: false, + current: Some(current), + original: term.into(), + last_iteration: false, + } + } + + fn decrement(&mut self) { + if let Some(ref mut current) = self.current { + if let Some((pos, val)) = current.iter().enumerate().find(|(idx, val)| **val > 0) { + if pos > 0 && *val == 2 { + for elem in &mut current[0..pos] { + *elem = 2; + } + } + current[pos] -= 1; + if self.last_iteration { + if current.iter().all(|val| *val == 0) { + self.current = None; + } + } + } else if !self.last_iteration { + let len = current.len(); + if len <= 1 { + self.current = None; + } else { + for elem in &mut current[0..len - 1] { + *elem = 2; + } + } + self.last_iteration = true; + } + } + } +} + +impl Iterator for ThreeValuedInterpretationsIterator { + type Item = Vec; + + fn next(&mut self) -> Option { + if self.started { + if let Some(current) = &self.current { + self.decrement(); + } + } else { + self.started = true; + } + if let Some(current) = &self.current { + let mut result = self.original.clone(); + for (idx, val) in current.iter().enumerate() { + result[self.indexes[idx]] = match val { + 0 => Term::BOT, + 1 => Term::TOP, + _ => self.original[self.indexes[idx]], + } + } + return Some(result); + } + None + } +} + #[cfg(test)] mod test { use super::*; + use test_log::test; + #[test] fn init_varcontainer() { let vc = VarContainer::default(); @@ -181,4 +270,83 @@ mod test { assert_eq!(iter.next(), Some(vec![Term::TOP, Term::TOP])); assert_eq!(iter.next(), None); } + + #[test] + fn three_valued_interpretations() { + let testinterpretation = vec![Term::TOP, Term(22), Term::BOT, Term(12), Term::TOP]; + let mut iter = ThreeValuedInterpretationsIterator::new(&testinterpretation); + assert_eq!( + iter.next(), + Some(vec![Term::TOP, Term(22), Term::BOT, Term(12), Term::TOP]) + ); + assert_eq!( + iter.next(), + Some(vec![Term::TOP, Term(22), Term::BOT, Term::TOP, Term::TOP]) + ); + assert_eq!( + iter.next(), + Some(vec![Term::TOP, Term(22), Term::BOT, Term::BOT, Term::TOP]) + ); + assert_eq!( + iter.next(), + Some(vec![Term::TOP, Term::TOP, Term::BOT, Term(12), Term::TOP]) + ); + assert_eq!( + iter.next(), + Some(vec![Term::TOP, Term::TOP, Term::BOT, Term::TOP, Term::TOP]) + ); + assert_eq!( + iter.next(), + Some(vec![Term::TOP, Term::TOP, Term::BOT, Term::BOT, Term::TOP]) + ); + assert_eq!( + iter.next(), + Some(vec![Term::TOP, Term::BOT, Term::BOT, Term::BOT, Term::TOP]) + ); + assert_eq!( + iter.next(), + Some(vec![Term::TOP, Term::BOT, Term::BOT, Term(12), Term::TOP]) + ); + assert_eq!( + iter.next(), + Some(vec![Term::TOP, Term::BOT, Term::BOT, Term::TOP, Term::TOP]) + ); + assert_eq!(iter.next(), None); + } + + #[test] + fn tvi_decrement() { + let testinterpretation = vec![Term::TOP, Term(22), Term::BOT, Term(12), Term::TOP]; + let mut iter = ThreeValuedInterpretationsIterator::new(&testinterpretation); + assert_eq!(iter.current, Some(vec![2, 2])); + iter.decrement(); + assert_eq!(iter.current, Some(vec![1, 2])); + iter.decrement(); + assert_eq!(iter.current, Some(vec![0, 2])); + iter.decrement(); + assert_eq!(iter.current, Some(vec![2, 1])); + iter.decrement(); + assert_eq!(iter.current, Some(vec![1, 1])); + iter.decrement(); + assert_eq!(iter.current, Some(vec![0, 1])); + iter.decrement(); + assert_eq!(iter.current, Some(vec![0, 0])); + iter.decrement(); + assert_eq!(iter.current, Some(vec![2, 0])); + iter.decrement(); + assert_eq!(iter.current, Some(vec![1, 0])); + iter.decrement(); + assert_eq!(iter.current, None); + + let testinterpretation = vec![Term::TOP, Term(22), Term::BOT, Term::TOP, Term::TOP]; + let mut iter = ThreeValuedInterpretationsIterator::new(&testinterpretation); + + assert_eq!(iter.current, Some(vec![2])); + iter.decrement(); + assert_eq!(iter.current, Some(vec![1])); + iter.decrement(); + assert_eq!(iter.current, Some(vec![0])); + iter.decrement(); + assert_eq!(iter.current, None); + } } diff --git a/src/main.rs b/src/main.rs index e71d46d..1e768c7 100644 --- a/src/main.rs +++ b/src/main.rs @@ -39,6 +39,9 @@ struct App { /// Compute the stable models #[structopt(long = "stm")] stable: bool, + /// Compute the complete models + #[structopt(long = "com")] + complete: bool, /// Import an adf- bdd state instead of an adf #[structopt(long)] import: bool, @@ -106,12 +109,18 @@ impl App { } if self.grounded { let grounded = adf.grounded(); - println!("{}", adf.print_interpretation(&grounded)); + print!("{}", adf.print_interpretation(&grounded)); + } + if self.complete { + let complete = adf.complete(0); + for model in complete { + print!("{}", adf.print_interpretation(&model)); + } } if self.stable { let stable = adf.stable(0); for model in stable { - println!("{}", adf.print_interpretation(&model)); + print!("{}", adf.print_interpretation(&model)); } } } diff --git a/src/obdd.rs b/src/obdd.rs index 410970e..a1515b4 100644 --- a/src/obdd.rs +++ b/src/obdd.rs @@ -1,4 +1,5 @@ //! Represents an obdd +pub mod vectorize; use crate::datatypes::*; use serde::{Deserialize, Serialize}; use std::{cmp::min, collections::HashMap, fmt::Display}; @@ -14,7 +15,7 @@ impl Display for Bdd { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { writeln!(f, " ")?; for (idx, elem) in self.nodes.iter().enumerate() { - writeln!(f, "{} {}", idx, *elem)?; + writeln!(f, "{} {}", idx, *elem)?; } Ok(()) } @@ -227,34 +228,18 @@ mod test { let x = bdd.restrict(end, Var(1), false); assert_eq!(x, Term(2)); } -} -/// vectorize maps with non-standard keys -pub mod vectorize { - use serde::{Deserialize, Deserializer, Serialize, Serializer}; - use std::iter::FromIterator; + #[test] + fn display() { + let mut bdd = Bdd::new(); - /// Serialise into a Vector from a Map - pub fn serialize<'a, T, K, V, S>(target: T, ser: S) -> Result - where - S: Serializer, - T: IntoIterator, - K: Serialize + 'a, - V: Serialize + 'a, - { - let container: Vec<_> = target.into_iter().collect(); - serde::Serialize::serialize(&container, ser) - } + let v1 = bdd.variable(Var(0)); + let v2 = bdd.variable(Var(1)); + let v3 = bdd.variable(Var(2)); - /// Deserialize from a Vector to a Map - pub fn deserialize<'de, T, K, V, D>(des: D) -> Result - where - D: Deserializer<'de>, - T: FromIterator<(K, V)>, - K: Deserialize<'de>, - V: Deserialize<'de>, - { - let container: Vec<_> = serde::Deserialize::deserialize(des)?; - Ok(T::from_iter(container.into_iter())) + let a1 = bdd.and(v1, v2); + let a2 = bdd.or(a1, v3); + + assert_eq!(format!("{}", bdd), " \n0 BddNode: Var(18446744073709551614), lo: Term(0), hi: Term(0)\n1 BddNode: Var(18446744073709551615), lo: Term(1), hi: Term(1)\n2 BddNode: Var(0), lo: Term(0), hi: Term(1)\n3 BddNode: Var(1), lo: Term(0), hi: Term(1)\n4 BddNode: Var(2), lo: Term(0), hi: Term(1)\n5 BddNode: Var(0), lo: Term(0), hi: Term(3)\n6 BddNode: Var(1), lo: Term(4), hi: Term(1)\n7 BddNode: Var(0), lo: Term(4), hi: Term(6)\n"); } } diff --git a/src/obdd/vectorize.rs b/src/obdd/vectorize.rs new file mode 100644 index 0000000..9619288 --- /dev/null +++ b/src/obdd/vectorize.rs @@ -0,0 +1,27 @@ +//! vectorize maps with non-standard keys +use serde::{Deserialize, Deserializer, Serialize, Serializer}; +use std::iter::FromIterator; + +/// Serialise into a Vector from a Map +pub fn serialize<'a, T, K, V, S>(target: T, ser: S) -> Result +where + S: Serializer, + T: IntoIterator, + K: Serialize + 'a, + V: Serialize + 'a, +{ + let container: Vec<_> = target.into_iter().collect(); + serde::Serialize::serialize(&container, ser) +} + +/// Deserialize from a Vector to a Map +pub fn deserialize<'de, T, K, V, D>(des: D) -> Result +where + D: Deserializer<'de>, + T: FromIterator<(K, V)>, + K: Deserialize<'de>, + V: Deserialize<'de>, +{ + let container: Vec<_> = serde::Deserialize::deserialize(des)?; + Ok(T::from_iter(container.into_iter())) +} diff --git a/tests/cli.rs b/tests/cli.rs index a660261..1d463b4 100644 --- a/tests/cli.rs +++ b/tests/cli.rs @@ -66,14 +66,14 @@ fn runs() -> Result<(), Box> { cmd = Command::cargo_bin("adf_bdd")?; cmd.arg(file.path()).arg("--an").arg("--grd").arg("--stm"); cmd.assert().success().stdout(predicate::str::contains( - "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n\n", + "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n", )); cmd = Command::cargo_bin("adf_bdd")?; cmd.env_clear(); cmd.arg(file.path()).arg("--an").arg("--grd"); cmd.assert().success().stdout(predicate::str::contains( - "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n\n", + "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n", )); cmd = Command::cargo_bin("adf_bdd")?; @@ -83,7 +83,7 @@ fn runs() -> Result<(), Box> { .arg("--rust_log") .arg("trace"); cmd.assert().success().stdout(predicate::str::contains( - "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n\n", + "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n", )); cmd = Command::cargo_bin("adf_bdd")?; @@ -93,7 +93,7 @@ fn runs() -> Result<(), Box> { .arg("--rust_log") .arg("warn"); cmd.assert().success().stdout(predicate::str::contains( - "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n\n", + "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n", )); let tempdir = assert_fs::TempDir::new()?; @@ -105,7 +105,7 @@ fn runs() -> Result<(), Box> { .arg("--export") .arg(tempdir.path().with_file_name("test.json")); cmd.assert().success().stdout(predicate::str::contains( - "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n\n", + "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n", )); cmd = Command::cargo_bin("adf_bdd")?; @@ -115,7 +115,7 @@ fn runs() -> Result<(), Box> { .arg("--export") .arg(tempdir.path().with_file_name("test.json")); cmd.assert().success().stdout(predicate::str::contains( - "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n\n", + "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n", )); cmd = Command::cargo_bin("adf_bdd")?; @@ -124,7 +124,17 @@ fn runs() -> Result<(), Box> { .arg("--grd") .arg("--import"); cmd.assert().success().stdout(predicate::str::contains( - "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n\n", + "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n", + )); + + cmd = Command::cargo_bin("adf_bdd")?; + cmd.arg(file.path()) + .arg("--an") + .arg("--com") + .arg("--rust_log") + .arg("warn"); + cmd.assert().success().stdout(predicate::str::contains( + "u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n", )); Ok(()) }