Skip to content
Snippets Groups Projects
Commit 0681b87d authored by Philippe Suter's avatar Philippe Suter
Browse files

Removing legacy code.

parent 00d90a46
No related branches found
No related tags found
No related merge requests found
package leon
/** Creates a thread that, when started, counts for maxsecs seconds and then
* calls the callback, unless the timer was halted first. */
class Timer(callback : () => Unit, maxSecs : Int) extends Thread {
private var keepRunning = true
private val asMillis : Long = 1000L * maxSecs
override def run : Unit = {
val startTime : Long = System.currentTimeMillis
var exceeded : Boolean = false
while(!exceeded && keepRunning) {
if(asMillis < (System.currentTimeMillis - startTime)) {
exceeded = true
}
Thread.sleep(100) //is needed on my (regis) machine, if not here, the loop does not stop when halt is called.
}
if(exceeded && keepRunning) {
callback()
}
}
def halt : Unit = {
keepRunning = false
}
}
package leon
package solvers
import purescala.Common._
import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
import scala.sys.error
class TimeoutSolver(solver : Solver, timeout : Int) extends Solver(solver.context) with NaiveIncrementalSolver {
val description = solver.description + ", with timeout"
override val shortDescription = solver.shortDescription + "+t"
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
}
override def init() {
solver.init
}
override 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