Skip to content

Commit

Permalink
fix vtree_idx in SDDs, prep for more complicated apply scenarios
Browse files Browse the repository at this point in the history
  • Loading branch information
@jsfpdn
jsfpdn committed Oct 13, 2024
1 parent 3a7de80 commit 59c59f9
Show file tree
Hide file tree
Showing 3 changed files with 105 additions and 64 deletions.
99 changes: 71 additions & 28 deletions sdd-rs-lib/manager.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ use crate::{
literal::{self, Polarity},
options::SddOptions,
sdd::{Decision, Element, Sdd, SddType},
vtree::{VTree, VTreeManager},
vtree::{VTreeManager, VTreeOrder},
Result,
};

Expand Down Expand Up @@ -88,15 +88,21 @@ impl SddManager {
}

pub fn literal(&self, literal: &str, polarity: Polarity) -> Sdd {
self.vtree_manager
.borrow_mut()
.add_variable(literal::VarLabel::new(literal));
let var_label = literal::VarLabel::new(literal);
self.vtree_manager.borrow_mut().add_variable(&var_label);
let vtree_idx = self
.vtree_manager
.borrow()
.get_variable_vtree(&var_label)
.expect("var_label was just inserted, therefore it must be present and found")
.borrow()
.get_index();

let literal = Sdd {
// TODO: Fix vtree index.
vtree_idx: 0,
sdd_type: SddType::Literal(literal::Literal::new(polarity, literal)),
vtree_idx,
};

self.insert_node(&literal);
literal
}
Expand Down Expand Up @@ -210,21 +216,28 @@ impl SddManager {
/// Apply operation on the two Sdds.
#[must_use]
fn apply(&self, fst: &Sdd, snd: &Sdd, op: Operation) -> Sdd {
// TODO: Check post-conditions, namely trimming & compression of the resulting Sdd.
if fst.is_constant_or_literal() && snd.is_constant_or_literal() {
let (fst, snd) = if fst.vtree_idx < snd.vtree_idx {
(fst, snd)
} else {
(snd, fst)
};
let (vtree, _) = self
.vtree_manager
.borrow()
.least_common_ancestor(fst.vtree_idx, snd.vtree_idx);

return Sdd {
// TODO: Fix vtree_idx
vtree_idx: 123,
// TODO: Double-check correctness of vtree index.
vtree_idx: vtree.borrow().get_index(),
sdd_type: match op {
// TODO: Fix variable ordering.
Operation::Conjoin => SddType::DecisionRegular(Decision {
elements: btreeset!(Element {
prime: fst.id(),
sub: snd.id()
}),
}),

// TODO: Fix variable ordering.
Operation::Disjoin => SddType::DecisionRegular(Decision {
elements: btreeset!(
Element {
Expand Down Expand Up @@ -252,11 +265,32 @@ impl SddManager {
.clone();
}

self._apply(fst, snd, op)
let (lca, order) = self
.vtree_manager
.borrow()
.least_common_ancestor(fst.vtree_idx, snd.vtree_idx);

let elements = match order {
VTreeOrder::Equal => self._apply_eq(fst, snd, op),
VTreeOrder::Inequal => self._apply_ineq(fst, snd, op),
VTreeOrder::LeftSubOfRight => self._apply_left_sub_of_right(fst, snd, op),
VTreeOrder::RightSubOfLeft => self._apply_right_sub_of_left(fst, snd, op),
};

let mut sdd = Sdd::unique_d(elements, lca.borrow().get_index());
sdd.canonicalize(self);

self.insert_node(&sdd);
self.cache_operation(fst.id(), snd.id(), op, sdd.id());

debug_assert!(sdd.is_trimmed(self));
debug_assert!(sdd.is_compressed(self));

sdd
}

fn _apply(&self, fst: &Sdd, snd: &Sdd, op: Operation) -> Sdd {
let mut gamma = BTreeSet::new();
fn _apply_eq(&self, fst: &Sdd, snd: &Sdd, op: Operation) -> BTreeSet<Element> {
let mut elements = BTreeSet::new();
for fst_elem in fst.expand().elements.iter() {
for snd_elem in snd.expand().elements.iter() {
let res_prime = self.conjoin(
Expand All @@ -268,18 +302,24 @@ impl SddManager {
.expect("snd_prime not present"),
);

if res_prime.is_consistent() {
// TODO: Is checking against `false` sufficient? Do we have to get bit more involved here?
if res_prime.is_false() {
let fst_sub = &self.get_node(fst_elem.sub).expect("fst_sub not present");
let snd_sub = &self.get_node(snd_elem.sub).expect("snd_sub not present");
let res_sub = match op {
Operation::Conjoin => self.disjoin(fst_sub, snd_sub),
Operation::Disjoin => self.conjoin(fst_sub, snd_sub),
};

// TODO: Should we cache primes and subs computed here? The paper caches only the resulting SDD.
if res_sub.is_true() && res_prime.is_true() {
println!(
"_apply_eq: we can optimize since res_sub and res_prime are both true"
)
}

self.insert_node(&res_prime);
self.insert_node(&res_sub);
gamma.insert(Element {
elements.insert(Element {
prime: res_prime.id(),
sub: res_sub.id(),
});
Expand All @@ -288,12 +328,19 @@ impl SddManager {
}
}

let result = Sdd::unique_d(gamma);
self.insert_node(&result);
self.cache_operation(fst.id(), snd.id(), op, result.id());
println!("{:?} {:?} {:?} = {:?}", fst, op, snd, result);
elements
}

fn _apply_ineq(&self, fst: &Sdd, snd: &Sdd, op: Operation) -> BTreeSet<Element> {
unimplemented!("_apply_ineq not yet implemented")
}

fn _apply_left_sub_of_right(&self, fst: &Sdd, snd: &Sdd, op: Operation) -> BTreeSet<Element> {
unimplemented!("_apply_left_sub_of_right not yet implemented")
}

result
fn _apply_right_sub_of_left(&self, fst: &Sdd, snd: &Sdd, op: Operation) -> BTreeSet<Element> {
unimplemented!("_apply_right_sub_of_left not yet implemented")
}

pub fn condition() {}
Expand Down Expand Up @@ -445,8 +492,7 @@ mod test {
let a_and_b = manager.conjoin(&lit_a, &lit_b);
assert_eq!(
Sdd {
// TODO: Fix vtree_idx
vtree_idx: 123,
vtree_idx: 1,
sdd_type: SddType::DecisionRegular(Decision {
elements: btreeset!(Element {
prime: lit_a.id(),
Expand All @@ -460,8 +506,7 @@ mod test {
let a_or_b = manager.disjoin(&lit_a, &lit_b);
assert_eq!(
Sdd {
// TODO: Fix vtree_idx
vtree_idx: 123,
vtree_idx: 1,
sdd_type: SddType::DecisionRegular(Decision {
elements: btreeset!(
Element {
Expand All @@ -477,7 +522,5 @@ mod test {
},
a_or_b
);

// TODO: Implement is_consistent next to unlock more complicated apply scenarios.
}
}
16 changes: 5 additions & 11 deletions sdd-rs-lib/sdd.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -263,7 +263,7 @@ impl Sdd {
}
}

fn is_trimmed(&self, manager: &SddManager) -> bool {
pub(crate) fn is_trimmed(&self, manager: &SddManager) -> bool {
match self.sdd_type.clone() {
SddType::True | SddType::False | SddType::Literal(_) => true,
SddType::DecisionRegular(decision) | SddType::DecisionComplement(decision) => {
Expand All @@ -272,7 +272,7 @@ impl Sdd {
}
}

fn is_compressed(&self, manager: &SddManager) -> bool {
pub(crate) fn is_compressed(&self, manager: &SddManager) -> bool {
match self.sdd_type.clone() {
SddType::True | SddType::False | SddType::Literal(_) => true,
SddType::DecisionRegular(decision) | SddType::DecisionComplement(decision) => {
Expand Down Expand Up @@ -306,11 +306,7 @@ impl Sdd {
};
}

pub(crate) fn is_consistent(&self) -> bool {
unimplemented!();
}

pub(crate) fn unique_d<'b>(gamma: BTreeSet<Element>) -> Sdd {
pub(crate) fn unique_d<'b>(gamma: BTreeSet<Element>, vtree_idx: u16) -> Sdd {
// gamma == {(T, T)}?
if gamma.eq(&btreeset![Element {
prime: Sdd::new_true().id(),
Expand All @@ -329,8 +325,7 @@ impl Sdd {

Sdd {
sdd_type: SddType::DecisionRegular(Decision { elements: gamma }),
// TODO: What's the proper vtree index?
vtree_idx: 0,
vtree_idx,
}
}

Expand Down Expand Up @@ -424,7 +419,6 @@ impl Decision {
/// and {(alpha, true), (!alpha, false)} with alpha. Returns a Boolean
/// denoting whether the decision node had to be trimmed.
fn trim(&mut self, manager: &SddManager) -> Option<Sdd> {
println!("trimming...");
let elements: Vec<&Element> = self.elements.iter().collect();
if self.elements.len() == 1 {
let el = elements.get(0).unwrap();
Expand Down Expand Up @@ -633,7 +627,7 @@ mod test {
elements: btreeset!(element_1_1),
};

let mut sdd_1 = Sdd {
let sdd_1 = Sdd {
sdd_type: SddType::DecisionRegular(decision_1),
vtree_idx: 0, // TODO: Fix vtree index
};
Expand Down
54 changes: 29 additions & 25 deletions sdd-rs-lib/vtree.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,10 @@ impl VTree {
Rc::new(RefCell::new(VTree::new(parent, idx, node)))
}

pub(crate) fn get_index(&self) -> u16 {
self.idx
}

/// Sets the left child of this [`VTree`].
///
/// # Panics
Expand Down Expand Up @@ -155,8 +159,8 @@ impl VTreeManager {

/// Add variable to the variable tree. The variable is inserted to the very end of the total
/// variable order.
pub(crate) fn add_variable(&mut self, label: VarLabel) {
let new_leaf = VTree::new_as_ref(None, self.next_idx, Node::Leaf(label));
pub(crate) fn add_variable(&mut self, label: &VarLabel) {
let new_leaf = VTree::new_as_ref(None, self.next_idx, Node::Leaf(label.clone()));
new_leaf.borrow_mut().inorder_last = Some(new_leaf.clone());

if self.root.is_none() {
Expand Down Expand Up @@ -530,10 +534,10 @@ mod test {
// 0 2 4 6
// A B C D
let mut manager = VTreeManager::new();
manager.add_variable(VarLabel::new("A"));
manager.add_variable(VarLabel::new("B"));
manager.add_variable(VarLabel::new("C"));
manager.add_variable(VarLabel::new("D"));
manager.add_variable(&VarLabel::new("A"));
manager.add_variable(&VarLabel::new("B"));
manager.add_variable(&VarLabel::new("C"));
manager.add_variable(&VarLabel::new("D"));

// Rotate the right child of root to the left to make the tree balanced as in the diagram.
let Node::Internal(_, rc) = manager
Expand Down Expand Up @@ -594,20 +598,20 @@ mod test {
let mut manager = VTreeManager::new();
assert!(manager.root.is_none());

manager.add_variable(VarLabel::new("A"));
manager.add_variable(&VarLabel::new("A"));
assert!(manager.root.is_some());
assert!(manager
.root
.clone()
.is_some_and(|root| root.as_ref().borrow().node.is_leaf()));

manager.add_variable(VarLabel::new("B"));
manager.add_variable(&VarLabel::new("B"));
assert!(manager
.root
.clone()
.is_some_and(|root| root.as_ref().borrow().node.is_internal()));

manager.add_variable(VarLabel::new("C"));
manager.add_variable(&VarLabel::new("C"));

// Test that the vtree has the following structure:
// *
Expand Down Expand Up @@ -636,9 +640,9 @@ mod test {
#[test]
fn variables_total_order_simple() {
let mut manager = VTreeManager::new();
manager.add_variable(VarLabel::new("A"));
manager.add_variable(VarLabel::new("B"));
manager.add_variable(VarLabel::new("C"));
manager.add_variable(&VarLabel::new("A"));
manager.add_variable(&VarLabel::new("B"));
manager.add_variable(&VarLabel::new("C"));

let want_order = vec![VarLabel::new("A"), VarLabel::new("B"), VarLabel::new("C")];
orders_eq(manager.variables_total_order(), want_order);
Expand All @@ -647,8 +651,8 @@ mod test {
#[test]
fn variables_total_order_swap() {
let mut manager = VTreeManager::new();
manager.add_variable(VarLabel::new("A"));
manager.add_variable(VarLabel::new("B"));
manager.add_variable(&VarLabel::new("A"));
manager.add_variable(&VarLabel::new("B"));

let root = manager.root.clone().unwrap();

Expand All @@ -670,9 +674,9 @@ mod test {
#[test]
fn variables_total_order() {
let mut manager = VTreeManager::new();
manager.add_variable(VarLabel::new("A"));
manager.add_variable(VarLabel::new("B"));
manager.add_variable(VarLabel::new("C"));
manager.add_variable(&VarLabel::new("A"));
manager.add_variable(&VarLabel::new("B"));
manager.add_variable(&VarLabel::new("C"));
let want_order = vec![VarLabel::new("A"), VarLabel::new("B"), VarLabel::new("C")];

// The tree intially looks like this:
Expand Down Expand Up @@ -763,10 +767,10 @@ mod test {
#[test]
fn least_common_ancestor() {
let mut manager = VTreeManager::new();
manager.add_variable(VarLabel::new("A"));
manager.add_variable(VarLabel::new("B"));
manager.add_variable(VarLabel::new("C"));
manager.add_variable(VarLabel::new("D"));
manager.add_variable(&VarLabel::new("A"));
manager.add_variable(&VarLabel::new("B"));
manager.add_variable(&VarLabel::new("C"));
manager.add_variable(&VarLabel::new("D"));
// 3
// / \
// 1 5
Expand Down Expand Up @@ -807,10 +811,10 @@ mod test {
let var_label_index = |vtree: Option<VTreeRef>| -> u16 { vtree.unwrap().borrow().idx };

let mut manager = VTreeManager::new();
manager.add_variable(VarLabel::new("A"));
manager.add_variable(VarLabel::new("B"));
manager.add_variable(VarLabel::new("C"));
manager.add_variable(VarLabel::new("D"));
manager.add_variable(&VarLabel::new("A"));
manager.add_variable(&VarLabel::new("B"));
manager.add_variable(&VarLabel::new("C"));
manager.add_variable(&VarLabel::new("D"));
// 1
// / \
// 0 3
Expand Down

0 comments on commit 59c59f9

Please sign in to comment.