BinarySDD/SddOr-related cleanup

src/builder/sdd/builder.rs

@@ -104,7 +104,7 @@ pub trait SddBuilder<'a>: BottomUpBuilder<'a, SddPtr<'a>> {
         if bdd.high().is_neg() || self.is_false(bdd.high()) || bdd.high().is_neg_var() {
             let low = bdd.low().neg();
             let high = bdd.high().neg();
-            let neg_bdd = BinarySDD::new(bdd.label(), low, high, bdd.vtree());
+            let neg_bdd = BinarySDD::new(bdd.label(), low, high, bdd.index());
 
             return self.get_or_insert_bdd(neg_bdd).neg();
         }
@@ -146,11 +146,11 @@ pub trait SddBuilder<'a>: BottomUpBuilder<'a, SddPtr<'a>> {
             SddPtr::BDD(bdd) | SddPtr::ComplBDD(bdd) => {
                 let l = self.and(r.low(), d);
                 let h = self.and(r.high(), d);
-                self.unique_bdd(BinarySDD::new(bdd.label(), l, h, bdd.vtree()))
+                self.unique_bdd(BinarySDD::new(bdd.label(), l, h, bdd.index()))
             }
             SddPtr::Reg(or) | SddPtr::Compl(or) => {
-                let mut v: Vec<SddAnd> = Vec::with_capacity(or.nodes.len());
-                for a in or.nodes.iter() {
+                let mut v: Vec<SddAnd> = Vec::with_capacity(or.iter().len());
+                for a in or.iter() {
                     let root_p = a.prime();
                     let root_s = a.sub();
                     let root_s = if r.is_neg() { root_s.neg() } else { root_s };
@@ -487,7 +487,7 @@ pub trait SddBuilder<'a>: BottomUpBuilder<'a, SddPtr<'a>> {
                 }
                 SddPtr::Reg(or) | SddPtr::Compl(or) => {
                     let mut doc: Doc<BoxDoc> = Doc::from("");
-                    for a in or.nodes.iter() {
+                    for a in or.iter() {
                         let sub = a.sub();
                         let prime = a.prime();
                         let s = if ptr.is_neg() { sub.neg() } else { sub };

src/repr/sdd.rs

@@ -179,27 +179,12 @@ impl<'a> SddPtr<'a> {
         SddNodeIter::new(*self)
     }
 
-    /// gets the total number of nodes that are a child to this SDD
-    pub fn num_child_nodes(&self) -> usize {
-        match &self {
-            PtrTrue | PtrFalse | Var(_, _) => 1,
-            BDD(or) | ComplBDD(or) => 1 + or.low().num_child_nodes() + or.high().num_child_nodes(),
-            Compl(or) | Reg(or) => {
-                1 + or
-                    .nodes
-                    .iter()
-                    .map(|n| 1 + n.prime.num_child_nodes() + n.sub.num_child_nodes())
-                    .sum::<usize>()
-            }
-        }
-    }
-
     /// retrieve the vtree index (as its index in a left-first depth-first traversal)
     ///
     /// panics if this is not a node
     pub fn vtree(&self) -> VTreeIndex {
         match self {
-            BDD(bdd) | ComplBDD(bdd) => bdd.vtree(),
+            BDD(bdd) | ComplBDD(bdd) => bdd.index(),
             Reg(or) | Compl(or) => or.index(),
             _ => panic!("called vtree() on a constant"),
         }
@@ -223,14 +208,14 @@ impl<'a> SddPtr<'a> {
             }
             Reg(or) | Compl(or) => {
                 let mut visited_sdds: HashSet<SddPtr> = HashSet::new();
-                for and in or.nodes.iter() {
+                for and in or.iter() {
                     if visited_sdds.contains(&and.sub) {
                         return false;
                     }
                     visited_sdds.insert(and.sub);
                 }
 
-                or.nodes.iter().all(|and| and.prime.is_compressed())
+                or.iter().all(|and| and.prime.is_compressed())
             }
         }
     }
@@ -253,7 +238,7 @@ impl<'a> SddPtr<'a> {
                 // and an arbitrary prime. we are looking for untrimmed decomposition pairs of the form (a, T) and (~a, F)
                 let mut visited_primes: HashSet<SddPtr> = HashSet::new();
 
-                for and in or.nodes.iter() {
+                for and in or.iter() {
                     let prime = and.prime;
 
                     // decomposition of the form (T, a)
@@ -274,7 +259,7 @@ impl<'a> SddPtr<'a> {
                     visited_primes.insert(prime.neg());
                 }
 
-                or.nodes.iter().all(|s| s.prime.is_trimmed())
+                or.iter().all(|s| s.prime.is_trimmed())
             }
         }
     }
@@ -355,16 +340,17 @@ impl<'a> DDNNFPtr<'a> for SddPtr<'a> {
     fn count_nodes(&self) -> usize {
         debug_assert!(self.is_scratch_cleared());
         fn count_h(ptr: SddPtr) -> usize {
-            if ptr.is_const() || ptr.is_var() {
-                return 0;
-            }
-            match ptr.scratch::<usize>() {
-                Some(_) => 0,
-                None => {
-                    // found a new node
+            match ptr {
+                PtrTrue | PtrFalse | Var(_, _) => 0,
+                BDD(_) | ComplBDD(_) | Reg(_) | Compl(_) if ptr.scratch::<usize>().is_some() => 0,
+                BDD(node) | ComplBDD(node) => {
+                    ptr.set_scratch::<usize>(0);
+                    1 + count_h(node.low()) + 1 + count_h(node.high())
+                }
+                Reg(or) | Compl(or) => {
                     ptr.set_scratch::<usize>(0);
                     let mut c = 0;
-                    for a in ptr.node_iter() {
+                    for a in or.iter() {
                         c += count_h(a.sub());
                         c += count_h(a.prime());
                         c += 1;

src/repr/sdd/binary_sdd.rs

@@ -18,7 +18,7 @@ use std::{
 #[derive(Debug)]
 pub struct BinarySDD<'a> {
     label: VarLabel,
-    vtree: VTreeIndex,
+    index: VTreeIndex,
     low: SddPtr<'a>,
     high: SddPtr<'a>,
 
@@ -32,21 +32,21 @@ impl<'a> BinarySDD<'a> {
         label: VarLabel,
         low: SddPtr<'a>,
         high: SddPtr<'a>,
-        vtree: VTreeIndex,
+        index: VTreeIndex,
     ) -> BinarySDD<'a> {
         BinarySDD {
             label,
             low,
             high,
-            vtree,
+            index,
             semantic_hash: RefCell::new(None),
             scratch: RefCell::new(None),
         }
     }
 
     #[inline]
-    pub fn vtree(&self) -> VTreeIndex {
-        self.vtree
+    pub fn index(&self) -> VTreeIndex {
+        self.index
     }
 
     #[inline]
@@ -124,7 +124,7 @@ impl<'a> BinarySDD<'a> {
 
 impl<'a> Hash for BinarySDD<'a> {
     fn hash<H: Hasher>(&self, state: &mut H) {
-        self.vtree.hash(state);
+        self.index.hash(state);
         self.label.hash(state);
         self.low.hash(state);
         self.high.hash(state);
@@ -133,7 +133,7 @@ impl<'a> Hash for BinarySDD<'a> {
 
 impl<'a> PartialEq for BinarySDD<'a> {
     fn eq(&self, other: &Self) -> bool {
-        self.vtree == other.vtree
+        self.index == other.index
             && self.low == other.low
             && self.high == other.high
             && self.label == other.label
@@ -154,7 +154,7 @@ impl<'a> Ord for BinarySDD<'a> {
             core::cmp::Ordering::Equal => {}
             ord => return ord,
         }
-        match self.vtree.cmp(&other.vtree) {
+        match self.index.cmp(&other.index) {
             core::cmp::Ordering::Equal => {}
             ord => return ord,
         }
@@ -174,7 +174,7 @@ impl<'a> Clone for BinarySDD<'a> {
     fn clone(&self) -> Self {
         Self {
             label: self.label,
-            vtree: self.vtree,
+            index: self.index,
             low: self.low,
             high: self.high,
             scratch: RefCell::new(None),

src/repr/sdd/sdd_or.rs

@@ -16,7 +16,7 @@ use std::{
 #[derive(Debug)]
 pub struct SddOr<'a> {
     index: VTreeIndex,
-    pub nodes: Vec<SddAnd<'a>>,
+    nodes: Vec<SddAnd<'a>>,
 
     // scratch
     scratch: RefCell<Option<Box<dyn Any>>>,
@@ -38,6 +38,10 @@ impl<'a> SddOr<'a> {
         self.index
     }
 
+    pub fn iter(&self) -> std::slice::Iter<'_, SddAnd<'_>> {
+        self.nodes.iter()
+    }
+
     pub fn semantic_hash<const P: u128>(
         &self,
         vtree: &VTreeManager,

src/repr/var_order.rs

@@ -6,7 +6,7 @@ use crate::{
     repr::{bdd::BddPtr, var_label::VarLabel},
     util,
 };
-use std::{fmt::Display, slice::Iter};
+use std::fmt::Display;
 
 #[derive(Debug, Clone)]
 pub struct VarOrder {
@@ -139,12 +139,6 @@ impl VarOrder {
         }
     }
 
-    /// Produces an iterator of var -> position, where the
-    /// result\[i\] gives the position of variable i in the order
-    pub fn order_iter(&self) -> Iter<usize> {
-        self.var_to_pos.iter()
-    }
-
     /// Iterate through the variables in the order in which they appear in the order
     pub fn in_order_iter(&self) -> impl Iterator<Item = VarLabel> + '_ {
         self.pos_to_var.iter().map(|x| VarLabel::new_usize(*x))

src/serialize/ser_sdd.rs

@@ -89,7 +89,6 @@ impl SDDSerializer {
             }
             SddPtr::Compl(or) | SddPtr::Reg(or) => {
                 let o: Vec<SDDAnd> = or
-                    .nodes
                     .iter()
                     .map(|and| {
                         let p = SDDSerializer::serialize_helper(and.prime(), table, nodes);