[daemontus]

Summary by CodeRabbit

• New Features
  • Added valuation analysis methods to compute variables with most true or false literals.
  • Added safe variable substitution operation for BDD transformations.
  • Added constructor for creating BDDs satisfying exactly k variable constraints.
  • Made variable access computation publicly available.
  • Added convenience constructors for variable identifiers.

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

[coderabbitai]

Walkthrough

The changes introduce new BDD analysis utilities for valuation computation, safe variable substitution, and SAT cardinality constraint generation. Additionally, VariableId receives convenience constructors for zero and increment operations, and previously internal used_variables functionality is exposed publicly.

Changes

Cohort / File(s)	Summary
BDD Analysis Utilities src/split/bdd.rs	Added public methods: most_positive_valuation() and most_negative_valuation() for extracting valuations with most true/false literals; safe_substitution() for variable substitution with dependency checking; new_sat_exactly_k() constructor for cardinality constraints; used_variables() for accessing utilized variables. Introduced private helper functions for valuation computation and expanded imports.
Variable ID Constructors src/variable_id.rs	Added public methods: zero() returning VariableId(0) and next() returning incremented VariableId.

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~20–25 minutes

• Special attention areas:
  • safe_substitution() — logic for ensuring substitute BDD independence from the substituted variable requires careful validation
  • new_sat_exactly_k() — SAT cardinality constraint construction logic and correctness of the BDD representation
  • Private helper functions most_positive_valuation and most_negative_valuation — ensure valuation traversal logic and variable handling up to last_var boundary are correct
  • Test coverage for new public methods, particularly edge cases in cardinality constraints and valuations

Poem

🐰 Behold! New valuations bloom so bright,
With substitutions safe and cardinality right,
The BDD grows wise with used_variables revealed,
While VariableId skips ahead—zero to next unsealed! ✨

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 PR title accurately describes the main changes: adding utility functions for working with valuations in split BDDs, which is reflected in the new methods like most_positive_valuation, most_negative_valuation, safe_substitution, and new_sat_exactly_k.
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/valuation-utils

---

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 (3)

src/variable_id.rs (1)

735-741: Consider adding overflow protection to next().

The next() method increments without checking if the resulting ID exceeds MAX_64_BIT_ID. While overflow is unlikely in practice (max valid ID is (u64::MAX >> 3) - 1), defensive coding would either panic on overflow in debug mode or return an Option<VariableId>.

Example approach:

 pub fn next(&self) -> Self {
+    debug_assert!(self.0 < Self::MAX_64_BIT_ID, "Variable ID overflow");
     Self(self.0 + 1)
 }

src/split/bdd.rs (2)

724-732: Consider a more descriptive assertion message.

The assertion correctly validates the safety precondition, but the message could be more helpful:

-    assert!(!substitute.used_variables().contains(&variable));
+    assert!(
+        !substitute.used_variables().contains(&variable),
+        "Unsafe substitution: substitute BDD depends on variable {:?}", variable
+    );

---

768-893: Algorithm looks correct but note significant code duplication.

The dynamic programming implementation correctly computes the most positive valuation. However, most_positive_valuation (lines 768-893) and most_negative_valuation (lines 895-1018) share approximately 90% of their logic, differing only in:

• Whether skipped variables are set to true vs false
• Slight differences in the branch selection logic (lines 839-850 vs 964-974)

Consider extracting a parameterized helper function to reduce duplication.

Example approach:

fn compute_valuation<TNodeId, TVarId, F>(
    bdd: &BddImpl<TNodeId, TVarId>,
    last_var: TVarId,
    default_value: bool,
    choose_branch: F,
) -> BTreeMap<VariableId, bool>
where
    F: Fn(usize, usize, bool, bool) -> (usize, bool),
{
    // Common logic with default_value for skipped vars
    // and choose_branch callback for branch selection
}

📜 Review details

Configuration used: CodeRabbit UI

Review profile: CHILL

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between e5449eb and 930a0dc.

📒 Files selected for processing (2)

• src/split/bdd.rs (2 hunks)
• src/variable_id.rs (1 hunks)

⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (1)

• GitHub Check: Code coverage

🔇 Additional comments (5)

src/split/bdd.rs (5)

9-9: LGTM!

The BTreeMap import is needed for the new valuation methods that return BTreeMap<VariableId, bool>.

---

691-698: LGTM!

Exposing used_variables() as a public method is a useful addition to the API for BDD introspection. The implementation correctly delegates to the internal BddImpl variants.

---

700-722: Good API addition with minor documentation suggestion.

The valuation methods provide useful functionality. The documentation correctly notes the precondition about last_var, but consider clarifying what happens if the precondition is violated (the implementation panics at line 811 in the helper function).

Also, be aware that if last_var is close to VariableId::MAX_64_BIT_ID, the internal loops using VariableId::next() (lines 787, 874, 889, etc.) could theoretically overflow, though this is unlikely in practice.

Consider adding a debug assertion at the start of these methods:

pub fn most_positive_valuation(&self, last_var: VariableId) -> BTreeMap<VariableId, bool> {
    debug_assert!(last_var.fits_in_packed64(), "last_var exceeds maximum representable ID");
    // ... existing code
}

---

734-766: LGTM!

The cardinality constraint implementation is correct and well-documented. The TODO comment at line 752 appropriately notes a potential optimization if value flipping is ever supported directly.

---

1022-1022: LGTM!

The test import adjustment supports the existing test patterns that match on BddInner variants.