From a0474680f6b64d3441199dfad90ff2124ee2b4f8 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Mon, 29 Sep 2014 18:57:44 +0200
Subject: [PATCH] Implement maps for CVC4, now that it supports constant arrays
reactivate tests for CVC4, if available. Remove non-linear testcase that
worked only on z3 (SumAndMax)
---
project/Build.scala | 2 +-
.../solvers/smtlib/SMTLIBCVC4Target.scala | 39 +++-
.../leon/solvers/smtlib/SMTLIBTarget.scala | 220 +++++++++++++-----
.../leon/solvers/smtlib/SMTLIBZ3Target.scala | 81 -------
.../purescala/valid/SumAndMax.scala | 48 ----
.../PureScalaVerificationRegression.scala | 4 +-
6 files changed, 204 insertions(+), 190 deletions(-)
delete mode 100644 src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
diff --git a/project/Build.scala b/project/Build.scala
index 343e7dd8b..34aa37019 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", "acd60b52bac56e47ef1b855d91a1515a6d9178de")
+ lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "1b85768a2a5384170a6d90f4aea56ca7330939fd")
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index b68f06ec1..7f14022d6 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -10,9 +10,11 @@ import Common._
import Trees._
import Extractors._
import TypeTrees._
+import TreeOps.simplestValue
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
import _root_.smtlib.parser.Commands._
+import _root_.smtlib.theories._
import _root_.smtlib.interpreters.CVC4Interpreter
trait SMTLIBCVC4Target extends SMTLIBTarget {
@@ -31,8 +33,10 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
val cmd = DeclareSort(s, 0)
sendCommand(cmd)
Sort(SMTIdentifier(s))
+
case SetType(base) =>
Sort(SMTIdentifier(SSymbol("Set")), Seq(declareSort(base)))
+
case _ =>
super[SMTLIBTarget].declareSort(t)
}
@@ -47,9 +51,22 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
case (QualifiedIdentifier(SMTIdentifier(SSymbol("emptyset"), Seq()), _), SetType(base)) =>
FiniteSet(Set()).setType(tpe)
- case (FunctionApplication(SimpleSymbol(SSymbol("setenum")), elems), SetType(base)) =>
+ case (FunctionApplication(SimpleSymbol(SSymbol("__array_store_all__")), Seq(_, elem)), RawArrayType(k,v)) =>
+ RawArrayValue(k, Map(), fromSMT(elem, v))
+
+ case (FunctionApplication(SimpleSymbol(SSymbol("store")), Seq(arr, key, elem)), RawArrayType(k,v)) =>
+ val RawArrayValue(_, elems, base) = fromSMT(arr, tpe)
+
+ RawArrayValue(k, elems + (fromSMT(key, k) -> fromSMT(elem, v)), base)
+
+ case (FunctionApplication(SimpleSymbol(SSymbol("singleton")), elems), SetType(base)) =>
FiniteSet(elems.map(fromSMT(_, base)).toSet).setType(tpe)
+ case (FunctionApplication(SimpleSymbol(SSymbol("insert")), elems), SetType(base)) =>
+ val selems = elems.init.map(fromSMT(_, base))
+ val FiniteSet(se) = fromSMT(elems.last, tpe)
+ FiniteSet(se ++ selems).setType(tpe)
+
case (FunctionApplication(SimpleSymbol(SSymbol("union")), elems), SetType(base)) =>
FiniteSet(elems.map(fromSMT(_, tpe) match {
case FiniteSet(elems) => elems
@@ -59,6 +76,12 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
super[SMTLIBTarget].fromSMT(s, tpe)
}
+ def encodeMapType(tpe: TypeTree): TypeTree = tpe match {
+ case MapType(from, to) =>
+ TupleType(Seq(SetType(from), RawArrayType(from, to)))
+ case _ => sys.error("Woot")
+ }
+
override def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]) = e match {
case a @ FiniteArray(elems) =>
val tpe @ ArrayType(base) = normalizeType(a.getType)
@@ -79,14 +102,22 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
if (elems.isEmpty) {
QualifiedIdentifier(SMTIdentifier(SSymbol("emptyset")), Some(declareSort(fs.getType)))
} else {
- FunctionApplication(SSymbol("singleton"), elems.toSeq.map(toSMT))
+ val selems = elems.toSeq.map(toSMT)
+
+ val sgt = FunctionApplication(SSymbol("singleton"), Seq(selems.head));
+
+ if (selems.size > 1) {
+ FunctionApplication(SSymbol("insert"), selems.tail :+ sgt)
+ } else {
+ sgt
+ }
}
case SubsetOf(ss, s) =>
- FunctionApplication(SSymbol("subseteq"), Seq(toSMT(ss), toSMT(s)))
+ FunctionApplication(SSymbol("subset"), Seq(toSMT(ss), toSMT(s)))
case ElementOfSet(e, s) =>
- FunctionApplication(SSymbol("in"), Seq(toSMT(e), toSMT(s)))
+ FunctionApplication(SSymbol("member"), Seq(toSMT(e), toSMT(s)))
case SetDifference(a, b) =>
FunctionApplication(SSymbol("setminus"), Seq(toSMT(a), toSMT(b)))
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index da8533fc4..303276bdf 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -69,6 +69,19 @@ trait SMTLIBTarget {
// Should NEVER escape past SMT-world
case class RawArrayValue(keyTpe: TypeTree, elems: Map[Expr, Expr], default: Expr) extends Expr
+ def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match {
+ case SetType(base) =>
+ assert(r.default == BooleanLiteral(false) && r.keyTpe == base)
+
+ FiniteSet(r.elems.keySet).setType(tpe)
+
+ case RawArrayType(from, to) =>
+ r
+
+ case _ =>
+ unsupported("Unable to extract from raw array for "+tpe)
+ }
+
def unsupported(str: Any) = reporter.fatalError(s"Unsupported in smt-$targetName: $str")
def declareSort(t: TypeTree): Sort = {
@@ -81,99 +94,164 @@ trait SMTLIBTarget {
case RawArrayType(from, to) =>
Sort(SMTIdentifier(SSymbol("Array")), Seq(declareSort(from), declareSort(to)))
+ case MapType(from, to) =>
+ declareMapSort(from, to)
+
case TypeParameter(id) =>
val s = id2sym(id)
val cmd = DeclareSort(s, 0)
sendCommand(cmd)
Sort(SMTIdentifier(s))
+
case _: ClassType | _: TupleType | _: ArrayType | UnitType =>
declareStructuralSort(tpe)
+
case _ =>
unsupported("Sort "+t)
}
}
}
- def freshSym(id: Identifier): SSymbol = freshSym(id.name)
- def freshSym(name: String): SSymbol = id2sym(FreshIdentifier(name))
+ var mapSort: Option[SSymbol] = None
+ var optionSort: Option[SSymbol] = None
- def declareStructuralSort(t: TypeTree): Sort = {
+ def declareOptionSort(of: TypeTree): Sort = {
+ optionSort match {
+ case None =>
+ val t = SSymbol("T")
- def getHierarchy(ct: ClassType): (ClassType, Seq[CaseClassType]) = ct match {
- case act: AbstractClassType =>
- (act, act.knownCCDescendents)
- case cct: CaseClassType =>
- cct.parent match {
- case Some(p) =>
- getHierarchy(p)
- case None =>
- (cct, List(cct))
- }
+ val s = SSymbol("Option")
+ val some = SSymbol("Some")
+ val some_v = SSymbol("Some_v")
+ val none = SSymbol("None")
+
+ val caseSome = SList(some, SList(some_v, t))
+ val caseNone = SList(none)
+
+ val cmd = NonStandardCommand(SList(SSymbol("declare-datatypes"), SList(t), SList(SList(s, caseSome, caseNone))))
+ sendCommand(cmd)
+
+ optionSort = Some(s)
+ case _ =>
}
- case class DataType(sym: SSymbol, cases: Seq[Constructor])
- case class Constructor(sym: SSymbol, tpe: TypeTree, fields: Seq[(SSymbol, TypeTree)])
+ Sort(SMTIdentifier(optionSort.get), Seq(declareSort(of)))
+ }
+
+ def declareMapSort(from: TypeTree, to: TypeTree): Sort = {
+ mapSort match {
+ case None =>
+ val m = SSymbol("Map")
+ val a = SSymbol("A")
+ val b = SSymbol("B")
+ mapSort = Some(m)
- var datatypes = Map[TypeTree, DataType]()
+ val optSort = declareOptionSort(to)
+ val arraySort = Sort(SMTIdentifier(SSymbol("Array")),
+ Seq(Sort(SMTIdentifier(a)), optSort))
- def findDependencies(t: TypeTree): Unit = t match {
- case ct: ClassType =>
- val (root, sub) = getHierarchy(ct)
+ val cmd = DefineSort(m, Seq(a, b), arraySort)
+ sendCommand(cmd)
+ case _ =>
+ }
- if (!(datatypes contains root) && !(sorts containsA root)) {
- val sym = freshSym(ct.id)
+ Sort(SMTIdentifier(mapSort.get), Seq(declareSort(from), declareSort(to)))
+ }
- val conss = sub.map { case cct =>
- Constructor(freshSym(cct.id), cct, cct.fields.map(vd => (freshSym(vd.id), vd.tpe)))
- }
- datatypes += root -> DataType(sym, conss)
- // look for dependencies
- for (ct <- root +: sub; f <- ct.fields) findDependencies(f.tpe)
- }
- case tt @ TupleType(bases) =>
- if (!(datatypes contains t) && !(sorts containsA t)) {
- val sym = freshSym("tuple"+bases.size)
+ def freshSym(id: Identifier): SSymbol = freshSym(id.name)
+ def freshSym(name: String): SSymbol = id2sym(FreshIdentifier(name))
+
+ def getHierarchy(ct: ClassType): (ClassType, Seq[CaseClassType]) = ct match {
+ case act: AbstractClassType =>
+ (act, act.knownCCDescendents)
+ case cct: CaseClassType =>
+ cct.parent match {
+ case Some(p) =>
+ getHierarchy(p)
+ case None =>
+ (cct, List(cct))
+ }
+ }
- val c = Constructor(freshSym(sym.name), tt, bases.zipWithIndex.map {
- case (tpe, i) => (freshSym("_"+(i+1)), tpe)
- })
- datatypes += tt -> DataType(sym, Seq(c))
+ case class DataType(sym: SSymbol, cases: Seq[Constructor])
+ case class Constructor(sym: SSymbol, tpe: TypeTree, fields: Seq[(SSymbol, TypeTree)])
- bases.foreach(findDependencies)
- }
+ def findDependencies(t: TypeTree, dts: Map[TypeTree, DataType] = Map()): Map[TypeTree, DataType] = t match {
+ case ct: ClassType =>
+ val (root, sub) = getHierarchy(ct)
- case UnitType =>
- if (!(datatypes contains t) && !(sorts containsA t)) {
+ if (!(dts contains root) && !(sorts containsA root)) {
+ val sym = freshSym(ct.id)
+
+ val conss = sub.map { case cct =>
+ Constructor(freshSym(cct.id), cct, cct.fields.map(vd => (freshSym(vd.id), vd.tpe)))
+ }
- val sym = freshSym("Unit")
+ var cdts = dts + (root -> DataType(sym, conss))
- datatypes += t -> DataType(sym, Seq(Constructor(freshSym(sym.name), t, Nil)))
+ // look for dependencies
+ for (ct <- root +: sub; f <- ct.fields) {
+ cdts ++= findDependencies(f.tpe, cdts)
}
- case at @ ArrayType(base) =>
- if (!(datatypes contains t) && !(sorts containsA t)) {
- val sym = freshSym("array")
+ cdts
+ } else {
+ dts
+ }
- val c = Constructor(freshSym(sym.name), at, List(
- (freshSym("size"), Int32Type),
- (freshSym("content"), RawArrayType(Int32Type, base))
- ))
+ case tt @ TupleType(bases) =>
+ if (!(dts contains t) && !(sorts containsA t)) {
+ val sym = freshSym("tuple"+bases.size)
- datatypes += at -> DataType(sym, Seq(c))
+ val c = Constructor(freshSym(sym.name), tt, bases.zipWithIndex.map {
+ case (tpe, i) => (freshSym("_"+(i+1)), tpe)
+ })
- findDependencies(base)
+ var cdts = dts + (tt -> DataType(sym, Seq(c)))
+
+ for (b <- bases) {
+ cdts ++= findDependencies(b, cdts)
}
+ cdts
+ } else {
+ dts
+ }
- case _ =>
- }
+ case UnitType =>
+ if (!(dts contains t) && !(sorts containsA t)) {
- // Populates the dependencies of the structural type to define.
- findDependencies(t)
+ val sym = freshSym("Unit")
+
+ dts + (t -> DataType(sym, Seq(Constructor(freshSym(sym.name), t, Nil))))
+ } else {
+ dts
+ }
+
+ case at @ ArrayType(base) =>
+ if (!(dts contains t) && !(sorts containsA t)) {
+ val sym = freshSym("array")
+
+ val c = Constructor(freshSym(sym.name), at, List(
+ (freshSym("size"), Int32Type),
+ (freshSym("content"), RawArrayType(Int32Type, base))
+ ))
+
+ var cdts = dts + (at -> DataType(sym, Seq(c)))
+
+ findDependencies(base, cdts)
+ } else {
+ dts
+ }
+
+ case _ =>
+ dts
+ }
+ def declareDatatypes(datatypes: Map[TypeTree, DataType]): Unit = {
// We pre-declare ADTs
for ((tpe, DataType(sym, _)) <- datatypes) {
sorts += tpe -> Sort(SMTIdentifier(sym))
@@ -199,6 +277,13 @@ trait SMTLIBTarget {
val cmd = DeclareDatatypes(adts)
sendCommand(cmd)
+ }
+
+ def declareStructuralSort(t: TypeTree): Sort = {
+ // Populates the dependencies of the structural type to define.
+ val datatypes = findDependencies(t)
+
+ declareDatatypes(datatypes)
sorts.toB(t)
}
@@ -310,6 +395,33 @@ trait SMTLIBTarget {
val constructor = constructors.toB(tpe)
FunctionApplication(constructor, Seq(ssize, newcontent))
+ /**
+ * ===== Map operations =====
+ */
+ case m @ FiniteMap(elems) =>
+ val mt @ MapType(from, to) = m.getType
+ val ms = declareSort(mt)
+
+ val opt = declareOptionSort(to)
+
+ var res: Term = FunctionApplication(QualifiedIdentifier(SMTIdentifier(SSymbol("const")), Some(ms)), List(QualifiedIdentifier(SMTIdentifier(SSymbol("None")), Some(opt))))
+ for ((k, v) <- elems) {
+ res = ArraysEx.Store(res, toSMT(k), FunctionApplication(SSymbol("Some"), List(toSMT(v))))
+ }
+
+ res
+
+ 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)
+ FunctionApplication(SSymbol("is-Some"), List(ArraysEx.Select(toSMT(m), toSMT(k))))
+
+ /**
+ * ===== Everything else =====
+ */
case e @ UnaryOperator(u, _) =>
e match {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 48d602402..f781cdc48 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -29,15 +29,11 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
val extSym = SSymbol("_")
var setSort: Option[SSymbol] = None
- var mapSort: Option[SSymbol] = None
- var optionSort: Option[SSymbol] = None
override def declareSort(t: TypeTree): Sort = {
val tpe = normalizeType(t)
sorts.cachedB(tpe) {
tpe match {
- case MapType(from, to) =>
- declareMapSort(from, to)
case SetType(base) =>
declareSetSort(base)
case _ =>
@@ -64,49 +60,6 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
Sort(SMTIdentifier(setSort.get), Seq(declareSort(of)))
}
- def declareOptionSort(of: TypeTree): Sort = {
- optionSort match {
- case None =>
- val t = SSymbol("T")
-
- val s = SSymbol("Option")
- val some = SSymbol("Some")
- val some_v = SSymbol("Some_v")
- val none = SSymbol("None")
-
- val caseSome = SList(some, SList(some_v, t))
- val caseNone = none
-
- val cmd = NonStandardCommand(SList(SSymbol("declare-datatypes"), SList(t), SList(SList(s, caseSome, caseNone))))
- sendCommand(cmd)
-
- optionSort = Some(s)
- case _ =>
- }
-
- Sort(SMTIdentifier(optionSort.get), Seq(declareSort(of)))
- }
-
- def declareMapSort(from: TypeTree, to: TypeTree): Sort = {
- mapSort match {
- case None =>
- val m = SSymbol("Map")
- val a = SSymbol("A")
- val b = SSymbol("B")
- mapSort = Some(m)
- declareOptionSort(to)
-
- val arraySort = Sort(SMTIdentifier(SSymbol("Array")),
- Seq(Sort(SMTIdentifier(a)), Sort(SMTIdentifier(optionSort.get), Seq(Sort(SMTIdentifier(b))))))
-
- val cmd = DefineSort(m, Seq(a, b), arraySort)
- sendCommand(cmd)
- case _ =>
- }
-
- Sort(SMTIdentifier(mapSort.get), Seq(declareSort(from), declareSort(to)))
- }
-
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
@@ -145,27 +98,6 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
FunctionApplication(constructors.toB(tpe), List(toSMT(IntLiteral(elems.size)), ar))
- /**
- * ===== 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)
- FunctionApplication(SSymbol("is-Some"), List(ArraysEx.Select(toSMT(m), toSMT(k))))
-
- case m @ FiniteMap(elems) =>
- val ms = declareSort(m.getType)
-
- 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
-
/**
* ===== Set operations =====
*/
@@ -230,19 +162,6 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
unsupported("Unable to extract "+s)
}
- def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match {
- case SetType(base) =>
- assert(r.default == BooleanLiteral(false) && r.keyTpe == base)
-
- FiniteSet(r.elems.keySet).setType(tpe)
-
- case RawArrayType(from, to) =>
- r
-
- case _ =>
- unsupported("Unable to extract from raw array for "+tpe)
- }
-
// EK: We use get-model instead in order to extract models for arrays
override def getModel: Map[Identifier, Expr] = {
diff --git a/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala b/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
deleted file mode 100644
index ea6305cd9..000000000
--- a/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
+++ /dev/null
@@ -1,48 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.lang._
-import leon.annotation._
-
-object SumAndMax {
- sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
- case class Nil() extends List
-
- def max(list : List) : Int = {
- require(list != Nil())
- list match {
- case Cons(x, Nil()) => x
- case Cons(x, xs) => {
- val m2 = max(xs)
- if(m2 > x) m2 else x
- }
- }
- }
-
- def sum(list : List) : Int = list match {
- case Nil() => 0
- case Cons(x, xs) => x + sum(xs)
- }
-
- def size(list : List) : Int = (list match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring(_ >= 0)
-
- def allPos(list : List) : Boolean = list match {
- case Nil() => true
- case Cons(x, xs) => x >= 0 && allPos(xs)
- }
-
- def prop0(list : List) : Boolean = {
- require(list != Nil())
- !allPos(list) || max(list) >= 0
- }.holds
-
- @induct
- def property(list : List) : Boolean = {
- // This precondition was given in the problem but isn't actually useful :D
- // require(allPos(list))
- sum(list) <= size(list) * (if(list == Nil()) 0 else max(list))
- }.holds
-}
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 878bc19da..a52125854 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -71,9 +71,9 @@ class PureScalaVerificationRegression extends LeonTestSuite {
}
val isCVC4Available = try {
- //new CVC4Interpreter()
+ new CVC4Interpreter()
// @EK: CVC4 works on most testcases already, but not all and thus cannot be used in regression.
- false
+ true
} catch {
case e: java.io.IOException =>
false
--
GitLab