Also optimize bottoms in leaf bdd intersections

Author: josevalim

lib/elixir/lib/module/types/descr.ex

@@ -3069,6 +3069,20 @@ defmodule Module.Types.Descr do
     end
   end
 
+  defp map_bdd_intersection({bdd_leaf(:closed, _) = leaf, :bdd_bot, u, d}, bdd) do
+    case map_bdd_intersection(u, bdd) do
+      result when d == :bdd_bot -> result
+      result -> bdd_union(result, bdd_intersection(bdd, {leaf, :bdd_bot, :bdd_bot, d}))
+    end
+  end
+
+  defp map_bdd_intersection(bdd, {bdd_leaf(:closed, _) = leaf, :bdd_bot, u, d}) do
+    case map_bdd_intersection(u, bdd) do
+      result when d == :bdd_bot -> result
+      result -> bdd_union(result, bdd_intersection(bdd, {leaf, :bdd_bot, :bdd_bot, d}))
+    end
+  end
+
   defp map_bdd_intersection(bdd1, bdd2) do
     bdd_intersection(bdd1, bdd2)
   end
@@ -6085,14 +6099,16 @@ defmodule Module.Types.Descr do
   end
 
   # Take two BDDs, B1 = {a1, C1, U2, D2} and B2.
-  # We can treat a1 as a leaf if C1 = :bdd_top.
-  # Then we have:
+  #
+  # When C1 = :bdd_top, we have:
   #
   #     ((a1 and C1) or U2 or (not a1 and D2)) and B2
+  #     (a1 and B2) or (B2 and U2) or (B2 and not a1 and D2)
   #
-  # Which is equivalent to:
+  # When C1 = :bdd_bot, we have:
   #
-  #     (a1 and B2) or (B2 and U2) or (B2 and not a1 and D2)
+  #     (U2 or (not a1 and D2)) and B2
+  #     (B2 and U2) or (B2 and not a1 and D2)
   defp bdd_intersection({leaf, :bdd_top, u, d}, bdd, leaf_intersection) do
     bdd_leaf_intersection(leaf, bdd, leaf_intersection)
     |> bdd_union(bdd_intersection(u, bdd, leaf_intersection))
@@ -6111,6 +6127,20 @@ defmodule Module.Types.Descr do
     end
   end
 
+  defp bdd_intersection({leaf, :bdd_bot, u, d}, bdd, leaf_intersection) do
+    case bdd_intersection(u, bdd, leaf_intersection) do
+      result when d == :bdd_bot -> result
+      result -> bdd_union(result, bdd_intersection(bdd, {leaf, :bdd_bot, :bdd_bot, d}))
+    end
+  end
+
+  defp bdd_intersection(bdd, {leaf, :bdd_bot, u, d}, leaf_intersection) do
+    case bdd_intersection(u, bdd, leaf_intersection) do
+      result when d == :bdd_bot -> result
+      result -> bdd_union(result, bdd_intersection(bdd, {leaf, :bdd_bot, :bdd_bot, d}))
+    end
+  end
+
   defp bdd_intersection(bdd1, bdd2, _leaf_intersection) do
     bdd_intersection(bdd1, bdd2)
   end