typed obdd, adf still using usizes

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

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
+            self.stmts.push(Statement::new(
-                .push(Statement::new(statement, self.bdd.variable(pos)));
+                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] {
+                match Term(curint[pos]) {
-                    super::obdd::BDD_BOT => {
+                    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<usize>) -> Vec<usize> {
         let mut new_interpretation = interpretation.clone();
         for (pos, it) in interpretation.iter().enumerate() {
-            match *it {
+            match Term(*it) {
-                super::obdd::BDD_BOT => {
+                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<usize> = 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 lterm: Term = self.parse_formula(left).into();
-                    let rterm = self.parse_formula(right);
+                    let rterm: Term = self.parse_formula(right).into();
-                    return self.bdd.and(lterm, rterm);
+                    return self.bdd.and(lterm, rterm).value();
                 }
                 "iff(" => {
                     let (left, right) = Adf::findpairs(&ac[4..]);
-                    let lterm = self.parse_formula(left);
+                    let lterm: Term = self.parse_formula(left).into();
-                    let rterm = self.parse_formula(right);
+                    let rterm: Term = self.parse_formula(right).into();
-                    let notlt = self.bdd.not(lterm);
+                    return self.bdd.iff(lterm, rterm).value();
-                    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);
                 }
                 "xor(" => {
                     let (left, right) = Adf::findpairs(&ac[4..]);
-                    let lterm = self.parse_formula(left);
+                    let lterm: Term = self.parse_formula(left).into();
-                    let rterm = self.parse_formula(right);
+                    let rterm: Term = self.parse_formula(right).into();
-                    let notlt = self.bdd.not(lterm);
+                    return self.bdd.xor(lterm, rterm).value();
-                    let notrt = self.bdd.not(rterm);
+                }
-                    let con1 = self.bdd.and(notlt, rterm);
+                "imp(" => {
-                    let con2 = self.bdd.and(lterm, notrt);
+                    let (left, right) = Adf::findpairs(&ac[4..]);
-                    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.imp(lterm, rterm).value();
                 }
                 "neg(" => {
                     let pos = Adf::findterm(&ac[4..]).unwrap() + 4;
-                    let term = self.parse_formula(&ac[4..pos]);
+                    let term: Term = self.parse_formula(&ac[4..pos]).into();
-                    return self.bdd.not(term);
+                    return self.bdd.not(term).value();
                 }
-                "c(f)" => return self.bdd.constant(false),
+                "c(f)" => return Bdd::constant(false).value(),
-                "c(v)" => return self.bdd.constant(true),
+                "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 lterm: Term = self.parse_formula(left).into();
-                    let rterm = self.parse_formula(right);
+                    let rterm: Term = self.parse_formula(right).into();
-                    return self.bdd.or(lterm, rterm);
+                    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))");

src/lib.rs

@@ -34,4 +34,4 @@
 pub mod adf;
 pub mod datatypes;
 pub mod obdd;
-pub mod obdd2;
+//pub mod obdd2;

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;

src/obdd.rs

@@ -1,127 +1,104 @@
-use std::usize;
+use crate::datatypes::*;
-
+use std::{cmp::min, collections::HashMap, fmt::Display};
-/// 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
-    }
-}
 
+#[derive(Debug)]
 pub(crate) struct Bdd {
     pub(crate) nodes: Vec<BddNode>,
-    hash: HashMap<BddNode, Term>,
+    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 {
-        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],
+            nodes: vec![BddNode::bot_node(), BddNode::top_node()],
-            hash: HashMap::new(),
+            cache: HashMap::new(),
         }
     }
 
-    fn create_node(&mut self, var: usize, lo: Term, hi: Term) -> Term {
+    pub fn variable(&mut self, var: Var) -> Term {
-        if lo == hi {
+        self.node(var, Term::BOT, Term::TOP)
-            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: usize) -> Term {
+    pub fn constant(val: bool) -> Term {
-        self.create_node(var, BDD_BOT, BDD_TOP)
-    }
-
-    pub fn constant(&self, 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 {
+    pub fn not(&mut self, term: Term) -> Term {
-        let treenode = self.nodes[subtree];
+        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
+        // Readability of algorithm > code-elegance
-        if treenode.var > var || treenode.var == usize::MAX {
+        if node.var() > var || node.var() >= Var::BOT {
-            subtree
+            tree
-        } else if treenode.var < var {
+        } else if node.var() < var {
-            let lonode = self.restrict(treenode.lo, var, val);
+            let lonode = self.restrict(node.lo(), var, val);
-            let hinode = self.restrict(treenode.hi, var, val);
+            let hinode = self.restrict(node.hi(), var, val);
-            self.create_node(treenode.var, lonode, hinode)
+            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 minvar = Var(min(
-            let tvar = self.nodes[t].var;
+                self.nodes[i.value()].var().value(),
-            let evar = self.nodes[e].var;
+                min(
-
+                    self.nodes[t.value()].var().value(),
-            let minvar = std::cmp::min(ivar, std::cmp::min(tvar, evar));
+                    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 top_ite = self.if_then_else(itop, ttop, etop);
-            let botite = self.if_then_else(ibot, tbot, ebot);
+            let bot_ite = self.if_then_else(ibot, tbot, ebot);
-            self.create_node(minvar, botite, topite)
+            self.node(minvar, bot_ite, top_ite)
         }
     }
-
+    fn node(&mut self, var: Var, lo: Term, hi: Term) -> Term {
-    pub fn not(&mut self, term: Term) -> Term {
+        if lo == hi {
-        self.if_then_else(term, BDD_BOT, BDD_TOP)
+            lo
-    }
+        } else {
-
+            let node = BddNode::new(var, lo, hi);
-    pub fn and(&mut self, terma: Term, termb: Term) -> Term {
+            match self.cache.get(&node) {
-        self.if_then_else(terma, termb, BDD_BOT)
+                Some(t) => *t,
-    }
+                None => {
-
+                    let new_term = Term(self.nodes.len());
-    pub fn or(&mut self, terma: Term, termb: Term) -> Term {
+                    self.nodes.push(node);
-        self.if_then_else(terma, BDD_TOP, termb)
+                    self.cache.insert(node, new_term);
-    }
+                    new_term
-
+                }
-    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);
         }
     }
 }
@@ -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(Var(0)), Term(2));
-        assert_eq!(bdd.variable(1), 3);
+        assert_eq!(bdd.variable(Var(1)), Term(3));
-        assert_eq!(bdd.variable(0), 2);
+        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);
+        let v1 = bdd.variable(Var(0));
-        assert_eq!(v1, 2);
+        assert_eq!(v1, 2.into());
-        assert_eq!(bdd.not(v1), 3);
+        assert_eq!(bdd.not(v1), Term(3));
     }
 
     #[test]
     fn use_add() {
         let mut bdd = Bdd::new();
-        let v1 = bdd.variable(0);
+        let v1 = bdd.variable(Var(0));
-        let v2 = bdd.variable(1);
+        let v2 = bdd.variable(Var(1));
-        let v3 = bdd.variable(2);
+        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 v1 = bdd.variable(Var(0));
-        let v2 = bdd.variable(1);
+        let v2 = bdd.variable(Var(1));
-        let v3 = bdd.variable(2);
+        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 v1 = bdd.variable(Var(0));
-        let v2 = bdd.variable(1);
+        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, Var(0), false), Term::BOT);
-        assert_eq!(bdd.restrict(conj, 0, true), v2);
+        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);
+        let x = bdd.restrict(end, Var(1), false);
-        assert_eq!(x, 2);
+        assert_eq!(x, Term(2));
     }
 }

src/obdd2.rs

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