@@ -5830,7 +5830,7 @@ defmodule Module.Types.Descr do
58305830
58315831 { :eq , { lit , c1 , u1 , d1 } , { _ , c2 , u2 , d2 } } ->
58325832 # The formula is:
5833- # {a1, (C1 or U1) and not (C2 or U2), :bottom , (D1 or U1) and not (D2 or U2)} when a1 == a2
5833+ # {a1, (C1 or U1) and not (C2 or U2), :bdd_bot , (D1 or U1) and not (D2 or U2)} when a1 == a2
58345834 #
58355835 # Constrained: (C1 and not C2 and not U2) or (U1 and not C2 and not U2)
58365836 # Dual: (D1 and not D2 and not U2) or (U1 and not D2 and not U2)
@@ -5914,8 +5914,11 @@ defmodule Module.Types.Descr do
59145914 other -> other
59155915 end
59165916
5917+ :none when bdd2 < a1 ->
5918+ { bdd2 , :bdd_bot , :bdd_bot , bdd1 }
5919+
59175920 :none ->
5918- bdd_difference ( bdd1 , bdd2 )
5921+ { bdd2 , :bdd_bot , :bdd_bot , bdd_union ( u1 , d1 ) }
59195922 end
59205923 end
59215924
@@ -5955,8 +5958,11 @@ defmodule Module.Types.Descr do
59555958 other -> other
59565959 end
59575960
5961+ :none when bdd1 < a2 ->
5962+ { bdd1 , bdd_negation ( bdd2 ) , :bdd_bot , :bdd_bot }
5963+
59585964 :none ->
5959- bdd_difference ( bdd1 , bdd2 )
5965+ bdd1 |> bdd_difference ( c2 , leaf_compare ) |> bdd_difference ( u2 , leaf_compare )
59605966 end
59615967 end
59625968
@@ -5990,7 +5996,7 @@ defmodule Module.Types.Descr do
59905996
59915997 # Notice that (a, c1, u1, d1) and (a, c2, u2, d2) is described as:
59925998 #
5993- # {a, (C1 or U1) and (C2 or U2), :bottom , (D1 or U1) and (D2 or U2)}
5999+ # {a, (C1 or U1) and (C2 or U2), :bdd_bot , (D1 or U1) and (D2 or U2)}
59946000 #
59956001 # However, if we distribute the intersection over the unions, we find a
59966002 # common term, U1 and U2, leading to:
0 commit comments