Commit 3e5749af authored by Fabian Ritter's avatar Fabian Ritter Committed by Anastasiia

Implement timeouts for DRealSolver

parent 7e95cd0f
......@@ -11,6 +11,9 @@ package solvers
import scala.collection.immutable.Seq
import scala.concurrent.{Future, blocking, ExecutionContext, Await, TimeoutException}
import scala.concurrent.duration._
import _root_.smtlib.interpreters.{Z3Interpreter, ProcessInterpreter}
import _root_.smtlib.parser.Commands._
import _root_.smtlib.parser.Terms.{SKeyword, Attribute, SNumeral, SExpr, SSymbol}
......@@ -26,13 +29,9 @@ object DRealSolver {
// automatically populated on creation of first Context
var context: Context = null
// val timeoutOption = AttributeOption(Attribute(
// SKeyword("timeout"), value = Some(SNumeral(1000))))
def checkSat(query: Expr): Option[Boolean] = {
val solver = new DRealSolver(context)
solver.writeLogic()
// solver.emit(SetOption(timeoutOption))
solver.assertConstraint(query)
val res = solver.checkSat
solver.free()
......@@ -106,7 +105,7 @@ class DRealInterpreter(executable: String, args: Array[String])
* "delat-sat with delta = <some number>"
* instead of "sat".
* It makes use of internal parser functions and can therefore be considered
* as a HACK.
* a HACK.
*/
private def parseCheckSatResult(): SExpr = {
// In the case of "delta-sat", further tokens which need to be consumed
......@@ -148,18 +147,31 @@ class DRealInterpreter(executable: String, args: Array[String])
in.write("\n")
in.flush()
in.close()
val res = parseCheckSatResult()
// now kill the process
invalidated = true
kill()
res
// dReal does not support timeouts, so we have to use this Future
// construction to achieve similar results.
val f = Future {
blocking {
parseCheckSatResult()
}
} (ExecutionContext.global)
try {
Await.result(f, 1.second) // TODO parameter?
} catch {
case e: TimeoutException => CheckSatStatus(UnknownStatus)
} finally {
// now kill the process
invalidated = true
kill()
}
case _ =>
// otherwise, just accept further input
Success
}
} catch {
case (ex: Exception) => {
println("foo" + ex)
if(cmd == CheckSat()) CheckSatStatus(UnknownStatus)
else ErrorResponse("Solver encountered exception: " + ex)
}
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment