From 0ad6460d40b11d6cfba305bd70354504b35a1e8c Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 23 Nov 2021 17:16:08 +0100 Subject: [PATCH] first step towards issue 1 added strong typing to base-datatypes and ordered bdds relates to #1 Signed-off-by: Stefan Ellmauthaler --- Cargo.lock | 133 ++++++++++++++++++++++++++++ Cargo.toml | 7 +- flake.nix | 1 + src/datatypes.rs | 114 ++++++++++++++++++++++++ src/lib.rs | 2 + src/obdd2.rs | 222 +++++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 478 insertions(+), 1 deletion(-) create mode 100644 src/datatypes.rs create mode 100644 src/obdd2.rs diff --git a/Cargo.lock b/Cargo.lock index 7bc572c..bd031c5 100644 --- a/Cargo.lock +++ b/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" diff --git a/Cargo.toml b/Cargo.toml index 507a040..d6b685b 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -11,4 +11,9 @@ description = "Solver for ADFs grounded semantics by utilising OBDDs - ordered b # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -clap = "2.33.*" \ No newline at end of file +clap = "2.33.*" +log = "0.4" + +[dev-dependencies] +env_logger = "*" +test-env-log = "0.2.*" \ No newline at end of file diff --git a/flake.nix b/flake.nix index a5658f6..4df9d51 100644 --- a/flake.nix +++ b/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 diff --git a/src/datatypes.rs b/src/datatypes.rs new file mode 100644 index 0000000..4a8eb38 --- /dev/null +++ b/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 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 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, + } + } +} diff --git a/src/lib.rs b/src/lib.rs index 3a652a8..e4c4b59 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -32,4 +32,6 @@ //! ac(d,d). //! ``` pub mod adf; +pub mod datatypes; pub mod obdd; +pub mod obdd2; diff --git a/src/obdd2.rs b/src/obdd2.rs new file mode 100644 index 0000000..67f0800 --- /dev/null +++ b/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, + cache: HashMap, +} + +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)); + } +}