From 40ea81b4178578e2029fc9d84173fcc482f32ea3 Mon Sep 17 00:00:00 2001
From: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
Date: Wed, 23 Jun 2021 16:02:29 +0200
Subject: [PATCH] changed structure, added basic functionality for formulae and
 statements (adf representation)

Signed-off-by: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
---
 src/adf.rs  | 141 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 src/lib.rs  |   3 +-
 src/obdd.rs |   6 +--
 3 files changed, 146 insertions(+), 4 deletions(-)
 create mode 100644 src/adf.rs

diff --git a/src/adf.rs b/src/adf.rs
new file mode 100644
index 0000000..1d9d0e6
--- /dev/null
+++ b/src/adf.rs
@@ -0,0 +1,141 @@
+use std::{
+    collections::HashMap,
+    num::ParseFloatError,
+    str::{self, FromStr},
+};
+
+use super::obdd::Bdd;
+
+struct Statement {
+    label: String,     // label of the statement
+    var: usize,        // variable node in bdd
+    ac: Option<usize>, // node in bdd
+}
+
+impl Statement {
+    pub fn new(label: &str, var: usize) -> Self {
+        Statement {
+            label: String::from_str(label).unwrap(),
+            var: var,
+            ac: None,
+        }
+    }
+
+    pub fn add_ac(&mut self, ac: usize) {
+        self.ac = Some(ac);
+    }
+}
+
+struct Adf {
+    bdd: Bdd,
+    stmts: Vec<Statement>,
+    dict: HashMap<String, usize>, // label to pos in vec
+}
+
+impl Adf {
+    pub fn new() -> Self {
+        Adf {
+            bdd: Bdd::new(),
+            stmts: Vec::new(),
+            dict: HashMap::new(),
+        }
+    }
+
+    fn add_statement(&mut self, statement: &str) {
+        if self.dict.get(statement).is_none() {
+            let pos = self.stmts.len();
+            self.stmts
+                .push(Statement::new(statement, self.bdd.variable(pos).clone()));
+            self.dict.insert(self.stmts[pos].label.to_string(), pos);
+        }
+    }
+
+    fn parseformula(&mut self, ac: &str) -> usize {
+        if let Some(split) = ac.find(',') {
+            let (l, r) = ac.split_at(split);
+            let rterm = self.parseformula(&r[1..r.len() - 1]);
+            if ac.starts_with("and(") {
+                let lterm = self.parseformula(&l[4..]);
+                self.bdd.and(lterm, rterm)
+            } else if ac.starts_with("or(") {
+                let lterm = self.parseformula(&l[3..]);
+                self.bdd.or(lterm, rterm)
+            } else if ac.starts_with("iff(") {
+                let lterm = self.parseformula(&l[4..]);
+                let neglterm = self.bdd.not(lterm);
+                let negrterm = self.bdd.not(rterm);
+                let con1 = self.bdd.and(lterm, rterm);
+                let con2 = self.bdd.and(neglterm, negrterm);
+
+                self.bdd.or(con1, con2)
+            } else {
+                //if ac.starts_with("xor("){
+                let lterm = self.parseformula(&l[4..]);
+                let neglterm = self.bdd.not(lterm);
+                let negrterm = self.bdd.not(rterm);
+                let con1 = self.bdd.and(neglterm, rterm);
+                let con2 = self.bdd.and(lterm, negrterm);
+
+                self.bdd.or(con1, con2)
+            }
+        } else {
+            if ac.starts_with("neg(") {
+                let term = self.parseformula(&ac[4..ac.len() - 1]);
+                self.bdd.not(term)
+            } else if ac.eq("c(v)") {
+                self.bdd.constant(true)
+            } else if ac.eq("c(f)") {
+                self.bdd.constant(false)
+            } else {
+                match self.dict.get(ac) {
+                    Some(it) => self.stmts[*it].var,
+                    _ => unreachable!(),
+                }
+            }
+        }
+    }
+}
+
+#[cfg(test)]
+mod test {
+    use super::*;
+
+    #[test]
+    fn add_statement() {
+        let mut adf = Adf::new();
+
+        adf.add_statement("A");
+        adf.add_statement("B");
+        adf.add_statement("A");
+
+        assert_eq!(adf.stmts.len(), 2);
+
+        adf.add_statement("C");
+        assert_eq!(adf.stmts.len(), 3);
+    }
+
+    #[test]
+    fn parseformula(){
+        let mut adf = Adf::new();
+
+        adf.add_statement("a");
+        adf.add_statement("b");
+        adf.add_statement("c");
+
+        assert_eq!(adf.parseformula("and(a,or(b,c))"),6);
+        assert_eq!(adf.parseformula("xor(a,b)"),11);
+        assert_eq!(adf.parseformula("or(c(f),b)"),3); // is b
+    }
+
+    #[test]
+    #[should_panic]
+    fn parseformula_panic(){
+      let mut adf = Adf::new();
+
+      adf.add_statement("a");
+      adf.add_statement("b");
+      adf.add_statement("c");
+
+      adf.parseformula("and(a,or(b,d))");
+    }
+}
diff --git a/src/lib.rs b/src/lib.rs
index 8090139..0902895 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1 +1,2 @@
-pub mod obdd;
\ No newline at end of file
+pub mod obdd;
+pub mod adf;
\ No newline at end of file
diff --git a/src/obdd.rs b/src/obdd.rs
index 6719975..8dedf56 100644
--- a/src/obdd.rs
+++ b/src/obdd.rs
@@ -20,7 +20,7 @@ impl std::fmt::Display for BddNode {
     }
 }
 
-struct Bdd {
+pub (crate) struct Bdd {
     nodes: Vec<BddNode>,
     hash: HashMap<BddNode, Term>,
 }
@@ -67,11 +67,11 @@ impl Bdd {
         }
     }
 
-    fn variable(&mut self, var: usize) -> Term {
+    pub fn variable(&mut self, var: usize) -> Term {
         self.create_node(var, BDD_BOT, BDD_TOP)
     }
 
-    fn constant(&self, val: bool) -> Term {
+    pub fn constant(&self, val: bool) -> Term {
         if val {
             BDD_TOP
         } else {