diff --git a/src/adf.rs b/src/adf.rs index f58ca69..810b835 100644 --- a/src/adf.rs +++ b/src/adf.rs @@ -14,7 +14,9 @@ use std::{ usize, }; -use super::obdd::Bdd; +use crate::datatypes::{Term, Var}; + +use crate::obdd::Bdd; struct Statement { label: String, // label of the statement @@ -68,8 +70,10 @@ impl Adf { //self.bdd.variable(pos); //self.stmts // .push(Statement::new(statement, pos.clone())); - self.stmts - .push(Statement::new(statement, self.bdd.variable(pos))); + self.stmts.push(Statement::new( + statement, + self.bdd.variable(Var(pos)).value(), + )); self.dict.insert(self.stmts[pos].label.to_string(), pos); } } @@ -120,21 +124,21 @@ impl Adf { change = false; for pos in 0..self.stmts.len() - 1 { let curint = interpretation.clone(); - match curint[pos] { - super::obdd::BDD_BOT => { + match Term(curint[pos]) { + Term::BOT => { if let Some(n) = self.setvarvalue( curint, - self.bdd.nodes[self.stmts[pos].var].var(), + self.bdd.nodes[self.stmts[pos].var].var().value(), false, ) { interpretation.clone_from(&n); change = true; } } - super::obdd::BDD_TOP => { + Term::TOP => { if let Some(n) = self.setvarvalue( curint, - self.bdd.nodes[self.stmts[pos].var].var(), + self.bdd.nodes[self.stmts[pos].var].var().value(), true, ) { interpretation.clone_from(&n); @@ -224,20 +228,20 @@ impl Adf { fn apply_interpretation(&mut self, interpretation: &Vec) -> Vec { let mut new_interpretation = interpretation.clone(); for (pos, it) in interpretation.iter().enumerate() { - match *it { - super::obdd::BDD_BOT => { + match Term(*it) { + Term::BOT => { if let Some(n) = self.setvarvalue( new_interpretation.clone(), - self.bdd.nodes[self.stmts[pos].var].var(), + self.bdd.nodes[self.stmts[pos].var].var().value(), false, ) { new_interpretation.clone_from(&n); } } - super::obdd::BDD_TOP => { + Term::TOP => { if let Some(n) = self.setvarvalue( new_interpretation.clone(), - self.bdd.nodes[self.stmts[pos].var].var(), + self.bdd.nodes[self.stmts[pos].var].var().value(), true, ) { new_interpretation.clone_from(&n); @@ -273,7 +277,10 @@ impl Adf { let mut interpretation2: Vec = vec![0; interpretation.len()]; let mut change: bool = false; for (pos, _it) in interpretation.iter().enumerate() { - interpretation2[pos] = self.bdd.restrict(interpretation[pos], var, val); + interpretation2[pos] = self + .bdd + .restrict(Term(interpretation[pos]), Var(var), val) + .value(); if interpretation[pos] != interpretation2[pos] { change = true } @@ -290,48 +297,46 @@ impl Adf { match &ac[..4] { "and(" => { let (left, right) = Adf::findpairs(&ac[4..]); - let lterm = self.parse_formula(left); - let rterm = self.parse_formula(right); - return self.bdd.and(lterm, rterm); + let lterm: Term = self.parse_formula(left).into(); + let rterm: Term = self.parse_formula(right).into(); + return self.bdd.and(lterm, rterm).value(); } "iff(" => { let (left, right) = Adf::findpairs(&ac[4..]); - let lterm = self.parse_formula(left); - let rterm = self.parse_formula(right); - let notlt = self.bdd.not(lterm); - let notrt = self.bdd.not(rterm); - let con1 = self.bdd.and(lterm, rterm); - let con2 = self.bdd.and(notlt, notrt); - return self.bdd.or(con1, con2); + let lterm: Term = self.parse_formula(left).into(); + let rterm: Term = self.parse_formula(right).into(); + return self.bdd.iff(lterm, rterm).value(); } "xor(" => { let (left, right) = Adf::findpairs(&ac[4..]); - let lterm = self.parse_formula(left); - let rterm = self.parse_formula(right); - let notlt = self.bdd.not(lterm); - let notrt = self.bdd.not(rterm); - let con1 = self.bdd.and(notlt, rterm); - let con2 = self.bdd.and(lterm, notrt); - return self.bdd.or(con1, con2); + let lterm: Term = self.parse_formula(left).into(); + let rterm: Term = self.parse_formula(right).into(); + return self.bdd.xor(lterm, rterm).value(); + } + "imp(" => { + let (left, right) = Adf::findpairs(&ac[4..]); + let lterm: Term = self.parse_formula(left).into(); + let rterm: Term = self.parse_formula(right).into(); + return self.bdd.imp(lterm, rterm).value(); } "neg(" => { let pos = Adf::findterm(&ac[4..]).unwrap() + 4; - let term = self.parse_formula(&ac[4..pos]); - return self.bdd.not(term); + let term: Term = self.parse_formula(&ac[4..pos]).into(); + return self.bdd.not(term).value(); } - "c(f)" => return self.bdd.constant(false), - "c(v)" => return self.bdd.constant(true), + "c(f)" => return Bdd::constant(false).value(), + "c(v)" => return Bdd::constant(true).value(), _ if &ac[..3] == "or(" => { let (left, right) = Adf::findpairs(&ac[3..]); - let lterm = self.parse_formula(left); - let rterm = self.parse_formula(right); - return self.bdd.or(lterm, rterm); + let lterm: Term = self.parse_formula(left).into(); + let rterm: Term = self.parse_formula(right).into(); + return self.bdd.or(lterm, rterm).value(); } _ => (), } } match self.dict.get(ac) { - Some(it) => self.bdd.variable(*it), + Some(it) => self.bdd.variable(Var(*it)).value(), _ => { println!("{}", ac); unreachable!() @@ -426,7 +431,7 @@ mod test { adf.add_statement("c"); assert_eq!(adf.parse_formula("and(a,or(b,c))"), 6); - assert_eq!(adf.parse_formula("xor(a,b)"), 11); + assert_eq!(adf.parse_formula("xor(a,b)"), 8); assert_eq!(adf.parse_formula("or(c(f),b)"), 3); // is b adf.parse_formula("and(or(c(f),a),and(b,c))"); diff --git a/src/lib.rs b/src/lib.rs index e4c4b59..e309ce6 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -34,4 +34,4 @@ pub mod adf; pub mod datatypes; pub mod obdd; -pub mod obdd2; +//pub mod obdd2; diff --git a/src/main.rs b/src/main.rs index 97cbf29..b9dd763 100644 --- a/src/main.rs +++ b/src/main.rs @@ -5,6 +5,7 @@ use std::time::Instant; use std::usize; pub mod adf; +pub mod datatypes; pub mod obdd; use adf::Adf; diff --git a/src/obdd.rs b/src/obdd.rs index 70a4b31..016444e 100644 --- a/src/obdd.rs +++ b/src/obdd.rs @@ -1,127 +1,104 @@ -use std::usize; - -/// constant which represents the bottom concept (i.e. inconsistency) -pub const BDD_BOT: usize = 0; -/// constant which represents the top concept (i.e. universal truth) -pub const BDD_TOP: usize = 1; - -use std::collections::HashMap; - -/// Convenience type substition -type Term = usize; - -/// Represents a node in the BDD -/// -/// -#[derive(Eq, PartialEq, Hash, Clone, Copy)] -pub(crate) struct BddNode { - var: usize, - lo: Term, - hi: Term, -} - -impl std::fmt::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 var(self) -> usize { - self.var - } -} +use crate::datatypes::*; +use std::{cmp::min, collections::HashMap, fmt::Display}; +#[derive(Debug)] pub(crate) struct Bdd { pub(crate) nodes: Vec, - hash: HashMap, + 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 { - let botnode = BddNode { - var: usize::MAX, - lo: BDD_BOT, - hi: BDD_BOT, - }; - let topnode = BddNode { - var: usize::MAX, - lo: BDD_TOP, - hi: BDD_TOP, - }; Self { - nodes: vec![botnode, topnode], - hash: HashMap::new(), + nodes: vec![BddNode::bot_node(), BddNode::top_node()], + cache: HashMap::new(), } } - fn create_node(&mut self, var: usize, lo: Term, hi: Term) -> Term { - if lo == hi { - lo - } else { - let node = BddNode { var, lo, hi }; - match self.hash.get(&node) { - Some(n) => *n, - None => { - let newid = self.nodes.len(); - if newid == usize::MAX { - panic!("Maximal amount of elements in node-table reached!") - } - self.nodes.push(node); - self.hash.insert(node, newid); - newid - } - } - } + pub fn variable(&mut self, var: Var) -> Term { + self.node(var, Term::BOT, Term::TOP) } - pub fn variable(&mut self, var: usize) -> Term { - self.create_node(var, BDD_BOT, BDD_TOP) - } - - pub fn constant(&self, val: bool) -> Term { + pub fn constant(val: bool) -> Term { if val { - BDD_TOP + Term::TOP } else { - BDD_BOT + Term::BOT } } - pub fn restrict(&mut self, subtree: Term, var: usize, val: bool) -> Term { - let treenode = self.nodes[subtree]; + 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]; #[allow(clippy::collapsible_else_if)] - // Better readabilty of the if/then/else structure of the algorithm - if treenode.var > var || treenode.var == usize::MAX { - subtree - } else if treenode.var < var { - let lonode = self.restrict(treenode.lo, var, val); - let hinode = self.restrict(treenode.hi, var, val); - self.create_node(treenode.var, lonode, hinode) + // Readability of algorithm > code-elegance + 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(treenode.hi, var, val) + self.restrict(node.hi(), var, val) } else { - self.restrict(treenode.lo, var, val) + self.restrict(node.lo(), var, val) } } } fn if_then_else(&mut self, i: Term, t: Term, e: Term) -> Term { - if i == BDD_TOP { + if i == Term::TOP { t - } else if i == BDD_BOT { + } else if i == Term::BOT { e } else if t == e { t - } else if t == BDD_TOP && e == BDD_BOT { + } else if t == Term::TOP && e == Term::BOT { i } else { - let ivar = self.nodes[i].var; - let tvar = self.nodes[t].var; - let evar = self.nodes[e].var; - - let minvar = std::cmp::min(ivar, std::cmp::min(tvar, evar)); - + 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); @@ -129,31 +106,25 @@ impl Bdd { let tbot = self.restrict(t, minvar, false); let ebot = self.restrict(e, minvar, false); - let topite = self.if_then_else(itop, ttop, etop); - let botite = self.if_then_else(ibot, tbot, ebot); - self.create_node(minvar, botite, topite) + 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) } } - - pub fn not(&mut self, term: Term) -> Term { - self.if_then_else(term, BDD_BOT, BDD_TOP) - } - - pub fn and(&mut self, terma: Term, termb: Term) -> Term { - self.if_then_else(terma, termb, BDD_BOT) - } - - pub fn or(&mut self, terma: Term, termb: Term) -> Term { - self.if_then_else(terma, BDD_TOP, termb) - } - - fn _printtree(&self, tree: Term) { - let node = self.nodes[tree]; - println!("Index: {}, Node: {}", tree, node); - - if tree > BDD_TOP { - self._printtree(node.lo); - self._printtree(node.hi); + 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 + } + } } } } @@ -171,72 +142,75 @@ mod test { #[test] fn addconst() { let bdd = Bdd::new(); - assert_eq!(bdd.constant(true), BDD_TOP); - assert_eq!(bdd.constant(false), BDD_BOT); + + 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(0), 2); - assert_eq!(bdd.variable(1), 3); - assert_eq!(bdd.variable(0), 2); + 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(0); - assert_eq!(v1, 2); - assert_eq!(bdd.not(v1), 3); + 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(0); - let v2 = bdd.variable(1); - let v3 = bdd.variable(2); + 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, 7); + assert_eq!(a2, Term(7)); } #[test] fn use_or() { let mut bdd = Bdd::new(); - let v1 = bdd.variable(0); - let v2 = bdd.variable(1); - let v3 = bdd.variable(2); + 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, 7); + assert_eq!(a2, Term(7)); } #[test] fn produce_different_conversions() { let mut bdd = Bdd::new(); - let v1 = bdd.variable(0); - let v2 = bdd.variable(1); + 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, BDD_TOP); + assert_eq!(ft, Term::TOP); - let v3 = bdd.variable(2); + let v3 = bdd.variable(Var(2)); let nv3 = bdd.not(v3); - assert_eq!(bdd.and(v3, nv3), BDD_BOT); + assert_eq!(bdd.and(v3, nv3), Term::BOT); let conj = bdd.and(v1, v2); - assert_eq!(bdd.restrict(conj, 0, false), BDD_BOT); - assert_eq!(bdd.restrict(conj, 0, true), 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); @@ -244,7 +218,7 @@ mod test { let con1 = bdd.and(a, conj); let end = bdd.or(con1, b); - let x = bdd.restrict(end, 1, false); - assert_eq!(x, 2); + let x = bdd.restrict(end, Var(1), false); + assert_eq!(x, Term(2)); } } diff --git a/src/obdd2.rs b/src/obdd2.rs deleted file mode 100644 index 67f0800..0000000 --- a/src/obdd2.rs +++ /dev/null @@ -1,222 +0,0 @@ -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)); - } -}