From 62ed1089d3cac4526d21ecbd67676e02b8881b4d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Tue, 16 Sep 2014 17:53:41 +0200
Subject: [PATCH] Fix support with new SMT-Lib API (base + Z3)
---
project/Build.scala | 2 +-
.../solvers/smtlib/SMTLIBCVC4Target.scala | 2 +-
.../leon/solvers/smtlib/SMTLIBTarget.scala | 82 +++++----
.../leon/solvers/smtlib/SMTLIBZ3Target.scala | 162 ++++++++++--------
4 files changed, 140 insertions(+), 108 deletions(-)
diff --git a/project/Build.scala b/project/Build.scala
index 9fb755bee..a9a95b2bd 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", "51742fa4652243827c34703365e26f0d34adec81")
+ lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "e676aab157382847b27eb436b43d2e0abd8e29ba")
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 155e84522..d26e4d47d 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -39,7 +39,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
}
}
- override def fromSMT(s: Term, tpe: TypeTree)(implicit letDefs: Map[SSymbol, Term]): Expr = (s, tpe) match {
+ override def fromSMT(s: Term, tpe: TypeTree)(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): Expr = (s, tpe) match {
case (SimpleSymbol(s), tp: TypeParameter) =>
val n = s.name.split("_").toList.last
GenericValue(tp, n.toInt)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 51ea6f67e..fe1149bb0 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -219,13 +219,12 @@ trait SMTLIBTarget {
e match {
case Variable(id) =>
declareSort(e.getType)
- bindings.getOrElse(id, QualifiedIdentifier(SMTIdentifier(variables.toB(id))))
+ bindings.getOrElse(id, variables.toB(id))
case UnitLiteral() =>
declareSort(UnitType)
- QualifiedIdentifier(SMTIdentifier(
- declareVariable(FreshIdentifier("Unit").setType(UnitType))
- ))
+
+ declareVariable(FreshIdentifier("Unit").setType(UnitType))
case IntLiteral(i) => if (i > 0) Ints.NumeralLit(i) else Ints.Neg(Ints.NumeralLit(-i))
case BooleanLiteral(v) => Core.BoolConst(v)
@@ -233,7 +232,7 @@ trait SMTLIBTarget {
case Let(b,d,e) =>
val id = id2sym(b)
val value = toSMT(d)
- val newBody = toSMT(e)(bindings + (b -> QualifiedIdentifier(SMTIdentifier(id))))
+ val newBody = toSMT(e)(bindings + (b -> id))
SMTLet(
VarBinding(id, value),
@@ -243,55 +242,63 @@ trait SMTLIBTarget {
case er @ Error(_) =>
val s = declareVariable(FreshIdentifier("error_value").setType(er.getType))
- QualifiedIdentifier(SMTIdentifier(s))
+ s
case s @ CaseClassSelector(cct, e, id) =>
declareSort(cct)
val selector = selectors.toB((cct, s.selectorIndex))
- FunctionApplication(QualifiedIdentifier(SMTIdentifier(selector)), Seq(toSMT(e)))
+ FunctionApplication(selector, Seq(toSMT(e)))
case CaseClassInstanceOf(cct, e) =>
declareSort(cct)
val tester = testers.toB(cct)
- FunctionApplication(QualifiedIdentifier(SMTIdentifier(tester)), Seq(toSMT(e)))
+ FunctionApplication(tester, Seq(toSMT(e)))
case CaseClass(cct, es) =>
declareSort(cct)
val constructor = constructors.toB(cct)
if (es.isEmpty) {
- QualifiedIdentifier(SMTIdentifier(constructor))
+ constructor
} else {
- FunctionApplication(QualifiedIdentifier(SMTIdentifier(constructor)), es.map(toSMT))
+ FunctionApplication(constructor, es.map(toSMT))
}
case t @ Tuple(es) =>
val tpe = normalizeType(t.getType)
declareSort(tpe)
val constructor = constructors.toB(tpe)
- FunctionApplication(QualifiedIdentifier(SMTIdentifier(constructor)), es.map(toSMT))
+ FunctionApplication(constructor, es.map(toSMT))
case ts @ TupleSelect(t, i) =>
val tpe = normalizeType(t.getType)
declareSort(tpe)
val selector = selectors.toB((tpe, i-1))
- FunctionApplication(QualifiedIdentifier(SMTIdentifier(selector)), Seq(toSMT(t)))
+ FunctionApplication(selector, Seq(toSMT(t)))
+
+ case al @ ArrayLength(a) =>
+ val tpe = normalizeType(a.getType)
+ val selector = selectors.toB((tpe, 0))
+
+ FunctionApplication(selector, Seq(toSMT(a)))
+
+ case al @ ArraySelect(a, i) =>
+ val tpe = normalizeType(a.getType)
- //TODO
- //case al @ ArrayLength(a) =>
- // val tpe = normalizeType(a.getType)
- // SList(selectors.toB((tpe, 0)), toSMT(a))
+ val scontent = FunctionApplication(selectors.toB((tpe, 1)), Seq(toSMT(a)))
- //case as @ ArraySelect(a, i) =>
- // val tpe = normalizeType(a.getType)
- // SList(SSymbol("select"), SList(selectors.toB((tpe, 1)), toSMT(a)), toSMT(i))
+ ArraysEx.Select(scontent, toSMT(i))
- //case as @ ArrayUpdated(a, i, e) =>
- // val tpe = normalizeType(a.getType)
+ case al @ 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 sa = toSMT(a)
+ val ssize = FunctionApplication(selectors.toB((tpe, 0)), Seq(sa))
+ val scontent = FunctionApplication(selectors.toB((tpe, 1)), Seq(sa))
- // SList(constructors.toB(tpe), ssize, SList(SSymbol("store"), scontent, toSMT(i), toSMT(e)))
+ val newcontent = ArraysEx.Store(scontent, toSMT(i), toSMT(e))
+
+ val constructor = constructors.toB(tpe)
+ FunctionApplication(constructor, Seq(ssize, newcontent))
case e @ UnaryOperator(u, _) =>
@@ -325,7 +332,7 @@ trait SMTLIBTarget {
case (_: IfExpr) => Core.ITE(toSMT(sub(0)), toSMT(sub(1)), toSMT(sub(2)))
case (f: FunctionInvocation) =>
FunctionApplication(
- QualifiedIdentifier(SMTIdentifier(declareFunction(f.tfd))),
+ declareFunction(f.tfd),
sub.map(toSMT)
)
case _ => reporter.fatalError("Unhandled nary "+e)
@@ -336,11 +343,11 @@ trait SMTLIBTarget {
}
}
- def fromSMT(pair: (Term, TypeTree))(implicit letDefs: Map[SSymbol, Term]): Expr = {
+ def fromSMT(pair: (Term, TypeTree))(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): Expr = {
fromSMT(pair._1, pair._2)
}
- def fromSMT(s: Term, tpe: TypeTree)(implicit letDefs: Map[SSymbol, Term]): Expr = (s, tpe) match {
+ def fromSMT(s: Term, tpe: TypeTree)(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): Expr = (s, tpe) match {
case (_, UnitType) =>
UnitLiteral()
@@ -360,8 +367,8 @@ trait SMTLIBTarget {
unsupported("woot? for a single constructor for non-case-object: "+t)
}
- case (SimpleSymbol(s), tpe) if letDefs contains s =>
- fromSMT(letDefs(s), tpe)
+ case (SimpleSymbol(s), tpe) if lets contains s =>
+ fromSMT(lets(s), tpe)
case (SimpleSymbol(s), _) =>
variables.getA(s).map(_.toVariable).getOrElse {
@@ -396,10 +403,10 @@ trait SMTLIBTarget {
case VarBinding(s, value) => (s, value)
}.toMap
- fromSMT(body, tpe)(letDefs ++ defsMap)
+ fromSMT(body, tpe)(lets ++ defsMap, letDefs)
case (FunctionApplication(SimpleSymbol(SSymbol(app)), args), tpe) => {
- name match {
+ app match {
case "-" =>
args match {
case List(a) => UMinus(fromSMT(a, Int32Type))
@@ -407,9 +414,11 @@ trait SMTLIBTarget {
}
case _ =>
- unsupported(s)
+ unsupported("Function "+app+" not handled in fromSMT: "+s)
}
}
+ case (QualifiedIdentifier(id, sort), tpe) =>
+ unsupported("Unhandled case in fromSMT: " + id +": "+sort +" ("+tpe+")")
case _ =>
unsupported("Unhandled case in fromSMT: " + (s, tpe))
}
@@ -444,7 +453,7 @@ trait SMTLIBTarget {
override def getModel: Map[Identifier, Expr] = {
val syms = variables.bSet.toList
val cmd: Command =
- GetValue(QualifiedIdentifier(SMTIdentifier(syms.head)),
+ GetValue(syms.head,
syms.tail.map(s => QualifiedIdentifier(SMTIdentifier(s)))
)
@@ -455,7 +464,7 @@ trait SMTLIBTarget {
case (SimpleSymbol(sym), value) if variables.containsB(sym) =>
val id = variables.toA(sym)
- (id, fromSMT(value, id.getType)(Map()))
+ (id, fromSMT(value, id.getType)(Map(), Map()))
}.toMap
}
@@ -475,4 +484,9 @@ trait SMTLIBTarget {
}
+ import scala.language.implicitConversions
+ implicit def symbolToQualifiedId(s: SSymbol): QualifiedIdentifier = {
+ QualifiedIdentifier(SMTIdentifier(s))
+ }
+
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 779d759c1..4feb6a394 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -16,7 +16,7 @@ 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.parser.CommandsResponses.{SExprResponse, GetModelResponse}
-import _root_.smtlib.theories.Core._
+import _root_.smtlib.theories.Core.{Equals => SMTEquals, _}
import _root_.smtlib.theories.ArraysEx
trait SMTLIBZ3Target extends SMTLIBTarget {
@@ -97,7 +97,7 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
declareOptionSort(to)
val arraySort = Sort(SMTIdentifier(SSymbol("Array")),
- Seq(Sort(SMTIdentifier(optionSort.get)), Sort(SMTIdentifier(b))))
+ Seq(Sort(SMTIdentifier(a)), Sort(SMTIdentifier(optionSort.get), Seq(Sort(SMTIdentifier(b))))))
val cmd = DefineSort(m, Seq(a, b), arraySort)
sendCommand(cmd)
@@ -107,64 +107,64 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
Sort(SMTIdentifier(mapSort.get), Seq(declareSort(from), declareSort(to)))
}
- override def fromSMT(s: Term, tpe: TypeTree)(implicit letDefs: Map[SSymbol, Term]): Expr = (s, tpe) match {
+ override def fromSMT(s: Term, tpe: TypeTree)(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): 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 (QualifiedIdentifier(ExtendedIdentifier(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(Sort(SMTIdentifier(k)))
- // val vtpe = sorts.fromB(Sort(SMTIdentifier(v)))
+ case (FunctionApplication(QualifiedIdentifier(SimpleSymbol(SSymbol("const")), Some(ArraysEx.ArraySort(k, v))), Seq(defV)), tpe) =>
+ val ktpe = sorts.fromB(k)
+ val vtpe = sorts.fromB(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, Term]): Term = e match {
- //case a @ FiniteArray(elems) =>
- // val tpe @ ArrayType(base) = normalizeType(a.getType)
- // declareSort(tpe)
+ 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: Term = ArrayConst(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 = ArraysEx.Store(ar, toSMT(IntLiteral(i)), toSMT(e))
+ }
- // SList(constructors.toB(tpe), toSMT(IntLiteral(elems.size)), ar)
+ FunctionApplication(constructors.toB(tpe), List(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)
+ FunctionApplication(SSymbol("Some_v"), List(ArraysEx.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)
+ FunctionApplication(SSymbol("is-Some"), List(ArraysEx.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: Term = FunctionApplication(QualifiedIdentifier(SMTIdentifier(SSymbol("const")), Some(ms)), List(SSymbol("None")))
+ for ((k, v) <- elems) {
+ res = ArraysEx.Store(res, toSMT(k), FunctionApplication(SSymbol("Some"), List(toSMT(v))))
+ }
- // res
+ res
/**
* ===== Set operations =====
@@ -182,49 +182,50 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
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 = ArrayConst(declareSort(s.getType), True())
+
+ SMTEquals(ArrayMap(SSymbol("implies"), toSMT(ss), toSMT(s)), allTrue)
- // SList(SSymbol("="), mapImplies, allTrue)
+ case ElementOfSet(e, s) =>
+ ArraysEx.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)
+
+ ArrayMap(SSymbol("and"), toSMT(a), ArrayMap(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) =>
- FunctionApplication(
- QualifiedIdentifier(SMTIdentifier(SSymbol("(_ map or)"))), //hack to get around Z3 syntax
- Seq(toSMT(l), toSMT(r)))
+ ArrayMap(SSymbol("or"), toSMT(l), toSMT(r))
- //case SetIntersection(l, r) =>
- // SList(SList(extSym, SSymbol("map"), SSymbol("and")), toSMT(l), toSMT(r))
+ case SetIntersection(l, r) =>
+ ArrayMap(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(Sort(SMTIdentifier(akind)))
- // val retTpe = sorts.toA(Sort(SMTIdentifier(rkind)))
+ def extractRawArray(s: DefineFun)(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): RawArrayValue = s match {
+ case DefineFun(a, List(SortedVar(arg, akind)), 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))
- // }
+ def extractCases(e: Term): (Map[Expr, Expr], Expr) = e match {
+ case ITE(SMTEquals(SimpleSymbol(`arg`), k), v, e) =>
+ val (cs, d) = extractCases(e)
+ (Map(fromSMT(k, argTpe) -> fromSMT(v, retTpe)) ++ cs, d)
+ case e =>
+ (Map(),fromSMT(e, retTpe))
+ }
+
+ val (cases, default) = extractCases(body)
- // val (cases, default) = extractCases(body)
+ RawArrayValue(argTpe, cases, default)
- // RawArrayValue(argTpe, cases, default)
case _ =>
unsupported("Unable to extract "+s)
}
@@ -249,7 +250,7 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
val res = sendCommand(cmd)
- val smodel: Seq[DefineFun] = res match {
+ val smodel: Seq[SExpr] = res match {
case GetModelResponse(model) => model
case _ => Nil
}
@@ -258,7 +259,7 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
// First pass to gather functions (arrays defs)
for (me <- smodel) me match {
- case DefineFun(a, args, _, _) if args.nonEmpty =>
+ case me @ DefineFun(a, args, _, _) if args.nonEmpty =>
modelFunDefs += a -> me
case _ =>
}
@@ -270,11 +271,28 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
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)(null)//modelFunDefs)
+ model += id -> fromSMT(e, id.getType)(Map(), modelFunDefs)
}
+ case _ =>
}
model
}
+
+ object ArrayMap {
+ def apply(op: SSymbol, arrs: Term*) = {
+ FunctionApplication(
+ QualifiedIdentifier(SMTIdentifier(SSymbol("(_ map "+op.name+")"))), //hack to get around Z3 syntax
+ arrs)
+ }
+ }
+
+ object ArrayConst {
+ def apply(sort: Sort, default: Term) = {
+ FunctionApplication(
+ QualifiedIdentifier(SMTIdentifier(SSymbol("const")), Some(sort)),
+ List(default))
+ }
+ }
}
--
GitLab