SI-6582 Use Tseitin's algorithm for CNF conversion in pattern matching analysis. #2796

adriaanm · 2013-08-06T00:11:36Z

This chops #2724 into smaller commits.

I made Lit into a value class and encapsulated a bit more.
Please double check my refactorings were correctness-preserving.

review by @gbasler

adriaanm · 2013-08-06T00:14:08Z

src/compiler/scala/tools/nsc/transform/patmat/Logic.scala

-      andFormula(eqAxioms, pure)
+    def propToSolvable(p: Prop): Solvable = {
+      val (eqAxiom, pure :: Nil) = removeVarEq(List(p), modelNull = false)
+      eqFreePropToSolvable(simplify(And(eqAxiom, pure)))


Note that I added a simplify call here compared to the original PR. Necessary?

eqFreePropToSolvable calls simplify internally, so it can be omitted here

adriaanm · 2013-08-11T19:38:02Z

I cheated on a check file. We should figure out what changed before merging, if possible.

retronym · 2013-08-13T09:03:44Z

I'm hopeful that checkfile issue will be caused by the non-determinism fixed in #2826 / SI-7020

JamesIry · 2013-08-13T15:52:08Z

Is #2826 the only hold back on this PR?

adriaanm · 2013-08-13T15:54:07Z

The only issue with this PR is that I had to change test/files/neg/patmatexhaust.check, which should not have been necessary. I hope we'll know today whether #2826 solves that.

adriaanm · 2013-08-13T16:30:59Z

I'll rebase on top of the other PR and see if it helps.

Remove redundant UniqueSym class.

This resolves the `AnalysisBudgetException` problem for big pattern matches. Initial experiments indicate that the problem is even simpler than initially thought: all formulae I got from the exhaustiveness check could be transformed directly into CNF. Thus the framework introduced here might be overkill and a much simpler implementation could work as well. For Scala 2.11 I'd suggest to replace the DPLL procedure with Sat4j.

adriaanm · 2013-08-13T23:59:00Z

I think I found the issue. I probably made a mistake refactoring findAllModelsFor. Seems ok now.

adriaanm · 2013-08-14T00:00:50Z

Here's the diff with my previous version of the PR:

diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
index 64128b82ac..1f2dc33f07 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
@@ -201,31 +201,33 @@ trait Solving extends Logic {
       // (i.e. the blocking clause - used for ALL-SAT)
       def negateModel(m: TseitinModel) = m.map(lit => -lit)

-      def findAllModels(clauses: Array[Clause], models: List[TseitinModel] = Nil, recursionDepthAllowed: Int = 10): List[TseitinModel] =
+      def findAllModels(clauses: Array[Clause], models: List[TseitinModel], recursionDepthAllowed: Int = 10): List[TseitinModel] =
         if (recursionDepthAllowed == 0) models
         else {
           debug.patmat("find all models for\n" + cnfString(clauses))
-          findTseitinModelFor(clauses, stoppingNanos) match {
-            case NoTseitinModel => models
-            case model =>
-              // if we found a solution, conjunct the formula with the model's negation and recurse
-              val unassigned = (allVars -- model).toList
-              debug.patmat("unassigned " + unassigned + " in " + model)
-
-              def force(lit: Lit) =
-                withLit(findTseitinModelFor(dropUnit(clauses.toArray, lit), stoppingNanos), lit) match {
-                  case NoTseitinModel => Nil
-                  case _              => List(model)
-                }
-              val forced = unassigned flatMap (l => force(l) ++ force(-l))
-              debug.patmat("forced " + forced)
-
-              val negated = negateModel(model)
-              findAllModels(clauses :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1)
+          val model = findTseitinModelFor(clauses, stoppingNanos)
+          // if we found a solution, conjunct the formula with the model's negation and recurse
+          if (model ne NoTseitinModel) {
+            val unassigned = (allVars -- model.map(lit => Lit(lit.variable))).toList
+            debug.patmat(s"unassigned ${unassigned map (lit => solvable.symForVar(lit.variable))} in ${projectToModel(model, solvable.symForVar)}")
+
+            def force(lit: Lit) = {
+              val model = withLit(findTseitinModelFor(dropUnit(clauses.toArray, lit), stoppingNanos), lit)
+              if (model ne NoTseitinModel) List(model)
+              else Nil
+            }
+            val forced = unassigned flatMap { l =>
+              force(Lit(l.variable)) ++ force(Lit(-l.variable))
+            }
+            debug.patmat("forced " + forced)
+
+            val negated = negateModel(model)
+            findAllModels(clauses :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1)
           }
+          else models
         }

-      val tseitinModels = findAllModels(solvable.cnf.clauses)
+      val tseitinModels = findAllModels(solvable.cnf.clauses, Nil)
       val models = tseitinModels.map(projectToModel(_, solvable.symForVar))

adriaanm · 2013-08-14T05:46:42Z

Darn.. Looks like it got a little less deterministic. I'm not sure we'll be able to make it deterministic, and maybe should look into more clever merging of counterexamples (going into the structure, say: the examples List(a) and List(b) are merged into the single example List(a | b)). I'm afraid this is going to be tricky for 2.10.3 :(

retronym · 2013-08-14T05:48:54Z

While you're looking at that piece of code, could you explain/comment what forced is doing? That part is responsible for a wrong counter example in SI-7746, I removed it retronym/scala@scala:2.10.x...ticket/7746

That changes:

 patmatexhaust.scala:49: error: match may not be exhaustive.
-It would fail on the following input: Gp()
+It would fail on the following inputs: Gp(), Gu

and

testing: [...]/files/neg/t7020.scala                                  [FAILED]
--- t7020-neg.log
+++ t7020.check
@@ -1,3 +1,3 @@
 t7020.scala:3: error: match may not be exhaustive.
-It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List((x: Int forSome x not in (1, 2, 4, 5, 6, 7)), _), List(1, _), List(2, _), List(4, _), List(5, _), List(6, _), List(7, _)
+It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List(_, _)
   List(5) match {

adriaanm · 2013-08-14T05:49:05Z

I stashed my wip in my branch patmat-tseitin-2.10-wip

adriaanm · 2013-08-14T05:51:54Z

Forced assigns the unassigned variable to yes/no and checks for satisfiable to force these variables to be assigned. Gotta go now, sorry.

adriaanm · 2013-08-14T06:46:02Z

It would probably be faster/read better as:

def force(lit: Lit): Option[TseitinModel] = {
  val model = withLit(findTseitinModelFor(dropUnit(clauses.toArray, lit), stoppingNanos), lit)
  if (model ne NoTseitinModel) Some(model)
  else None
}
val forced = unassigned flatMap { l =>
  (force(Lit(l.variable)) orElse force(Lit(-l.variable))).toList
}

gbasler · 2013-08-14T07:50:51Z

@adriaanm If there's a solution and there are unassigned variables left, then they do not influence the solution, so why would you need to assign a value to them? My assumption is that you can't handle unassigned variables when you map the solution back to a counter example. Would it not be easier to fix it there? If there are multiple counter examples corresponding to a solution you could just return the most precise one.

retronym · 2013-08-14T08:04:47Z

Tracing out SI-7020:

def f[T](x: Option[T]) = x match {
    case Some(Some(5)) => true // It would fail on the following inputs: None, Some((x: T forSome x not in Some[?])), Some(Some((x: Any forSome x not in 5))), Some(_)
  }

unassigned List(V1=None.type#11, V3=5#10) in Map(V1=Some[?]#8 -> true, V2=Some[?]#9 -> false)

...

dropUnit(
  ArrayBuffer(Set(V1=None.type#11, V1=Some[?]#8), Set(-V1=Some[?]#8, -V2=Some[?]#9, -V3=5#10), Set(V1=Some[?]#8, -V1=None.type#11)),
  V3=5#10
) = ArrayBuffer(Set(V1=None.type#11, V1=Some[?]#8), Set(-V1=Some[?]#8, -V2=Some[?]#9), Set(V1=Some[?]#8, -V1=None.type#11))
DPLL
 V1=None.type#11 \/   V1=Some[?]#8    /\
  -V1=Some[?]#8  \/  -V2=Some[?]#9    /\
  V1=Some[?]#8   \/ -V1=None.type#11
DPLL
 V1=None.type#11 \/   V1=Some[?]#8    /\
  V1=Some[?]#8   \/ -V1=None.type#11
DPLL

dropUnit(
  ArrayBuffer
8000
(Set(V1=None.type#11, V1=Some[?]#8), Set(-V1=Some[?]#8, -V2=Some[?]#9, -V3=5#10), Set(V1=Some[?]#8, -V1=None.type#11)),
  -V3=5#10
) = ArrayBuffer(Set(V1=None.type#11, V1=Some[?]#8), Set(V1=Some[?]#8, -V1=None.type#11))
DPLL
 V1=None.type#11 \/   V1=Some[?]#8    /\
  V1=Some[?]#8   \/ -V1=None.type#11
DPLL

forcedYes(V3=5#10) Map(V1=Some[?]#8 -> true, V2=Some[?]#9 -> false, V3=5#10 -> true)
forcedNo(V3=5#10) Map(V1=Some[?]#8 -> true, V3=5#10 -> false)
...
var assignment for model Map(V1=Some[?]#8 -> true, V3=5#10 -> false):
V1(=x1: Option[?]) == (Some[?])  != ()
V3(=x1.x.x: Any) == ()  != (5)
describing (V1,List(Some[?]),List(),Map(),class Some,true)
described as: Some(_)

Taking the unassigned V3=5 as false leads us to simplify the model to a point where we suggest Some(_) as a counter example. But for V3 to be assignable at all (as i understand things), we need V2 = Some[?] to be true.

Is Map(V1=Some[?]#8 -> true, V3=5#10 -> false): a valid counter example that is wrongly described, or an invalid counter example? (To me, it seems like the latter.)

adriaanm · 2013-08-14T17:07:22Z

I'm very open to improvements to the counter example algorithm (though I'm
getting more anxious about changing any of this in 2.10 due to the risk of
undetected regressions). I really wish I had more time to work on this
right now, but I can't. I'd be more at ease if this was happening in
master. I have budgeted time during the polish milestones to work on this
kind of stuff (sept-oct).

On Wednesday, August 14, 2013, Jason Zaugg wrote:

Tracing out SI-7020:

def f[T](x: Option[T]) = x match {
case Some(Some(5)) => true // It would fail on the following inputs: None, Some((x: T forSome x not in Some[?])), Some(Some((x: Any forSome x not in 5))), Some(_)
}

unassigned List(V1=None.type#11, V3=5#10) in Map(V1=Some[?]#8 -> true, V2=Some[?]#9 -> false)

...

dropUnit(
ArrayBuffer(Set(V1=None.type#11, V1=Some[?]#8), Set(-V1=Some[?]#8, -V2=Some[?]#9, -V3=5#10), Set(V1=Some[?]#8, -V1=None.type#11)),
V3=5#10
) = ArrayBuffer(Set(V1=None.type#11, V1=Some[?]#8), Set(-V1=Some[?]#8, -V2=Some[?]#9), Set(V1=Some[?]#8, -V1=None.type#11))
DPLL
V1=None.type#11 / V1=Some[?]#8 /
-V1=Some[?]#8 / -V2=Some[?]#9 /
V1=Some[?]#8 / -V1=None.type#11
DPLL
V1=None.type#11 / V1=Some[?]#8 /
V1=Some[?]#8 / -V1=None.type#11
DPLL

dropUnit(
ArrayBuffer(Set(V1=None.type#11, V1=Some[?]#8), Set(-V1=Some[?]#8, -V2=Some[?]#9, -V3=5#10), Set(V1=Some[?]#8, -V1=None.type#11)),
-V3=5#10
) = ArrayBuffer(Set(V1=None.type#11, V1=Some[?]#8), Set(V1=Some[?]#8, -V1=None.type#11))
DPLL
V1=None.type#11 / V1=Some[?]#8 /
V1=Some[?]#8 / -V1=None.type#11
DPLL

forcedYes(V3=5#10) Map(V1=Some[?]#8 -> true, V2=Some[?]#9 -> false, V3=5#10 -> true)
forcedNo(V3=5#10) Map(V1=Some[?]#8 -> true, V3=5#10 -> false)
...
var assignment for model Map(V1=Some[?]#8 -> true, V3=5#10 -> false):
V1(=x1: Option[?]) == (Some[?]) != ()
V3(=x1.x.x: Any) == () != (5)
describing (V1,List(Some[?]),List(),Map(),class Some,true)
described as: Some(_)

Taking the unassigned V3=5 as false leads us to simplify the model to a
point where we suggest Some(_) as a counter example. But for V3 to be
assignable at all (as i understand things), we need V2 = Some[?] to be
true.

—
Reply to this email directly or view it on GitHubhttps://github.com//pull/2796#issuecomment-22620569
.

adriaanm · 2013-08-15T17:12:51Z

Is Map(V1=Some[?]#8 -> true, V3=5#10 -> false): a valid counter example that is wrongly described, or an invalid counter example? (To me, it seems like the latter.)

Yeah, the whole logic of dependencies between variables' types is not encoded in the formula. That's why the counter examples need to be pruned (https://github.com/scala/scala/blob/master/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala#L352)

adriaanm · 2013-08-15T17:38:32Z

@gbasler, how would you feel about having your work go to 2.11.0-M6 (September), instead of 2.10.3? 2.10 is in maintenance mode, and I'm not sure we have enough test coverage to change the algorithm this deeply without causing regressions.

gbasler · 2013-08-16T07:55:51Z

@adriaanm Sure. I really liked your improvements to the code (I totally missed to use a value class for Lits). I also don't have much time to look into this right now and it's better to clean up a bit before we merge these changes. I'll try to find the time and also look at the two other commits from Jason. Better be correct than fast and wrong!

retronym · 2013-08-16T08:49:02Z

Thanks for the explanation. I've noted this over on SI-7746.

JamesIry · 2013-08-16T15:22:51Z

Kicking to 2.10.4...but perhaps it's really 2.11 material?

628C

adriaanm · 2013-08-16T18:13:11Z

@gbasler, thanks! I really want this in, but I agree we should take our time to do it right. I feel 2.11 is the right target.

adriaanm reviewed Aug 6, 2013
View reviewed changes

ghost assigned retronym and JamesIry Aug 13, 2013

adriaanm added 4 commits August 13, 2013 15:34

Debug printing for Any, not AnyRef, to include primitives

ac9bce9

Add sequence method via reflect.internal.Sequenceable implicit

c508402

And, Or take sets of Props

88604da

Remove redundant UniqueSym class.

adriaanm closed this Aug 16, 2013

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

SI-6582 Use Tseitin's algorithm for CNF conversion in pattern matching analysis. #2796

SI-6582 Use Tseitin's algorithm for CNF conversion in pattern matching analysis. #2796

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

SI-6582 Use Tseitin's algorithm for CNF conversion in pattern matching analysis. #2796

SI-6582 Use Tseitin's algorithm for CNF conversion in pattern matching analysis. #2796

Uh oh!

Conversation

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!