Skip to content

Commit bffb696

Browse files
committed
Implement one key difference for leaf bdd difference
This allows us to implement previous as a series of unions, which performs better across all cases. Closes #15195.
1 parent c39d9ea commit bffb696

2 files changed

Lines changed: 147 additions & 99 deletions

File tree

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

Lines changed: 134 additions & 79 deletions
Original file line numberDiff line numberDiff line change
@@ -2376,14 +2376,14 @@ defmodule Module.Types.Descr do
23762376
do: :bdd_bot,
23772377
else: bdd_leaf(list1, difference(last1, last2))
23782378
else
2379-
bdd_difference(bdd1, bdd2, &list_leaf_difference/2)
2379+
bdd_difference(bdd1, bdd2, &list_leaf_difference/3)
23802380
end
23812381
end
23822382

23832383
defp list_difference(bdd1, bdd2),
2384-
do: bdd_difference(bdd1, bdd2, &list_leaf_difference/2)
2384+
do: bdd_difference(bdd1, bdd2, &list_leaf_difference/3)
23852385

2386-
defp list_leaf_difference(bdd_leaf(list1, last1), bdd_leaf(list2, last2)) do
2386+
defp list_leaf_difference(bdd_leaf(list1, last1), bdd_leaf(list2, last2), _) do
23872387
if disjoint?(list1, list2) or disjoint?(last1, last2) do
23882388
:disjoint
23892389
else
@@ -3077,68 +3077,73 @@ defmodule Module.Types.Descr do
30773077
end
30783078
end
30793079

3080-
# Optimizations on single maps.
3081-
defp map_difference(bdd_leaf(tag, fields) = map1, bdd_leaf(neg_tag, neg_fields) = map2) do
3082-
# Case 1: we are removing an open map with one field. Just do the difference of that field.
3083-
case neg_fields do
3084-
[{key, value}] when neg_tag == :open ->
3085-
{found?, pos_value} =
3086-
case fields_find(key, fields) do
3087-
{:ok, value} -> {true, value}
3088-
:error -> {false, map_key_tag_to_type(tag)}
3089-
end
3080+
defp map_difference(_, bdd_leaf(:open, [])),
3081+
do: :bdd_bot
30903082

3091-
if tag == :closed and not found? and not is_optional_static(value) do
3092-
map1
3093-
else
3094-
t_diff = difference(fields_get(fields, key, pos_value), value)
3083+
defp map_difference(bdd_leaf(tag, fields) = map1, bdd_leaf(:open, [{key, v2}])) do
3084+
{found?, v1} =
3085+
case fields_find(key, fields) do
3086+
{:ok, value} -> {true, value}
3087+
:error -> {false, map_key_tag_to_type(tag)}
3088+
end
30953089

3096-
if empty?(t_diff) do
3097-
:bdd_bot
3098-
else
3099-
bdd_leaf(tag, fields_store(key, t_diff, fields))
3100-
end
3101-
end
3090+
if tag == :closed and not found? and not is_optional_static(v2) do
3091+
map1
3092+
else
3093+
v_diff = difference(v1, v2)
31023094

3103-
_ when is_atom(tag) and is_atom(neg_tag) ->
3104-
case map_difference_strategy(fields, neg_fields, tag, neg_tag, true) do
3105-
:disjoint ->
3106-
bdd_leaf(tag, fields)
3095+
if empty?(v_diff) do
3096+
:bdd_bot
3097+
else
3098+
bdd_leaf(tag, fields_store(key, v_diff, fields))
3099+
end
3100+
end
3101+
end
31073102

3108-
:left_subtype_of_right ->
3109-
:bdd_bot
3103+
defp map_difference(bdd1, bdd2),
3104+
do: bdd_difference(bdd1, bdd2, &map_leaf_difference/3)
31103105

3111-
{:one_key_difference, key, v1, v2} ->
3112-
t_diff = difference(fields_get(fields, key, v1), v2)
3106+
defp map_leaf_difference(bdd_leaf(tag, fields), bdd_leaf(neg_tag, neg_fields), type) do
3107+
case map_difference_strategy(fields, neg_fields, tag, neg_tag) do
3108+
:disjoint ->
3109+
:disjoint
31133110

3114-
if empty?(t_diff) do
3115-
:bdd_bot
3116-
else
3117-
bdd_leaf(tag, fields_store(key, t_diff, fields))
3118-
end
3111+
:left_subtype_of_right ->
3112+
:subtype
31193113

3120-
:none ->
3121-
bdd_difference(map1, map2)
3122-
end
3114+
{:one_key_difference, key, v1, v2} ->
3115+
map_leaf_one_key_difference(tag, fields, key, v1, v2, type)
31233116

3124-
_ ->
3125-
bdd_difference(map1, map2, &map_leaf_difference/2)
3117+
:none ->
3118+
:none
31263119
end
31273120
end
31283121

3129-
defp map_difference(bdd_leaf(:open, []), bdd2),
3130-
do: bdd_negation(bdd2)
3122+
defp map_leaf_one_key_difference(tag, fields, key, v1, v2, type) do
3123+
v_diff = difference(v1, v2)
31313124

3132-
defp map_difference(bdd1, bdd2) do
3133-
bdd_difference(bdd1, bdd2, &map_leaf_difference/2)
3134-
end
3125+
if empty?(v_diff) do
3126+
:subtype
3127+
else
3128+
a_diff = bdd_leaf(tag, fields_store(key, v_diff, fields))
31353129

3136-
defp map_leaf_difference(bdd_leaf(tag, fields), bdd_leaf(neg_tag, neg_fields)) do
3137-
case map_difference_strategy(fields, neg_fields, tag, neg_tag, false) do
3138-
:disjoint -> :disjoint
3139-
:left_subtype_of_right -> :subtype
3140-
{:one_key_difference, _, v1, v2} -> if subtype?(v1, v2), do: :subtype, else: :none
3141-
:none -> :none
3130+
a_type =
3131+
case type do
3132+
:none ->
3133+
:bdd_bot
3134+
3135+
:union ->
3136+
bdd_leaf(tag, fields_store(key, union(v1, v2), fields))
3137+
3138+
:intersection ->
3139+
v_int = intersection(v1, v2)
3140+
3141+
if empty?(v_int),
3142+
do: :bdd_bot,
3143+
else: bdd_leaf(tag, fields_store(key, v_int, fields))
3144+
end
3145+
3146+
{:one_key_difference, a_diff, a_type}
31423147
end
31433148
end
31443149

@@ -4499,7 +4504,7 @@ defmodule Module.Types.Descr do
44994504
if empty_intersection? do
45004505
{acc_fields, acc_negs}
45014506
else
4502-
case map_difference_strategy(acc_fields, neg_fields, tag, neg_tag, true) do
4507+
case map_difference_strategy(acc_fields, neg_fields, tag, neg_tag) do
45034508
{:one_key_difference, key, v1, v2} ->
45044509
{fields_store(key, difference(v1, v2), acc_fields), acc_negs}
45054510

@@ -4516,16 +4521,16 @@ defmodule Module.Types.Descr do
45164521
end)
45174522
end
45184523

4519-
defp map_difference_strategy(fields1, fields2, tag1, tag2, okd?) do
4524+
defp map_difference_strategy(fields1, fields2, tag1, tag2) do
45204525
if is_atom(tag1) and is_atom(tag2) do
45214526
status = if tag1 == tag2 or tag2 == :open, do: :all_equal, else: :none
4522-
map_difference_strategy(fields1, fields2, tag1, tag2, okd?, status)
4527+
map_difference_strategy(fields1, fields2, tag1, tag2, status)
45234528
else
45244529
:none
45254530
end
45264531
end
45274532

4528-
defp map_difference_strategy([{k1, value} | t1], [{k2, _} | _] = l2, tag1, tag2, okd?, status)
4533+
defp map_difference_strategy([{k1, value} | t1], [{k2, _} | _] = l2, tag1, tag2, status)
45294534
when k1 < k2 do
45304535
# Left side has a key the right side does not have,
45314536
# left can only be a subtype if the right side is open.
@@ -4535,71 +4540,70 @@ defmodule Module.Types.Descr do
45354540
if not is_optional_static(value) do
45364541
:disjoint
45374542
else
4538-
map_difference_strategy(t1, l2, tag1, tag2, okd?, :none)
4543+
map_difference_strategy(t1, l2, tag1, tag2, :none)
45394544
end
45404545

45414546
:all_equal ->
4542-
map_difference_strategy(t1, l2, tag1, tag2, okd?, :left_subtype_of_right)
4547+
map_difference_strategy(t1, l2, tag1, tag2, :left_subtype_of_right)
45434548

45444549
{:one_key_difference, _, p1, p2} ->
45454550
if subtype?(p1, p2),
4546-
do: map_difference_strategy(t1, l2, tag1, tag2, okd?, :left_subtype_of_right),
4551+
do: map_difference_strategy(t1, l2, tag1, tag2, :left_subtype_of_right),
45474552
else: :none
45484553

45494554
:left_subtype_of_right ->
4550-
map_difference_strategy(t1, l2, tag1, tag2, okd?, :left_subtype_of_right)
4555+
map_difference_strategy(t1, l2, tag1, tag2, :left_subtype_of_right)
45514556

45524557
_ ->
45534558
:none
45544559
end
45554560
end
45564561

4557-
defp map_difference_strategy([{k1, _} | _] = l1, [{k2, value} | t2], tag1, tag2, okd?, _status)
4562+
defp map_difference_strategy([{k1, _} | _] = l1, [{k2, value} | t2], tag1, tag2, _status)
45584563
when k1 > k2 do
45594564
# Right side has a key the left side does not have,
45604565
# if left-side is closed, they are disjoint.
45614566
if tag1 == :closed and not is_optional_static(value) do
45624567
:disjoint
45634568
else
4564-
map_difference_strategy(l1, t2, tag1, tag2, okd?, :none)
4569+
map_difference_strategy(l1, t2, tag1, tag2, :none)
45654570
end
45664571
end
45674572

4568-
defp map_difference_strategy([{_, v} | t1], [{_, v} | t2], tag1, tag2, okd?, status) do
4573+
defp map_difference_strategy([{_, v} | t1], [{_, v} | t2], tag1, tag2, status) do
45694574
# Same key and same value, nothing changes
4570-
map_difference_strategy(t1, t2, tag1, tag2, okd?, status)
4575+
map_difference_strategy(t1, t2, tag1, tag2, status)
45714576
end
45724577

4573-
defp map_difference_strategy([{k1, v1} | t1], [{_, v2} | t2], tag1, tag2, okd?, status) do
4578+
defp map_difference_strategy([{k1, v1} | t1], [{_, v2} | t2], tag1, tag2, status) do
45744579
# They have the same key but different values
45754580
if disjoint?(v1, v2) do
45764581
:disjoint
45774582
else
45784583
case status do
4579-
# Only upgrade to one key difference if we can do something with it
4580-
:all_equal when okd? and tag1 == tag2 ->
4581-
map_difference_strategy(t1, t2, tag1, tag2, okd?, {:one_key_difference, k1, v1, v2})
4584+
:all_equal when tag1 == tag2 ->
4585+
map_difference_strategy(t1, t2, tag1, tag2, {:one_key_difference, k1, v1, v2})
45824586

45834587
{:one_key_difference, _key, p1, p2} ->
45844588
if subtype?(p1, p2) and subtype?(v1, v2) do
4585-
map_difference_strategy(t1, t2, tag1, tag2, okd?, :left_subtype_of_right)
4589+
map_difference_strategy(t1, t2, tag1, tag2, :left_subtype_of_right)
45864590
else
45874591
:none
45884592
end
45894593

45904594
_ ->
45914595
if status in [:all_equal, :left_subtype_of_right] and subtype?(v1, v2),
4592-
do: map_difference_strategy(t1, t2, tag1, tag2, okd?, :left_subtype_of_right),
4593-
else: map_difference_strategy(t1, t2, tag1, tag2, okd?, :none)
4596+
do: map_difference_strategy(t1, t2, tag1, tag2, :left_subtype_of_right),
4597+
else: map_difference_strategy(t1, t2, tag1, tag2, :none)
45944598
end
45954599
end
45964600
end
45974601

4598-
defp map_difference_strategy([], [], _tag1, _tag2, _okd?, status) do
4602+
defp map_difference_strategy([], [], _tag1, _tag2, status) do
45994603
if status == :all_equal, do: :left_subtype_of_right, else: status
46004604
end
46014605

4602-
defp map_difference_strategy(l1, l2, tag1, tag2, _okd?, status) do
4606+
defp map_difference_strategy(l1, l2, tag1, tag2, status) do
46034607
cond do
46044608
tag2 == :open and l2 == [] ->
46054609
case status do
@@ -4991,9 +4995,9 @@ defmodule Module.Types.Descr do
49914995
do: bdd_negation(bdd2)
49924996

49934997
defp tuple_difference(bdd1, bdd2),
4994-
do: bdd_difference(bdd1, bdd2, &tuple_leaf_difference/2)
4998+
do: bdd_difference(bdd1, bdd2, &tuple_leaf_difference/3)
49954999

4996-
defp tuple_leaf_difference(bdd_leaf(tag1, elements1), bdd_leaf(tag2, elements2)) do
5000+
defp tuple_leaf_difference(bdd_leaf(tag1, elements1), bdd_leaf(tag2, elements2), _) do
49975001
case tuple_sizes_strategy(tag1, length(elements1), tag2, length(elements2)) do
49985002
:disjoint -> :disjoint
49995003
other -> tuple_leaf_difference(elements1, elements2, other == :left_subtype_of_right)
@@ -5880,6 +5884,17 @@ defmodule Module.Types.Descr do
58805884

58815885
## Optimize differences
58825886

5887+
defp bdd_difference(bdd_leaf(_, _) = bdd1, bdd_leaf(_, _) = bdd2, leaf_compare) do
5888+
case leaf_compare.(bdd1, bdd2, :none) do
5889+
:disjoint -> bdd1
5890+
{:one_key_difference, a_diff, _a_none} -> a_diff
5891+
:subtype -> :bdd_bot
5892+
:none when bdd2 < bdd1 -> {bdd2, :bdd_bot, :bdd_bot, bdd1}
5893+
:none when bdd1 < bdd2 -> {bdd1, bdd_negation(bdd2), :bdd_bot, :bdd_bot}
5894+
:none -> :bdd_bot
5895+
end
5896+
end
5897+
58835898
# For the right-side being a leaf, we have:
58845899
#
58855900
# ((a1 and C1) or U1 or (not a1 and D1)) and not a2
@@ -5891,9 +5906,16 @@ defmodule Module.Types.Descr do
58915906
# If subtype?(a1, a2), we end up with:
58925907
#
58935908
# (U1 and not d2) or (D1 and not a2)
5909+
#
5910+
# If one key difference, then we compute the difference
5911+
# and the union of said keys, returning a_union and a_diff:
5912+
#
5913+
# ((a1 and C1) or U1 or (not a1 and D1)) and not a2
5914+
# (a_diff and C1) or (U1 and not a2) or (not a1 and not a2 and D1)
5915+
#
58945916
defp bdd_difference({a1, c1, u1, d1} = bdd1, bdd_leaf(_, _) = bdd2, leaf_compare)
58955917
when is_tuple(bdd2) do
5896-
case leaf_compare.(a1, bdd2) do
5918+
case leaf_compare.(a1, bdd2, :union) do
58975919
:disjoint ->
58985920
res =
58995921
bdd_union(
@@ -5903,6 +5925,11 @@ defmodule Module.Types.Descr do
59035925

59045926
if c1 == :bdd_bot, do: res, else: bdd_union(res, {a1, c1, :bdd_bot, :bdd_bot})
59055927

5928+
{:one_key_difference, a_diff, a_union} ->
5929+
bdd_intersection(a_diff, c1)
5930+
|> bdd_union(bdd_difference(u1, bdd2, leaf_compare))
5931+
|> bdd_union(bdd_difference(d1, a_union, leaf_compare))
5932+
59065933
:subtype ->
59075934
bdd_union(bdd_difference(u1, bdd2, leaf_compare), bdd_difference(d1, bdd2, leaf_compare))
59085935

@@ -5942,15 +5969,43 @@ defmodule Module.Types.Descr do
59425969
# a1 and (a2 or not D2) = a1 (a1 and a2 = a1)
59435970
#
59445971
# Result: a1 and not C2 and not U2
5972+
#
5973+
# If one key difference, then we compute the difference
5974+
# and the intersection of said keys, returning a_union and a_diff:
5975+
#
5976+
# a1 and not (a2 and C2) and not U2 and (a2 or not D2)
5977+
# ((a1 and not a2) or (a1 and not C2)) and not U2 and (a2 or not D2)
5978+
# (a_diff or (a1 and not C2)) and not U2 and (a2 or not D2)
5979+
#
5980+
# Now distribute into (a2 or not D2):
5981+
#
5982+
# ((a_diff and (a2 or not D2)) or
5983+
# ((a1 and not C2) and (a2 or not D2))) and not U2
5984+
# ((a_diff and not D2) or
5985+
# (a_int and not C2) or
5986+
# (a1 and not C2 and not D2)) and not U2
5987+
#
5988+
# Now, we know that a1 is a_diff or a_int, which means
5989+
# (a1 and not C2 and not D2) is a subset of the other two
5990+
# expressions, so we end up with:
5991+
#
5992+
# ((a_diff and not D2) or (a_int and not C2)) and not U2
5993+
#
59455994
defp bdd_difference(bdd_leaf(_, _) = bdd1, bdd2, leaf_compare) when is_tuple(bdd2) do
59465995
{a2, c2, u2, d2} = bdd_expand(bdd2)
59475996

5948-
case leaf_compare.(bdd1, a2) do
5997+
case leaf_compare.(bdd1, a2, :intersection) do
59495998
:disjoint ->
5950-
bdd1 |> bdd_difference(u2, leaf_compare) |> bdd_difference(d2, leaf_compare)
5999+
bdd1 |> bdd_difference(d2, leaf_compare) |> bdd_difference(u2, leaf_compare)
6000+
6001+
{:one_key_difference, a_diff, a_int} ->
6002+
bdd_union(
6003+
a_diff |> bdd_difference(d2, leaf_compare) |> bdd_difference(u2, leaf_compare),
6004+
a_int |> bdd_difference(c2, leaf_compare) |> bdd_difference(u2, leaf_compare)
6005+
)
59516006

59526007
:subtype ->
5953-
bdd1 |> bdd_difference(u2, leaf_compare) |> bdd_difference(c2, leaf_compare)
6008+
bdd1 |> bdd_difference(c2, leaf_compare) |> bdd_difference(u2, leaf_compare)
59546009

59556010
:none when a2 < bdd1 ->
59566011
{a2, bdd_difference(bdd1, bdd_union(c2, u2), leaf_compare), :bdd_bot,

0 commit comments

Comments
 (0)