Skip to content
Snippets Groups Projects
Commit 28632c2c authored by Régis Blanc's avatar Régis Blanc
Browse files

adding TimeoutSolver and adapting Analysis to wrap solvers into TimeoutSolver when needed

parent 82dec5d7
No related branches found
No related tags found
No related merge requests found
...@@ -13,7 +13,18 @@ class Analysis(val program: Program, val reporter: Reporter = Settings.reporter) ...@@ -13,7 +13,18 @@ class Analysis(val program: Program, val reporter: Reporter = Settings.reporter)
val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions
val trivialSolver = new TrivialSolver(reporter) // This one you can't disable :D val trivialSolver = new TrivialSolver(reporter) // This one you can't disable :D
val solverExtensions: Seq[Solver] = trivialSolver +: loadedSolverExtensions
val solverExtensions1: Seq[Solver] = trivialSolver +: loadedSolverExtensions
//TODO: is it really correct?
val solverExtensions =
if(Settings.solverTimeout == None) {
solverExtensions1
} else {
val t = Settings.solverTimeout.get
solverExtensions1.map(s => new TimeoutSolver(reporter, s, t))
}
solverExtensions.foreach(_.setProgram(program)) solverExtensions.foreach(_.setProgram(program))
val defaultTactic = new DefaultTactic(reporter) val defaultTactic = new DefaultTactic(reporter)
......
package purescala
import Common._
import Definitions._
import Extensions._
import Trees._
import TypeTrees._
import scala.sys.error
class TimeoutSolver(reporter: Reporter, solver : Solver, timeout : Int) extends Solver(reporter) {
val description = solver.description + ", with timeout"
override val shortDescription = solver.shortDescription + "+timeout"
override def setProgram(prog: Program): Unit = {
solver.setProgram(prog)
}
def solve(expression: Expr) : Option[Boolean] = {
val timer = new Timer(() => solver.halt, timeout)
timer.start
val res = solver.solve(expression)
timer.halt
res
}
def halt() {
solver.halt
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment