Timeout solvers

src/main/scala/inox/solvers/SolverFactory.scala

@@ -16,7 +16,7 @@ trait SolverFactory {
 
   def shutdown(): Unit = {}
 
-  def reclaim(s: Solver) {
+  def reclaim(s: S) {
     s.free()
   }
 }

src/main/scala/inox/solvers/TimeoutSolver.scala

 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon
+package inox
 package solvers
 
 import utils._
-import purescala.Expressions.Expr
-
 import scala.concurrent.duration._
 
 trait TimeoutSolver extends Solver {
+  import program.trees._
 
   val ti = new TimeoutFor(this)
 
@@ -24,25 +23,26 @@ trait TimeoutSolver extends Solver {
     this
   }
 
-  abstract override def check: Option[Boolean] = {
+  abstract override def check[R](config: Configuration { type Response <: R }): R = {
     optTimeout match {
       case Some(to) =>
         ti.interruptAfter(to) {
-          super.check
+          super.check(config)
         }
       case None =>
-        super.check
+        super.check(config)
     }
   }
 
-  abstract override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
+  abstract override def checkAssumptions[R](config: Configuration { type Response <: R })
+                                           (assumptions: Set[Expr]): R = {
     optTimeout match {
       case Some(to) =>
         ti.interruptAfter(to) {
-          super.checkAssumptions(assumptions)
+          super.checkAssumptions(config)(assumptions)
         }
       case None =>
-        super.checkAssumptions(assumptions)
+        super.checkAssumptions(config)(assumptions)
     }
   }
 

src/main/scala/inox/solvers/TimeoutSolverFactory.scala

 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon
+package inox
 package solvers
 
 import scala.reflect.runtime.universe._
 
-class TimeoutSolverFactory[+S <: TimeoutSolver : TypeTag](val sf: SolverFactory[S], to: Long) extends SolverFactory[S] {
-  override def getNewSolver() = sf.getNewSolver().setTimeout(to)
+trait TimeoutSolverFactory extends SolverFactory {
+  type S <: TimeoutSolver { val program: TimeoutSolverFactory.this.program.type }
 
-  override val name = sf.name+" with t.o"
+  val factory: SolverFactory {
+    val program: TimeoutSolverFactory.this.program.type
+    type S = TimeoutSolverFactory.this.S
+  }
 
-  override def reclaim(s: Solver) = sf.reclaim(s)
+  val to: Long
 
-  override def shutdown() = sf.shutdown()
+  override def getNewSolver() = factory.getNewSolver().setTimeout(to)
+
+  override val name = factory.name+" with t.o"
+
+  override def reclaim(s: S) = factory.reclaim(s)
+
+  override def shutdown() = factory.shutdown()
 }