Commit 836a5836 authored by Fabian Ritter's avatar Fabian Ritter Committed by Anastasiia

Make unsat queries work

parent 9cbd8084
......@@ -36,7 +36,7 @@ object DRealSolver {
def checkSat(query: Expr): Option[Boolean] = {
val solver = new DRealSolver(context)
solver.emit(SetLogic(QF_NRA))
solver.writeLogic()
// solver.emit(SetOption(timeoutOption))
solver.assertConstraint(query)
......@@ -58,6 +58,10 @@ class DRealSolver(context: Context) extends SMTLibSolver(context) {
val interpreterOpts = Seq("--in", "--precision "+precision)
def writeLogic() = {
emit(SetLogic(QF_NRA))
}
override protected def emit(cmd: SExpr, rawOut: Boolean = false): SExpr = {
debugOut foreach { o =>
SMTPrinter.printSExpr(cmd, o)
......@@ -105,11 +109,13 @@ class DRealInterpreter(executable: String, args: Array[String])
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
......@@ -119,6 +125,7 @@ class DRealInterpreter(executable: String, args: Array[String])
}
} catch {
case (ex: Exception) => {
println("foo" + ex)
if(cmd == CheckSat()) CheckSatStatus(UnknownStatus)
else ErrorResponse("Solver encountered exception: " + ex)
}
......
......@@ -111,10 +111,22 @@ class SolverTest extends UnitSuite {
val constr = Equals(x, Plus(y, bigError))
val solver = new DRealSolver(context)
solver.writeLogic()
solver.assertConstraint(constr)
val res = solver.checkSat
assert(res == Some(true))
solver.free()
}
test("dReal simple unsat") {
val constr = And(GreaterThan(x, RealLiteral(one)),
LessThan(Times(x, x), RealLiteral(zero)))
val solver = new DRealSolver(context)
solver.writeLogic()
solver.assertConstraint(constr)
val res = solver.checkSat
assert(res == Some(false))
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