From 4207c1e70c5ccf0dfb63b3ff3523672a2a80708f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Mon, 26 Oct 2015 14:50:07 +0100
Subject: [PATCH] Added string support in smtlib interface Added more
documentation
---
build.sbt | 2 +-
.../leon/solvers/EnumerationSolver.scala | 2 ++
src/main/scala/leon/solvers/Solver.scala | 2 ++
.../leon/solvers/smtlib/SMTLIBTarget.scala | 36 +++++++++++++++++++
.../scala/leon/utils/IncrementalSet.scala | 12 ++++++-
5 files changed, 52 insertions(+), 2 deletions(-)
diff --git a/build.sbt b/build.sbt
index 9215fea00..5c7ac9891 100644
--- a/build.sbt
+++ b/build.sbt
@@ -143,7 +143,7 @@ def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${versi
lazy val bonsai = ghProject("git://github.com/colder/bonsai.git", "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
-lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "3b6ef4992b6af15d08a7320fd12202f35e97b905")
+lazy val scalaSmtLib = ghProject("git://github.com/MikaelMayer/scala-smtlib.git", "8ef13ef3294ab823aed0bad40678f507b1fe63e2")
lazy val root = (project in file(".")).
configs(RegressionTest, IsabelleTest, IntegrTest).
diff --git a/src/main/scala/leon/solvers/EnumerationSolver.scala b/src/main/scala/leon/solvers/EnumerationSolver.scala
index d7d52d371..a9bbe8b45 100644
--- a/src/main/scala/leon/solvers/EnumerationSolver.scala
+++ b/src/main/scala/leon/solvers/EnumerationSolver.scala
@@ -48,6 +48,7 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
private var model = Model.empty
+ /** @inheritdoc */
def check: Option[Boolean] = {
val timer = context.timers.solvers.enum.check.start()
val res = try {
@@ -78,6 +79,7 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
res
}
+ /** @inheritdoc */
def getModel: Model = {
model
}
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 10902ebbf..85b196a3a 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -23,7 +23,9 @@ trait Solver extends Interruptible {
assertCnstr(Not(vc.condition))
}
+ /** Returns Some(true) if it found a satisfying model, Some(false) if no model exists, and None otherwise */
def check: Option[Boolean]
+ /** Returns the model if it exists */
def getModel: Model
def getResultSolver: Option[Solver] = Some(this)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 01b35d9de..5d11ec592 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -26,6 +26,7 @@ import _root_.smtlib.parser.Terms.{
}
import _root_.smtlib.parser.CommandsResponses.{ Error => ErrorResponse, _ }
import _root_.smtlib.theories._
+import _root_.smtlib.theories.experimental._
import _root_.smtlib.interpreters.ProcessInterpreter
trait SMTLIBTarget extends Interruptible {
@@ -233,6 +234,7 @@ trait SMTLIBTarget extends Interruptible {
case RealType => Reals.RealSort()
case Int32Type => FixedSizeBitVectors.BitVectorSort(32)
case CharType => FixedSizeBitVectors.BitVectorSort(32)
+ case StringType => Strings.StringSort()
case RawArrayType(from, to) =>
Sort(SMTIdentifier(SSymbol("Array")), Seq(declareSort(from), declareSort(to)))
@@ -356,6 +358,9 @@ trait SMTLIBTarget extends Interruptible {
case FractionalLiteral(n, d) => Reals.Div(Reals.NumeralLit(n), Reals.NumeralLit(d))
case CharLiteral(c) => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(c.toInt))
case BooleanLiteral(v) => Core.BoolConst(v)
+ case StringLiteral(v) =>
+ declareSort(StringType)
+ Strings.StringLit(v)
case Let(b, d, e) =>
val id = id2sym(b)
val value = toSMT(d)
@@ -586,6 +591,12 @@ trait SMTLIBTarget extends Interruptible {
case RealMinus(a, b) => Reals.Sub(toSMT(a), toSMT(b))
case RealTimes(a, b) => Reals.Mul(toSMT(a), toSMT(b))
case RealDivision(a, b) => Reals.Div(toSMT(a), toSMT(b))
+
+ case StringLength(a) => Strings.Length(toSMT(a))
+ case StringConcat(a, b) => Strings.Concat(toSMT(a), toSMT(b))
+ case SubString(a, start, Plus(start2, length)) if start == start2 =>
+ Strings.Substring(toSMT(a),toSMT(start),toSMT(length))
+ case SubString(a, start, end) => Strings.Substring(toSMT(a),toSMT(start),toSMT(Minus(end, start)))
case And(sub) => Core.And(sub.map(toSMT): _*)
case Or(sub) => Core.Or(sub.map(toSMT): _*)
@@ -641,6 +652,31 @@ trait SMTLIBTarget extends Interruptible {
case (SNumeral(n), Some(RealType)) =>
FractionalLiteral(n, 1)
+
+ case (SString(v), Some(StringType)) =>
+ StringLiteral(v)
+
+ case (Strings.Length(a), _) =>
+ val aa = fromSMT(a)
+ StringLength(aa)
+
+ case (Strings.Concat(a, b, c @ _*), _) =>
+ val aa = fromSMT(a)
+ val bb = fromSMT(b)
+ (StringConcat(aa, bb) /: c.map(fromSMT(_))) {
+ case (s, cc) => StringConcat(s, cc)
+ }
+
+ case (Strings.Substring(s, start, offset), _) =>
+ val ss = fromSMT(s)
+ val tt = fromSMT(start)
+ val oo = fromSMT(offset)
+ oo match {
+ case Minus(otherEnd, `tt`) => SubString(ss, tt, otherEnd)
+ case _ => SubString(ss, tt, Plus(tt, oo))
+ }
+
+ case (Strings.At(a, b), _) => fromSMT(Strings.Substring(a, b, SNumeral(1)))
case (FunctionApplication(SimpleSymbol(SSymbol("ite")), Seq(cond, thenn, elze)), t) =>
IfExpr(
diff --git a/src/main/scala/leon/utils/IncrementalSet.scala b/src/main/scala/leon/utils/IncrementalSet.scala
index 163da296c..311e55096 100644
--- a/src/main/scala/leon/utils/IncrementalSet.scala
+++ b/src/main/scala/leon/utils/IncrementalSet.scala
@@ -6,6 +6,7 @@ import scala.collection.mutable.{Stack, Set => MSet}
import scala.collection.mutable.Builder
import scala.collection.{Iterable, IterableLike, GenSet}
+/** A stack of mutable sets with a set-like API and methods to push and pop */
class IncrementalSet[A] extends IncrementalState
with Iterable[A]
with IterableLike[A, Set[A]]
@@ -14,32 +15,41 @@ class IncrementalSet[A] extends IncrementalState
private[this] val stack = new Stack[MSet[A]]()
override def repr = stack.flatten.toSet
+ /** Removes all the elements */
override def clear(): Unit = {
stack.clear()
}
+ /** Removes all the elements and creates a new set */
def reset(): Unit = {
clear()
push()
}
+ /** Creates one more set level */
def push(): Unit = {
stack.push(MSet())
}
+ /** Removes one set level */
def pop(): Unit = {
stack.pop()
}
+ /** Returns true if the set contains elem */
def apply(elem: A) = repr.contains(elem)
+ /** Returns true if the set contains elem */
def contains(elem: A) = repr.contains(elem)
+ /** Returns an iterator over all the elements */
def iterator = stack.flatten.iterator
+ /** Add an element to the head set */
def += (elem: A) = { stack.head += elem; this }
+ /** Removes an element from all stacked sets */
def -= (elem: A) = { stack.foreach(_ -= elem); this }
override def newBuilder = new scala.collection.mutable.SetBuilder(Set.empty[A])
def result = this
- push()
+ push() // By default, creates a new empty mutable set ready to add elements to it.
}
--
GitLab