From 59c59f970ad3f0438bfa54a01b12bc3f5e0e41e4 Mon Sep 17 00:00:00 2001 From: Josef Podany Date: Sun, 13 Oct 2024 18:43:47 +0200 Subject: [PATCH] fix vtree_idx in SDDs, prep for more complicated apply scenarios --- sdd-rs-lib/manager.rs | 99 +++++++++++++++++++++++++++++++------------ sdd-rs-lib/sdd.rs | 16 +++---- sdd-rs-lib/vtree.rs | 54 ++++++++++++----------- 3 files changed, 105 insertions(+), 64 deletions(-) diff --git a/sdd-rs-lib/manager.rs b/sdd-rs-lib/manager.rs index 2279882..01b8bbc 100644 --- a/sdd-rs-lib/manager.rs +++ b/sdd-rs-lib/manager.rs @@ -4,7 +4,7 @@ use crate::{ literal::{self, Polarity}, options::SddOptions, sdd::{Decision, Element, Sdd, SddType}, - vtree::{VTree, VTreeManager}, + vtree::{VTreeManager, VTreeOrder}, Result, }; @@ -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 } @@ -210,13 +216,21 @@ 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(), @@ -224,7 +238,6 @@ impl SddManager { }), }), - // TODO: Fix variable ordering. Operation::Disjoin => SddType::DecisionRegular(Decision { elements: btreeset!( Element { @@ -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 { + 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( @@ -268,7 +302,8 @@ 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 { @@ -276,10 +311,15 @@ impl SddManager { 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(), }); @@ -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 { + unimplemented!("_apply_ineq not yet implemented") + } + + fn _apply_left_sub_of_right(&self, fst: &Sdd, snd: &Sdd, op: Operation) -> BTreeSet { + unimplemented!("_apply_left_sub_of_right not yet implemented") + } - result + fn _apply_right_sub_of_left(&self, fst: &Sdd, snd: &Sdd, op: Operation) -> BTreeSet { + unimplemented!("_apply_right_sub_of_left not yet implemented") } pub fn condition() {} @@ -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(), @@ -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 { @@ -477,7 +522,5 @@ mod test { }, a_or_b ); - - // TODO: Implement is_consistent next to unlock more complicated apply scenarios. } } diff --git a/sdd-rs-lib/sdd.rs b/sdd-rs-lib/sdd.rs index 69ee624..1f4b704 100644 --- a/sdd-rs-lib/sdd.rs +++ b/sdd-rs-lib/sdd.rs @@ -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) => { @@ -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) => { @@ -306,11 +306,7 @@ impl Sdd { }; } - pub(crate) fn is_consistent(&self) -> bool { - unimplemented!(); - } - - pub(crate) fn unique_d<'b>(gamma: BTreeSet) -> Sdd { + pub(crate) fn unique_d<'b>(gamma: BTreeSet, vtree_idx: u16) -> Sdd { // gamma == {(T, T)}? if gamma.eq(&btreeset![Element { prime: Sdd::new_true().id(), @@ -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, } } @@ -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 { - println!("trimming..."); let elements: Vec<&Element> = self.elements.iter().collect(); if self.elements.len() == 1 { let el = elements.get(0).unwrap(); @@ -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 }; diff --git a/sdd-rs-lib/vtree.rs b/sdd-rs-lib/vtree.rs index e8ac1bc..d579104 100644 --- a/sdd-rs-lib/vtree.rs +++ b/sdd-rs-lib/vtree.rs @@ -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 @@ -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() { @@ -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 @@ -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: // * @@ -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); @@ -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(); @@ -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: @@ -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 @@ -807,10 +811,10 @@ mod test { let var_label_index = |vtree: Option| -> 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