Permalink
Browse files

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
  • Loading branch information...
1 parent 1a63cf8 commit f5397818aa6c9822ce6593e3eec02edfffdc4f2e @adriaanm adriaanm committed Jan 17, 2013
@@ -1954,7 +1954,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
//
// TODO: for V1 representing x1 and V2 standing for x1.head, encode that
// V1 = Nil implies -(V2 = Ci) for all Ci in V2's domain (i.e., it is unassignable)
- def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Prop, List[Prop]) = {
+ // may throw an AnalysisBudget.Exception
+ def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Formula, List[Formula]) = {
val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaVarEq) else null
val vars = new scala.collection.mutable.HashSet[Var]
@@ -1978,10 +1979,10 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
props foreach gatherEqualities.apply
if (modelNull) vars foreach (_.registerNull)
- val pure = props map rewriteEqualsToProp.apply
+ val pure = props map (p => eqFreePropToSolvable(rewriteEqualsToProp(p)))
- var eqAxioms: Prop = True
- def addAxiom(p: Prop) = eqAxioms = And(eqAxioms, p)
+ val eqAxioms = formulaBuilder
+ @inline def addAxiom(p: Prop) = addFormula(eqAxioms, eqFreePropToSolvable(p))
patmatDebug("removeVarEq vars: "+ vars)
vars.foreach { v =>
@@ -2007,23 +2008,37 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
}
}
- patmatDebug("eqAxioms:\n"+ cnfString(eqFreePropToSolvable(eqAxioms)))
- patmatDebug("pure:"+ pure.map(p => cnfString(eqFreePropToSolvable(p))).mkString("\n"))
+ patmatDebug("eqAxioms:\n"+ cnfString(toFormula(eqAxioms)))
+ patmatDebug("pure:"+ pure.map(p => cnfString(p)).mkString("\n"))
if (Statistics.canEnable) Statistics.stopTimer(patmatAnaVarEq, start)
- (eqAxioms, pure)
+ (toFormula(eqAxioms), pure)
}
+ // an interface that should be suitable for feeding a SAT solver when the time comes
type Formula
+ type FormulaBuilder
+
+ // creates an empty formula builder to which more formulae can be added
+ def formulaBuilder: FormulaBuilder
+
+ // val f = formulaBuilder; addFormula(f, f1); ... addFormula(f, fN)
+ // toFormula(f) == andFormula(f1, andFormula(..., fN))
+ def addFormula(buff: FormulaBuilder, f: Formula): Unit
+ def toFormula(buff: FormulaBuilder): Formula
+
+ // the conjunction of formulae `a` and `b`
def andFormula(a: Formula, b: Formula): Formula
+ // equivalent formula to `a`, but simplified in a lightweight way (drop duplicate clauses)
+ def simplifyFormula(a: Formula): Formula
// may throw an AnalysisBudget.Exception
def propToSolvable(p: Prop): Formula = {
val (eqAxioms, pure :: Nil) = removeVarEq(List(p), modelNull = false)
- eqFreePropToSolvable(And(eqAxioms, pure))
+ andFormula(eqAxioms, pure)
}
// may throw an AnalysisBudget.Exception
@@ -2039,24 +2054,34 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
}
trait CNF extends Logic {
- // CNF: a formula is a conjunction of clauses
- type Formula = Array[Clause]
/** Override Array creation for efficiency (to not go through reflection). */
private implicit val clauseTag: scala.reflect.ClassTag[Clause] = new scala.reflect.ClassTag[Clause] {
def runtimeClass: java.lang.Class[Clause] = classOf[Clause]
final override def newArray(len: Int): Array[Clause] = new Array[Clause](len)
}
+
+ import scala.collection.mutable.ArrayBuffer
+ type FormulaBuilder = ArrayBuffer[Clause]
+ def formulaBuilder = ArrayBuffer[Clause]()
+ def addFormula(buff: FormulaBuilder, f: Formula): Unit = buff ++= f
+ def toFormula(buff: FormulaBuilder): Formula = buff.toArray
+
+ // CNF: a formula is a conjunction of clauses
+ type Formula = Array[Clause]
def formula(c: Clause*): Formula = c.toArray
- def andFormula(a: Formula, b: Formula): Formula = a ++ b
+ type Clause = Set[Lit]
// a clause is a disjunction of distinct literals
- type Clause = Set[Lit]
def clause(l: Lit*): Clause = l.toSet
- private def merge(a: Clause, b: Clause) = a ++ b
type Lit
def Lit(sym: Sym, pos: Boolean = true): Lit
+ def andFormula(a: Formula, b: Formula): Formula = a ++ b
+ def simplifyFormula(a: Formula): Formula = a.distinct
+
+ private def merge(a: Clause, b: Clause) = a ++ b
+
// throws an AnalysisBudget.Exception when the prop results in a CNF that's too big
// TODO: be smarter/more efficient about this (http://lara.epfl.ch/w/sav09:tseitin_s_encoding)
def eqFreePropToSolvable(p: Prop): Formula = {
@@ -2621,23 +2646,22 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
val propsCasesOk = testCasesOk map (t => symbolicCase(t, modelNull = true))
val propsCasesFail = testCasesFail map (t => Not(symbolicCase(t, modelNull = true)))
- val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, modelNull = true)
- val (eqAxiomsOk, symbolicCasesOk) = removeVarEq(propsCasesOk, modelNull = true)
try {
- // most of the time eqAxiomsFail == eqAxiomsOk, but the different approximations might cause different variables to disapper in general
- val eqAxiomsCNF =
- if (eqAxiomsFail == eqAxiomsOk) eqFreePropToSolvable(eqAxiomsFail)
- else eqFreePropToSolvable(And(eqAxiomsFail, eqAxiomsOk))
+ val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, modelNull = true)
+ val (eqAxiomsOk, symbolicCasesOk) = removeVarEq(propsCasesOk, modelNull = true)
+ val eqAxioms = simplifyFormula(andFormula(eqAxiomsOk, eqAxiomsFail)) // I'm pretty sure eqAxiomsOk == eqAxiomsFail, but not 100% sure.
+
+ val prefix = formulaBuilder
+ addFormula(prefix, eqAxioms)
- var prefix = eqAxiomsCNF
var prefixRest = symbolicCasesFail
var current = symbolicCasesOk
var reachable = true
var caseIndex = 0
patmatDebug("reachability, vars:\n"+ ((propsCasesFail flatMap gatherVariables).distinct map (_.describe) mkString ("\n")))
- patmatDebug("equality axioms:\n"+ cnfString(eqAxiomsCNF))
+ patmatDebug("equality axioms:\n"+ cnfString(eqAxiomsOk))
// invariant (prefixRest.length == current.length) && (prefix.reverse ++ prefixRest == symbolicCasesFail)
// termination: prefixRest.length decreases by 1
@@ -2647,11 +2671,11 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
prefixRest = prefixRest.tail
if (prefixRest.isEmpty) reachable = true
else {
- prefix = andFormula(eqFreePropToSolvable(prefHead), prefix)
+ addFormula(prefix, prefHead)
current = current.tail
- val model = findModelFor(andFormula(eqFreePropToSolvable(current.head), prefix))
+ val model = findModelFor(andFormula(current.head, toFormula(prefix)))
- // patmatDebug("trying to reach:\n"+ cnfString(eqFreePropToSolvable(current.head)) +"\nunder prefix:\n"+ cnfString(prefix))
+ // patmatDebug("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix))
// if (NoModel ne model) patmatDebug("reached: "+ modelString(model))
reachable = NoModel ne model
@@ -0,0 +1 @@
+-Xfatal-warnings
@@ -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")*/;
+
+}
Oops, something went wrong.

0 comments on commit f539781

Please sign in to comment.