Solver package (implicit timeoutSolver wrapper)

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

@@ -2,6 +2,7 @@
 
 package inox
 package solvers
+package combinators
 
 import utils._
 import scala.concurrent.duration._

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

@@ -2,6 +2,7 @@
 
 package inox
 package solvers
+package combinators
 
 import scala.reflect.runtime.universe._
 

src/main/scala/inox/solvers/package.scala

 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon
+package inox
 
-import scala.reflect.runtime.universe._
 import scala.concurrent.duration._
 
 package object solvers {
-  implicit class TimeoutableSolverFactory[+S <: TimeoutSolver : TypeTag](val sf: SolverFactory[S]) {
-    def withTimeout(to: Long): TimeoutSolverFactory[S] = {
-      sf match {
-        case tsf: TimeoutSolverFactory[_] =>
-          new TimeoutSolverFactory[S](tsf.sf, to)
-        case _ =>
-          new TimeoutSolverFactory[S](sf, to)
+  import combinators._
+
+  implicit class TimeoutableSolverFactory[S1 <: TimeoutSolver](val sf: SolverFactory { type S = S1 }) {
+    def withTimeout(timeout: Long): TimeoutSolverFactory { type S <: S1 } = {
+      val innerFactory = (sf match {
+        case tsf: TimeoutSolverFactory => tsf.factory
+        case _ => sf
+      }).asInstanceOf[SolverFactory {
+        val program: sf.program.type
+        type S = S1 { val program: sf.program.type }
+      }]
+
+      new TimeoutSolverFactory {
+        val program: sf.program.type = sf.program
+        type S = S1 { val program: sf.program.type }
+        val to = timeout
+        val factory = innerFactory
       }
     }
 
-    def withTimeout(du: Duration): TimeoutSolverFactory[S] = {
+    def withTimeout(du: Duration): TimeoutSolverFactory { type S <: S1 } = {
       withTimeout(du.toMillis)
     }
   }