Commit 1f0dd83
committed
Add memoization to BDD operations to prevent exponential blowup
The type system's BDD (Binary Decision Diagram) operations could
experience exponential recursion on certain type patterns, causing
compilation to hang. This happened when bdd_difference/2 and
bdd_union/2 recursively computed identical sub-problems without
caching results.
This commit adds memoization to all BDD operations following the
existing phi/4 pattern:
- bdd_union/3 - Caches union operations
- bdd_difference/3 - Caches difference operations
- bdd_intersection/3 - Caches intersection operations
- Helper functions updated: bdd_difference_union/4,
bdd_intersection_union/4, bdd_negation/2
Implementation:
- Functions accept optional cache parameter (defaults to nil)
- When cache=nil: Initialize cache, compute, return result only
- When cache is map: Check cache first, return {result, cache}
- Cache shared across all BDD operations in single traversal
This reduces complexity from exponential to polynomial for complex
type patterns while maintaining backward compatibility.1 parent 43aeded commit 1f0dd83
1 file changed
+251
-153
lines changed
0 commit comments