[daemontus]

Summary by CodeRabbit

• New Features
  • Added a new valuation iterator API for Binary Decision Diagrams enabling efficient enumeration of all satisfying valuations in lexicographic order within specified variable ranges. The enhancement streamlines constraint analysis and Boolean formula exploration workflows, providing improved accessibility and performance for applications working with complex logical specifications and formal verification tasks.

_{✏️ Tip: You can customize this high-level summary in your review settings.}

[coderabbitai]

Walkthrough

This pull request introduces an iterator-based API for traversing satisfying valuations of a BDD in lexicographic order. It adds a public iter_satisfying_valuations method on the Bdd type, implements a new ValuationsIterator struct with supporting path management logic, and includes helper functions to upcast lower-width BDD representations to 64-bit.

Changes

Cohort / File(s)	Summary
BDD API Extension src/split/bdd.rs	Added public method iter_satisfying_valuations(min, max) to Bdd that upcasts to 64-bit representation and returns ValuationsIterator. Added two helper functions: bdd_16_to_64 and bdd_32_to_64 for upcasting lower-width BDD types.
Iterator Implementation src/split/bdd_iterator.rs	New module implementing ValuationsIterator for enumerating satisfying valuations in lexicographic order. Includes internal PathChoice enum for tracking decision paths, iterator logic with find_first_path and find_next_path methods, and comprehensive test suite validating behavior across various BDD configurations.
Module Exports src/split/mod.rs	Added internal module bdd_iterator and re-exported ValuationsIterator as a public item for external crate access.

Sequence Diagram

sequenceDiagram
    participant Client
    participant Bdd
    participant ValuationsIterator
    participant PathFinding as Path Finding Logic

    Client->>Bdd: iter_satisfying_valuations(min, max)
    Bdd->>Bdd: upcast to Bdd64 if needed
    Bdd->>ValuationsIterator: new(bdd64, min, max)
    ValuationsIterator->>PathFinding: find_first_path()
    PathFinding-->>ValuationsIterator: initial path
    
    loop next() calls
        Client->>ValuationsIterator: next()
        alt path exists
            ValuationsIterator->>ValuationsIterator: construct BTreeMap from path
            ValuationsIterator->>PathFinding: find_next_path()
            PathFinding-->>ValuationsIterator: advanced path
            ValuationsIterator-->>Client: Some(valuation)
        else no more paths
            ValuationsIterator-->>Client: None
        end
    end

Loading

Estimated code review effort

🎯 4 (Complex) | ⏱️ ~60 minutes

• Path finding logic: The find_first_path and find_next_path methods contain intricate BDD traversal and decision-path manipulation that requires careful verification for correctness and lexicographic ordering guarantees.
• Iterator state management: The next_path state transitions and path extension logic in extend_path demand scrutiny to ensure all edge cases (free variables, terminal nodes, non-advancable paths) are handled correctly.
• Upcast helper functions: While simpler, the bdd_16_to_64 and bdd_32_to_64 functions need verification that variable ID mappings and node transformations are accurate.
• Test coverage validation: Extensive test suite requires review to ensure all critical paths and boundary conditions are exercised (multi-variable BDDs, gaps in variables, logical operations, lexicographic ordering).

Poem

🐰 Through BDD paths, we hop and bound,
Lexicographic treasures found!
Iterator hops from node to node,
Finding valuations down the road,
One decision at a time we go! 🌳✨

Pre-merge checks and finishing touches

✅ Passed checks (3 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title accurately describes the main change: introducing a new iterator implementation (ValuationsIterator) that owns the BDD, as evidenced by the addition of iter_satisfying_valuations() method and the new ValuationsIterator struct in the changeset.
Docstring Coverage	✅ Passed	Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%.

✨ Finishing touches

• 📝 Generate docstrings

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Post copyable unit tests in a comment
• Commit unit tests in branch daemontus/feat/owned-iterator

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[coderabbitai]

Actionable comments posted: 0

🧹 Nitpick comments (5)

src/split/bdd.rs (1)

796-836: Consider consolidating duplicate conversion logic.

The bdd_16_to_64 and bdd_32_to_64 functions are nearly identical, differing only in their input types. While the existing impl_unchecked_from! macro handles the opposite direction (downcasting), you could reduce duplication here.

One approach using a generic helper:

+fn bdd_to_64<TNodeId, TVarId>(bdd: &BddImpl<TNodeId, TVarId>) -> Bdd64
+where
+    TNodeId: NodeIdAny + Into<NodeId64>,
+    TVarId: VarIdPackedAny + Into<VarIdPacked64>,
+{
+    let new_nodes = bdd.nodes.iter().map(|x| {
+        if x.is_zero() {
+            BddNodeImpl::zero()
+        } else if x.is_one() {
+            BddNodeImpl::one()
+        } else {
+            BddNodeImpl::new(x.variable.into(), x.low.into(), x.high.into())
+        }
+    }).collect();
+    Bdd64 {
+        root: bdd.root.into(),
+        nodes: new_nodes,
+    }
+}
+
-fn bdd_16_to_64(bdd: &Bdd16) -> Bdd64 { ... }
-fn bdd_32_to_64(bdd: &Bdd32) -> Bdd64 { ... }

This would require the appropriate Into trait bounds to be satisfied, which may need verification.

src/split/bdd_iterator.rs (4)

7-15: Consider documenting why PositiveNode stores the unused node ID.

The #[allow(dead_code)] on line 10 indicates the second field in PositiveNode is never read, while NegativeNode uses its node ID to look up the high link when advancing. A brief comment explaining this asymmetry would help future maintainers understand the design choice (e.g., keeping variants structurally consistent, or for potential future use).

---

68-81: The TODO on line 71 flags an important validation gap.

If max_variable is less than the largest variable in the BDD, the iterator could produce valuations that don't include all BDD variables. The extend_path loop exits when next_var > self.max_variable, potentially leaving BDD decisions unresolved.

Consider adding validation (as noted in the TODO) or documenting this as a precondition. The Bdd::iter_satisfying_valuations doc comment says variables must be within bounds, but without enforcement, misuse could silently produce incorrect results.

Would you like me to suggest validation logic that checks the BDD's used variables against the provided range?

---

378-382: Update stale test comments.

These comments describe previous buggy behavior ("Current: Panics...", "Current: Returns 3 valuations...") that appears to be fixed now since the tests pass. Consider updating or removing these comments to avoid confusion.

     #[test]
     fn test_single_literal_with_free_variables() {
-        // Issue: When a literal BDD has free variables in the range that lead to terminal nodes,
-        // the iterator fails to handle the terminal node when extending the path.
         // Expected: Should return 4 valuations (v0 and v2 are free, v1 must be true)
-        // Current: Panics when trying to unpack variable from terminal node
+        // v0 and v2 are free, v1 must be true

     #[test]
     fn test_xor_two_variables() {
-        // Issue: XOR creates paths that lead to terminal nodes, causing failures.
         // Expected: Should return 2 valuations: (true, false), (false, true)
-        // Current: Returns 3 valuations (includes an extra valuation due to iterator behavior)

Also applies to: 451-453

---

590-590: Minor: prefer is_empty() over len() > 0.

-        assert!(iter_valuations.len() > 0);
+        assert!(!iter_valuations.is_empty());

📜 Review details

Configuration used: CodeRabbit UI

Review profile: CHILL

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between b7dfb72 and 7d9d095.

📒 Files selected for processing (3)

• src/split/bdd.rs (3 hunks)
• src/split/bdd_iterator.rs (1 hunks)
• src/split/mod.rs (1 hunks)

🧰 Additional context used

🧬 Code graph analysis (2)

src/split/bdd.rs (2)

src/split/bdd_iterator.rs (1)

• new (69-81)

src/bdd_node.rs (6)

• new (35-35)
• new (114-123)
• zero (47-47)
• zero (133-139)
• one (49-49)
• one (141-147)

src/split/bdd_iterator.rs (1)

src/split/bdd.rs (17)

• root (65-65)
• root (345-347)
• root (609-615)
• new_false (44-44)
• new_false (312-317)
• new_false (495-497)
• new_literal (46-46)
• new_literal (319-329)
• new_literal (500-510)
• get (68-68)
• get (349-351)
• from (471-473)
• from (477-479)
• from (483-485)
• new_true (42-42)
• new_true (305-310)
• new_true (490-492)

🔇 Additional comments (7)

src/split/mod.rs (1)

6-6: LGTM!

The module declaration and public re-export follow the established pattern in this file, correctly exposing ValuationsIterator as part of the public API while keeping the implementation module crate-internal.

Also applies to: 13-13

src/split/bdd.rs (1)

676-695: LGTM! Method correctly implements owned iterator pattern.

The implementation properly upcasts all BDD variants to Bdd64 before passing ownership to the iterator. The clone on line 691 for the Bdd64 case is consistent with the owned iterator design.

One consideration: the doc comment mentions panicking if variables are outside bounds, but the actual assertion (min_variable <= max_variable) is in ValuationsIterator::new. Additionally, the assertion at line 152 in find_first_path validates that min_variable <= root_var. You may want to clarify in the doc that the panic can also occur if min > max.

src/split/bdd_iterator.rs (5)

46-51: LGTM!

The struct correctly encapsulates the owned BDD and iteration state. Using Option<Vec<PathChoice>> elegantly represents both the current path and the exhausted state.

---

53-66: LGTM!

The Iterator implementation correctly captures the current valuation before advancing to the next path. The use of BTreeMap provides predictable ordering of variables in the output.

---

86-129: LGTM!

The find_next_path correctly implements lexicographic advancement by backtracking through the path until finding a choice that can progress (negative → positive). The check on line 113 properly skips invalid paths where the high link leads to zero.

---

132-172: LGTM!

The find_first_path correctly handles all cases:

• False BDD returns None
• True BDD (root is 1) treats all variables as free
• Non-trivial BDD correctly identifies whether the first variable is a decision node or free choice
• Choosing negative/low paths first ensures lexicographically smallest valuation is found first

---

176-227: LGTM!

The extend_path method correctly extends a partial path to a complete valuation by:

• Handling terminal 1 nodes by treating remaining variables as free
• Making forced positive choices when the low link leads to zero
• Otherwise preferring negative choices for lexicographic ordering
• Properly validating BDD invariants with assertions