From f1d7ec44bea7b8bfca02f8b41a1807d686559947 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 5 Mar 2015 20:25:46 +0100
Subject: [PATCH] update to a more robust smtlib version
---
project/Build.scala | 2 +-
src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala | 8 ++++----
src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala | 4 ++--
3 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/project/Build.scala b/project/Build.scala
index c00065927..11b47c426 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", "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
- lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "cdaf4707ffad39924262b91d33b660ae8d3e6471")
+ lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "48cec57d0a62d206ac553cb1d4a67f50fdf7dbb1")
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index bce269e7a..64503feee 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -619,9 +619,9 @@ trait SMTLIBTarget {
}
override def check: Option[Boolean] = sendCommand(CheckSat()) match {
- case CheckSatResponse(SatStatus) => Some(true)
- case CheckSatResponse(UnsatStatus) => Some(false)
- case CheckSatResponse(UnknownStatus) => None
+ case CheckSatStatus(SatStatus) => Some(true)
+ case CheckSatStatus(UnsatStatus) => Some(false)
+ case CheckSatStatus(UnknownStatus) => None
case _ => None
}
@@ -633,7 +633,7 @@ trait SMTLIBTarget {
)
- val GetValueResponse(valuationPairs) = sendCommand(cmd)
+ val GetValueResponseSuccess(valuationPairs) = sendCommand(cmd)
valuationPairs.collect {
case (SimpleSymbol(sym), value) if variables.containsB(sym) =>
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 5eb55860c..6c0e9cfbf 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -15,7 +15,7 @@ import TreeOps.simplestValue
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
import _root_.smtlib.parser.Commands.{DefineSort, GetModel, DefineFun}
import _root_.smtlib.interpreters.Z3Interpreter
-import _root_.smtlib.parser.CommandsResponses.GetModelResponse
+import _root_.smtlib.parser.CommandsResponses.GetModelResponseSuccess
import _root_.smtlib.theories.Core.{Equals => SMTEquals, _}
import _root_.smtlib.theories.ArraysEx
@@ -171,7 +171,7 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
val res = sendCommand(cmd)
val smodel: Seq[SExpr] = res match {
- case GetModelResponse(model) => model
+ case GetModelResponseSuccess(model) => model
case _ => Nil
}
--
GitLab