[bdd] Optimize BddQueryEngine performance and reduce BDD node creation - #4802
Merged
Conversation
copybara-service
Bot
changed the title
copybara-service
Bot
force-pushed
the
test_965159664
branch
3 times, most recently
from
August 22, 2026 02:41
de01876 to
485df96
Compare
This change introduces several optimizations to `BddQueryEngine` and `BinaryDecisionDiagram` to avoid creating unnecessary BDD nodes and bypass expensive operations: - Adds a `MutuallyExclusive` helper to check if two BDD nodes are mutually exclusive without constructing new BDD nodes. - Enable early-exit for `KnownValue`, `IsAllZeros`, `IsAllOnes`, and `IsFullyKnown` by querying BDD nodes directly, rather than constructing a ternary. - Optimizes `KnownEquals` and `KnownNotEquals` to use direct BDD index comparison when no assumption is present. - Refactors `AtMostOneTrue` and `AtLeastOneTrue` to minimize BDD operations and handle untracked bits more efficiently. - Skips redundant bounds checks (e.g., zero lower bounds or maximal intervals) during interval specialization. Also takes advantage of the new MutuallyExclusive helper in the visibility analysis. PiperOrigin-RevId: 968839585
copybara-service
Bot
force-pushed
the
test_965159664
branch
from
August 22, 2026 03:24
485df96 to
dc311d6
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
[bdd] Optimize BddQueryEngine performance and reduce BDD node creation
This change introduces several optimizations to
BddQueryEngineandBinaryDecisionDiagramto avoid creating unnecessary BDD nodes and bypass expensive operations:MutuallyExclusivehelper to check if two BDD nodes are mutually exclusive without constructing new BDD nodes.KnownValue,IsAllZeros,IsAllOnes, andIsFullyKnownby querying BDD nodes directly, rather than constructing a ternary.KnownEqualsandKnownNotEqualsto use direct BDD index comparison when no assumption is present.AtMostOneTrueandAtLeastOneTrueto minimize BDD operations and handle untracked bits more efficiently.Also takes advantage of the new MutuallyExclusive helper in the visibility analysis.