Fix ZBDD subset/change

crates/oxidd-core/src/function.rs

@@ -1201,7 +1201,7 @@ pub trait BooleanVecSet: Function {
         Self::from_edge(manager, Self::base_edge(manager))
     }
 
-    /// Get the set of subsets of `self` not containing `var`, formally
+    /// Get the subset of `self` not containing `var`, formally
     /// `{s ∈ self | var ∉ s}`
     ///
     /// `var` must be a singleton set, otherwise the result is unspecified.
@@ -1217,8 +1217,8 @@ pub trait BooleanVecSet: Function {
         })
     }
 
-    /// Get the set of subsets of `self` containing `var`, formally
-    /// `{s ∈ self | var ∈ s}`
+    /// Get the subset of `self` containing `var` with `var` removed afterwards,
+    /// formally `{s ∖ {var} | s ∈ self ∧ var ∈ s}`
     ///
     /// `var` must be a singleton set, otherwise the result is unspecified.
     /// Ideally, the implementation panics.
@@ -1233,9 +1233,8 @@ pub trait BooleanVecSet: Function {
         })
     }
 
-    /// Get the set of subsets derived from `self` by adding `var` to the
-    /// subsets that do not contain `var`, and removing `var` from the subsets
-    /// that contain `var`, formally
+    /// Swap [`subset0`][Self::subset0] and [`subset1`][Self::subset1] with
+    /// respect to `var`, formally
     /// `{s ∪ {var} | s ∈ self ∧ var ∉ s} ∪ {s ∖ {var} | s ∈ self ∧ var ∈ s}`
     ///
     /// `var` must be a singleton set, otherwise the result is unspecified.

crates/oxidd-ffi-c/src/zbdd.rs

@@ -419,8 +419,8 @@ pub unsafe extern "C" fn oxidd_zbdd_cofactor_false(f: zbdd_t) -> zbdd_t {
     }
 }
 
-/// Get the set of subsets of `set` not containing `var`, formally
-/// `{s ∈ set | var ∉ s}`
+/// Get the subset of `self` not containing `var`, formally
+/// `{s ∈ self | var ∉ s}`
 ///
 /// `var` must be a singleton set.
 ///
@@ -432,8 +432,8 @@ pub unsafe extern "C" fn oxidd_zbdd_subset0(set: zbdd_t, var: zbdd_t) -> zbdd_t
     op2(set, var, ZBDDFunction::subset0)
 }
 
-/// Get the set of subsets of `set` containing `var`, formally
-/// `{s ∈ set | var ∈ s}`
+/// Get the subsets of `set` containing `var` with `var` removed afterwards,
+/// formally `{s ∖ {var} | s ∈ set ∧ var ∈ s}`
 ///
 /// `var` must be a singleton set.
 ///
@@ -445,9 +445,7 @@ pub unsafe extern "C" fn oxidd_zbdd_subset1(set: zbdd_t, var: zbdd_t) -> zbdd_t
     op2(set, var, ZBDDFunction::subset1)
 }
 
-/// Get the set of subsets derived from `set` by adding `var` to the
-/// subsets that do not contain `var`, and removing `var` from the subsets
-/// that contain `var`, formally
+/// Swap `subset0` and `subset1` with respect to `var`, formally
 /// `{s ∪ {var} | s ∈ set ∧ var ∉ s} ∪ {s ∖ {var} | s ∈ set ∧ var ∈ s}`
 ///
 /// `var` must be a singleton set.

crates/oxidd-rules-zbdd/src/apply_rec.rs

@@ -40,6 +40,9 @@ where
     M: Manager<Terminal = ZBDDTerminal> + HasApplyCache<M, ZBDDOp>,
     M::InnerNode: HasLevel,
 {
+    if rec.should_switch_to_sequential() {
+        return subset::<M, _, VAL>(manager, SequentialRecursor, f, var, var_level);
+    }
     let op = match VAL {
         -1 => ZBDDOp::Change,
         0 => ZBDDOp::Subset0,
@@ -53,7 +56,7 @@ where
     };
     let level = node.level();
     match level.cmp(&var_level) {
-        Ordering::Less => {}
+        Ordering::Less => {} // level above var_level
         Ordering::Equal => {
             if op == ZBDDOp::Change {
                 // The swap of `hi` and `lo` below is intentional
@@ -63,7 +66,19 @@ where
             return Ok(manager.clone_edge(&node.child(VAL as usize)));
         }
         Ordering::Greater => {
-            return Ok(manager.get_terminal(ZBDDTerminal::Empty).unwrap());
+            // var_level above level
+            return match op {
+                ZBDDOp::Subset0 => Ok(manager.clone_edge(&f)),
+                ZBDDOp::Subset1 => Ok(manager.get_terminal(ZBDDTerminal::Empty).unwrap()),
+                ZBDDOp::Change => reduce(
+                    manager,
+                    var_level,
+                    manager.clone_edge(&f),
+                    manager.get_terminal(ZBDDTerminal::Empty).unwrap(),
+                    ZBDDOp::Change,
+                ),
+                _ => unreachable!(),
+            };
         }
     }