From ef3642c69e9ec7e6faad88c26918f0845b9fc103 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 4 Feb 2015 20:36:14 +0100
Subject: [PATCH] unrolling solver correclty interrupts its solver
Fixes a bug, where UnrollingSolver was interrupted but was not
stopping its internal solver, leading to a timeout not being
respected if the internal solver was stucked in a complicated
check operation. UnrollingSolver now takes a Solver with
Interruptible.
In order to do that, Leon now relies on a more recent version of
scala-smtlib, that provides a feature to kill the solver process
in a relatively clean way. Update the SMTLIBSolver code to
actually perform the kill operation on the interrupt.
---
project/Build.scala | 2 +-
.../leon/solvers/combinators/UnrollingSolver.scala | 4 +++-
src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala | 11 +++++++++--
src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala | 6 +++---
4 files changed, 16 insertions(+), 7 deletions(-)
diff --git a/project/Build.scala b/project/Build.scala
index 34aa37019..7d50352f7 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -80,6 +80,6 @@ object Leon extends Build {
def project(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
lazy val bonsai = project("git://github.com/colder/bonsai.git", "8f485605785bda98ac61885b0c8036133783290a")
- lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "1b85768a2a5384170a6d90f4aea56ca7330939fd")
+ lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "e721cf606f73c6ba41f7622c141a1eefef2c712d")
}
}
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 56f7f4af4..8f4d216f7 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -14,7 +14,7 @@ import solvers.templates._
import utils.Interruptible
import evaluators._
-class UnrollingSolver(val context: LeonContext, program: Program, underlying: IncrementalSolver) extends Solver with Interruptible {
+class UnrollingSolver(val context: LeonContext, program: Program, underlying: IncrementalSolver with Interruptible) extends Solver with Interruptible {
val (feelingLucky, useCodeGen) = locally {
var lucky = false
@@ -255,9 +255,11 @@ class UnrollingSolver(val context: LeonContext, program: Program, underlying: In
override def interrupt(): Unit = {
interrupted = true
+ solver.interrupt()
}
override def recoverInterrupt(): Unit = {
+ solver.recoverInterrupt()
interrupted = false
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 51ac76726..5c0276201 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -18,8 +18,15 @@ abstract class SMTLIBSolver(val context: LeonContext,
val program: Program)
extends IncrementalSolver with Interruptible with SMTLIBTarget {
- override def interrupt: Unit = {}
- override def recoverInterrupt(): Unit = {}
+ protected var interrupted = false
+
+ override def interrupt: Unit = {
+ interrupted = true
+ interpreter.interrupt()
+ }
+ override def recoverInterrupt(): Unit = {
+ interrupted = false
+ }
override def name: String = "smt-"+targetName
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index c31506240..53264c59c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -13,7 +13,7 @@ import Definitions._
import utils.Bijection
import _root_.smtlib.common._
-import _root_.smtlib.printer.{PrettyPrinter => SMTPrinter}
+import _root_.smtlib.printer.{RecursivePrinter => SMTPrinter}
import _root_.smtlib.parser.Commands.{Constructor => SMTConstructor, _}
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, Let => SMTLet, _}
import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
@@ -323,7 +323,7 @@ trait SMTLIBTarget {
declareVariable(FreshIdentifier("Unit").setType(UnitType))
case IntLiteral(i) => if (i > 0) Ints.NumeralLit(i) else Ints.Neg(Ints.NumeralLit(-i))
- case CharLiteral(c) => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(c.toInt).get)
+ case CharLiteral(c) => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(c.toInt))
case BooleanLiteral(v) => Core.BoolConst(v)
case StringLiteral(s) => SString(s)
case Let(b,d,e) =>
@@ -558,7 +558,7 @@ trait SMTLIBTarget {
}
interpreter.eval(cmd) match {
- case ErrorResponse(msg) =>
+ case err@ErrorResponse(msg) if !interrupted =>
reporter.fatalError("Unnexpected error from smt-"+targetName+" solver: "+msg)
case res => res
}
--
GitLab