Hash-cons and simplify descriptor BDDs#15292
Draft
gldubc wants to merge 5 commits intoelixir-lang:mainfrom
Draft
Hash-cons and simplify descriptor BDDs#15292gldubc wants to merge 5 commits intoelixir-lang:mainfrom
gldubc wants to merge 5 commits intoelixir-lang:mainfrom
Conversation
Member
Author
|
Those are the expected type-checking times for this PR: And those are the times with Long times to be solved by caching bdd ops (coming later) |
Store hashes directly on BDD leaves and nodes so equality checks can short-circuit while still normalizing legacy two- and four-tuple forms. Route BDD construction through bdd_leaf_new/2 and bdd_node_new/4 to keep descriptors in the hashed representation. Centralize node construction through bdd_split/4 and use it from union, difference, intersection, and negation paths. This lets construction immediately discard redundant branches, simplify branches under union assumptions, and preserve normalized hashes after transformations. When unioning a BDD node with its own literal, put the literal into the union arm instead of replacing the positive branch with top. Then collapse splits whose union arm already covers the split literal, removing redundant negative occurrences such as (t2 \ t1) | t1 into the plain t1 | t2 shape. Add descriptor coverage for union(difference(t2, t1), t1) over nested list BDDs. The test documents the exact-match normalization invariant: the redundant negation is removed, while leaf-level semantic union may still decide whether t1 | t2 further collapses to t2.
Map unions were taking the map-specific merge path eagerly. In large inferred descriptors that can repeatedly merge field shapes even when preserving the generic BDD union is enough for the hot path. Route maps through the generic BDD union and keep the fallback equal cases for difference and intersection in split form. This avoids expanding the decision literal back into a union, which reduces repeated normalization and simplification work on large chained refinements. Add a regression for chained list differences and unions so the rewritten BDD operations keep the expected semantic shape.
gldubc
force-pushed
the
hash-consing-bdd-simplifications
branch
from
0d476f6 to
d159d77
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.
Summary
Keeping hashes on the BDD structure and simplifying through the generic operations reduces repeated structural work and makes equivalent fragments cheaper to compare and reuse.
Validation
Module.Types.DescrTest(leaving this as a draft PR)