From 988fbcd3f416eaf87d8a5291c3269056d4bc05e9 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Thu, 4 Aug 2016 11:25:59 +0200
Subject: [PATCH] Timeout solvers
---
.../scala/inox/solvers/SolverFactory.scala | 2 +-
.../scala/inox/solvers/TimeoutSolver.scala | 18 ++++++++--------
.../inox/solvers/TimeoutSolverFactory.scala | 21 +++++++++++++------
3 files changed, 25 insertions(+), 16 deletions(-)
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index c82a9b0d4..fc36dd3ff 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/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()
}
}
diff --git a/src/main/scala/inox/solvers/TimeoutSolver.scala b/src/main/scala/inox/solvers/TimeoutSolver.scala
index 90ce09b79..3b0d516ef 100644
--- a/src/main/scala/inox/solvers/TimeoutSolver.scala
+++ b/src/main/scala/inox/solvers/TimeoutSolver.scala
@@ -1,14 +1,13 @@
/* 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)
}
}
diff --git a/src/main/scala/inox/solvers/TimeoutSolverFactory.scala b/src/main/scala/inox/solvers/TimeoutSolverFactory.scala
index f3f8ca200..b45e5bffa 100644
--- a/src/main/scala/inox/solvers/TimeoutSolverFactory.scala
+++ b/src/main/scala/inox/solvers/TimeoutSolverFactory.scala
@@ -1,17 +1,26 @@
/* 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()
}
--
GitLab