Skip to content

Commit

Permalink
Moves compose() to BottomUpBuilder (from Bdd and Sdd builders) (
Browse files Browse the repository at this point in the history
#168)

Cherry-picking this change over from #163, to make it easier to review (and to revert this if necessary).
  • Loading branch information
mattxwang committed Aug 3, 2023
1 parent 36ce136 commit a27cf0d
Show file tree
Hide file tree
Showing 4 changed files with 10 additions and 23 deletions.
2 changes: 1 addition & 1 deletion src/backing_store/bump_table.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
11 changes: 0 additions & 11 deletions src/builder/bdd/builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand Down
10 changes: 9 additions & 1 deletion src/builder/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
10 changes: 0 additions & 10 deletions src/builder/sdd/builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand Down

0 comments on commit a27cf0d

Please sign in to comment.