TimeoutSolver Improvements

Timeouts are now specified in milliseconds instead of seconds.

TimeoutSolvers that hit a timeout no longer makes the wrapped solver
useless for all subsequent invocations.

src/main/scala/leon/solvers/IncrementalSolver.scala

@@ -10,7 +10,7 @@ trait IncrementalSolverBuilder {
   def getNewSolver: IncrementalSolver
 }
 
-trait IncrementalSolver {
+trait IncrementalSolver extends InterruptibleSolver {
   // New Solver API
   // Moslty for z3 solvers since z3 4.3
 
@@ -19,6 +19,8 @@ trait IncrementalSolver {
   def assertCnstr(expression: Expr): Unit
 
   def halt(): Unit
+  def init(): Unit = {}
+
   def check: Option[Boolean]
   def checkAssumptions(assumptions: Set[Expr]): Option[Boolean]
   def getModel: Map[Identifier, Expr]

src/main/scala/leon/solvers/InterruptibleSolver.scala

+package leon
+package solvers
+
+trait InterruptibleSolver {
+  def halt(): Unit
+  def init(): Unit
+}

src/main/scala/leon/solvers/Solver.scala

@@ -6,7 +6,7 @@ import purescala.Definitions._
 import purescala.TreeOps._
 import purescala.Trees._
 
-abstract class Solver(val context : LeonContext) extends IncrementalSolverBuilder with LeonComponent {
+abstract class Solver(val context : LeonContext) extends IncrementalSolverBuilder with InterruptibleSolver with LeonComponent {
   // This can be used by solvers to "see" the programs from which the
   // formulas come. (e.g. to set up some datastructures for the defined
   // ADTs, etc.) 

src/main/scala/leon/solvers/TimeoutSolver.scala

@@ -8,12 +8,12 @@ import purescala.TypeTrees._
 
 import scala.sys.error
 
-class TimeoutSolver(solver : Solver with  IncrementalSolverBuilder, timeout : Int) extends Solver(solver.context) with IncrementalSolverBuilder {
+class TimeoutSolver(solver : Solver with  IncrementalSolverBuilder, timeoutMs : Long) extends Solver(solver.context) with IncrementalSolverBuilder {
   // I'm making this an inner class to fight the temptation of using it for anything meaningful.
   // We have Akka, these days, which whould be better in any respect for non-trivial things.
   private class Timer(onTimeout: => Unit) extends Thread {
     private var keepRunning = true
-    private val asMillis : Long = 1000L * timeout
+    private val asMillis : Long = timeoutMs
 
     override def run : Unit = {
       val startTime : Long = System.currentTimeMillis
@@ -23,7 +23,7 @@ class TimeoutSolver(solver : Solver with  IncrementalSolverBuilder, timeout : In
         if(asMillis < (System.currentTimeMillis - startTime)) {
           exceeded = true
         }
-        Thread.sleep(10) 
+        Thread.sleep(10)
       }
       if(exceeded && keepRunning) {
         onTimeout
@@ -35,14 +35,28 @@ class TimeoutSolver(solver : Solver with  IncrementalSolverBuilder, timeout : In
     }
   }
 
-  def withTimeout[T](onTimeout: => Unit)(body: => T): T = {
-    val timer = new Timer(onTimeout)
+  def withTimeout[T](solver: InterruptibleSolver)(body: => T): T = {
+    val timer = new Timer(timeout(solver))
     timer.start
     val res = body
     timer.halt
+    recoverFromTimeout(solver)
     res
   }
 
+  var reachedTimeout = false
+  def timeout(solver: InterruptibleSolver) {
+    solver.halt
+    reachedTimeout = true
+  }
+
+  def recoverFromTimeout(solver: InterruptibleSolver) {
+    if (reachedTimeout) {
+      solver.init
+      reachedTimeout = false
+    }
+  }
+
   val description = solver.description + ", with timeout"
   val name = solver.name + "+to"
 
@@ -51,19 +65,19 @@ class TimeoutSolver(solver : Solver with  IncrementalSolverBuilder, timeout : In
   }
 
   def solve(expression: Expr) : Option[Boolean] = {
-    withTimeout(solver.halt) {
+    withTimeout(solver) {
       solver.solve(expression)
     }
   }
 
   override def solveSAT(expression: Expr): (Option[Boolean], Map[Identifier, Expr]) = {
-    withTimeout(solver.halt) {
+    withTimeout(solver) {
       solver.solveSAT(expression)
     }
   }
 
   override def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = {
-    withTimeout(solver.halt) {
+    withTimeout(solver) {
       solver.solveSATWithCores(expression, assumptions)
     }
   }
@@ -88,13 +102,13 @@ class TimeoutSolver(solver : Solver with  IncrementalSolverBuilder, timeout : In
     }
 
     def check: Option[Boolean] = {
-      withTimeout(solver.halt){
+      withTimeout(solver){
         solver.check
       }
     }
 
     def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
-      withTimeout(solver.halt){
+      withTimeout(solver){
         solver.checkAssumptions(assumptions)
       }
     }

src/main/scala/leon/verification/AnalysisPhase.scala

@@ -42,7 +42,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
 
     val solvers0 : Seq[Solver] = trivialSolver :: fairZ3 :: Nil
     val solvers: Seq[Solver] = timeout match {
-      case Some(t) => solvers0.map(s => new TimeoutSolver(s, t))
+      case Some(t) => solvers0.map(s => new TimeoutSolver(s, 1000L * t))
       case None => solvers0
     }
 

src/test/scala/leon/test/solvers/TimeoutSolverTests.scala

@@ -27,7 +27,7 @@ class TimeoutSolverTests extends FunSuite {
   }
 
   private def getTOSolver : Solver = {
-    val s = new TimeoutSolver(new IdioticSolver(LeonContext()), 1)
+    val s = new TimeoutSolver(new IdioticSolver(LeonContext()), 1000L)
     s.setProgram(Program.empty)
     s
   }