From cfa1325d15e65dae2b3c50a5c4090544782024d6 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 7 Jul 2014 13:23:28 +0200
Subject: [PATCH] Use most recent version of scala smt-lib
Update the build to reference the most recent version of
scala smt-lib and adapt the code to the new API.
Replace some use of NonStandardCommand by built-in standard
Commands of scala smt-lib.
---
project/Build.scala | 6 +-
src/main/scala/leon/Settings.scala | 1 -
.../solvers/combinators/UnrollingSolver.scala | 4 +
.../solvers/smtlib/SMTLIBCVC4Target.scala | 80 +++---
.../leon/solvers/smtlib/SMTLIBTarget.scala | 231 ++++++++++--------
.../leon/solvers/smtlib/SMTLIBZ3Target.scala | 200 +++++++--------
.../solvers/templates/TemplateGenerator.scala | 3 +-
7 files changed, 278 insertions(+), 247 deletions(-)
diff --git a/project/Build.scala b/project/Build.scala
index cad27e6d3..9fb755bee 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -77,9 +77,9 @@ object Leon extends Build {
).dependsOn(Github.bonsai, Github.scalaSmtLib)
object Github {
- lazy val bonsai = RootProject(uri("git://github.com/colder/bonsai.git#8f485605785bda98ac61885b0c8036133783290a"))
+ def project(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
- private val scalaSmtLibVersion = "4cc4cb1ce38fe62790b674666ab141d0430b0f00"
- lazy val scalaSmtLib = RootProject(uri("git://github.com/regb/scala-smtlib.git#%s".format(scalaSmtLibVersion)))
+ lazy val bonsai = project("git://github.com/colder/bonsai.git", "8f485605785bda98ac61885b0c8036133783290a")
+ lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "51742fa4652243827c34703365e26f0d34adec81")
}
}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 0165a03b9..52ede3a61 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -12,6 +12,5 @@ case class Settings(
val xlang: Boolean = false,
val verify: Boolean = true,
val injectLibrary: Boolean = false,
- val classPath: List[String] = Settings.defaultClassPath(),
val selectedSolvers: Set[String] = Set("fairz3")
)
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 96450da43..56f7f4af4 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -128,6 +128,10 @@ class UnrollingSolver(val context: LeonContext, program: Program, underlying: In
reporter.debug("- Invalid model.")
false
+ case Successful(e) =>
+ reporter.warning("- Model leads unexpected result: "+e)
+ false
+
case RuntimeError(msg) =>
reporter.debug("- Model leads to runtime error.")
false
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index cf2ae8760..155e84522 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -11,9 +11,9 @@ import Trees._
import Extractors._
import TypeTrees._
-import _root_.smtlib.sexpr.SExprs._
+import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
+import _root_.smtlib.parser.Commands._
import _root_.smtlib.interpreters.CVC4Interpreter
-import _root_.smtlib.Commands.{Identifier => _, _}
trait SMTLIBCVC4Target extends SMTLIBTarget {
this: SMTLIBSolver =>
@@ -22,35 +22,35 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
def getNewInterpreter() = new CVC4Interpreter
- override def declareSort(t: TypeTree): SExpr = {
+ override def declareSort(t: TypeTree): Sort = {
val tpe = normalizeType(t)
sorts.cachedB(tpe) {
tpe match {
case TypeParameter(id) =>
val s = id2sym(id)
- val cmd = NonStandardCommand(SList(SSymbol("declare-sort"), s, SInt(0)))
+ val cmd = DeclareSort(s, 0)
sendCommand(cmd)
- s
+ Sort(SMTIdentifier(s))
case SetType(base) =>
- SList(SSymbol("Set"), declareSort(base))
+ Sort(SMTIdentifier(SSymbol("Set")), Seq(declareSort(base)))
case _ =>
super[SMTLIBTarget].declareSort(t)
}
}
}
- override def fromSMT(s: SExpr, tpe: TypeTree)(implicit letDefs: Map[SSymbol, SExpr]): Expr = (s, tpe) match {
- case (s: SSymbol, tp: TypeParameter) =>
- val n = s.s.split("_").toList.last
+ override def fromSMT(s: Term, tpe: TypeTree)(implicit letDefs: Map[SSymbol, Term]): Expr = (s, tpe) match {
+ case (SimpleSymbol(s), tp: TypeParameter) =>
+ val n = s.name.split("_").toList.last
GenericValue(tp, n.toInt)
- case (SList(SSymbol("as") :: SSymbol("emptyset") :: _), SetType(base)) =>
+ case (QualifiedIdentifier(SMTIdentifier(SSymbol("emptyset"), Seq()), _), SetType(base)) =>
FiniteSet(Seq()).setType(tpe)
- case (SList(SSymbol("setenum") :: elems), SetType(base)) =>
+ case (FunctionApplication(SimpleSymbol(SSymbol("setenum")), elems), SetType(base)) =>
FiniteSet(elems.map(fromSMT(_, base))).setType(tpe)
- case (SList(SSymbol("union") :: elems), SetType(base)) =>
+ case (FunctionApplication(SimpleSymbol(SSymbol("union")), elems), SetType(base)) =>
FiniteSet(elems.map(fromSMT(_, tpe) match {
case FiniteSet(elems) => elems
}).flatten).setType(tpe)
@@ -59,43 +59,43 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
super[SMTLIBTarget].fromSMT(s, tpe)
}
- override def toSMT(e: Expr)(implicit bindings: Map[Identifier, SExpr]) = e match {
- case a @ FiniteArray(elems) =>
- val tpe @ ArrayType(base) = normalizeType(a.getType)
- declareSort(tpe)
+ override def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]) = e match {
+ //case a @ FiniteArray(elems) =>
+ // val tpe @ ArrayType(base) = normalizeType(a.getType)
+ // declareSort(tpe)
- var ar: SExpr = declareVariable(FreshIdentifier("arrayconst").setType(RawArrayType(Int32Type, base)))
+ // var ar: SExpr = declareVariable(FreshIdentifier("arrayconst").setType(RawArrayType(Int32Type, base)))
- for ((e, i) <- elems.zipWithIndex) {
- ar = SList(SSymbol("store"), ar, toSMT(IntLiteral(i)), toSMT(e))
- }
+ // for ((e, i) <- elems.zipWithIndex) {
+ // ar = SList(SSymbol("store"), ar, toSMT(IntLiteral(i)), toSMT(e))
+ // }
- SList(constructors.toB(tpe), toSMT(IntLiteral(elems.size)), ar)
+ // SList(constructors.toB(tpe), toSMT(IntLiteral(elems.size)), ar)
- /**
- * ===== Set operations =====
- */
- case fs @ FiniteSet(elems) =>
- if (elems.isEmpty) {
- SList(SSymbol("as"), SSymbol("emptyset"), declareSort(fs.getType))
- } else {
- SList(SSymbol("setenum") :: elems.map(toSMT).toList)
- }
+ ///**
+ // * ===== Set operations =====
+ // */
+ //case fs @ FiniteSet(elems) =>
+ // if (elems.isEmpty) {
+ // SList(SSymbol("as"), SSymbol("emptyset"), declareSort(fs.getType))
+ // } else {
+ // SList(SSymbol("setenum") :: elems.map(toSMT).toList)
+ // }
- case SubsetOf(ss, s) =>
- SList(SSymbol("subseteq"), toSMT(ss), toSMT(s))
+ //case SubsetOf(ss, s) =>
+ // SList(SSymbol("subseteq"), toSMT(ss), toSMT(s))
- case ElementOfSet(e, s) =>
- SList(SSymbol("in"), toSMT(e), toSMT(s))
+ //case ElementOfSet(e, s) =>
+ // SList(SSymbol("in"), toSMT(e), toSMT(s))
- case SetDifference(a, b) =>
- SList(SSymbol("setminus"), toSMT(a), toSMT(b))
+ //case SetDifference(a, b) =>
+ // SList(SSymbol("setminus"), toSMT(a), toSMT(b))
- case SetUnion(a, b) =>
- SList(SSymbol("union"), toSMT(a), toSMT(b))
+ //case SetUnion(a, b) =>
+ // SList(SSymbol("union"), toSMT(a), toSMT(b))
- case SetIntersection(a, b) =>
- SList(SSymbol("intersection"), toSMT(a), toSMT(b))
+ //case SetIntersection(a, b) =>
+ // SList(SSymbol("intersection"), toSMT(a), toSMT(b))
case _ =>
super[SMTLIBTarget].toSMT(e)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 720e238f8..51ea6f67e 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -12,11 +12,13 @@ import TypeTrees._
import Definitions._
import utils.Bijection
-import _root_.smtlib.{PrettyPrinter => SMTPrinter, Interpreter => SMTInterpreter}
-import _root_.smtlib.Commands.{Identifier => _, _}
-import _root_.smtlib.CommandResponses.{Error => ErrorResponse, _}
-import _root_.smtlib.sexpr.SExprs._
-import _root_.smtlib.interpreters._
+import _root_.smtlib.common._
+import _root_.smtlib.printer.{PrettyPrinter => SMTPrinter}
+import _root_.smtlib.parser.Commands.{Constructor => SMTConstructor, _}
+import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, Let => SMTLet, _}
+import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
+import _root_.smtlib.theories._
+import _root_.smtlib.{Interpreter => SMTInterpreter}
trait SMTLIBTarget {
this: SMTLIBSolver =>
@@ -40,7 +42,7 @@ trait SMTLIBTarget {
val selectors = new Bijection[(TypeTree, Int), SSymbol]()
val testers = new Bijection[TypeTree, SSymbol]()
val variables = new Bijection[Identifier, SSymbol]()
- val sorts = new Bijection[TypeTree, SExpr]()
+ val sorts = new Bijection[TypeTree, Sort]()
val functions = new Bijection[TypedFunDef, SSymbol]()
def normalizeType(t: TypeTree): TypeTree = t match {
@@ -59,21 +61,21 @@ trait SMTLIBTarget {
def unsupported(str: Any) = reporter.fatalError(s"Unsupported in smt-$targetName: $str")
- def declareSort(t: TypeTree): SExpr = {
+ def declareSort(t: TypeTree): Sort = {
val tpe = normalizeType(t)
sorts.cachedB(tpe) {
tpe match {
- case BooleanType => SSymbol("Bool")
- case Int32Type => SSymbol("Int")
+ case BooleanType => Core.BoolSort()
+ case Int32Type => Ints.IntSort()
case RawArrayType(from, to) =>
- SList(SSymbol("Array"), declareSort(from), declareSort(to))
+ Sort(SMTIdentifier(SSymbol("Array")), Seq(declareSort(from), declareSort(to)))
case TypeParameter(id) =>
val s = id2sym(id)
- val cmd = NonStandardCommand(SList(SSymbol("declare-sort"), s))
+ val cmd = DeclareSort(s, 0)
sendCommand(cmd)
- s
+ Sort(SMTIdentifier(s))
case _: ClassType | _: TupleType | _: ArrayType | UnitType =>
declareStructuralSort(tpe)
case _ =>
@@ -85,7 +87,7 @@ trait SMTLIBTarget {
def freshSym(id: Identifier): SSymbol = freshSym(id.name)
def freshSym(name: String): SSymbol = id2sym(FreshIdentifier(name))
- def declareStructuralSort(t: TypeTree): SExpr = {
+ def declareStructuralSort(t: TypeTree): Sort = {
def getHierarchy(ct: ClassType): (ClassType, Seq[CaseClassType]) = ct match {
case act: AbstractClassType =>
@@ -125,7 +127,7 @@ trait SMTLIBTarget {
if (!(datatypes contains t) && !(sorts containsA t)) {
val sym = freshSym("tuple"+bases.size)
- val c = Constructor(freshSym(sym.s), tt, bases.zipWithIndex.map {
+ val c = Constructor(freshSym(sym.name), tt, bases.zipWithIndex.map {
case (tpe, i) => (freshSym("_"+(i+1)), tpe)
})
@@ -139,14 +141,14 @@ trait SMTLIBTarget {
val sym = freshSym("Unit")
- datatypes += t -> DataType(sym, Seq(Constructor(freshSym(sym.s), t, Nil)))
+ datatypes += t -> DataType(sym, Seq(Constructor(freshSym(sym.name), t, Nil)))
}
case at @ ArrayType(base) =>
if (!(datatypes contains t) && !(sorts containsA t)) {
val sym = freshSym("array")
- val c = Constructor(freshSym(sym.s), at, List(
+ val c = Constructor(freshSym(sym.name), at, List(
(freshSym("size"), Int32Type),
(freshSym("content"), RawArrayType(Int32Type, base))
))
@@ -164,28 +166,28 @@ trait SMTLIBTarget {
// We pre-declare ADTs
for ((tpe, DataType(sym, _)) <- datatypes) {
- sorts += tpe -> sym
+ sorts += tpe -> Sort(SMTIdentifier(sym))
}
- def toDecl(c: Constructor): SExpr = {
+ def toDecl(c: Constructor): SMTConstructor = {
val s = c.sym
- testers += c.tpe -> SSymbol("is-"+s.s)
+ testers += c.tpe -> SSymbol("is-"+s.name)
constructors += c.tpe -> s
- SList(s :: c.fields.zipWithIndex.map {
+ SMTConstructor(s, c.fields.zipWithIndex.map {
case ((cs, t), i) =>
selectors += (c.tpe, i) -> cs
- SList(cs, declareSort(t))
- }.toList)
+ (cs, declareSort(t))
+ })
}
val adts = for ((tpe, DataType(sym, cases)) <- datatypes.toList) yield {
- SList(sym :: cases.map(toDecl).toList)
+ (sym, cases.map(toDecl))
}
- val cmd = NonStandardCommand(SList(SSymbol("declare-datatypes"), SList(), SList(adts)))
+ val cmd = DeclareDatatypes(adts)
sendCommand(cmd)
sorts.toB(t)
@@ -194,7 +196,7 @@ trait SMTLIBTarget {
def declareVariable(id: Identifier): SSymbol = {
variables.cachedB(id) {
val s = id2sym(id)
- val cmd = NonStandardCommand(SList(SSymbol("declare-const"), s, declareSort(id.getType)))
+ val cmd = DeclareFun(s, List(), declareSort(id.getType))
sendCommand(cmd)
s
}
@@ -208,142 +210,149 @@ trait SMTLIBTarget {
FreshIdentifier(tfd.id.name)
}
val s = id2sym(id)
- sendCommand(DeclareFun(s.s, tfd.params.map(p => declareSort(p.tpe)), declareSort(tfd.returnType)))
+ sendCommand(DeclareFun(s, tfd.params.map(p => declareSort(p.tpe)), declareSort(tfd.returnType)))
s
}
}
- def toSMT(e: Expr)(implicit bindings: Map[Identifier, SExpr]): SExpr = {
+ def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]): Term = {
e match {
case Variable(id) =>
declareSort(e.getType)
- bindings.getOrElse(id, variables.toB(id))
+ bindings.getOrElse(id, QualifiedIdentifier(SMTIdentifier(variables.toB(id))))
case UnitLiteral() =>
declareSort(UnitType)
- declareVariable(FreshIdentifier("Unit").setType(UnitType))
+ QualifiedIdentifier(SMTIdentifier(
+ declareVariable(FreshIdentifier("Unit").setType(UnitType))
+ ))
- case IntLiteral(i) => if (i > 0) SInt(i) else SList(SSymbol("-"), SInt(-i))
- case BooleanLiteral(v) => SSymbol(if (v) "true" else "false")
+ case IntLiteral(i) => if (i > 0) Ints.NumeralLit(i) else Ints.Neg(Ints.NumeralLit(-i))
+ case BooleanLiteral(v) => Core.BoolConst(v)
case StringLiteral(s) => SString(s)
case Let(b,d,e) =>
val id = id2sym(b)
val value = toSMT(d)
- val newBody = toSMT(e)(bindings + (b -> id))
+ val newBody = toSMT(e)(bindings + (b -> QualifiedIdentifier(SMTIdentifier(id))))
- SList(
- SSymbol("let"),
- SList(
- SList(id, value)
- ),
+ SMTLet(
+ VarBinding(id, value),
+ Seq(),
newBody
)
case er @ Error(_) =>
- declareVariable(FreshIdentifier("error_value").setType(er.getType))
+ val s = declareVariable(FreshIdentifier("error_value").setType(er.getType))
+ QualifiedIdentifier(SMTIdentifier(s))
case s @ CaseClassSelector(cct, e, id) =>
declareSort(cct)
- SList(selectors.toB((cct, s.selectorIndex)), toSMT(e))
+ val selector = selectors.toB((cct, s.selectorIndex))
+ FunctionApplication(QualifiedIdentifier(SMTIdentifier(selector)), Seq(toSMT(e)))
case CaseClassInstanceOf(cct, e) =>
declareSort(cct)
- SList(testers.toB(cct), toSMT(e))
+ val tester = testers.toB(cct)
+ FunctionApplication(QualifiedIdentifier(SMTIdentifier(tester)), Seq(toSMT(e)))
case CaseClass(cct, es) =>
declareSort(cct)
+ val constructor = constructors.toB(cct)
if (es.isEmpty) {
- constructors.toB(cct)
+ QualifiedIdentifier(SMTIdentifier(constructor))
} else {
- SList(constructors.toB(cct) :: es.map(toSMT).toList)
+ FunctionApplication(QualifiedIdentifier(SMTIdentifier(constructor)), es.map(toSMT))
}
case t @ Tuple(es) =>
val tpe = normalizeType(t.getType)
declareSort(tpe)
- SList(constructors.toB(tpe) :: es.map(toSMT).toList)
+ val constructor = constructors.toB(tpe)
+ FunctionApplication(QualifiedIdentifier(SMTIdentifier(constructor)), es.map(toSMT))
case ts @ TupleSelect(t, i) =>
val tpe = normalizeType(t.getType)
declareSort(tpe)
- SList(selectors.toB((tpe, i-1)), toSMT(t))
+ val selector = selectors.toB((tpe, i-1))
+ FunctionApplication(QualifiedIdentifier(SMTIdentifier(selector)), Seq(toSMT(t)))
- case al @ ArrayLength(a) =>
- val tpe = normalizeType(a.getType)
- SList(selectors.toB((tpe, 0)), toSMT(a))
+ //TODO
+ //case al @ ArrayLength(a) =>
+ // val tpe = normalizeType(a.getType)
+ // SList(selectors.toB((tpe, 0)), toSMT(a))
- case as @ ArraySelect(a, i) =>
- val tpe = normalizeType(a.getType)
- SList(SSymbol("select"), SList(selectors.toB((tpe, 1)), toSMT(a)), toSMT(i))
+ //case as @ ArraySelect(a, i) =>
+ // val tpe = normalizeType(a.getType)
+ // SList(SSymbol("select"), SList(selectors.toB((tpe, 1)), toSMT(a)), toSMT(i))
- case as @ ArrayUpdated(a, i, e) =>
- val tpe = normalizeType(a.getType)
+ //case as @ ArrayUpdated(a, i, e) =>
+ // val tpe = normalizeType(a.getType)
- val ssize = SList(selectors.toB((tpe, 0)), toSMT(a))
- val scontent = SList(selectors.toB((tpe, 1)), toSMT(a))
+ // val ssize = SList(selectors.toB((tpe, 0)), toSMT(a))
+ // val scontent = SList(selectors.toB((tpe, 1)), toSMT(a))
- SList(constructors.toB(tpe), ssize, SList(SSymbol("store"), scontent, toSMT(i), toSMT(e)))
+ // SList(constructors.toB(tpe), ssize, SList(SSymbol("store"), scontent, toSMT(i), toSMT(e)))
case e @ UnaryOperator(u, _) =>
- val op = e match {
- case _: Not => SSymbol("not")
- case _: UMinus => SSymbol("-")
+ e match {
+ case (_: Not) => Core.Not(toSMT(u))
+ case (_: UMinus) => Ints.Neg(toSMT(u))
case _ => reporter.fatalError("Unhandled unary "+e)
}
- SList(op :: List(u).map(toSMT))
-
case e @ BinaryOperator(a, b, _) =>
- val op = e match {
- case _: Equals => SSymbol("=")
- case _: Implies => SSymbol("=>")
- case _: Iff => SSymbol("=")
- case _: Plus => SSymbol("+")
- case _: Minus => SSymbol("-")
- case _: Times => SSymbol("*")
- case _: Division => SSymbol("div")
- case _: Modulo => SSymbol("mod")
- case _: LessThan => SSymbol("<")
- case _: LessEquals => SSymbol("<=")
- case _: GreaterThan => SSymbol(">")
- case _: GreaterEquals => SSymbol(">=")
+ e match {
+ case (_: Equals) => Core.Equals(toSMT(a), toSMT(b))
+ case (_: Implies) => Core.Implies(toSMT(a), toSMT(b))
+ case (_: Iff) => Core.Equals(toSMT(a), toSMT(b))
+ case (_: Plus) => Ints.Add(toSMT(a), toSMT(b))
+ case (_: Minus) => Ints.Sub(toSMT(a), toSMT(b))
+ case (_: Times) => Ints.Mul(toSMT(a), toSMT(b))
+ case (_: Division) => Ints.Div(toSMT(a), toSMT(b))
+ case (_: Modulo) => Ints.Mod(toSMT(a), toSMT(b))
+ case (_: LessThan) => Ints.LessThan(toSMT(a), toSMT(b))
+ case (_: LessEquals) => Ints.LessEquals(toSMT(a), toSMT(b))
+ case (_: GreaterThan) => Ints.GreaterThan(toSMT(a), toSMT(b))
+ case (_: GreaterEquals) => Ints.GreaterEquals(toSMT(a), toSMT(b))
case _ => reporter.fatalError("Unhandled binary "+e)
}
- SList(op :: List(a, b).map(toSMT))
-
case e @ NAryOperator(sub, _) =>
- val op = e match {
- case _: And => SSymbol("and")
- case _: Or => SSymbol("or")
- case _: IfExpr => SSymbol("ite")
- case f: FunctionInvocation => declareFunction(f.tfd)
+ e match {
+ case (_: And) => Core.And(sub.map(toSMT): _*)
+ case (_: Or) => Core.Or(sub.map(toSMT): _*)
+ case (_: IfExpr) => Core.ITE(toSMT(sub(0)), toSMT(sub(1)), toSMT(sub(2)))
+ case (f: FunctionInvocation) =>
+ FunctionApplication(
+ QualifiedIdentifier(SMTIdentifier(declareFunction(f.tfd))),
+ sub.map(toSMT)
+ )
case _ => reporter.fatalError("Unhandled nary "+e)
}
- SList(op :: sub.map(toSMT).toList)
-
case o => unsupported("Tree: " + o)
}
}
- def fromSMT(pair: (SExpr, TypeTree))(implicit letDefs: Map[SSymbol, SExpr]): Expr = {
+ def fromSMT(pair: (Term, TypeTree))(implicit letDefs: Map[SSymbol, Term]): Expr = {
fromSMT(pair._1, pair._2)
}
- def fromSMT(s: SExpr, tpe: TypeTree)(implicit letDefs: Map[SSymbol, SExpr]): Expr = (s, tpe) match {
+ def fromSMT(s: Term, tpe: TypeTree)(implicit letDefs: Map[SSymbol, Term]): Expr = (s, tpe) match {
case (_, UnitType) =>
UnitLiteral()
- case (SInt(n), Int32Type) =>
+ case (SNumeral(n), Int32Type) =>
IntLiteral(n.toInt)
- case (SSymbol(s), BooleanType) =>
- BooleanLiteral(s == "true")
+ case (Core.True(), BooleanType) => BooleanLiteral(true)
+ case (Core.False(), BooleanType) => BooleanLiteral(false)
- case (s: SSymbol, _: ClassType) if constructors.containsB(s) =>
+ case (SHexadecimal(hexa), Int32Type) => IntLiteral(hexa.toInt)
+
+ case (SimpleSymbol(s), _: ClassType) if constructors.containsB(s) =>
constructors.toA(s) match {
case cct: CaseClassType =>
CaseClass(cct, Nil)
@@ -351,15 +360,15 @@ trait SMTLIBTarget {
unsupported("woot? for a single constructor for non-case-object: "+t)
}
- case (s: SSymbol, tpe) if letDefs contains s =>
+ case (SimpleSymbol(s), tpe) if letDefs contains s =>
fromSMT(letDefs(s), tpe)
- case (s: SSymbol, _) =>
+ case (SimpleSymbol(s), _) =>
variables.getA(s).map(_.toVariable).getOrElse {
unsupported("Unknown symbol: "+s)
}
- case (SList((s: SSymbol) :: args), tpe) if constructors.containsB(s) =>
+ case (FunctionApplication(SimpleSymbol(s), args), tpe) if constructors.containsB(s) =>
constructors.toA(s) match {
case cct: CaseClassType =>
val rargs = args.zip(cct.fields.map(_.tpe)).map(fromSMT)
@@ -382,16 +391,15 @@ trait SMTLIBTarget {
// EK: Since we have no type information, we cannot do type-directed
// extraction of defs, instead, we expand them in smt-world
- case (SList(List(SSymbol("let"), SList(defs), body)), tpe) =>
- val defsMap: Map[SSymbol, SExpr] = defs.map {
- case SList(List(s : SSymbol, value)) =>
- (s, value)
+ case (SMTLet(binding, bindings, body), tpe) =>
+ val defsMap: Map[SSymbol, Term] = (binding +: bindings).map {
+ case VarBinding(s, value) => (s, value)
}.toMap
fromSMT(body, tpe)(letDefs ++ defsMap)
- case (SList(SSymbol(app) :: args), tpe) => {
- app match {
+ case (FunctionApplication(SimpleSymbol(SSymbol(app)), args), tpe) => {
+ name match {
case "-" =>
args match {
case List(a) => UMinus(fromSMT(a, Int32Type))
@@ -403,12 +411,12 @@ trait SMTLIBTarget {
}
}
case _ =>
- unsupported(s)
+ unsupported("Unhandled case in fromSMT: " + (s, tpe))
}
def sendCommand(cmd: Command): CommandResponse = {
reporter.ifDebug { debug =>
- SMTPrinter(cmd, out)
+ SMTPrinter.printCommand(cmd, out)
out.write("\n")
out.flush
}
@@ -422,24 +430,29 @@ trait SMTLIBTarget {
override def assertCnstr(expr: Expr): Unit = {
variablesOf(expr).foreach(declareVariable)
- val sexpr = toSMT(expr)(Map())
- sendCommand(Assert(sexpr))
+ val term = toSMT(expr)(Map())
+ sendCommand(Assert(term))
}
- override def check: Option[Boolean] = sendCommand(CheckSat) match {
+ override def check: Option[Boolean] = sendCommand(CheckSat()) match {
case CheckSatResponse(SatStatus) => Some(true)
case CheckSatResponse(UnsatStatus) => Some(false)
case CheckSatResponse(UnknownStatus) => None
+ case _ => None
}
override def getModel: Map[Identifier, Expr] = {
val syms = variables.bSet.toList
- val cmd: Command = GetValue(syms.head, syms.tail)
+ val cmd: Command =
+ GetValue(QualifiedIdentifier(SMTIdentifier(syms.head)),
+ syms.tail.map(s => QualifiedIdentifier(SMTIdentifier(s)))
+ )
+
val GetValueResponse(valuationPairs) = sendCommand(cmd)
valuationPairs.collect {
- case (sym: SSymbol, value) if variables.containsB(sym) =>
+ case (SimpleSymbol(sym), value) if variables.containsB(sym) =>
val id = variables.toA(sym)
(id, fromSMT(value, id.getType)(Map()))
@@ -452,4 +465,14 @@ trait SMTLIBTarget {
override def pop(lvl: Int = 1): Unit = {
sendCommand(Pop(1))
}
+
+ protected object SimpleSymbol {
+
+ def unapply(term: Term): Option[SSymbol] = term match {
+ case QualifiedIdentifier(SMTIdentifier(sym, Seq()), None) => Some(sym)
+ case _ => None
+ }
+
+ }
+
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 1bd4f6b13..779d759c1 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -12,10 +12,12 @@ import Extractors._
import TypeTrees._
import TreeOps.simplestValue
-import _root_.smtlib.sexpr.SExprs._
+import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
+import _root_.smtlib.parser.Commands.{DefineSort, GetValue, NonStandardCommand, GetModel, DefineFun}
import _root_.smtlib.interpreters.Z3Interpreter
-import _root_.smtlib.Commands.{GetValue, NonStandardCommand}
-import _root_.smtlib.CommandResponses.SExprResponse
+import _root_.smtlib.parser.CommandsResponses.{SExprResponse, GetModelResponse}
+import _root_.smtlib.theories.Core._
+import _root_.smtlib.theories.ArraysEx
trait SMTLIBZ3Target extends SMTLIBTarget {
this: SMTLIBSolver =>
@@ -30,7 +32,7 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
var mapSort: Option[SSymbol] = None
var optionSort: Option[SSymbol] = None
- override def declareSort(t: TypeTree): SExpr = {
+ override def declareSort(t: TypeTree): Sort = {
val tpe = normalizeType(t)
sorts.cachedB(tpe) {
tpe match {
@@ -44,22 +46,25 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
}
}
- def declareSetSort(of: TypeTree) = {
+ def declareSetSort(of: TypeTree): Sort = {
setSort match {
case None =>
val s = SSymbol("Set")
val t = SSymbol("T")
setSort = Some(s)
- val cmd = NonStandardCommand(SList(SSymbol("define-sort"), s, SList(t), SList(SSymbol("Array"), t, SSymbol("Bool"))))
+ val arraySort = Sort(SMTIdentifier(SSymbol("Array")),
+ Seq(Sort(SMTIdentifier(t)), BoolSort()))
+
+ val cmd = DefineSort(s, Seq(t), arraySort)
sendCommand(cmd)
case _ =>
}
- SList(setSort.get, declareSort(of))
+ Sort(SMTIdentifier(setSort.get), Seq(declareSort(of)))
}
- def declareOptionSort(of: TypeTree) = {
+ def declareOptionSort(of: TypeTree): Sort = {
optionSort match {
case None =>
val t = SSymbol("T")
@@ -79,10 +84,10 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
case _ =>
}
- SList(optionSort.get, declareSort(of))
+ Sort(SMTIdentifier(optionSort.get), Seq(declareSort(of)))
}
- def declareMapSort(from: TypeTree, to: TypeTree) = {
+ def declareMapSort(from: TypeTree, to: TypeTree): Sort = {
mapSort match {
case None =>
val m = SSymbol("Map")
@@ -91,127 +96,135 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
mapSort = Some(m)
declareOptionSort(to)
- val cmd = NonStandardCommand(SList(SSymbol("define-sort"), m, SList(a, b), SList(SSymbol("Array"), a, SList(optionSort.get, b))))
+ val arraySort = Sort(SMTIdentifier(SSymbol("Array")),
+ Seq(Sort(SMTIdentifier(optionSort.get)), Sort(SMTIdentifier(b))))
+
+ val cmd = DefineSort(m, Seq(a, b), arraySort)
sendCommand(cmd)
case _ =>
}
- SList(mapSort.get, declareSort(from), declareSort(to))
+ Sort(SMTIdentifier(mapSort.get), Seq(declareSort(from), declareSort(to)))
}
- override def fromSMT(s: SExpr, tpe: TypeTree)(implicit letDefs: Map[SSymbol, SExpr]): Expr = (s, tpe) match {
- case (s: SSymbol, tp: TypeParameter) =>
- val n = s.s.split("!").toList.last
+ override def fromSMT(s: Term, tpe: TypeTree)(implicit letDefs: Map[SSymbol, Term]): Expr = (s, tpe) match {
+ case (SimpleSymbol(s), tp: TypeParameter) =>
+ val n = s.name.split("!").toList.last
GenericValue(tp, n.toInt)
- case (SList(List(`extSym`, SSymbol("as-array"), k: SSymbol)), tpe) =>
- if (letDefs contains k) {
- // Need to recover value form function model
- fromRawArray(extractRawArray(letDefs(k)), tpe)
- } else {
- unsupported(" as-array on non-function or unknown symbol "+k)
- }
+ //case (SList(List(`extSym`, SSymbol("as-array"), k: SSymbol)), tpe) =>
+ // if (letDefs contains k) {
+ // // Need to recover value form function model
+ // fromRawArray(extractRawArray(letDefs(k)), tpe)
+ // } else {
+ // unsupported(" as-array on non-function or unknown symbol "+k)
+ // }
// SMT representation for empty sets: Array(* -> false)
- case (SList(List(SList(List(SSymbol("as"), SSymbol("const"), SList(List(SSymbol("Array"), k, v)))), defV)), tpe) =>
- val ktpe = sorts.fromB(k)
- val vtpe = sorts.fromB(v)
+ //case (SList(List(SList(List(SSymbol("as"), SSymbol("const"), SList(List(SSymbol("Array"), k, v)))), defV)), tpe) =>
+ // val ktpe = sorts.fromB(Sort(SMTIdentifier(k)))
+ // val vtpe = sorts.fromB(Sort(SMTIdentifier(v)))
- fromRawArray(RawArrayValue(ktpe, Map(), fromSMT(defV, vtpe)), tpe)
+ // fromRawArray(RawArrayValue(ktpe, Map(), fromSMT(defV, vtpe)), tpe)
case _ =>
super[SMTLIBTarget].fromSMT(s, tpe)
}
- override def toSMT(e: Expr)(implicit bindings: Map[Identifier, SExpr]) = e match {
- case a @ FiniteArray(elems) =>
- val tpe @ ArrayType(base) = normalizeType(a.getType)
- declareSort(tpe)
+ override def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]): Term = e match {
+ //case a @ FiniteArray(elems) =>
+ // val tpe @ ArrayType(base) = normalizeType(a.getType)
+ // declareSort(tpe)
- var ar = SList(SList(SSymbol("as"), SSymbol("const"), declareSort(RawArrayType(Int32Type, base))), toSMT(simplestValue(base)))
+ // var ar = SList(SList(SSymbol("as"), SSymbol("const"), declareSort(RawArrayType(Int32Type, base))), toSMT(simplestValue(base)))
- for ((e, i) <- elems.zipWithIndex) {
- ar = SList(SSymbol("store"), ar, toSMT(IntLiteral(i)), toSMT(e))
- }
+ // for ((e, i) <- elems.zipWithIndex) {
+ // ar = SList(SSymbol("store"), ar, toSMT(IntLiteral(i)), toSMT(e))
+ // }
- SList(constructors.toB(tpe), toSMT(IntLiteral(elems.size)), ar)
+ // SList(constructors.toB(tpe), toSMT(IntLiteral(elems.size)), ar)
- /**
- * ===== Map operations =====
- */
- case MapGet(m, k) =>
- declareSort(m.getType)
- SList(SSymbol("Some_v"), SList(SSymbol("select"), toSMT(m), toSMT(k)))
+ ///**
+ // * ===== Map operations =====
+ // */
+ //case MapGet(m, k) =>
+ // declareSort(m.getType)
+ // SList(SSymbol("Some_v"), SList(SSymbol("select"), toSMT(m), toSMT(k)))
- case MapIsDefinedAt(m, k) =>
- declareSort(m.getType)
- SList(SSymbol("is-Some"), SList(SSymbol("select"), toSMT(m), toSMT(k)))
+ //case MapIsDefinedAt(m, k) =>
+ // declareSort(m.getType)
+ // SList(SSymbol("is-Some"), SList(SSymbol("select"), toSMT(m), toSMT(k)))
- case m @ FiniteMap(elems) =>
- val ms = declareSort(m.getType)
+ //case m @ FiniteMap(elems) =>
+ // val ms = declareSort(m.getType)
- var res = SList(SList(SSymbol("as"), SSymbol("const"), ms), SSymbol("None"))
- for ((k, v) <- elems) {
- res = SList(SSymbol("store"), res, toSMT(k), SList(SSymbol("Some"), toSMT(v)))
- }
+ // var res = SList(SList(SSymbol("as"), SSymbol("const"), ms), SSymbol("None"))
+ // for ((k, v) <- elems) {
+ // res = SList(SSymbol("store"), res, toSMT(k), SList(SSymbol("Some"), toSMT(v)))
+ // }
- res
+ // res
/**
* ===== Set operations =====
*/
case fs @ FiniteSet(elems) =>
val ss = declareSort(fs.getType)
- var res = SList(SList(SSymbol("as"), SSymbol("const"), ss), toSMT(BooleanLiteral(false)))
+ var res: Term = FunctionApplication(
+ QualifiedIdentifier(SMTIdentifier(SSymbol("const")), Some(ss)),
+ Seq(toSMT(BooleanLiteral(false)))
+ )
for (e <- elems) {
- res = SList(SSymbol("store"), res, toSMT(e), toSMT(BooleanLiteral(true)))
+ res = ArraysEx.Store(res, toSMT(e), toSMT(BooleanLiteral(true)))
}
res
- case SubsetOf(ss, s) =>
- // a isSubset b ==> (a zip b).map(implies) == (* => true)
- val allTrue = SList(SList(SSymbol("as"), SSymbol("const"), declareSort(s.getType)), SSymbol("true"))
- val mapImplies = SList(SList(extSym, SSymbol("map"), SSymbol("implies")), toSMT(ss), toSMT(s))
+ //case SubsetOf(ss, s) =>
+ // // a isSubset b ==> (a zip b).map(implies) == (* => true)
+ // val allTrue = SList(SList(SSymbol("as"), SSymbol("const"), declareSort(s.getType)), SSymbol("true"))
+ // val mapImplies = SList(SList(extSym, SSymbol("map"), SSymbol("implies")), toSMT(ss), toSMT(s))
- SList(SSymbol("="), mapImplies, allTrue)
+ // SList(SSymbol("="), mapImplies, allTrue)
- case ElementOfSet(e, s) =>
- SList(SSymbol("select"), toSMT(s), toSMT(e))
+ //case ElementOfSet(e, s) =>
+ // SList(SSymbol("select"), toSMT(s), toSMT(e))
- case SetDifference(a, b) =>
- // a -- b
- // becomes:
- // a && not(b)
- SList(SList(extSym, SSymbol("map"), SSymbol("and")), toSMT(a), SList(SList(extSym, SSymbol("map"), SSymbol("not")), toSMT(b)))
+ //case SetDifference(a, b) =>
+ // // a -- b
+ // // becomes:
+ // // a && not(b)
+ // SList(SList(extSym, SSymbol("map"), SSymbol("and")), toSMT(a), SList(SList(extSym, SSymbol("map"), SSymbol("not")), toSMT(b)))
case SetUnion(l, r) =>
- SList(SList(extSym, SSymbol("map"), SSymbol("or")), toSMT(l), toSMT(r))
+ FunctionApplication(
+ QualifiedIdentifier(SMTIdentifier(SSymbol("(_ map or)"))), //hack to get around Z3 syntax
+ Seq(toSMT(l), toSMT(r)))
- case SetIntersection(l, r) =>
- SList(SList(extSym, SSymbol("map"), SSymbol("and")), toSMT(l), toSMT(r))
+ //case SetIntersection(l, r) =>
+ // SList(SList(extSym, SSymbol("map"), SSymbol("and")), toSMT(l), toSMT(r))
case _ =>
super.toSMT(e)
}
def extractRawArray(s: SExpr)(implicit letDefs: Map[SSymbol, SExpr]): RawArrayValue = s match {
- case SList(List(SSymbol("define-fun"), a: SSymbol, SList(SList(List(arg, akind)) :: Nil), rkind, body)) =>
- val argTpe = sorts.toA(akind)
- val retTpe = sorts.toA(rkind)
-
- def extractCases(e: SExpr): (Map[Expr, Expr], Expr) = e match {
- case SList(SSymbol("ite") :: SList(SSymbol("=") :: `arg` :: k :: Nil) :: v :: e :: Nil) =>
- val (cs, d) = extractCases(e)
- (Map(fromSMT(k, argTpe) -> fromSMT(v, retTpe)) ++ cs, d)
- case e =>
- (Map(),fromSMT(e, retTpe))
- }
+ //case SList(List(SSymbol("define-fun"), a: SSymbol, SList(SList(List(arg, akind)) :: Nil), rkind, body)) =>
+ // val argTpe = sorts.toA(Sort(SMTIdentifier(akind)))
+ // val retTpe = sorts.toA(Sort(SMTIdentifier(rkind)))
- val (cases, default) = extractCases(body)
+ // def extractCases(e: SExpr): (Map[Expr, Expr], Expr) = e match {
+ // case SList(SSymbol("ite") :: SList(SSymbol("=") :: `arg` :: k :: Nil) :: v :: e :: Nil) =>
+ // val (cs, d) = extractCases(e)
+ // (Map(fromSMT(k, argTpe) -> fromSMT(v, retTpe)) ++ cs, d)
+ // case e =>
+ // (Map(),fromSMT(e, retTpe))
+ // }
- RawArrayValue(argTpe, cases, default)
+ // val (cases, default) = extractCases(body)
+
+ // RawArrayValue(argTpe, cases, default)
case _ =>
unsupported("Unable to extract "+s)
}
@@ -232,20 +245,20 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
// EK: We use get-model instead in order to extract models for arrays
override def getModel: Map[Identifier, Expr] = {
- val cmd = NonStandardCommand(SList(SSymbol("get-model")))
+ val cmd = GetModel()
val res = sendCommand(cmd)
- val smodel = res match {
- case SExprResponse(SList(SSymbol("model") :: entries)) => entries
+ val smodel: Seq[DefineFun] = res match {
+ case GetModelResponse(model) => model
case _ => Nil
}
- var modelFunDefs = Map[SSymbol, SExpr]()
+ var modelFunDefs = Map[SSymbol, DefineFun]()
// First pass to gather functions (arrays defs)
for (me <- smodel) me match {
- case SList(List(SSymbol("define-fun"), a: SSymbol, SList(args), _, _)) if args.nonEmpty =>
+ case DefineFun(a, args, _, _) if args.nonEmpty =>
modelFunDefs += a -> me
case _ =>
}
@@ -253,21 +266,12 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
var model = Map[Identifier, Expr]()
for (me <- smodel) me match {
- case SList(List(SSymbol("define-fun"), s: SSymbol, SList(args), kind, e)) =>
- if (args.isEmpty) {
+ case DefineFun(s, args, kind, e) =>
+ if(args.isEmpty) {
val id = variables.toA(s)
// EK: this is a little hack, we pass models for array functions as let-defs
- model += id -> fromSMT(e, id.getType)(modelFunDefs)
+ model += id -> fromSMT(e, id.getType)(null)//modelFunDefs)
}
-
- case SList(SSymbol("forall") :: _) => // no body
- // Ignore
-
- case SList(SSymbol("declare-fun") :: _) => // no body
- // Ignore
-
- case _ =>
- unsupported("Unknown model entry: "+me)
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 72ffca0b5..cfe2c4221 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -26,7 +26,8 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
val fakeFunDef = new FunDef(FreshIdentifier("fake", true),
Nil,
body.getType,
- variablesOf(body).toSeq.map(id => ValDef(id, id.getType)))
+ variablesOf(body).toSeq.map(id => ValDef(id, id.getType)),
+ DefType.MethodDef)
fakeFunDef.body = Some(body)
--
GitLab