From 28632c2ce79a8719773340c6a69bb0c224bf1eba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com> Date: Thu, 2 Jun 2011 00:55:03 +0000 Subject: [PATCH] adding TimeoutSolver and adapting Analysis to wrap solvers into TimeoutSolver when needed --- src/purescala/Analysis.scala | 13 ++++++++++++- src/purescala/TimeoutSolver.scala | 32 +++++++++++++++++++++++++++++++ 2 files changed, 44 insertions(+), 1 deletion(-) create mode 100644 src/purescala/TimeoutSolver.scala diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala index fc96acf40..6fc70728d 100644 --- a/src/purescala/Analysis.scala +++ b/src/purescala/Analysis.scala @@ -13,7 +13,18 @@ class Analysis(val program: Program, val reporter: Reporter = Settings.reporter) val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions 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)) val defaultTactic = new DefaultTactic(reporter) diff --git a/src/purescala/TimeoutSolver.scala b/src/purescala/TimeoutSolver.scala new file mode 100644 index 000000000..5d04209dc --- /dev/null +++ b/src/purescala/TimeoutSolver.scala @@ -0,0 +1,32 @@ +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 + } + +} -- GitLab