Commit 7e95cd0f authored by Fabian Ritter's avatar Fabian Ritter Committed by Anastasiia

cherry-pick two

parent 836a5836
......@@ -8,19 +8,15 @@
package daisy
package solvers
<<<<<<< HEAD
import scala.collection.immutable.Seq
=======
import scala.collection.immutable.Seq
import _root_.smtlib.interpreters.{Z3Interpreter, ProcessInterpreter}
import _root_.smtlib.parser.Commands._
import _root_.smtlib.parser.Terms.{SKeyword, Attribute, SNumeral, SExpr}
import _root_.smtlib.parser.Terms.{SKeyword, Attribute, SNumeral, SExpr, SSymbol}
import _root_.smtlib.printer.{RecursivePrinter => SMTPrinter}
import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
import lang.Trees._
import lang.Identifiers._
......@@ -33,13 +29,11 @@ object DRealSolver {
// 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()
res
......@@ -59,6 +53,7 @@ class DRealSolver(context: Context) extends SMTLibSolver(context) {
val interpreterOpts = Seq("--in", "--precision "+precision)
def writeLogic() = {
// without this, dReal segfaults
emit(SetLogic(QF_NRA))
}
......@@ -85,7 +80,6 @@ class DRealSolver(context: Context) extends SMTLibSolver(context) {
}
}
// model generation is not supported for dReal
override protected def getModel(filter: Identifier => Boolean): Model = ???
......@@ -100,37 +94,76 @@ class DRealSolver(context: Context) extends SMTLibSolver(context) {
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
* as 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 = {
try {
SMTPrinter.printSExpr(cmd, in)
in.write("\n")
in.flush
cmd match {
case CheckSat() =>
println("bar")
// if we are checking the query, close the pipe and parse the response
SMTPrinter.printCommand(Exit(), in)
in.write("\n")
in.flush
in.close()
// println("next token: " + parser.lexer.nextToken)
parseResponseOf(cmd)
//TODO make unusable for further queries
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)
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()
val res = parseCheckSatResult()
// now kill the process
invalidated = true
kill()
res
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