Skip to content

Commit

Permalink
BinarySDD/SddOr-related cleanup (#147)
Browse files Browse the repository at this point in the history 
- make `SddOr::nodes` private, expose `.iter()` instead
- rename misleading `vtree` to `index`
- remove unused code
  • Loading branch information
@mattxwang
mattxwang authored Jul 20, 2023
1 parent 3399c56 commit 5fb0f8f
Show file tree
Hide file tree
Showing 6 changed files with 34 additions and 51 deletions.
10 changes: 5 additions & 5 deletions src/builder/sdd/builder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}
Expand Down Expand Up @@ -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 };
Expand Down Expand Up @@ -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 };
Expand Down
42 changes: 14 additions & 28 deletions src/repr/sdd.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"),
}
Expand All @@ -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())
}
}
}
Expand All @@ -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)
Expand All @@ -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())
}
}
}
Expand Down Expand Up @@ -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;
Expand Down
18 changes: 9 additions & 9 deletions src/repr/sdd/binary_sdd.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ use std::{
#[derive(Debug)]
pub struct BinarySDD<'a> {
label: VarLabel,
vtree: VTreeIndex,
index: VTreeIndex,
low: SddPtr<'a>,
high: SddPtr<'a>,

Expand All @@ -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]
Expand Down Expand Up @@ -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);
Expand All @@ -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
Expand All @@ -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,
}
Expand All @@ -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),
Expand Down
6 changes: 5 additions & 1 deletion src/repr/sdd/sdd_or.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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>>>,
Expand All @@ -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,
Expand Down
8 changes: 1 addition & 7 deletions src/repr/var_order.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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))
Expand Down
1 change: 0 additions & 1 deletion src/serialize/ser_sdd.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down

0 comments on commit 5fb0f8f

Please sign in to comment.