refac: store only decision nodes in unique_table

Also renamed `SddOr` to `Decision` and `SddAnd` to `Element` to better
match papers' terminology.

src/literal.rs

@@ -1,4 +1,4 @@
-#[derive(Hash, Eq, PartialEq, Debug, Copy, Clone)]
+#[derive(Hash, Eq, PartialEq, Debug, Copy, Clone, PartialOrd, Ord)]
 pub struct VarLabel(u64);
 
 impl VarLabel {
@@ -27,7 +27,7 @@ impl Default for VarLabelManager {
 }
 
 // Either true or false
-#[derive(Hash, Eq, PartialEq, Debug, Clone, Copy)]
+#[derive(Hash, Eq, PartialEq, Debug, Clone, Copy, PartialOrd, Ord)]
 pub struct Literal {
     var_label: VarLabel,
     polarity: bool,
@@ -43,10 +43,10 @@ impl Literal {
     }
 
     #[must_use]
-    pub fn negate(literal: &Literal) -> Literal {
+    pub fn negate(&self) -> Literal {
         Literal {
-            var_label: VarLabel::new(literal.var_label.0),
-            polarity: !literal.polarity,
+            var_label: VarLabel::new(self.var_label.0),
+            polarity: !self.polarity,
         }
     }
 

src/manager.rs

@@ -3,7 +3,6 @@ use std::collections::HashMap;
 use crate::literal::VarLabelManager;
 use crate::options::SddOptions;
 use crate::sdd::Node;
-use crate::sdd::Sdd;
 use crate::vtree::VTreeManager;
 
 #[allow(clippy::module_name_repetitions)]
@@ -21,6 +20,8 @@ pub struct SddManager {
     // Unique table holding all the decision nodes.
     // More details can be found in [Algorithms and Data Structures in VLSI Design](https://link.springer.com/book/10.1007/978-3-642-58940-9).
     unqiue_table: HashMap<u64, Node>,
+    // u64 is the hash of sdd::Decision
+    // TODO: Should we store sdd::Decision or sdd::Node?
 }
 
 impl SddManager {
@@ -49,11 +50,11 @@ impl SddManager {
         self.unqiue_table.get(id)
     }
 
-    pub fn conjoin(&self, _fst: &Sdd, _snd: &Sdd) {}
-    pub fn disjoin(&self, _fst: &Sdd, _snd: &Sdd) {}
-    pub fn negate(&self, _fst: &Sdd) {}
-    pub fn imply(&self, _fst: &Sdd, _snd: &Sdd) {}
-    pub fn equiv(&self, _fst: &Sdd, _snd: &Sdd) {}
+    pub fn conjoin(&self, _fst: &Node, _snd: &Node) {}
+    pub fn disjoin(&self, _fst: &Node, _snd: &Node) {}
+    pub fn negate(&self, _fst: &Node) {}
+    pub fn imply(&self, _fst: &Node, _snd: &Node) {}
+    pub fn equiv(&self, _fst: &Node, _snd: &Node) {}
 
     pub fn condition() {}
     pub fn exist() {}

src/sdd.rs

@@ -8,128 +8,109 @@ use crate::manager::SddManager;
 #[path = "./sdd_test.rs"]
 mod sdd_test;
 
-type NodeIndex = u64;
-
-#[derive(PartialEq, Eq, Clone, Hash)]
+#[derive(PartialEq, Eq, Clone)]
 pub struct Node {
-    sdd: Sdd,
-
-    // Index of the parent node in the SDDManager.nodes vector.
-    parent: Option<NodeIndex>,
-    index: NodeIndex, // index == sdd::hash
+    decision: Decision,
+
+    parents: u64,
+    refs: u64,
+    // TODO: Do we want field `parents: BTreeSet<u64>`? What would this point to? Since only the
+    // decision nodes will be stored in the unique_table, then it would have to point to decision
+    // node, not to the particular element pointing to it (since it is not hashed and stored
+    // directly in the unique_table).
 }
 
 impl Node {
     #[must_use]
-    pub fn new(sdd: Sdd, parent: Option<NodeIndex>, index: NodeIndex) -> Node {
-        Node { sdd, parent, index }
+    pub fn new(decision: Decision) -> Node {
+        Node {
+            decision,
+            parents: 0,
+            refs: 0,
+        }
     }
 }
 
 #[derive(PartialEq, Eq, Clone, Hash)]
-// TODO: Implement custom hashing scheme.
-pub enum Sdd {
-    False,
-    True,
-
-    Literal(Literal),
-
-    Decision(SddOr),      // Decision node represents decomposition
-    DecisionCompl(SddOr), // Complemented node
-
-    Element(SddAnd),
-    ElementCompl(SddAnd),
+pub struct Decision {
+    elements: BTreeSet<Element>,
 }
 
-impl Sdd {
-    fn is_true(&self) -> bool {
-        matches!(self, Sdd::True)
-    }
+// Element node (a paired box) is a conjunction of prime and sub.
+#[derive(PartialEq, Eq, Clone, Hash, Copy, PartialOrd, Ord)]
+pub struct Element {
+    prime: Box,
+    sub: Box,
+}
 
-    fn is_false(&self) -> bool {
-        matches!(self, Sdd::False)
+impl Element {
+    fn is_trimmed(&self, manager: &SddManager) -> bool {
+        self.prime.is_trimmed(manager) && self.sub.is_trimmed(manager)
     }
 
-    fn is_constant(&self) -> bool {
-        self.is_true() || self.is_false()
+    fn is_compressed(&self, manager: &SddManager) -> bool {
+        self.prime.is_compressed(manager) && self.sub.is_compressed(manager)
     }
+}
 
-    #[allow(dead_code)]
-    fn is_literal(&self) -> bool {
-        matches!(self, Sdd::Literal(_))
-    }
+type NodeIndex = u64;
 
-    #[allow(dead_code)]
-    fn is_decision_node(&self) -> bool {
-        matches!(self, Sdd::Decision(_)) || matches!(self, Sdd::DecisionCompl(_))
-    }
+#[derive(PartialEq, Eq, Clone, Hash, Copy, PartialOrd, Ord)]
+pub enum Box {
+    True,
+    False,
+    Literal(Literal),
+    DecisionRegular(NodeIndex),
+    DecisionComplement(NodeIndex),
+}
 
-    #[allow(dead_code)]
-    fn is_element_node(&self) -> bool {
-        matches!(self, Sdd::Element(_)) || matches!(self, Sdd::ElementCompl(_))
+impl Box {
+    fn is_true(&self) -> bool {
+        matches!(self, Box::True)
     }
 
-    fn as_element(&self) -> &SddAnd {
-        match self {
-            Sdd::Element(elem) | Sdd::ElementCompl(elem) => elem,
-            _ => panic!("Cannot cast to element!"),
-        }
+    fn is_false(&self) -> bool {
+        matches!(self, Box::False)
     }
 
-    #[allow(dead_code)]
-    fn as_decision(&self) -> &SddOr {
-        match self {
-            Sdd::Decision(decision) | Sdd::DecisionCompl(decision) => decision,
-            _ => panic!("Cannot cast to decision!"),
-        }
+    fn is_constant(&self) -> bool {
+        self.is_true() || self.is_false()
     }
 
-    #[must_use]
-    pub fn negate(&self) -> Sdd {
+    fn negate(&self) -> Box {
         match self {
-            Sdd::True => Sdd::False,
-            Sdd::False => Sdd::True,
-            Sdd::Literal(literal) => Sdd::Literal(Literal::negate(literal)),
-            Sdd::Decision(sdd) => Sdd::DecisionCompl(sdd.to_owned()),
-            Sdd::DecisionCompl(sdd) => Sdd::Decision(sdd.to_owned()),
-            Sdd::Element(sdd) => Sdd::ElementCompl(sdd.to_owned()),
-            Sdd::ElementCompl(sdd) => Sdd::Element(sdd.to_owned()),
+            Box::True => Box::False,
+            Box::False => Box::True,
+            Box::Literal(literal) => Box::Literal(literal.negate()),
+            Box::DecisionRegular(decision) => Box::DecisionComplement(decision.to_owned()),
+            Box::DecisionComplement(decision) => Box::DecisionRegular(decision.to_owned()),
         }
     }
 
-    #[must_use]
-    pub fn is_trimmed(&self, manager: &SddManager) -> bool {
+    fn is_trimmed(&self, manager: &SddManager) -> bool {
         match self {
-            Sdd::True | Sdd::False | Sdd::Literal(_) => true,
-            Sdd::Decision(sdd) | Sdd::DecisionCompl(sdd) => sdd.is_trimmed(manager),
-            Sdd::Element(sdd) | Sdd::ElementCompl(sdd) => {
-                let (prime, sub) = sdd.get_prime_sub(manager);
-                prime.sdd.is_trimmed(manager) && sub.sdd.is_trimmed(manager)
-            }
+            Box::True | Box::False | Box::Literal(_) => true,
+            Box::DecisionRegular(decision_idx) | Box::DecisionComplement(decision_idx) => manager
+                .get_node(decision_idx)
+                .unwrap()
+                .decision
+                .is_trimmed(manager),
         }
     }
 
-    #[must_use]
-    pub fn is_compressed(&self, manager: &SddManager) -> bool {
+    fn is_compressed(&self, manager: &SddManager) -> bool {
         match self {
-            Sdd::True | Sdd::False | Sdd::Literal(_) => true,
-            Sdd::Decision(sdd) | Sdd::DecisionCompl(sdd) => sdd.is_compressed(manager),
-            Sdd::Element(sdd) | Sdd::ElementCompl(sdd) => {
-                let (prime, sub) = sdd.get_prime_sub(manager);
-                prime.sdd.is_compressed(manager) && sub.sdd.is_compressed(manager)
-            }
+            Box::True | Box::False | Box::Literal(_) => true,
+            Box::DecisionRegular(decision_idx) | Box::DecisionComplement(decision_idx) => manager
+                .get_node(decision_idx)
+                .unwrap()
+                .decision
+                .is_compressed(manager),
         }
     }
 }
 
-// Decision node, disjunction of its elements
-#[derive(Hash, PartialEq, Eq, Clone)]
-#[allow(clippy::module_name_repetitions)]
-pub struct SddOr {
-    elements: BTreeSet<NodeIndex>,
-}
-
-impl SddOr {
+impl Decision {
     /// Recursivelly checks whether the decision node is trimmed.
     /// Decision node is `trimmed` if it does not contain decompositions of the form `{(True, A)}` or
     /// `{(A, True), (!A, False)}`.
@@ -142,40 +123,34 @@ impl SddOr {
     /// * the decision node contains something else than boxed elements.
     #[must_use]
     pub fn is_trimmed(&self, manager: &SddManager) -> bool {
-        let mut primes: HashSet<Sdd> = HashSet::new();
+        let mut primes: HashSet<Box> = HashSet::new();
 
         if self.elements.len() >= 3 {
             return true;
         }
 
-        for element_idx in &self.elements {
-            let element = manager.get_node(element_idx).unwrap().sdd.as_element();
-            let (prime, sub) = element.get_prime_sub(manager);
-
+        for element in &self.elements {
             // Check for `{(true, A)}`.
-            if prime.sdd.is_true() {
+            if element.prime.is_true() {
                 return false;
             }
-            // Note: Why don't we have to check for symmetric cases `{(A, True)}` and `{(True, A), (False, !A)}` etc.?
 
             // Check for elements `(A, True)` and `(!A, False)`. We can continue with the next iteration
             // if the sub is not True or False.
-            if !sub.sdd.is_constant() {
+            if !element.sub.is_constant() {
                 continue;
             }
 
             // Check whether we have already seen this literal but negated.
-            if primes.contains(&prime.sdd) {
+            if primes.contains(&element.prime) {
                 return false;
             }
 
-            primes.insert(prime.sdd.negate());
+            primes.insert(element.prime.negate());
         }
 
         // Check that elements are also trimmed.
-        self.elements
-            .iter()
-            .all(|el| manager.get_node(el).unwrap().sdd.is_trimmed(manager))
+        self.elements.iter().all(|el| el.is_trimmed(manager))
     }
 
     /// Recursivelly checks whether the decision node is compressed.
@@ -190,22 +165,17 @@ impl SddOr {
     /// * the decision node contains something else than boxed elements.
     #[must_use]
     pub fn is_compressed(&self, manager: &SddManager) -> bool {
-        let mut subs: HashSet<Sdd> = HashSet::new();
-        for element_idx in &self.elements {
-            let element = manager.get_node(element_idx).unwrap().sdd.as_element();
-            let sub = element.get_sub(manager);
-
-            if subs.contains(&sub.sdd) {
+        let mut subs: HashSet<Box> = HashSet::new();
+        for element in &self.elements {
+            if subs.contains(&element.sub) {
                 return false;
             }
 
-            subs.insert(sub.sdd);
+            subs.insert(element.sub);
         }
 
         // Check that all elements are also compressed.
-        self.elements
-            .iter()
-            .all(|el| manager.get_node(el).unwrap().sdd.is_compressed(manager))
+        self.elements.iter().all(|el| el.is_compressed(manager))
     }
 
     /// Recursivelly trims and compresses SDD.
@@ -217,34 +187,3 @@ impl SddOr {
         todo!("Implement me!")
     }
 }
-
-// Element node (a paired box) is a conjunction of prime and sub.
-#[allow(clippy::module_name_repetitions)]
-#[derive(Hash, PartialEq, Eq, Copy, Clone)]
-pub struct SddAnd {
-    prime: NodeIndex,
-    sub: NodeIndex,
-}
-
-impl SddAnd {
-    #[must_use]
-    pub fn get_prime_sub(&self, manager: &SddManager) -> (Node, Node) {
-        (self.get_prime(manager), self.get_sub(manager))
-    }
-
-    /// # Panics
-    /// Panics if the prime is not in the SDD Manager, which should not happen
-    /// under any circumstances.
-    #[must_use]
-    pub fn get_prime(&self, manager: &SddManager) -> Node {
-        manager.get_node(&self.prime).unwrap().clone()
-    }
-
-    /// # Panics
-    /// Panics if the sub is not in the SDD Manager, which should not happen
-    /// under any circumstances.
-    #[must_use]
-    pub fn get_sub(&self, manager: &SddManager) -> Node {
-        manager.get_node(&self.sub).unwrap().clone()
-    }
-}