@@ -4458,14 +4458,17 @@ defmodule Module.Types.Descr do
4458
4458
{ :gt , bdd1 , { lit2 , c2 , u2 , d2 } } ->
4459
4459
{ lit2 , c2 , bdd_union ( bdd1 , u2 ) , d2 }
4460
4460
4461
- { :eq , { _ , _ } , bdd2 } ->
4462
- bdd2
4463
-
4464
- { :eq , bdd1 , { _ , _ } } ->
4465
- bdd1
4466
-
4467
4461
{ :eq , { lit , c1 , u1 , d1 } , { _ , c2 , u2 , d2 } } ->
4468
4462
{ lit , bdd_union ( c1 , c2 ) , bdd_union ( u1 , u2 ) , bdd_union ( d1 , d2 ) }
4463
+
4464
+ { :eq , { lit , _ , u1 , d1 } , _ } ->
4465
+ { lit , :bdd_top , u1 , d1 }
4466
+
4467
+ { :eq , _ , { lit , _ , u2 , d2 } } ->
4468
+ { lit , :bdd_top , u2 , d2 }
4469
+
4470
+ { :eq , _ , _ } ->
4471
+ bdd1
4469
4472
end
4470
4473
end
4471
4474
end
@@ -4508,14 +4511,14 @@ defmodule Module.Types.Descr do
4508
4511
bdd_difference ( bdd_union ( d1 , u1 ) , bdd_union ( d2 , u2 ) ) }
4509
4512
end
4510
4513
4511
- { :eq , { _ , _ } , { _ , _ } } ->
4512
- :bdd_bot
4513
-
4514
4514
{ :eq , _ , { lit , c2 , u2 , _d2 } } ->
4515
4515
{ lit , bdd_negation ( bdd_union ( c2 , u2 ) ) , :bdd_bot , :bdd_bot }
4516
4516
4517
4517
{ :eq , { lit , _c1 , u1 , d1 } , _ } ->
4518
4518
{ lit , :bdd_bot , :bdd_bot , bdd_union ( d1 , u1 ) }
4519
+
4520
+ { :eq , _ , _ } ->
4521
+ :bdd_bot
4519
4522
end
4520
4523
end
4521
4524
end
@@ -4559,12 +4562,6 @@ defmodule Module.Types.Descr do
4559
4562
{ lit2 , bdd_intersection ( bdd1 , c2 ) , bdd_intersection ( bdd1 , u2 ) ,
4560
4563
bdd_intersection ( bdd1 , d2 ) }
4561
4564
4562
- { :eq , { _ , _ } = bdd1 , _ } ->
4563
- bdd1
4564
-
4565
- { :eq , _ , { _ , _ } = bdd2 } ->
4566
- bdd2
4567
-
4568
4565
# Notice that (l ? c1, u1, d1) and (l ? c2, u2, d2) is, on paper, equivalent to
4569
4566
# [(l /\ c1) \/ u1 \/ (not l /\ d1)] and [(l /\ c2) \/ u2 \/ (not l /\ d2)]
4570
4567
# which is equivalent, by distributivity of intersection over union, to
@@ -4580,6 +4577,15 @@ defmodule Module.Types.Descr do
4580
4577
{ lit , bdd_union ( bdd_intersection_union ( c1 , c2 , u2 ) , bdd_intersection ( u1 , c2 ) ) ,
4581
4578
bdd_intersection ( u1 , u2 ) ,
4582
4579
bdd_union ( bdd_intersection_union ( d1 , u2 , d2 ) , bdd_intersection ( u1 , d2 ) ) }
4580
+
4581
+ { :eq , { lit , c1 , u1 , _ } , _ } ->
4582
+ { lit , bdd_union ( c1 , u1 ) , :bdd_bot , :bdd_bot }
4583
+
4584
+ { :eq , _ , { lit , c2 , u2 , _ } } ->
4585
+ { lit , bdd_union ( c2 , u2 ) , :bdd_bot , :bdd_bot }
4586
+
4587
+ { :eq , bdd , _ } ->
4588
+ bdd
4583
4589
end
4584
4590
end
4585
4591
end
0 commit comments