SI-6942 more efficient unreachability analysis

Avoid blowing the stack/the analysis budget by more eagerly translating
the propositions that model matches to CNF.
First building a large proposition that represents the match,
and then converting to CNF tends to blow the stack.
Luckily, it's easy to convert to CNF as we go.

The optimization relies on `CNF(P1 /\ ... /\ PN) == CNF(P1) ++ CNF(...) ++ CNF(PN)`:

Normalizing a conjunction of propositions
    yields the same formula as
concatenating the normalized conjuncts.

CNF conversion is expensive for large propositions,
so we push it down into the conjunction and
then concatenate the resulting arrays of clauses (which is cheap).

(CNF converts a free-form proposition into an `Array[Set[Lit]]`, where:
 - the Array's elements are /\'ed together;
 - and the Set's elements are \/'ed;
 - a Lit is a possibly negated variable.)

NOTE:
 - removeVarEq may throw an AnalysisBudget.Exception
 - also reworked the interface used to build formula,
   so that we can more easily plug in SAT4J when the time comes

3 files changed, 300 insertions, 0 deletions

diff --git a/test/files/pos/t6942.flags b/test/files/pos/t6942.flags
new file mode 100644
index 0000000000..e8fb65d50c
--- /dev/null
+++ b/test/files/pos/t6942.flags
@@ -0,0 +1 @@
+-Xfatal-warnings
\ No newline at end of file
diff --git a/test/files/pos/t6942/Bar.java b/test/files/pos/t6942/Bar.java
new file mode 100644
index 0000000000..592f62efb4
--- /dev/null
+++ b/test/files/pos/t6942/Bar.java
@@ -0,0 +1,235 @@
+package foo;
+
+public enum Bar {
+    ANGUILLA                    /*("US")*/,
+    ANTIGUA_AND_BARBUDA         /*("US")*/,
+    ARGENTINA                   /*("US")*/,
+    ARUBA                       /*("US")*/,
+    BAHAMAS                     /*("US")*/,
+    BARBADOS                    /*("US")*/,
+    BELIZE                      /*("US")*/,
+    BERMUDA                     /*("US")*/,
+    BOLIVIA                     /*("US")*/,
+    BRAZIL                      /*("US")*/,
+    BRITISH_VIRGIN_ISLANDS      /*("US")*/,
+    CANADA                      /*("US")*/,
+    CAYMAN_ISLANDS              /*("US")*/,
+    CHILE                       /*("US")*/,
+    CHRISTMAS_ISLANDS           /*("US")*/,
+    COCOS                       /*("US")*/,
+    COLOMBIA                    /*("US")*/,
+    COSTA_RICA                  /*("US")*/,
+    CUBA                        /*("US")*/,
+    DOMINICA                    /*("US")*/,
+    DOMINICAN_REPUBLIC          /*("US")*/,
+    ECUADOR                     /*("US")*/,
+    EL_SALVADOR                 /*("US")*/,
+    FALKLAND_ISLANDS            /*("US")*/,
+    GRENADA                     /*("US")*/,
+    GUADALOUPE                  /*("US")*/,
+    GUATEMALA                   /*("US")*/,
+    HAITI                       /*("US")*/,
+    HONDURAS                    /*("US")*/,
+    NETHERLANDS_ANTILLES        /*("US")*/,
+    NICARAGUA                   /*("US")*/,
+    PANAMA                      /*("US")*/,
+    PARAGUAY                    /*("US")*/,
+    PERU                        /*("US")*/,
+    PUERTO_RICO                 /*("US")*/,
+    JAMAICA                     /*("US")*/,
+    MARTINIQUE                  /*("US")*/,
+    MEXICO                      /*("US")*/,
+    MONTSERRAT                  /*("US")*/,
+    ST_KITTS                    /*("US")*/,
+    ST_LUCIA                    /*("US")*/,
+    ST_VINCENT                  /*("US")*/,
+    SUPRA_NATIONAL              /*("US")*/,
+    TRINIDAD                    /*("US")*/,
+    TURKS_AND_CAICOS            /*("US")*/,
+    UNITED_STATES               /*("US")*/,
+    URUGUAY                     /*("US")*/,
+    VENEZUELA                   /*("US")*/,
+    VIRGIN_ISLANDS              /*("US")*/,
+
+    AUSTRALIA                   /*("AP")*/,
+    BANGLADESH                  /*("AP")*/,
+    BHUTAN                      /*("AP")*/,
+    CAMBODIA                    /*("AP")*/,
+    CHINA                       /*("AP")*/,
+    COOK_ISLANDS                /*("AP")*/,
+    EAST_TIMOR                  /*("AP")*/,
+    FIJI                        /*("AP")*/,
+    GUAM                        /*("AP")*/,
+    HONG_KONG                   /*("AP")*/,
+    INDIA                       /*("AP")*/,
+    INDONESIA                   /*("AP")*/,
+    JAPAN                       /*("AP")*/,
+    KIRIBATI                    /*("AP")*/,
+    LAOS                        /*("AP")*/,
+    MACAU                       /*("AP")*/,
+    MALAYSIA                    /*("AP")*/,
+    MICRONESIA                  /*("AP")*/,
+    MONGOLIA                    /*("AP")*/,
+    MYANMAR                     /*("AP")*/,
+    NEPAL                       /*("AP")*/,
+    NEW_CALEDONIA               /*("AP")*/,
+    NEW_ZEALAND                 /*("AP")*/,
+    NORFOLK_ISLAND              /*("AP")*/,
+    NORTH_KOREA                 /*("AP")*/,
+    PAKISTAN                    /*("AP")*/,
+    PALAU                       /*("AP")*/,
+    PAPUA_NEW_GUINEA            /*("AP")*/,
+    PHILIPPINES                 /*("AP")*/,
+    PITCAIRN_ISLANDS            /*("AP")*/,
+    SAMOA                       /*("AP")*/,
+    WEST_SAMOA                  /*("AP")*/,
+    SINGAPORE                   /*("AP")*/,
+    SOUTH_KOREA                 /*("AP")*/,
+    SRI_LANKA                   /*("AP")*/,
+    TAIWAN                      /*("AP")*/,
+    THAILAND                    /*("AP")*/,
+    TOKELAU                     /*("AP")*/,
+    TONGA                       /*("AP")*/,
+    TUVALU                      /*("AP")*/,
+    VANUATU                     /*("AP")*/,
+    VIETNAM                     /*("AP")*/,
+
+    AFGHANISTAN                 /*("EU")*/,
+    ALBANIA                     /*("EU")*/,
+    ALGERIA                     /*("EU")*/,
+    ANDORRA                     /*("EU")*/,
+    ANGOLA                      /*("EU")*/,
+    ARMENIA                     /*("EU")*/,
+    AUSTRIA                     /*("EU")*/,
+    AZERBAIJAN                  /*("EU")*/,
+    BAHRAIN                     /*("EU")*/,
+    BELARUS                     /*("EU")*/,
+    BELGIUM                     /*("EU")*/,
+    BENIN                       /*("EU")*/,
+    BOSNIA_AND_HERZEGOVINA      /*("EU")*/,
+    BOTSWANA                    /*("EU")*/,
+    BOUVET_ISLAND               /*("EU")*/,
+    BRUNEI                      /*("EU")*/,
+    BULGARIA                    /*("EU")*/,
+    BURKINA_FASO                /*("EU")*/,
+    BURUNDI                     /*("EU")*/,
+    CAMEROON                    /*("EU")*/,
+    CAPE_VERDE                  /*("EU")*/,
+    CHAD                        /*("EU")*/,
+    COMOROS                     /*("EU")*/,
+    CONGO                       /*("EU")*/,
+    CROATIA                     /*("EU")*/,
+    CYPRUS                      /*("EU")*/,
+    CZECH_REPUBLIC              /*("EU")*/,
+    DR_CONGO                    /*("EU")*/,
+    DENMARK                     /*("EU")*/,
+    DJIBOUTI                    /*("EU")*/,
+    EGYPT                       /*("EU")*/,
+    EQUATORIAL_GUINEA           /*("EU")*/,
+    ERITREA                     /*("EU")*/,
+    ESTONIA                     /*("EU")*/,
+    ETHIOPIA                    /*("EU")*/,
+    FAEROE_ISLANDS              /*("EU")*/,
+    FINLAND                     /*("EU")*/,
+    FRANCE                      /*("EU")*/,
+    FRENCH_GUIANA               /*("EU")*/,
+    GABON                       /*("EU")*/,
+    GAMBIA                      /*("EU")*/,
+    GEORGIA                     /*("EU")*/,
+    GERMANY                     /*("EU")*/,
+    GHANA                       /*("EU")*/,
+    GIBRALTAR                   /*("EU")*/,
+    GREAT_BRITAIN               /*("EU")*/,
+    GREECE                      /*("EU")*/,
+    GREENLAND                   /*("EU")*/,
+    GUINEA                      /*("EU")*/,
+    GUINEA_BISSAU               /*("EU")*/,
+    GUYANA                      /*("EU")*/,
+    HUNGARY                     /*("EU")*/,
+    ICELAND                     /*("EU")*/,
+    IRAN                        /*("EU")*/,
+    IRAQ                        /*("EU")*/,
+    IRELAND                     /*("EU")*/,
+    ISLE_OF_MAN                 /*("EU")*/,
+    ISRAEL                      /*("EU")*/,
+    ITALY                       /*("EU")*/,
+    IVORY_COAST                 /*("EU")*/,
+    JERSEY                      /*("EU")*/,
+    JORDAN                      /*("EU")*/,
+    KAZAKHSTAN                  /*("EU")*/,
+    KENYA                       /*("EU")*/,
+    KUWAIT                      /*("EU")*/,
+    KYRGYZSTAN                  /*("EU")*/,
+    LATVIA                      /*("EU")*/,
+    LEBANON                     /*("EU")*/,
+    LESOTHO                     /*("EU")*/,
+    LIBERIA                     /*("EU")*/,
+    LIBYA                       /*("EU")*/,
+    LIECHTENSTEIN               /*("EU")*/,
+    LITHUANIA                   /*("EU")*/,
+    LUXEMBOURG                  /*("EU")*/,
+    MACEDONIA                   /*("EU")*/,
+    MADAGASCAR                  /*("EU")*/,
+    MALAWI                      /*("EU")*/,
+    MALDIVES                    /*("EU")*/,
+    MALI                        /*("EU")*/,
+    MALTA                       /*("EU")*/,
+    MARSHALL_ISLAND             /*("EU")*/,
+    MAURITANIA                  /*("EU")*/,
+    MAURITIUS                   /*("EU")*/,
+    MAYOTTE                     /*("EU")*/,
+    MOLDOVA                     /*("EU")*/,
+    MONACO                      /*("EU")*/,
+    MOROCCO                     /*("EU")*/,
+    MOZAMBIQUE                  /*("EU")*/,
+    NAMIBIA                     /*("EU")*/,
+    NETHERLANDS                 /*("EU")*/,
+    NIGER_REPUBLIC              /*("EU")*/,
+    NIGERIA                     /*("EU")*/,
+    NORWAY                      /*("EU")*/,
+    OMAN                        /*("EU")*/,
+    PALESTINE                   /*("EU")*/,
+    POLAND                      /*("EU")*/,
+    PORTUGAL                    /*("EU")*/,
+    QATAR                       /*("EU")*/,
+    REUNION                     /*("EU")*/,
+    ROMANIA                     /*("EU")*/,
+    RUSSIA                      /*("EU")*/,
+    RWANDA                      /*("EU")*/,
+    SAN_MARINO                  /*("EU")*/,
+    SAO_TOME                    /*("EU")*/,
+    SAUDI_ARABIA                /*("EU")*/,
+    SENEGAL                     /*("EU")*/,
+    SERBIA                      /*("EU")*/,
+    SEYCHELLES                  /*("EU")*/,
+    SEIRRA_LEONE                /*("EU")*/,
+    SLOVAKIA                    /*("EU")*/,
+    SLOVENIA                    /*("EU")*/,
+    SOMALIA                     /*("EU")*/,
+    SOUTH_AFRICA                /*("EU")*/,
+    SPAIN                       /*("EU")*/,
+    ST_HELENA                   /*("EU")*/,
+    SUDAN                       /*("EU")*/,
+    SURINAME                    /*("EU")*/,
+    SVALBARD                    /*("EU")*/,
+    SWAZILAND                   /*("EU")*/,
+    SWEDEN                      /*("EU")*/,
+    SWITZERLAND                 /*("EU")*/,
+    SYRIA                       /*("EU")*/,
+    TAJIKSTAN                   /*("EU")*/,
+    TANZANIA                    /*("EU")*/,
+    TOGO                        /*("EU")*/,
+    TUNISIA                     /*("EU")*/,
+    TURKEY                      /*("EU")*/,
+    TURKMENISTAN                /*("EU")*/,
+    UAE                         /*("EU")*/,
+    UGANDA                      /*("EU")*/,
+    UKRAINE                     /*("EU")*/,
+    UZBEKISTAN                  /*("EU")*/,
+    VATICAN_CITY                /*("EU")*/,
+    WESTERN_SAHARA              /*("EU")*/,
+    YEMEN                       /*("EU")*/,
+    ZAMBIA                      /*("EU")*/,
+    ZIMBABWE                    /*("EU")*/;
+
+}
\ No newline at end of file
diff --git a/test/files/pos/t6942/t6942.scala b/test/files/pos/t6942/t6942.scala
new file mode 100644
index 0000000000..77963d2634
--- /dev/null
+++ b/test/files/pos/t6942/t6942.scala
@@ -0,0 +1,64 @@
+// not a peep out of the pattern matcher's unreachability analysis
+// its budget should suffice for these simple matches (they do have a large search space)
+class Test {
+  import foo.Bar // a large enum
+  def exhaustUnreachabilitysStack_ENUM_STYLE = (null: Bar) match {
+    case Bar.BULGARIA =>
+    case _            =>
+  }
+
+  // lots of strings
+  def exhaustUnreachabilitysStack_StringStyle = "foo" match {
+    case "a"          =>
+    case "b"          =>
+    case "c"          =>
+    case "d"          =>
+    case "e"          =>
+    case "f"          =>
+    case "aa"         =>
+    case "ba"         =>
+    case "ca"         =>
+    case "da"         =>
+    case "ea"         =>
+    case "f1a"        =>
+    case "a1a"        =>
+    case "b1a"        =>
+    case "c1a"        =>
+    case "d1a"        =>
+    case "e1a"        =>
+    case "f1a2"       =>
+    case "f1a0"       =>
+    case "a1a2"       =>
+    case "b1a2"       =>
+    case "c1a2"       =>
+    case "d1a2"       =>
+    case "e1a2"       =>
+    case "f1a3"       =>
+    case "_a"         =>
+    case "_b"         =>
+    case "_c"         =>
+    case "_d"         =>
+    case "_e"         =>
+    case "_f"         =>
+    case "_aa"        =>
+    case "_ba"        =>
+    case "_ca"        =>
+    case "_da"        =>
+    case "_ea"        =>
+    case "_f1a"       =>
+    case "_a1a"       =>
+    case "_b1a"       =>
+    case "_c1a"       =>
+    case "_d1a"       =>
+    case "_e1a"       =>
+    case "_f1a0"      =>
+    case "_f1a2"      =>
+    case "_a1a2"      =>
+    case "_b1a2"      =>
+    case "_c1a2"      =>
+    case "_d1a2"      =>
+    case "_e1a2"      =>
+    case "_f1a3"      =>
+    case _            =>
+  }
+}