Implements complete models in a dual manner to stable models

Signed-off-by: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "adf_bdd"
-version = "0.1.3"
+version = "0.1.4"
 authors = ["Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>"]
 edition = "2021"
 repository = "https://github.com/ellmau/adf-obdd/"

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 = {

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<Vec<Term>> {
+        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<Item = Vec<Term>> + '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)]
+            ]
+        );
+    }
 }

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<Term>,
+    indexes: Vec<usize>,
+    current: Option<Vec<usize>>,
+    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::<Vec<_>>();
+        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<Term>;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        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);
+    }
 }

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));
             }
         }
     }

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
+    #[test]
-pub mod vectorize {
+    fn display() {
-    use serde::{Deserialize, Deserializer, Serialize, Serializer};
+        let mut bdd = Bdd::new();
-    use std::iter::FromIterator;
 
-    /// Serialise into a Vector from a Map
+        let v1 = bdd.variable(Var(0));
-    pub fn serialize<'a, T, K, V, S>(target: T, ser: S) -> Result<S::Ok, S::Error>
+        let v2 = bdd.variable(Var(1));
-    where
+        let v3 = bdd.variable(Var(2));
-        S: Serializer,
-        T: IntoIterator<Item = (&'a K, &'a V)>,
-        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
+        let a1 = bdd.and(v1, v2);
-    pub fn deserialize<'de, T, K, V, D>(des: D) -> Result<T, D::Error>
+        let a2 = bdd.or(a1, v3);
-    where
+
-        D: Deserializer<'de>,
+        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");
-        T: FromIterator<(K, V)>,
-        K: Deserialize<'de>,
-        V: Deserialize<'de>,
-    {
-        let container: Vec<_> = serde::Deserialize::deserialize(des)?;
-        Ok(T::from_iter(container.into_iter()))
     }
 }

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<S::Ok, S::Error>
+where
+    S: Serializer,
+    T: IntoIterator<Item = (&'a K, &'a V)>,
+    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<T, D::Error>
+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()))
+}

tests/cli.rs

@@ -66,14 +66,14 @@ fn runs() -> Result<(), Box<dyn std::error::Error>> {
     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<dyn std::error::Error>> {
         .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<dyn std::error::Error>> {
         .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<dyn std::error::Error>> {
         .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<dyn std::error::Error>> {
         .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<dyn std::error::Error>> {
         .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(())
 }