From 01a8b038c2df9f44b469b161f8ef8843a37f953c Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sun, 7 Aug 2016 19:05:36 +0200
Subject: [PATCH] Solver package (implicit timeoutSolver wrapper)
---
.../{ => combinators}/TimeoutSolver.scala | 1 +
.../TimeoutSolverFactory.scala | 1 +
src/main/scala/inox/solvers/package.scala | 29 ++++++++++++-------
3 files changed, 21 insertions(+), 10 deletions(-)
rename src/main/scala/inox/solvers/{ => combinators}/TimeoutSolver.scala (98%)
rename src/main/scala/inox/solvers/{ => combinators}/TimeoutSolverFactory.scala (96%)
diff --git a/src/main/scala/inox/solvers/TimeoutSolver.scala b/src/main/scala/inox/solvers/combinators/TimeoutSolver.scala
similarity index 98%
rename from src/main/scala/inox/solvers/TimeoutSolver.scala
rename to src/main/scala/inox/solvers/combinators/TimeoutSolver.scala
index 17ae644b5..4c74587a0 100644
--- a/src/main/scala/inox/solvers/TimeoutSolver.scala
+++ b/src/main/scala/inox/solvers/combinators/TimeoutSolver.scala
@@ -2,6 +2,7 @@
package inox
package solvers
+package combinators
import utils._
import scala.concurrent.duration._
diff --git a/src/main/scala/inox/solvers/TimeoutSolverFactory.scala b/src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala
similarity index 96%
rename from src/main/scala/inox/solvers/TimeoutSolverFactory.scala
rename to src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala
index b45e5bffa..0c20fddc9 100644
--- a/src/main/scala/inox/solvers/TimeoutSolverFactory.scala
+++ b/src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala
@@ -2,6 +2,7 @@
package inox
package solvers
+package combinators
import scala.reflect.runtime.universe._
diff --git a/src/main/scala/inox/solvers/package.scala b/src/main/scala/inox/solvers/package.scala
index 34215c07e..2fcab5aba 100644
--- a/src/main/scala/inox/solvers/package.scala
+++ b/src/main/scala/inox/solvers/package.scala
@@ -1,22 +1,31 @@
/* 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)
}
}
--
GitLab