Commit 4b5c765c authored by Fabian Ritter's avatar Fabian Ritter Committed by Anastasiia

Split DRealSolver and DRealInterpreter into two files

parent 3e5749af
/*
The contents of this file is heaviy influenced and/or partly taken from
the Leon Project which is released under the BSD 2 clauses license.
See file LEON_LICENSE or go to https://github.com/epfl-lara/leon
for full license details.
*/
package daisy
package solvers
import scala.collection.immutable.Seq
import scala.concurrent.{Future, blocking, ExecutionContext, Await, TimeoutException}
import scala.concurrent.duration._
import _root_.smtlib.interpreters.ProcessInterpreter
import _root_.smtlib.parser.Commands._
import _root_.smtlib.parser.Terms.{SExpr, SSymbol}
import _root_.smtlib.printer.{RecursivePrinter => SMTPrinter}
import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
class DRealInterpreter(executable: String, args: Array[String])
extends ProcessInterpreter(executable, args) {
/**
* if this is set, we have already seen a check-sat query and the solver is
* therefore useless.
*/
private var invalidated: Boolean = false
/** A custom parsing function for the check-sat result.
*
* This is necessary because dReal outputs
* "delat-sat with delta = <some number>"
* instead of "sat".
* It makes use of internal parser functions and can therefore be considered
* a HACK.
*/
private def parseCheckSatResult(): SExpr = {
// In the case of "delta-sat", further tokens which need to be consumed
// would be following, however as the solver is unusable after a check-sat
// query anyway, this does not matter.
parser.parseSymbol match {
case SSymbol("delta-sat") => CheckSatStatus(SatStatus)
case SSymbol("unsat") => CheckSatStatus(UnsatStatus)
case SSymbol("unknown") => CheckSatStatus(UnknownStatus)
case SSymbol("unsupported") => Unsupported
case _ => CheckSatStatus(UnknownStatus)
}
}
/** A custom evaluation function for solver queries.
*
* This function has to be overridden to handle the inconvenient interactive
* behavior of dReal. dReal first reads all queries over stdin and waits for
* the pipe to it being closed (in contrast to writing the answer as soon as
* the query was read).
* Therefore, this method just writes all queries to the solver until a
* check-sat is queried. Then, it closes the pipe, parses the result, and
* makes sure that no further query is sent to the process.
* This is a HACK that prohibits any incremental use of the solver.
*/
override def eval(cmd: SExpr): SExpr = {
if (invalidated) {
ErrorResponse("Solver encountered query after check-sat")
} else {
try {
SMTPrinter.printSExpr(cmd, in)
in.write("\n")
in.flush
cmd match {
case CheckSat() =>
// if we are checking the query, close the pipe and parse the response
SMTPrinter.printCommand(Exit(), in)
in.write("\n")
in.flush()
in.close()
// 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) => {
if(cmd == CheckSat()) CheckSatStatus(UnknownStatus)
else ErrorResponse("Solver encountered exception: " + ex)
}
}
}
}
}
......@@ -11,12 +11,8 @@ 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}
import _root_.smtlib.parser.Terms.SExpr
import _root_.smtlib.printer.{RecursivePrinter => SMTPrinter}
import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
......@@ -89,93 +85,3 @@ class DRealSolver(context: Context) extends SMTLibSolver(context) {
new DRealInterpreter("dReal", opts.toArray)
}
}
class DRealInterpreter(executable: String, args: Array[String])
extends ProcessInterpreter(executable, args) {
/**
* if this is set, we have already seen a check-sat query and the solver is
* therefore useless.
*/
private var invalidated: Boolean = false
/** A custom parsing function for the check-sat result.
*
* This is necessary because dReal outputs
* "delat-sat with delta = <some number>"
* instead of "sat".
* It makes use of internal parser functions and can therefore be considered
* a HACK.
*/
private def parseCheckSatResult(): SExpr = {
// In the case of "delta-sat", further tokens which need to be consumed
// would be following, however as the solver is unusable after a check-sat
// query anyway, this does not matter.
parser.parseSymbol match {
case SSymbol("delta-sat") => CheckSatStatus(SatStatus)
case SSymbol("unsat") => CheckSatStatus(UnsatStatus)
case SSymbol("unknown") => CheckSatStatus(UnknownStatus)
case SSymbol("unsupported") => Unsupported
case _ => CheckSatStatus(UnknownStatus)
}
}
/** A custom evaluation function for solver queries.
*
* This function has to be overridden to handle the inconvenient interactive
* behavior of dReal. dReal first reads all queries over stdin and waits for
* the pipe to it being closed (in contrast to writing the answer as soon as
* the query was read).
* Therefore, this method just writes all queries to the solver until a
* check-sat is queried. Then, it closes the pipe, parses the result, and
* makes sure that no further query is sent to the process.
* This is a HACK that prohibits any incremental use of the solver.
*/
override def eval(cmd: SExpr): SExpr = {
if (invalidated) {
ErrorResponse("Solver encountered query after check-sat")
} else {
try {
SMTPrinter.printSExpr(cmd, in)
in.write("\n")
in.flush
cmd match {
case CheckSat() =>
// if we are checking the query, close the pipe and parse the response
SMTPrinter.printCommand(Exit(), in)
in.write("\n")
in.flush()
in.close()
// 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) => {
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