Commit 9cbd8084 authored by Fabian Ritter's avatar Fabian Ritter Committed by Anastasiia

cherry-pick one

parent 1e6eec4e
......@@ -8,47 +8,67 @@
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.printer.{RecursivePrinter => SMTPrinter}
import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
import lang.Trees._
import lang.Identifiers._
object DRealSolver {
// needs to be populated before the first call to checkSat, currently
// 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.emit(SetLogic(QF_NRA))
// solver.emit(SetOption(timeoutOption))
solver.assertConstraint(query)
// context.reporter.warning(s"check sat for $query")
val res = solver.checkSat
solver.free()
res
}
// global counter of "Unknown"s or timeouts
var unknownCounter = 0
}
class DRealSolver(context: Context) extends SMTLibSolver(context) {
override def targetName = "dReal"
// TODO make a parameter?
val precision = 0.000000000000000001
val precision = 0.0000000001
val interpreterOpts = Seq("--in", "--precision "+precision)
override protected def emit(cmd: SExpr, rawOut: Boolean = false): SExpr = {
debugOut foreach { o =>
SMTPrinter.printSExpr(cmd, o)
o.write("\n")
o.flush()
}
SMTPrinter.printSExpr(cmd, commandBuffer)
commandBuffer.write("\n")
commandBuffer.flush()
interpreter.eval(cmd) match {
case err @ ErrorResponse(msg) if !rawOut =>
reporter.warning(s"Unexpected error from $targetName solver: $msg")
......@@ -60,21 +80,29 @@ class DRealSolver(context: Context) extends SMTLibSolver(context) {
res
}
}
// model generation is not supported for dReal
override protected def getModel(filter: Identifier => Boolean): Model = ???
def getNewInterpreter = {
val opts = interpreterOpts
reporter.debug("Invoking solver "+targetName+" with "+opts.mkString(" "))
new DRealInterpreter("dReal", opts.toArray)
}
}
class DRealInterpreter(executable: String, args: Array[String])
extends ProcessInterpreter(executable, args) {
override def eval(cmd: SExpr): SExpr = {
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
......@@ -83,7 +111,8 @@ class DRealInterpreter(executable: String, args: Array[String])
in.flush
in.close()
parseResponseOf(cmd)
//TODO make unusable for further queries
//TODO make unusable for further queries
case _ =>
// otherwise, just accept further input
Success
......@@ -95,4 +124,6 @@ class DRealInterpreter(executable: String, args: Array[String])
}
}
}
}
\ No newline at end of file
}
......@@ -71,4 +71,4 @@ class Z3Solver(context: Context) extends SMTLibSolver(context) {
new Z3Interpreter("z3", opts.toArray)
}
}
\ No newline at end of file
}
......@@ -9,6 +9,7 @@ import utils.Rational
import Rational._
import solvers.Z3Solver
import solvers.DRealSolver
class SolverTest extends UnitSuite {
......@@ -106,4 +107,14 @@ class SolverTest extends UnitSuite {
}
\ No newline at end of file
test("dReal simple sat") {
val constr = Equals(x, Plus(y, bigError))
val solver = new DRealSolver(context)
solver.assertConstraint(constr)
val res = solver.checkSat
assert(res == Some(true))
solver.free()
}
}
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