Unrolling solver takes an incremental solver

UnrollingSolver now uses an underlying incremental solver
and use push and pop to drive the unrolling instead of creating
a new solver each time

src/main/scala/leon/solvers/combinators/UnrollingSolver.scala

@@ -10,15 +10,18 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.TypeTrees._
 
+import utils.Interruptible
+
 import scala.collection.mutable.{Map=>MutableMap}
 
-class UnrollingSolver(val context: LeonContext,
-                      underlyings: SolverFactory[Solver],
-                      maxUnrollings: Int = 3) extends Solver {
+class UnrollingSolver(val context: LeonContext, underlyings: SolverFactory[IncrementalSolver]) 
+        extends Solver with Interruptible {
 
   private var theConstraint : Option[Expr] = None
   private var theModel : Option[Map[Identifier,Expr]] = None
 
+  private var stop: Boolean = false
+
   def name = "Unr("+underlyings.name+")"
 
   def free {}
@@ -33,7 +36,7 @@ class UnrollingSolver(val context: LeonContext,
   }
 
   def check : Option[Boolean] = theConstraint.map { expr =>
-    val simpleSolver = SimpleSolverAPI(underlyings)
+    val solver = underlyings.getNewSolver//SimpleSolverAPI(underlyings)
 
     debugS("Check called on " + expr + "...")
 
@@ -43,23 +46,7 @@ class UnrollingSolver(val context: LeonContext,
     var allClauses : Seq[Expr] = Nil
     var allBlockers : Map[Identifier,Set[FunctionInvocation]] = Map.empty
 
-    def fullOpenExpr : Expr = {
-      // And(Variable(aVar), And(allClauses.reverse))
-      // Let's help the poor underlying guy a little bit...
-      // Note that I keep aVar around, because it may negate one of the blockers, and we can't miss that!
-      And(Variable(aVar), replace(Map(Variable(aVar) -> BooleanLiteral(true)), And(allClauses.reverse)))
-    }
-
-    def fullClosedExpr : Expr = {
-      val blockedVars : Seq[Expr] = allBlockers.toSeq.map(p => Variable(p._1))
-
-      And(
-        replace(blockedVars.map(v => (v -> BooleanLiteral(false))).toMap, fullOpenExpr),
-        And(blockedVars.map(Not(_)))
-      )
-    }
-
-    def unrollOneStep() {
+    def unrollOneStep() : List[Expr] = {
       val blockersBefore = allBlockers
 
       var newClauses : List[Seq[Expr]] = Nil
@@ -73,6 +60,7 @@ class UnrollingSolver(val context: LeonContext,
 
       allClauses = newClauses.flatten ++ allClauses
       allBlockers = newBlockers
+      newClauses.flatten
     }
 
     val (nc, nb) = template.instantiate(aVar, template.funDef.args.map(a => Variable(a.id)))
@@ -84,19 +72,26 @@ class UnrollingSolver(val context: LeonContext,
     var done : Boolean = false
     var result : Option[Boolean] = None
 
+    solver.assertCnstr(Variable(aVar))
+    solver.assertCnstr(And(allClauses))
     // We're now past the initial step.
-    while(!done && unrollingCount < maxUnrollings) {
+    while(!done && !stop) {
       debugS("At lvl : " + unrollingCount)
-      val closed : Expr = fullClosedExpr
 
-      debugS("Going for SAT with this:\n" + closed)
+      solver.push()
+      //val closed : Expr = fullClosedExpr
+      solver.assertCnstr(And(allBlockers.keySet.toSeq.map(id => Not(id.toVariable))))
 
-      simpleSolver.solveSAT(closed) match {
-        case (Some(false), _) =>
-          val open = fullOpenExpr
-          debugS("Was UNSAT... Going for UNSAT with this:\n" + open)
-          simpleSolver.solveSAT(open) match {
-            case (Some(false), _) =>
+      debugS("Going for SAT with this:\n")
+
+      solver.check match {
+
+        case Some(false) =>
+          solver.pop(1)
+          //val open = fullOpenExpr
+          debugS("Was UNSAT... Going for UNSAT with this:\n")
+          solver.check match {
+            case Some(false) =>
               debugS("Was UNSAT... Done !")
               done = true
               result = Some(false)
@@ -104,16 +99,19 @@ class UnrollingSolver(val context: LeonContext,
             case _ =>
               debugS("Was SAT or UNKNOWN. Let's unroll !")
               unrollingCount += 1
-              unrollOneStep()
+              val newClauses = unrollOneStep()
+              solver.assertCnstr(And(newClauses))
           }
 
-        case (Some(true), model) =>
+        case Some(true) =>
+          val model = solver.getModel
           debugS("WAS SAT ! We're DONE !")
           done = true
           result = Some(true)
           theModel = Some(model)
 
-        case (None, model) =>
+        case None =>
+          val model = solver.getModel
           debugS("WAS UNKNOWN ! We're DONE !")
           done = true
           result = Some(true)
@@ -131,6 +129,14 @@ class UnrollingSolver(val context: LeonContext,
     theModel.getOrElse(Map.empty).filter(p => vs(p._1))
   }
 
+  override def interrupt(): Unit = {
+    stop = true
+  }
+
+  override def recoverInterrupt(): Unit = {
+    stop = false
+  }
+
   private val funDefTemplateCache : MutableMap[FunDef, FunctionTemplate] = MutableMap.empty
   private val exprTemplateCache : MutableMap[Expr, FunctionTemplate] = MutableMap.empty