@@ -6106,18 +6106,39 @@ defmodule Module.Types.Descr do
61066106 { :eq , { _ , lit , c1 , u , d1 } , { _ , _ , c2 , u , d2 } } ->
61076107 bdd_node_new ( lit , bdd_intersection ( c1 , c2 ) , u , bdd_intersection ( d1 , d2 ) )
61086108
6109- # Otherwise normalize the result by splitting on `a` and keeping the
6110- # union branch empty. Although this duplicates U1 and U2 into the
6111- # constrained and dual branches, it avoids carrying a shared union
6112- # through subsequent equal-head intersections, where it can lead to
6113- # exponential growth.
61146109 { :eq , { _ , lit , c1 , u1 , d1 } , { _ , _ , c2 , u2 , d2 } } ->
6115- bdd_node_new (
6116- lit ,
6117- bdd_intersection ( bdd_union ( c1 , u1 ) , bdd_union ( c2 , u2 ) ) ,
6118- :bdd_bot ,
6119- bdd_intersection ( bdd_union ( d1 , u1 ) , bdd_union ( d2 , u2 ) )
6120- )
6110+ # The intersection can be factored as:
6111+ #
6112+ # {a,
6113+ # (C1 and (C2 or U2)) or (U1 and C2),
6114+ # U1 and U2,
6115+ # (D1 and (D2 or U2)) or (U1 and D2)}
6116+ #
6117+ # This form preserves U1 and U2 in a common union branch. It is
6118+ # beneficial when C1-C2 or D1-D2 start with the same literal, as
6119+ # at least one pair of equal-head BDDs can be combined immediately.
6120+ #
6121+ # Doing this allows us to optimize open_api_spex compilation,
6122+ # version 3.22.2 (f2c71bf320045b76c4bc2ea9a7a056c8d9092197).
6123+ #
6124+ # Otherwise keep the union branch empty: duplicating U1 and U2 is
6125+ # cheaper than carrying a shared union through subsequent
6126+ # equal-head intersections, where it can grow exponentially.
6127+ if same_lit? ( c1 , c2 ) or same_lit? ( d1 , d2 ) do
6128+ bdd_node_new (
6129+ lit ,
6130+ bdd_intersection_eq ( c1 , c2 , u1 , u2 ) ,
6131+ bdd_intersection ( u1 , u2 ) ,
6132+ bdd_intersection_eq ( d1 , d2 , u1 , u2 )
6133+ )
6134+ else
6135+ bdd_node_new (
6136+ lit ,
6137+ bdd_intersection ( bdd_union ( c1 , u1 ) , bdd_union ( c2 , u2 ) ) ,
6138+ :bdd_bot ,
6139+ bdd_intersection ( bdd_union ( d1 , u1 ) , bdd_union ( d2 , u2 ) )
6140+ )
6141+ end
61216142
61226143 { :eq , { _ , lit , c1 , u1 , _ } , _ } ->
61236144 bdd_node_new ( lit , bdd_union ( c1 , u1 ) , :bdd_bot , :bdd_bot )
@@ -6135,6 +6156,19 @@ defmodule Module.Types.Descr do
61356156 end
61366157 end
61376158
6159+ defp same_lit? ( { _ , lit , _ , _ , _ } , { _ , lit , _ , _ , _ } ) , do: true
6160+ defp same_lit? ( _ , _ ) , do: false
6161+
6162+ defp bdd_intersection_eq ( cd1 , cd2 , u1 , u2 ) do
6163+ case bdd_intersection ( cd1 , cd2 ) do
6164+ :bdd_top ->
6165+ :bdd_top
6166+
6167+ cd ->
6168+ bdd_union ( cd , bdd_union ( bdd_intersection ( cd1 , u2 ) , bdd_intersection ( u1 , cd2 ) ) )
6169+ end
6170+ end
6171+
61386172 # {lit, c, u, d} = (lit and c) or u or (not lit and d),
61396173 # so its negation is ((lit and not c) or (not lit and not d)) and not u.
61406174 def bdd_negation ( :bdd_top ) , do: :bdd_bot
0 commit comments