@@ -3029,63 +3029,7 @@ defmodule Module.Types.Descr do
30293029
30303030 defp map_intersection ( bdd_leaf ( :open , [ ] ) , bdd ) , do: bdd
30313031 defp map_intersection ( bdd , bdd_leaf ( :open , [ ] ) ) , do: bdd
3032- defp map_intersection ( bdd1 , bdd2 ) , do: map_bdd_intersection ( bdd1 , bdd2 )
3033-
3034- # A variant of bdd_intersection/3 that only continues if the maps are closed
3035- # or both sides are leafs.
3036- #
3037- # This is necessary because the intersection of open maps end-up accumulating
3038- # fields and it is unlikely to eliminate, which would lead to explosions.
3039- # However, note this optimization only works because closed nodes come first
3040- # in the BDD representation. If that was not the case, open nodes would come
3041- # first and this optimization would not happen if they were mixed.
3042- defp map_bdd_intersection ( bdd_leaf ( _ , _ ) = leaf1 , bdd_leaf ( _ , _ ) = leaf2 ) do
3043- map_leaf_intersection ( leaf1 , leaf2 )
3044- end
3045-
3046- defp map_bdd_intersection ( bdd_leaf ( :closed , _ ) = leaf , bdd ) do
3047- bdd_leaf_intersection ( leaf , bdd , & map_leaf_intersection / 2 )
3048- end
3049-
3050- defp map_bdd_intersection ( bdd , bdd_leaf ( :closed , _ ) = leaf ) do
3051- bdd_leaf_intersection ( leaf , bdd , & map_leaf_intersection / 2 )
3052- end
3053-
3054- defp map_bdd_intersection ( { bdd_leaf ( :closed , _ ) = leaf , :bdd_top , u , d } , bdd ) do
3055- bdd_leaf_intersection ( leaf , bdd , & map_leaf_intersection / 2 )
3056- |> bdd_union ( map_bdd_intersection ( u , bdd ) )
3057- |> case do
3058- result when d == :bdd_bot -> result
3059- result -> bdd_union ( result , bdd_intersection ( bdd , { leaf , :bdd_bot , :bdd_bot , d } ) )
3060- end
3061- end
3062-
3063- defp map_bdd_intersection ( bdd , { bdd_leaf ( :closed , _ ) = leaf , :bdd_top , u , d } ) do
3064- bdd_leaf_intersection ( leaf , bdd , & map_leaf_intersection / 2 )
3065- |> bdd_union ( map_bdd_intersection ( u , bdd ) )
3066- |> case do
3067- result when d == :bdd_bot -> result
3068- result -> bdd_union ( result , bdd_intersection ( bdd , { leaf , :bdd_bot , :bdd_bot , d } ) )
3069- end
3070- end
3071-
3072- defp map_bdd_intersection ( { bdd_leaf ( :closed , _ ) = leaf , :bdd_bot , u , d } , bdd ) do
3073- case map_bdd_intersection ( u , bdd ) do
3074- result when d == :bdd_bot -> result
3075- result -> bdd_union ( result , bdd_intersection ( bdd , { leaf , :bdd_bot , :bdd_bot , d } ) )
3076- end
3077- end
3078-
3079- defp map_bdd_intersection ( bdd , { bdd_leaf ( :closed , _ ) = leaf , :bdd_bot , u , d } ) do
3080- case map_bdd_intersection ( u , bdd ) do
3081- result when d == :bdd_bot -> result
3082- result -> bdd_union ( result , bdd_intersection ( bdd , { leaf , :bdd_bot , :bdd_bot , d } ) )
3083- end
3084- end
3085-
3086- defp map_bdd_intersection ( bdd1 , bdd2 ) do
3087- bdd_intersection ( bdd1 , bdd2 )
3088- end
3032+ defp map_intersection ( bdd1 , bdd2 ) , do: bdd_intersection ( bdd1 , bdd2 , & map_leaf_intersection / 2 )
30893033
30903034 defp map_leaf_intersection ( bdd_leaf ( tag1 , fields1 ) , bdd_leaf ( tag2 , fields2 ) ) do
30913035 try do
@@ -6090,11 +6034,17 @@ defmodule Module.Types.Descr do
60906034 # the number of nodes in the tree. So whenever we have a leaf,
60916035 # we actually propagate it throughout the whole tree, cutting
60926036 # down nodes.
6093- defp bdd_intersection ( bdd_leaf ( _ , _ ) = leaf , bdd , leaf_intersection ) do
6037+ defguardp is_not_open ( leaf ) when elem ( leaf , 0 ) != :open
6038+
6039+ defp bdd_intersection ( bdd_leaf ( _ , _ ) = leaf1 , bdd_leaf ( _ , _ ) = leaf2 , leaf_intersection ) do
6040+ leaf_intersection . ( leaf1 , leaf2 )
6041+ end
6042+
6043+ defp bdd_intersection ( bdd_leaf ( _ , _ ) = leaf , bdd , leaf_intersection ) when is_not_open ( leaf ) do
60946044 bdd_leaf_intersection ( leaf , bdd , leaf_intersection )
60956045 end
60966046
6097- defp bdd_intersection ( bdd , bdd_leaf ( _ , _ ) = leaf , leaf_intersection ) do
6047+ defp bdd_intersection ( bdd , bdd_leaf ( _ , _ ) = leaf , leaf_intersection ) when is_not_open ( leaf ) do
60986048 bdd_leaf_intersection ( leaf , bdd , leaf_intersection )
60996049 end
61006050
@@ -6109,7 +6059,7 @@ defmodule Module.Types.Descr do
61096059 #
61106060 # (U2 or (not a1 and D2)) and B2
61116061 # (B2 and U2) or (B2 and not a1 and D2)
6112- defp bdd_intersection ( { leaf , :bdd_top , u , d } , bdd , leaf_intersection ) do
6062+ defp bdd_intersection ( { leaf , :bdd_top , u , d } , bdd , leaf_intersection ) when is_not_open ( leaf ) do
61136063 bdd_leaf_intersection ( leaf , bdd , leaf_intersection )
61146064 |> bdd_union ( bdd_intersection ( u , bdd , leaf_intersection ) )
61156065 |> case do
@@ -6118,7 +6068,7 @@ defmodule Module.Types.Descr do
61186068 end
61196069 end
61206070
6121- defp bdd_intersection ( bdd , { leaf , :bdd_top , u , d } , leaf_intersection ) do
6071+ defp bdd_intersection ( bdd , { leaf , :bdd_top , u , d } , leaf_intersection ) when is_not_open ( leaf ) do
61226072 bdd_leaf_intersection ( leaf , bdd , leaf_intersection )
61236073 |> bdd_union ( bdd_intersection ( u , bdd , leaf_intersection ) )
61246074 |> case do
@@ -6127,14 +6077,14 @@ defmodule Module.Types.Descr do
61276077 end
61286078 end
61296079
6130- defp bdd_intersection ( { leaf , :bdd_bot , u , d } , bdd , leaf_intersection ) do
6080+ defp bdd_intersection ( { leaf , :bdd_bot , u , d } , bdd , leaf_intersection ) when is_not_open ( leaf ) do
61316081 case bdd_intersection ( u , bdd , leaf_intersection ) do
61326082 result when d == :bdd_bot -> result
61336083 result -> bdd_union ( result , bdd_intersection ( bdd , { leaf , :bdd_bot , :bdd_bot , d } ) )
61346084 end
61356085 end
61366086
6137- defp bdd_intersection ( bdd , { leaf , :bdd_bot , u , d } , leaf_intersection ) do
6087+ defp bdd_intersection ( bdd , { leaf , :bdd_bot , u , d } , leaf_intersection ) when is_not_open ( leaf ) do
61386088 case bdd_intersection ( u , bdd , leaf_intersection ) do
61396089 result when d == :bdd_bot -> result
61406090 result -> bdd_union ( result , bdd_intersection ( bdd , { leaf , :bdd_bot , :bdd_bot , d } ) )
@@ -6156,6 +6106,9 @@ defmodule Module.Types.Descr do
61566106 bdd_leaf ( _ , _ ) ->
61576107 intersection . ( leaf , bdd )
61586108
6109+ { bdd_leaf ( :open , _ ) , _ , _ , _ } ->
6110+ bdd_intersection ( leaf , bdd )
6111+
61596112 { lit , c , u , _ } when lit == leaf ->
61606113 case bdd_union ( c , u ) do
61616114 :bdd_bot -> :bdd_bot
@@ -6169,12 +6122,13 @@ defmodule Module.Types.Descr do
61696122 bdd_difference ( bdd_leaf_intersection ( leaf , d , intersection ) , lit )
61706123 )
61716124
6172- with true <- c != :bdd_bot ,
6173- new_leaf = intersection . ( leaf , lit ) ,
6174- true <- new_leaf != :bdd_bot do
6175- bdd_union ( bdd_leaf_intersection ( new_leaf , c , intersection ) , rest )
6125+ if c == :bdd_bot do
6126+ rest
61766127 else
6177- _ -> rest
6128+ case intersection . ( leaf , lit ) do
6129+ :bdd_bot -> rest
6130+ new_leaf -> bdd_union ( bdd_leaf_intersection ( new_leaf , c , intersection ) , rest )
6131+ end
61786132 end
61796133 end
61806134 end
0 commit comments