fix: compute cartesian product when swapping vtree nodes

jsfpdn · Nov 17, 2024 · f83754a · f83754a
1 parent a0899c7
commit f83754a
Show file tree

Hide file tree

Showing 2 changed files with 41 additions and 5 deletions.
diff --git a/sdd-rs-lib/manager/manager.rs b/sdd-rs-lib/manager/manager.rs
@@ -15,7 +15,6 @@ use bitvec::prelude::*;
 use std::{
     cell::RefCell,
     collections::{BTreeSet, HashMap},
-    env::consts::ARCH,
     ops::BitOr,
 };
 use tracing::instrument;

diff --git a/sdd-rs-lib/vtree/fragment.rs b/sdd-rs-lib/vtree/fragment.rs
@@ -445,28 +445,65 @@ pub(crate) fn swap_partition(node: &SddRef, v: &VTreeRef, manager: &SddManager)
 
     let mut elements = BTreeSet::new();
     for element in &decision.elements {
+        let mut current_elements = BTreeSet::new();
+
         let (a, b) = element.get_prime_sub(manager);
         let neg_b = manager.negate(&b);
         if !b.is_false() {
-            elements.insert(Element {
+            current_elements.insert(Element {
                 prime: b.id(),
                 sub: a.id(),
             });
         }
 
         if !neg_b.is_false() {
-            elements.insert(Element {
+            current_elements.insert(Element {
                 prime: neg_b.id(),
                 sub: FALSE_SDD_IDX,
             });
         }
-        // TODO: Compute Cartesian product of the two (or one) new elements
-        // added in this loop.
+
+        elements = cartesian_product(current_elements.clone(), elements.clone(), manager);
     }
 
     Decision { elements }.canonicalize(manager)
 }
 
+fn cartesian_product(
+    fst: BTreeSet<Element>,
+    snd: BTreeSet<Element>,
+    manager: &SddManager,
+) -> BTreeSet<Element> {
+    if fst.is_empty() {
+        return snd.clone();
+    }
+
+    if snd.is_empty() {
+        return fst.clone();
+    }
+
+    let mut out = BTreeSet::new();
+
+    for fst_element in &fst {
+        for snd_element in &snd {
+            let (fst_prime, fst_sub) = fst_element.get_prime_sub(&manager);
+            let (snd_prime, snd_sub) = snd_element.get_prime_sub(&manager);
+
+            let res_prime = manager.conjoin(&fst_prime, &snd_prime);
+            if !res_prime.is_false() {
+                let res_sub = manager.disjoin(&fst_sub, &snd_sub);
+
+                out.insert(Element {
+                    prime: res_prime.id(),
+                    sub: res_sub.id(),
+                });
+            }
+        }
+    }
+
+    out
+}
+
 #[cfg(test)]
 mod test {
     use crate::{