Update lib-bdd to 0.5.21 (#24)

* Add API listing.

* Update library version.

* Replace `BooleanExpression::support_set` with library implementation.

* Fix a minor bug in dnf construction.

* Add size limit to dnf construction.

* Add a note about owned iterators.

* Use group renaming method since it is safer.

* Add a note about cmp methods.

Cargo.toml

@@ -19,7 +19,7 @@ static-z3 = ["z3/static-link-z3"]
 [dependencies]
 pyo3 = { version = "0.22.2", features = ["abi3-py37", "extension-module", "num-bigint", "py-clone"] }
 biodivine-lib-param-bn = { version="0.5.11", features=["solver-z3"] }
-biodivine-lib-bdd = "0.5.13"
+biodivine-lib-bdd = "0.5.21"
 #biodivine-pbn-control = "0.3.1"
 biodivine-pbn-control = { git = "https://github.com/sybila/biodivine-pbn-control", rev = "99f9da756c370daf5428b3d61ef76c24e7d8de5f" }
 #biodivine-hctl-model-checker = "0.2.2"

api-coverage/lib-bdd.md

@@ -231,7 +231,7 @@ explore it in the future.
             <td><code>BddVariableSet.__len__</code></td>
         </tr>
         <tr>
-            <td></td>
+            <td><code>BddVariableSet::to_string</code></td>
             <td><code>BddVariableSet.__str__</code></td>
         </tr>
         <tr>
@@ -894,7 +894,10 @@ we will need either complicated generics, or heavy use of `Any`.
         </tr>
         <tr>
             <td><code>Bdd::rename_variable</code></td>
-            <td><code>Bdd.rename</code></td>
+            <td rowspan="2"><code>Bdd.rename</code></td>
+        </tr>
+        <tr>
+            <td><code>Bdd::rename_variables</code></td> 
         </tr>
         <tr>
             <td><code>Bdd::set_num_vars</code></td>
@@ -908,6 +911,26 @@ we will need either complicated generics, or heavy use of `Any`.
             <td><code>Bdd::to_nodes</code></td>
             <td></td>
         </tr>
+        <tr>
+            <td><code>Bdd::cmp_cardinality</code></td>
+            <td></td>
+        </tr>
+        <tr>
+            <td><code>Bdd::cmp_cardinality_strict</code></td>
+            <td></td>
+        </tr>
+        <tr>
+            <td><code>Bdd::cmp_implies</code></td>
+            <td></td>
+        </tr>
+        <tr>
+            <td><code>Bdd::cmp_size</code></td>
+            <td></td>
+        </tr>
+        <tr>
+            <td><code>Bdd::cmp_structural</code></td>
+            <td></td>
+        </tr>
     </tbody>
 </table>
 
@@ -923,7 +946,7 @@ The original Rust method is then called with a function that is based on
 this lookup table. Since the lookup tables are small, the overhead is acceptable 
 for any sufficiently large `Bdd`.
 
-## `BddPathIterator` and `ValuationsOfClauseIterator`
+## `BddPathIterator`, `ValuationsOfClauseIterator` and owned iterators.
 
 We do not export the iterator types directly, because the API is quite low level and 
 frankly kind of weird. Instead, we have two Python-only types: `BddClauseIterator` 
@@ -932,6 +955,10 @@ a single `Bdd` and have no other public API. If you still want to replicate the
 of the Rust iterators, you can always create a `Bdd` representing a single clause 
 (or a `True` BDD) and iterate over that.
 
+Owned iterators are currently ignored. We could use them instead of the unsafe trick that
+we have now, but that would require cloning the BDD, which we currently avoid (the BDD
+is tracked with python reference counting instead).
+
 <table>
     <thead>
         <tr>
@@ -1168,7 +1195,7 @@ added a bunch of utility methods similar to how `FnUpdate` is expected to work.
         </tr>
         <tr><td colspan="2" align="center">Other</td></tr>
         <tr>
-            <td></td>
+            <td><code>BooleanExpression::support_set</code></td>
             <td><code>BooleanExpression.support_set</code></td>
         </tr>
     </tbody>

biodivine_aeon/__init__.pyi

@@ -212,7 +212,7 @@ class Bdd:
         ...
     def to_expression(self) -> BooleanExpression:
         ...
-    def to_dnf(self, optimize: bool = True) -> list[BddPartialValuation]:
+    def to_dnf(self, optimize: bool = True, size_limit: Optional[int] = None) -> list[BddPartialValuation]:
         ...
     def to_cnf(self) -> list[BddPartialValuation]:
         ...

src/bindings/lib_bdd/bdd.rs

@@ -218,10 +218,26 @@ impl Bdd {
     /// actual canonical clauses of this BDD as reported by `Bdd.clause_iterator`.
     ///
     /// See also `BddVariableSet.mk_dnf`.
-    #[pyo3(signature = (optimize = true))]
-    fn to_dnf(&self, py: Python, optimize: bool) -> PyResult<Vec<BddPartialValuation>> {
+    #[pyo3(signature = (optimize = true, size_limit = None))]
+    fn to_dnf(
+        &self,
+        py: Python,
+        optimize: bool,
+        size_limit: Option<usize>,
+    ) -> PyResult<Vec<BddPartialValuation>> {
         let native = if optimize {
-            self.as_native()._to_optimized_dnf(&|| py.check_signals())?
+            self.as_native()._to_optimized_dnf(&|dnf| {
+                if let Some(size_limit) = size_limit {
+                    println!("{}, {}", size_limit, dnf.len());
+                    if size_limit < dnf.len() {
+                        return throw_interrupted_error(format!(
+                            "Exceeded size limit of {} clauses",
+                            size_limit
+                        ));
+                    }
+                }
+                py.check_signals()
+            })?
         } else {
             self.as_native().to_dnf()
         };
@@ -1008,13 +1024,15 @@ impl Bdd {
     /// identifiers with new ones. As such, rename operation is only permitted if it does not violate
     /// the current ordering. If this is not satisfied, the method panics.
     pub fn rename(&self, py: Python, replace_with: Vec<(Py<PyAny>, Py<PyAny>)>) -> PyResult<Bdd> {
-        let mut result = self.value.clone();
+        let mut permutation = HashMap::new();
         for (a, b) in replace_with {
             let a = self.ctx.get().resolve_variable(a.bind(py))?;
             let b = self.ctx.get().resolve_variable(b.bind(py))?;
-            unsafe {
-                result.rename_variable(a, b);
-            }
+            permutation.insert(a, b);
+        }
+        let mut result = self.value.clone();
+        unsafe {
+            result.rename_variables(&permutation);
         }
         Ok(self.new_from(result))
     }

src/bindings/lib_bdd/boolean_expression.rs

@@ -404,27 +404,7 @@ impl BooleanExpression {
 
     /// Return the set of Boolean variable names that appear in this `BooleanExpression`.
     pub fn support_set(&self) -> HashSet<String> {
-        fn recursive(e: &RsBooleanExpression, result: &mut HashSet<String>) {
-            match e {
-                RsBooleanExpression::Const(_) => (),
-                Variable(name) => {
-                    result.insert(name.clone());
-                }
-                Not(inner) => recursive(inner, result),
-                And(l, r) | Or(l, r) | Imp(l, r) | Iff(l, r) | Xor(l, r) => {
-                    recursive(l, result);
-                    recursive(r, result);
-                }
-                Cond(test, branch1, branch2) => {
-                    recursive(test, result);
-                    recursive(branch1, result);
-                    recursive(branch2, result);
-                }
-            };
-        }
-        let mut result = HashSet::new();
-        recursive(self.as_native(), &mut result);
-        result
+        self.as_native().support_set()
     }
 }
 

tests/test_bdd_module.py

@@ -255,15 +255,18 @@ def test_bdd():
     assert bdd_x.to_dot() != bdd_x.to_dot(zero_pruned=False)
     assert str(bdd_x.to_expression()) == "((a & b) | (!a & (b & !c)))"
     assert BddPartialValuation(ctx, {'a': True, 'b': True}) == BddPartialValuation(ctx, {'a': 1, 'b': 1})
-    # (!a & b & c) | (a & b)
+    # (b & !c) | (a & b)
     dnf = bdd_x.to_dnf()
     dnf_basic = bdd_x.to_dnf(optimize=False)
+    with pytest.raises(InterruptedError):
+        # The method should fail if the DNF is larger than requested.
+        bdd_x.to_dnf(size_limit=0)
     # For a very simple BDD like this, the optimization does not really do much.
     assert len(dnf) == len(dnf_basic)
     assert len(dnf_basic) == bdd_x.clause_cardinality()
     assert len(dnf) == 2
-    assert dnf[0] == BddPartialValuation(ctx, {'a': True, 'b': True})
-    assert dnf[1] == BddPartialValuation(ctx, {'a': False, 'b': True, 'c': False})
+    assert dnf[0] == BddPartialValuation(ctx, {'b': True, 'c': False})
+    assert dnf[1] == BddPartialValuation(ctx, {'a': True, 'b': True})
     # (a | b) & (a | !b | !c) & (!a | b)
     cnf = bdd_x.to_cnf()
     assert len(cnf) == 3