From a27cf0d3120906d1f85d9eb475ad1eae91e80594 Mon Sep 17 00:00:00 2001
From: Matt Wang <matt@matthewwang.me>
Date: Thu, 3 Aug 2023 14:22:22 -0400
Subject: [PATCH] Moves `compose()` to `BottomUpBuilder` (from `Bdd` and `Sdd`
 builders) (#168)

Cherry-picking this change over from #163, to make it easier to review (and to revert this if necessary).
---
 src/backing_store/bump_table.rs |  2 +-
 src/builder/bdd/builder.rs      | 11 -----------
 src/builder/mod.rs              | 10 +++++++++-
 src/builder/sdd/builder.rs      | 10 ----------
 4 files changed, 10 insertions(+), 23 deletions(-)

diff --git a/src/backing_store/bump_table.rs b/src/backing_store/bump_table.rs
index 6fa6b5ef..3be04d01 100644
--- a/src/backing_store/bump_table.rs
+++ b/src/backing_store/bump_table.rs
@@ -168,7 +168,7 @@ impl<'a, T: Eq + Hash + Clone> UniqueTable<'a, T> for BackedRobinhoodTable<'a, T
 }
 
 impl<'a, T: Eq + Hash + Clone> BackedRobinhoodTable<'a, T> {
-    /// use a hash to both allocate space in table, *and* form equalitySS
+    /// use a hash to both allocate space in table, *and* form equality
     pub fn get_or_insert_by_hash(
         &'a mut self,
         hash: u64,
diff --git a/src/builder/bdd/builder.rs b/src/builder/bdd/builder.rs
index cee00c92..96cd1bc4 100644
--- a/src/builder/bdd/builder.rs
+++ b/src/builder/bdd/builder.rs
@@ -175,17 +175,6 @@ where
         r
     }
 
-    /// Compose `g` into `f` by substituting for `lbl`
-    fn compose(&'a self, f: BddPtr<'a>, lbl: VarLabel, g: BddPtr<'a>) -> BddPtr<'a> {
-        // TODO this can be optimized with a specialized implementation to make
-        // it a single traversal
-        let var = self.var(lbl, true);
-        let iff = self.iff(var, g);
-        let a = self.and(iff, f);
-
-        self.exists(a, lbl)
-    }
-
     /// Compile a BDD from a CNF
     fn compile_cnf(&'a self, cnf: &Cnf) -> BddPtr<'a> {
         let mut cvec: Vec<BddPtr> = Vec::with_capacity(cnf.clauses().len());
diff --git a/src/builder/mod.rs b/src/builder/mod.rs
index 8706c9f4..8d3a8120 100644
--- a/src/builder/mod.rs
+++ b/src/builder/mod.rs
@@ -50,7 +50,15 @@ pub trait BottomUpBuilder<'a, Ptr> {
 
     /// compose g into f for variable v
     /// I.e., computes the logical function (exists v. (g <=> v) /\ f).
-    fn compose(&'a self, f: Ptr, lbl: VarLabel, g: Ptr) -> Ptr;
+    fn compose(&'a self, f: Ptr, lbl: VarLabel, g: Ptr) -> Ptr {
+        // TODO this can be optimized with a specialized implementation to make
+        // it a single traversal
+        let var = self.var(lbl, true);
+        let iff = self.iff(var, g);
+        let a = self.and(iff, f);
+
+        self.exists(a, lbl)
+    }
 
     // compilation
 
diff --git a/src/builder/sdd/builder.rs b/src/builder/sdd/builder.rs
index e39f700d..b0a040fc 100644
--- a/src/builder/sdd/builder.rs
+++ b/src/builder/sdd/builder.rs
@@ -591,16 +591,6 @@ where
         self.or(v1, v2)
     }
 
-    /// Compose `g` into `f` by substituting for `lbl`
-    fn compose(&'a self, f: SddPtr<'a>, lbl: VarLabel, g: SddPtr<'a>) -> SddPtr<'a> {
-        // TODO this can be optimized with a specialized implementation to make
-        // it a single traversal
-        let var = self.var(lbl, true);
-        let iff = self.iff(var, g);
-        let a = self.and(iff, f);
-        self.exists(a, lbl)
-    }
-
     /// compile an SDD from an input CNF
     fn compile_cnf(&'a self, cnf: &Cnf) -> SddPtr<'a> {
         let mut cvec: Vec<SddPtr> = Vec::with_capacity(cnf.clauses().len());