Permalink
Browse files

Merge pull request #1915 from adriaanm/ticket-6942

SI-6942 more efficient CNF conversion in patmat analysis
  • Loading branch information...
2 parents 6f72ed8 + 964776f commit 18a906bb9a6c6b50d286ca76f219a5b351514ae4 @paulp paulp committed Jan 20, 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)
}
- def formula(c: Clause*): Formula = c.toArray
- def andFormula(a: Formula, b: Formula): Formula = a ++ b
+ 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
+
+ // CNF: a formula is a conjunction of clauses
+ type Formula = FormulaBuilder
+ def formula(c: Clause*): Formula = ArrayBuffer(c: _*)
+
+ 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 18a906b

Please sign in to comment.