first step towards issue 1

added strong typing to base-datatypes and ordered bdds

relates to #1

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

Cargo.lock

@@ -7,6 +7,18 @@ name = "adf_bdd"
 version = "0.1.1"
 dependencies = [
  "clap",
+ "env_logger",
+ "log",
+ "test-env-log",
+]
+
+[[package]]
+name = "aho-corasick"
+version = "0.7.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1e37cfd5e7657ada45f742d6e99ca5788580b5c529dc78faf11ece6dc702656f"
+dependencies = [
+ "memchr",
 ]
 
 [[package]]
@@ -35,6 +47,12 @@ version = "1.3.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
 
+[[package]]
+name = "cfg-if"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
+
 [[package]]
 name = "clap"
 version = "2.33.3"
@@ -50,6 +68,19 @@ dependencies = [
  "vec_map",
 ]
 
+[[package]]
+name = "env_logger"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b2cf0344971ee6c64c31be0d530793fba457d322dfec2810c453d0ef228f9c3"
+dependencies = [
+ "atty",
+ "humantime",
+ "log",
+ "regex",
+ "termcolor",
+]
+
 [[package]]
 name = "hermit-abi"
 version = "0.1.19"
@@ -59,18 +90,105 @@ dependencies = [
  "libc",
 ]
 
+[[package]]
+name = "humantime"
+version = "2.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4"
+
 [[package]]
 name = "libc"
 version = "0.2.107"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "fbe5e23404da5b4f555ef85ebed98fb4083e55a00c317800bc2a50ede9f3d219"
 
+[[package]]
+name = "log"
+version = "0.4.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "51b9bbe6c47d51fc3e1a9b945965946b4c44142ab8792c50835a980d362c2710"
+dependencies = [
+ "cfg-if",
+]
+
+[[package]]
+name = "memchr"
+version = "2.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "308cc39be01b73d0d18f82a0e7b2a3df85245f84af96fdddc5d202d27e47b86a"
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.32"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ba508cc11742c0dc5c1659771673afbab7a0efab23aa17e854cbab0837ed0b43"
+dependencies = [
+ "unicode-xid",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "38bc8cc6a5f2e3655e0899c1b848643b2562f853f114bfec7be120678e3ace05"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "regex"
+version = "1.5.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d07a8629359eb56f1e2fb1652bb04212c072a87ba68546a04065d525673ac461"
+dependencies = [
+ "aho-corasick",
+ "memchr",
+ "regex-syntax",
+]
+
+[[package]]
+name = "regex-syntax"
+version = "0.6.25"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f497285884f3fcff424ffc933e56d7cbca511def0c9831a7f9b5f6153e3cc89b"
+
 [[package]]
 name = "strsim"
 version = "0.8.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a"
 
+[[package]]
+name = "syn"
+version = "1.0.81"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f2afee18b8beb5a596ecb4a2dce128c719b4ba399d34126b9e4396e3f9860966"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-xid",
+]
+
+[[package]]
+name = "termcolor"
+version = "1.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2dfed899f0eb03f32ee8c6a0aabdb8a7949659e3466561fc0adf54e26d88c5f4"
+dependencies = [
+ "winapi-util",
+]
+
+[[package]]
+name = "test-env-log"
+version = "0.2.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "877189d680101869f65ef94168105d6c188b3a143c13a2d42cf8a09c4c704f8a"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
 [[package]]
 name = "textwrap"
 version = "0.11.0"
@@ -86,6 +204,12 @@ version = "0.1.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3ed742d4ea2bd1176e236172c8429aaf54486e7ac098db29ffe6529e0ce50973"
 
+[[package]]
+name = "unicode-xid"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8ccb82d61f80a663efe1f787a51b16b5a51e3314d6ac365b08639f52387b33f3"
+
 [[package]]
 name = "vec_map"
 version = "0.8.2"
@@ -108,6 +232,15 @@ version = "0.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
 
+[[package]]
+name = "winapi-util"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "70ec6ce85bb158151cae5e5c87f95a8e97d2c0c4b001223f33a334e3ce5de178"
+dependencies = [
+ "winapi",
+]
+
 [[package]]
 name = "winapi-x86_64-pc-windows-gnu"
 version = "0.4.0"

Cargo.toml

@@ -12,3 +12,8 @@ description = "Solver for ADFs grounded semantics by utilising OBDDs - ordered b
 
 [dependencies]
 clap = "2.33.*"
+log = "0.4"
+
+[dev-dependencies]
+env_logger = "*"
+test-env-log = "0.2.*"

flake.nix

@@ -31,6 +31,7 @@
             RUST_LOG = "debug";
             RUST_BACKTRACE = 1;
             buildInputs = [
+              pkgs.rust-bin.nightly.latest.rustfmt
               pkgs.rust-bin.stable.latest.default
               pkgs.rust-analyzer
               pkgs.cargo-audit

src/datatypes.rs

@@ -0,0 +1,114 @@
+use std::{fmt::Display, ops::Deref};
+
+#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Copy, Clone)]
+pub struct Term(pub usize);
+
+impl Deref for Term {
+    type Target = usize;
+    fn deref(&self) -> &Self::Target {
+        &self.0
+    }
+}
+
+impl From<usize> for Term {
+    fn from(val: usize) -> Self {
+        Self(val)
+    }
+}
+
+impl Display for Term {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "Term({})", self.0)
+    }
+}
+
+impl Term {
+    pub const BOT: Term = Term(0);
+    pub const TOP: Term = Term(1);
+
+    pub fn new(val: usize) -> Term {
+        Term(val)
+    }
+
+    pub fn value(self) -> usize {
+        self.0
+    }
+}
+
+#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy)]
+pub struct Var(pub usize);
+
+impl Deref for Var {
+    type Target = usize;
+    fn deref(&self) -> &Self::Target {
+        &self.0
+    }
+}
+
+impl From<usize> for Var {
+    fn from(val: usize) -> Self {
+        Self(val)
+    }
+}
+
+impl Display for Var {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "Var({})", self.0)
+    }
+}
+
+impl Var {
+    pub const TOP: Var = Var(usize::MAX);
+    pub const BOT: Var = Var(usize::MAX - 1);
+
+    pub fn value(self) -> usize {
+        self.0
+    }
+}
+
+#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy)]
+pub(crate) struct BddNode {
+    var: Var,
+    lo: Term,
+    hi: Term,
+}
+
+impl Display for BddNode {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "BddNode: {}, lo: {}, hi: {}", self.var, self.lo, self.hi)
+    }
+}
+
+impl BddNode {
+    pub fn new(var: Var, lo: Term, hi: Term) -> Self {
+        Self { var, lo, hi }
+    }
+
+    pub fn var(self) -> Var {
+        self.var
+    }
+
+    pub fn lo(self) -> Term {
+        self.lo
+    }
+
+    pub fn hi(self) -> Term {
+        self.hi
+    }
+
+    pub fn bot_node() -> Self {
+        Self {
+            var: Var::BOT,
+            lo: Term::BOT,
+            hi: Term::BOT,
+        }
+    }
+
+    pub fn top_node() -> Self {
+        Self {
+            var: Var::TOP,
+            lo: Term::TOP,
+            hi: Term::TOP,
+        }
+    }
+}

src/lib.rs

@@ -32,4 +32,6 @@
 //! ac(d,d).
 //! ```
 pub mod adf;
+pub mod datatypes;
 pub mod obdd;
+pub mod obdd2;

src/obdd2.rs

@@ -0,0 +1,222 @@
+use crate::datatypes::*;
+use std::{cmp::min, collections::HashMap, fmt::Display, ops::Index};
+
+#[derive(Debug)]
+pub(crate) struct Bdd {
+    nodes: Vec<BddNode>,
+    cache: HashMap<BddNode, Term>,
+}
+
+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)?;
+        }
+        Ok(())
+    }
+}
+
+impl Bdd {
+    pub fn new() -> Self {
+        Self {
+            nodes: vec![BddNode::bot_node(), BddNode::top_node()],
+            cache: HashMap::new(),
+        }
+    }
+
+    pub fn variable(&mut self, var: Var) -> Term {
+        self.node(var, Term::BOT, Term::TOP)
+    }
+
+    pub fn constant(val: bool) -> Term {
+        if val {
+            Term::TOP
+        } else {
+            Term::BOT
+        }
+    }
+
+    pub fn not(&mut self, term: Term) -> Term {
+        self.if_then_else(term, Term::BOT, Term::TOP)
+    }
+
+    pub fn and(&mut self, term_a: Term, term_b: Term) -> Term {
+        self.if_then_else(term_a, term_b, Term::BOT)
+    }
+
+    pub fn or(&mut self, term_a: Term, term_b: Term) -> Term {
+        self.if_then_else(term_a, Term::TOP, term_b)
+    }
+
+    pub fn imp(&mut self, term_a: Term, term_b: Term) -> Term {
+        self.if_then_else(term_a, term_b, Term::TOP)
+    }
+
+    pub fn iff(&mut self, term_a: Term, term_b: Term) -> Term {
+        let not_b = self.not(term_b);
+        self.if_then_else(term_a, term_b, not_b)
+    }
+
+    pub fn xor(&mut self, term_a: Term, term_b: Term) -> Term {
+        let not_b = self.not(term_b);
+        self.if_then_else(term_a, not_b, term_b)
+    }
+
+    pub fn restrict(&mut self, tree: Term, var: Var, val: bool) -> Term {
+        let node = self.nodes[tree.0];
+        if node.var() > var || node.var() >= Var::BOT {
+            tree
+        } else if node.var() < var {
+            let lonode = self.restrict(node.lo(), var, val);
+            let hinode = self.restrict(node.hi(), var, val);
+            self.node(node.var(), lonode, hinode)
+        } else {
+            if val {
+                self.restrict(node.hi(), var, val)
+            } else {
+                self.restrict(node.lo(), var, val)
+            }
+        }
+    }
+
+    fn if_then_else(&mut self, i: Term, t: Term, e: Term) -> Term {
+        if i == Term::TOP {
+            t
+        } else if i == Term::BOT {
+            e
+        } else if t == e {
+            t
+        } else if t == Term::TOP && e == Term::BOT {
+            i
+        } else {
+            let minvar = Var(min(
+                self.nodes[i.value()].var().value(),
+                min(
+                    self.nodes[t.value()].var().value(),
+                    self.nodes[e.value()].var().value(),
+                ),
+            ));
+            let itop = self.restrict(i, minvar, true);
+            let ttop = self.restrict(t, minvar, true);
+            let etop = self.restrict(e, minvar, true);
+            let ibot = self.restrict(i, minvar, false);
+            let tbot = self.restrict(t, minvar, false);
+            let ebot = self.restrict(e, minvar, false);
+
+            let top_ite = self.if_then_else(itop, ttop, etop);
+            let bot_ite = self.if_then_else(ibot, tbot, ebot);
+            self.node(minvar, bot_ite, top_ite)
+        }
+    }
+    fn node(&mut self, var: Var, lo: Term, hi: Term) -> Term {
+        if lo == hi {
+            lo
+        } else {
+            let node = BddNode::new(var, lo, hi);
+            match self.cache.get(&node) {
+                Some(t) => *t,
+                None => {
+                    let new_term = Term(self.nodes.len());
+                    self.nodes.push(node);
+                    self.cache.insert(node, new_term);
+                    new_term
+                }
+            }
+        }
+    }
+}
+
+#[cfg(test)]
+mod test {
+    use super::*;
+
+    #[test]
+    fn newbdd() {
+        let bdd = Bdd::new();
+        assert_eq!(bdd.nodes.len(), 2);
+    }
+
+    #[test]
+    fn addconst() {
+        let bdd = Bdd::new();
+
+        assert_eq!(Bdd::constant(true), Term::TOP);
+        assert_eq!(Bdd::constant(false), Term::BOT);
+        assert_eq!(bdd.nodes.len(), 2);
+    }
+
+    #[test]
+    fn addvar() {
+        let mut bdd = Bdd::new();
+        assert_eq!(bdd.variable(Var(0)), Term(2));
+        assert_eq!(bdd.variable(Var(1)), Term(3));
+        assert_eq!(Var(1), Var(1));
+        bdd.variable(Var(0));
+        assert_eq!(bdd.variable(Var(0)), Term(2));
+    }
+
+    #[test]
+    fn use_negation() {
+        let mut bdd = Bdd::new();
+        let v1 = bdd.variable(Var(0));
+        assert_eq!(v1, 2.into());
+        assert_eq!(bdd.not(v1), Term(3));
+    }
+
+    #[test]
+    fn use_add() {
+        let mut bdd = Bdd::new();
+        let v1 = bdd.variable(Var(0));
+        let v2 = bdd.variable(Var(1));
+        let v3 = bdd.variable(Var(2));
+
+        let a1 = bdd.and(v1, v2);
+        let a2 = bdd.and(a1, v3);
+        assert_eq!(a2, Term(7));
+    }
+
+    #[test]
+    fn use_or() {
+        let mut bdd = Bdd::new();
+
+        let v1 = bdd.variable(Var(0));
+        let v2 = bdd.variable(Var(1));
+        let v3 = bdd.variable(Var(2));
+
+        let a1 = bdd.and(v1, v2);
+        let a2 = bdd.or(a1, v3);
+        assert_eq!(a2, Term(7));
+    }
+
+    #[test]
+    fn produce_different_conversions() {
+        let mut bdd = Bdd::new();
+
+        let v1 = bdd.variable(Var(0));
+        let v2 = bdd.variable(Var(1));
+
+        let t1 = bdd.and(v1, v2);
+        let nt1 = bdd.not(t1);
+        let ft = bdd.or(v1, nt1);
+
+        assert_eq!(ft, Term::TOP);
+
+        let v3 = bdd.variable(Var(2));
+        let nv3 = bdd.not(v3);
+        assert_eq!(bdd.and(v3, nv3), Term::BOT);
+
+        let conj = bdd.and(v1, v2);
+        assert_eq!(bdd.restrict(conj, Var(0), false), Term::BOT);
+        assert_eq!(bdd.restrict(conj, Var(0), true), v2);
+
+        let a = bdd.and(v3, v2);
+        let b = bdd.or(v2, v1);
+
+        let con1 = bdd.and(a, conj);
+
+        let end = bdd.or(con1, b);
+        let x = bdd.restrict(end, Var(1), false);
+        assert_eq!(x, Term(2));
+    }
+}