diff --git a/project/Build.scala b/project/Build.scala
index 4f6b4ddd0f3857eb0101cc26165d0bbe4d4f4b22..cad27e6d3252ec65ecf6c974791ac5d8818ddc4c 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -79,7 +79,7 @@ object Leon extends Build {
object Github {
lazy val bonsai = RootProject(uri("git://github.com/colder/bonsai.git#8f485605785bda98ac61885b0c8036133783290a"))
- private val scalaSmtLibVersion = "90f66cf07aef34b05dc5585bb35aca773b3d0d43"
+ private val scalaSmtLibVersion = "4cc4cb1ce38fe62790b674666ab141d0430b0f00"
lazy val scalaSmtLib = RootProject(uri("git://github.com/regb/scala-smtlib.git#%s".format(scalaSmtLibVersion)))
}
}
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index c70d835e5e59fa5ebcf9733b097da20457ade32d..7f5d5f4c64966890842fb5c57699e34c7dff358f 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -576,10 +576,12 @@ object Trees {
}
/* Array operations */
+ @deprecated("Unsupported Array operation with most solvers", "Leon 2.3")
case class ArrayFill(length: Expr, defaultValue: Expr) extends Expr with FixedType {
val fixedType = ArrayType(defaultValue.getType)
}
+ @deprecated("Unsupported Array operation with most solvers", "Leon 2.3")
case class ArrayMake(defaultValue: Expr) extends Expr with FixedType {
val fixedType = ArrayType(defaultValue.getType)
}
@@ -613,6 +615,8 @@ object Trees {
val fixedType = Int32Type
}
case class FiniteArray(exprs: Seq[Expr]) extends Expr
+
+ @deprecated("Unsupported Array operation with most solvers", "Leon 2.3")
case class ArrayClone(array: Expr) extends Expr {
if(array.getType != Untyped)
setType(array.getType)
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index a4b86d0722c0ec44ea51a041fed524b2e19bd42e..eb6908420247e0fb0c09efbb862711293423982d 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -49,7 +49,7 @@ object TypeTrees {
}
- sealed abstract class TypeTree extends Tree
+ abstract class TypeTree extends Tree
case object Untyped extends TypeTree
case object BooleanType extends TypeTree
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index ce5bb8c8907dbb233d5ecb93714b510512bbe2b2..7827dfd693859ce555ebb4fd223b154652775f3e 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -34,10 +34,10 @@ object SolverFactory {
SolverFactory(() => new EnumerationSolver(ctx, program) with TimeoutSolver)
case "smt" | "smt-z3" =>
- SolverFactory(() => new UnrollingSolver(ctx, new SMTLIBSolver(ctx, program) with SMTLIBZ3Target) with TimeoutSolver)
+ SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBSolver(ctx, program) with SMTLIBZ3Target) with TimeoutSolver)
case "smt-cvc4" =>
- SolverFactory(() => new UnrollingSolver(ctx, new SMTLIBSolver(ctx, program) with SMTLIBCVC4Target) with TimeoutSolver)
+ SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBSolver(ctx, program) with SMTLIBCVC4Target) with TimeoutSolver)
case _ =>
ctx.reporter.fatalError("Unknown solver "+name)
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 99dc09f0048f3d46773718d256d5b064d8517baa..96450da434f8e1e23029bf48a0a7cbcd9e2d66f2 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -12,23 +12,42 @@ import purescala.TypeTrees._
import solvers.templates._
import utils.Interruptible
+import evaluators._
-import scala.collection.mutable.{Map=>MutableMap}
+class UnrollingSolver(val context: LeonContext, program: Program, underlying: IncrementalSolver) extends Solver with Interruptible {
-class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
- extends Solver with Interruptible {
+ val (feelingLucky, useCodeGen) = locally {
+ var lucky = false
+ var codegen = false
- private var lastCheckResult: (Boolean, Option[Boolean], Option[Map[Identifier,Expr]]) = (false, None, None)
+ for(opt <- context.options) opt match {
+ case LeonFlagOption("feelinglucky", v) => lucky = v
+ case LeonFlagOption("codegen", v) => codegen = v
+ case _ =>
+ }
- val reporter = context.reporter
+ (lucky, codegen)
+ }
+ private val evaluator : Evaluator = {
+ if(useCodeGen) {
+ new CodeGenEvaluator(context, program)
+ } else {
+ new DefaultEvaluator(context, program)
+ }
+ }
+
+ private var lastCheckResult: (Boolean, Option[Boolean], Option[Map[Identifier,Expr]]) = (false, None, None)
+ private var varsInVC = List[Set[Identifier]](Set())
+ private var constraints = List[List[Expr]](Nil)
private var interrupted: Boolean = false
+ val reporter = context.reporter
+
def name = "U:"+underlying.name
def free {}
- var varsInVC = List[Set[Identifier]](Set())
val templateGenerator = new TemplateGenerator(new TemplateEncoder[Expr] {
def encodeId(id: Identifier): Expr= {
@@ -65,6 +84,7 @@ class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
}
varsInVC = (varsInVC.head ++ freeIds) :: varsInVC.tail
+ constraints = (constraints.head ++ newClauses) :: constraints.tail
}
@@ -72,12 +92,14 @@ class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
unrollingBank.push()
solver.push()
varsInVC = Set[Identifier]() :: varsInVC
+ constraints = Nil :: constraints
}
def pop(lvl: Int = 1) {
unrollingBank.pop(lvl)
solver.pop(lvl)
varsInVC = varsInVC.drop(lvl)
+ constraints = constraints.drop(lvl)
}
def check: Option[Boolean] = {
@@ -90,6 +112,36 @@ class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
lastCheckResult = (true, res, model)
}
+ def isValidModel(model: Map[Identifier, Expr], silenceErrors: Boolean = false): Boolean = {
+ import EvaluationResults._
+
+ val expr = And(constraints.flatten)
+
+ val fullModel = variablesOf(expr).map(v => v -> model.getOrElse(v, simplestValue(v.getType))).toMap
+
+ evaluator.eval(expr, fullModel) match {
+ case Successful(BooleanLiteral(true)) =>
+ reporter.debug("- Model validated.")
+ true
+
+ case Successful(BooleanLiteral(false)) =>
+ reporter.debug("- Invalid model.")
+ false
+
+ case RuntimeError(msg) =>
+ reporter.debug("- Model leads to runtime error.")
+ false
+
+ case EvaluatorError(msg) =>
+ if (silenceErrors) {
+ reporter.debug("- Model leads to evaluator error: " + msg)
+ } else {
+ reporter.warning("- Model leads to evaluator error: " + msg)
+ }
+ false
+ }
+ }
+
def genericCheck(assumptions: Set[Expr]): Option[Boolean] = {
lastCheckResult = (false, None, None)
@@ -99,12 +151,13 @@ class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
solver.push()
solver.assertCnstr(And((assumptions ++ unrollingBank.currentBlockers).toSeq))
val res = solver.check
- solver.pop()
reporter.debug(" - Finished search with blocked literals")
res match {
case None =>
+ solver.pop()
+
reporter.ifDebug { debug =>
reporter.debug("Solver returned unknown!?")
}
@@ -112,23 +165,29 @@ class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
case Some(true) => // SAT
val model = solver.getModel
+ solver.pop()
foundAnswer(Some(true), Some(model))
case Some(false) if !unrollingBank.canUnroll =>
+ solver.pop()
foundAnswer(Some(false))
case Some(false) =>
//debug("UNSAT BECAUSE: "+solver.getUnsatCore.mkString("\n AND \n"))
//debug("UNSAT BECAUSE: "+core.mkString(" AND "))
+ solver.pop()
if (!interrupted) {
- reporter.debug(" - Running search without blocked literals (w/o lucky test)")
+ if (feelingLucky) {
+ reporter.debug(" - Running search without blocked literals (w/ lucky test)")
+ } else {
+ reporter.debug(" - Running search without blocked literals (w/o lucky test)")
+ }
solver.push()
solver.assertCnstr(And(assumptions.toSeq))
val res2 = solver.check
- solver.pop()
res2 match {
case Some(false) =>
@@ -136,10 +195,19 @@ class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
foundAnswer(Some(false))
case Some(true) =>
+ if (feelingLucky && !interrupted) {
+ val model = solver.getModel
+
+ // we might have been lucky :D
+ if (isValidModel(model, silenceErrors = true)) {
+ foundAnswer(Some(true), Some(model))
+ }
+ }
case None =>
foundAnswer(None)
}
+ solver.pop()
}
if(interrupted) {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index f9f9a59e594d5b1663c0e1d4439d9a5624e63a68..cf2ae8760ac2e4df282d21ad9911b0049875da65 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -13,39 +13,91 @@ import TypeTrees._
import _root_.smtlib.sexpr.SExprs._
import _root_.smtlib.interpreters.CVC4Interpreter
+import _root_.smtlib.Commands.{Identifier => _, _}
trait SMTLIBCVC4Target extends SMTLIBTarget {
this: SMTLIBSolver =>
- val targetName = "cvc4"
+ def targetName = "cvc4"
def getNewInterpreter() = new CVC4Interpreter
- val extSym = SSymbol("_")
+ override def declareSort(t: TypeTree): SExpr = {
+ 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)))
+ sendCommand(cmd)
+ s
+ case SetType(base) =>
+ SList(SSymbol("Set"), 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
+ GenericValue(tp, n.toInt)
+
+ case (SList(SSymbol("as") :: SSymbol("emptyset") :: _), SetType(base)) =>
+ FiniteSet(Seq()).setType(tpe)
+
+ case (SList(SSymbol("setenum") :: elems), SetType(base)) =>
+ FiniteSet(elems.map(fromSMT(_, base))).setType(tpe)
+
+ case (SList(SSymbol("union") :: elems), SetType(base)) =>
+ FiniteSet(elems.map(fromSMT(_, tpe) match {
+ case FiniteSet(elems) => elems
+ }).flatten).setType(tpe)
+
+ case _ =>
+ super[SMTLIBTarget].fromSMT(s, tpe)
+ }
override def toSMT(e: Expr)(implicit bindings: Map[Identifier, SExpr]) = e match {
- case fs @ FiniteSet(elems) =>
- val ss = declareSort(fs.getType)
- var res = SList(SSymbol("as"), SSymbol("const"), ss, toSMT(BooleanLiteral(false)))
+ case a @ FiniteArray(elems) =>
+ val tpe @ ArrayType(base) = normalizeType(a.getType)
+ declareSort(tpe)
+
+ 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))
+ }
+
+ 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)
+ }
+
+ case SubsetOf(ss, s) =>
+ SList(SSymbol("subseteq"), toSMT(ss), toSMT(s))
- for (e <- elems) {
- res = SList(SSymbol("store"), res, toSMT(e), toSMT(BooleanLiteral(true)))
- }
+ case ElementOfSet(e, s) =>
+ SList(SSymbol("in"), toSMT(e), toSMT(s))
- res
+ case SetDifference(a, b) =>
+ SList(SSymbol("setminus"), toSMT(a), toSMT(b))
- case sd @ 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))
+ case SetUnion(a, b) =>
+ SList(SSymbol("union"), toSMT(a), toSMT(b))
- case SetIntersection(l, r) =>
- SList(SList(extSym, SSymbol("map"), SSymbol("and")), toSMT(l), toSMT(r))
+ case SetIntersection(a, b) =>
+ SList(SSymbol("intersection"), toSMT(a), toSMT(b))
- case _ =>
- super.toSMT(e)
+ 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 87196540dfde988a43af69440f495889bf07cba2..720e238f83117e60a477246928bd5ffee0107b34 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -49,7 +49,15 @@ trait SMTLIBTarget {
case _ => t
}
- def unsupported(str: Any) = reporter.fatalError(s"Unsupported in $targetName: $str")
+ // Corresponds to a smt map, not a leon/scala array
+ // Should NEVER escape past SMT-world
+ case class RawArrayType(from: TypeTree, to: TypeTree) extends TypeTree
+
+ // Corresponds to a raw array value, which is coerced to a Leon expr depending on target type (set/array)
+ // Should NEVER escape past SMT-world
+ case class RawArrayValue(keyTpe: TypeTree, elems: Map[Expr, Expr], default: Expr) extends Expr
+
+ def unsupported(str: Any) = reporter.fatalError(s"Unsupported in smt-$targetName: $str")
def declareSort(t: TypeTree): SExpr = {
val tpe = normalizeType(t)
@@ -57,17 +65,16 @@ trait SMTLIBTarget {
tpe match {
case BooleanType => SSymbol("Bool")
case Int32Type => SSymbol("Int")
- case UnitType =>
- val s = SSymbol("Unit")
- val cmd = NonStandardCommand(SList(SSymbol("declare-sort"), s))
- sendCommand(cmd)
- s
+
+ case RawArrayType(from, to) =>
+ SList(SSymbol("Array"), declareSort(from), declareSort(to))
+
case TypeParameter(id) =>
val s = id2sym(id)
val cmd = NonStandardCommand(SList(SSymbol("declare-sort"), s))
sendCommand(cmd)
s
- case _: ClassType | _: TupleType =>
+ case _: ClassType | _: TupleType | _: ArrayType | UnitType =>
declareStructuralSort(tpe)
case _ =>
unsupported("Sort "+t)
@@ -115,7 +122,7 @@ trait SMTLIBTarget {
for (ct <- root +: sub; f <- ct.fields) findDependencies(f.tpe)
}
case tt @ TupleType(bases) =>
- if (!(datatypes contains tt) && !(sorts containsA tt)) {
+ if (!(datatypes contains t) && !(sorts containsA t)) {
val sym = freshSym("tuple"+bases.size)
val c = Constructor(freshSym(sym.s), tt, bases.zipWithIndex.map {
@@ -127,8 +134,27 @@ trait SMTLIBTarget {
bases.foreach(findDependencies)
}
- case st @ SetType(base) =>
+ case UnitType =>
+ if (!(datatypes contains t) && !(sorts containsA t)) {
+
+ val sym = freshSym("Unit")
+
+ datatypes += t -> DataType(sym, Seq(Constructor(freshSym(sym.s), 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(
+ (freshSym("size"), Int32Type),
+ (freshSym("content"), RawArrayType(Int32Type, base))
+ ))
+ datatypes += at -> DataType(sym, Seq(c))
+
+ findDependencies(base)
+ }
case _ =>
}
@@ -193,7 +219,11 @@ trait SMTLIBTarget {
declareSort(e.getType)
bindings.getOrElse(id, variables.toB(id))
- case IntLiteral(v) => SInt(v)
+ case UnitLiteral() =>
+ declareSort(UnitType)
+ 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 StringLiteral(s) => SString(s)
case Let(b,d,e) =>
@@ -235,8 +265,26 @@ trait SMTLIBTarget {
case ts @ TupleSelect(t, i) =>
val tpe = normalizeType(t.getType)
+ declareSort(tpe)
SList(selectors.toB((tpe, i-1)), toSMT(t))
+ 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 @ 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))
+
+ 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")
@@ -281,15 +329,21 @@ trait SMTLIBTarget {
}
}
- def extractSpecialSymbols(s: SSymbol): Option[Expr] = {
- None
+ def fromSMT(pair: (SExpr, TypeTree))(implicit letDefs: Map[SSymbol, SExpr]): Expr = {
+ fromSMT(pair._1, pair._2)
}
- def fromSMT(s: SExpr)(implicit bindings: Map[SSymbol, Expr]): Expr = s match {
- case SInt(n) => IntLiteral(n.toInt)
- case SSymbol("true") => BooleanLiteral(true)
- case SSymbol("false") => BooleanLiteral(false)
- case s: SSymbol if constructors.containsB(s) =>
+ def fromSMT(s: SExpr, tpe: TypeTree)(implicit letDefs: Map[SSymbol, SExpr]): Expr = (s, tpe) match {
+ case (_, UnitType) =>
+ UnitLiteral()
+
+ case (SInt(n), Int32Type) =>
+ IntLiteral(n.toInt)
+
+ case (SSymbol(s), BooleanType) =>
+ BooleanLiteral(s == "true")
+
+ case (s: SSymbol, _: ClassType) if constructors.containsB(s) =>
constructors.toA(s) match {
case cct: CaseClassType =>
CaseClass(cct, Nil)
@@ -297,42 +351,51 @@ trait SMTLIBTarget {
unsupported("woot? for a single constructor for non-case-object: "+t)
}
- case s: SSymbol =>
- (bindings.get(s) orElse variables.getA(s).map(_.toVariable)
- orElse extractSpecialSymbols(s)).getOrElse {
+ case (s: SSymbol, tpe) if letDefs contains s =>
+ fromSMT(letDefs(s), tpe)
+
+ case (s: SSymbol, _) =>
+ variables.getA(s).map(_.toVariable).getOrElse {
unsupported("Unknown symbol: "+s)
}
- case SList((s: SSymbol) :: args) if(constructors.containsB(s)) =>
- val rargs = args.map(fromSMT)
+ case (SList((s: SSymbol) :: args), tpe) if constructors.containsB(s) =>
constructors.toA(s) match {
case cct: CaseClassType =>
+ val rargs = args.zip(cct.fields.map(_.tpe)).map(fromSMT)
CaseClass(cct, rargs)
case tt: TupleType =>
+ val rargs = args.zip(tt.bases).map(fromSMT)
Tuple(rargs)
+
+ case at: ArrayType =>
+ val IntLiteral(size) = fromSMT(args(0), Int32Type)
+ val RawArrayValue(_, elems, default) = fromSMT(args(1), RawArrayType(Int32Type, at.base))
+
+ val entries = for (i <- 0 to size-1) yield elems.getOrElse(IntLiteral(i), default)
+
+ FiniteArray(entries).setType(at)
+
case t =>
unsupported("Woot? structural type that is non-structural: "+t)
}
- case SList(List(SSymbol("let"), SList(defs), body)) =>
- val leonDefs: Seq[(SSymbol, Identifier, Expr)] = defs.map {
+ // 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, FreshIdentifier(s.s), fromSMT(value))
- }
+ (s, value)
+ }.toMap
- val newBindings = bindings ++ leonDefs.map(d => d._1 -> d._3)
- val newBody = fromSMT(body)(newBindings)
-
- LetTuple(leonDefs.map(_._2), Tuple(leonDefs.map(_._3)), newBody)
-
- case SList(SSymbol(app) :: args) => {
- val recArgs = args.map(fromSMT)
+ fromSMT(body, tpe)(letDefs ++ defsMap)
+ case (SList(SSymbol(app) :: args), tpe) => {
app match {
case "-" =>
- recArgs match {
- case List(a) => UMinus(a)
- case List(a, b) => Minus(a, b)
+ args match {
+ case List(a) => UMinus(fromSMT(a, Int32Type))
+ case List(a, b) => Minus(fromSMT(a, Int32Type), fromSMT(b, Int32Type))
}
case _ =>
@@ -350,9 +413,11 @@ trait SMTLIBTarget {
out.flush
}
- val response = interpreter.eval(cmd)
- assert(!response.isInstanceOf[Error])
- response
+ interpreter.eval(cmd) match {
+ case ErrorResponse(msg) =>
+ reporter.fatalError("Unnexpected error from smt-"+targetName+" solver: "+msg)
+ case res => res
+ }
}
override def assertCnstr(expr: Expr): Unit = {
@@ -375,7 +440,9 @@ trait SMTLIBTarget {
valuationPairs.collect {
case (sym: SSymbol, value) if variables.containsB(sym) =>
- (variables.toA(sym), fromSMT(value)(Map()))
+ val id = variables.toA(sym)
+
+ (id, fromSMT(value, id.getType)(Map()))
}.toMap
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 127f1e79cd40894687278c90ea9dcaafa992f322..1bd4f6b13f6bc4ea5a05278f30195a4823cbc0c1 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -10,6 +10,7 @@ import Common._
import Trees._
import Extractors._
import TypeTrees._
+import TreeOps.simplestValue
import _root_.smtlib.sexpr.SExprs._
import _root_.smtlib.interpreters.Z3Interpreter
@@ -26,14 +27,19 @@ 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): SExpr = {
val tpe = normalizeType(t)
sorts.cachedB(tpe) {
tpe match {
+ case MapType(from, to) =>
+ declareMapSort(from, to)
case SetType(base) =>
declareSetSort(base)
- case _ => super.declareSort(t)
+ case _ =>
+ super.declareSort(t)
}
}
}
@@ -53,35 +59,108 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
SList(setSort.get, declareSort(of))
}
- override def extractSpecialSymbols(s: SSymbol): Option[Expr] = {
- s.s.split("!").toList.reverse match {
- case n :: "val" :: rest =>
- val sort = rest.reverse.mkString("!")
+ def declareOptionSort(of: TypeTree) = {
+ optionSort match {
+ case None =>
+ val t = SSymbol("T")
- sorts.getA(SSymbol(sort)) match {
- case Some(tp : TypeParameter) =>
- Some(GenericValue(tp, n.toInt))
- case _ =>
- None
- }
+ 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 _ =>
+ }
+
+ SList(optionSort.get, declareSort(of))
+ }
+
+ def declareMapSort(from: TypeTree, to: TypeTree) = {
+ mapSort match {
+ case None =>
+ val m = SSymbol("Map")
+ val a = SSymbol("A")
+ val b = SSymbol("B")
+ mapSort = Some(m)
+ declareOptionSort(to)
+
+ val cmd = NonStandardCommand(SList(SSymbol("define-sort"), m, SList(a, b), SList(SSymbol("Array"), a, SList(optionSort.get, b))))
+ sendCommand(cmd)
case _ =>
- None
}
+
+ SList(mapSort.get, declareSort(from), declareSort(to))
}
- override def fromSMT(s: SExpr)(implicit bindings: Map[SSymbol, Expr]): Expr = s match {
- case SList(List(`extSym`, SSymbol("as-array"), k: SSymbol)) =>
- bindings(k)
+ 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
+ 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)
+ }
// SMT representation for empty sets: Array(* -> false)
- case SList(List(SList(List(SSymbol("as"), SSymbol("const"), SList(List(SSymbol("Array"), s, SSymbol("Bool"))))), SSymbol("false"))) =>
- FiniteSet(Nil).setType(sorts.fromB(s))
+ 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)
+
+ fromRawArray(RawArrayValue(ktpe, Map(), fromSMT(defV, vtpe)), tpe)
case _ =>
- super.fromSMT(s)
+ 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)
+
+ 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))
+ }
+
+ 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)))
+
+ 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)
+
+ 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
+
+ /**
+ * ===== Set operations =====
+ */
case fs @ FiniteSet(elems) =>
val ss = declareSort(fs.getType)
var res = SList(SList(SSymbol("as"), SSymbol("const"), ss), toSMT(BooleanLiteral(false)))
@@ -92,7 +171,17 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
res
- case sd @ SetDifference(a, b) =>
+ 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)
+
+ case ElementOfSet(e, s) =>
+ SList(SSymbol("select"), toSMT(s), toSMT(e))
+
+ case SetDifference(a, b) =>
// a -- b
// becomes:
// a && not(b)
@@ -107,7 +196,40 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
super.toSMT(e)
}
- // We use get-model instead
+ 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))
+ }
+
+ val (cases, default) = extractCases(body)
+
+ RawArrayValue(argTpe, cases, default)
+ case _ =>
+ 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.toSeq).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] = {
val cmd = NonStandardCommand(SList(SSymbol("get-model")))
@@ -119,40 +241,12 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
case _ => Nil
}
- var maps = Map[SSymbol, TypeTree]()
+ var modelFunDefs = Map[SSymbol, SExpr]()
// First pass to gather functions (arrays defs)
for (me <- smodel) me match {
- case SList(List(SSymbol("define-fun"), a: SSymbol, SList(Nil), _, SList(List(`extSym`, SSymbol("as-array"), k: SSymbol)))) =>
- maps += k -> variables.toA(a).getType
- case _ =>
- }
-
- var bindings = Map[SSymbol, Expr]()
-
- // Second pass to gather functions (arrays defs)
- for (me <- smodel) me match {
- case SList(List(SSymbol("define-fun"), s: SSymbol, SList(SList(List(arg, _)) :: Nil), _, e)) if maps contains s =>
- 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)(Map()) -> fromSMT(v)(Map())) ++ cs, d)
- case e =>
- (Map(),fromSMT(e)(Map()))
- }
-
- def buildValue(cases: Map[Expr, Expr], default: Expr, tpe: TypeTree): Expr = tpe match {
- case SetType(base) =>
- assert(default == BooleanLiteral(false))
- FiniteSet(cases.keySet.toSeq).setType(tpe)
- case _ =>
- unsupported("Cannot build array/map model to "+tpe)
- }
-
- val tpe = maps(s)
- val (cases, default) = extractCases(e)
-
- bindings += s -> buildValue(cases, default, tpe)
+ case SList(List(SSymbol("define-fun"), a: SSymbol, SList(args), _, _)) if args.nonEmpty =>
+ modelFunDefs += a -> me
case _ =>
}
@@ -161,7 +255,9 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
for (me <- smodel) me match {
case SList(List(SSymbol("define-fun"), s: SSymbol, SList(args), kind, e)) =>
if (args.isEmpty) {
- model += variables.toA(s) -> fromSMT(e)(bindings)
+ 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)
}
case SList(SSymbol("forall") :: _) => // no body
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 3a52f45070b48c057b90027daebbbfed8966c8a8..878bc19da64fa437ea43873778074caa9081dbbe 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -10,6 +10,8 @@ import leon.verification.{AnalysisPhase,VerificationReport}
import leon.frontends.scalac.ExtractionPhase
import leon.utils.PreprocessingPhase
+import _root_.smtlib.interpreters._
+
import java.io.File
class PureScalaVerificationRegression extends LeonTestSuite {
@@ -48,7 +50,6 @@ class PureScalaVerificationRegression extends LeonTestSuite {
pipeline.run(ctx)(file.getPath :: Nil)
}
} else {
-
val report = pipeline.run(ctx)(file.getPath :: Nil)
block(Output(report, ctx.reporter))
@@ -61,11 +62,33 @@ class PureScalaVerificationRegression extends LeonTestSuite {
"regression/verification/purescala/" + cat,
_.endsWith(".scala"))
+ val isZ3Available = try {
+ new Z3Interpreter()
+ true
+ } catch {
+ case e: java.io.IOException =>
+ false
+ }
+
+ val isCVC4Available = try {
+ //new CVC4Interpreter()
+ // @EK: CVC4 works on most testcases already, but not all and thus cannot be used in regression.
+ false
+ } catch {
+ case e: java.io.IOException =>
+ false
+ }
+
for(f <- fs) {
mkTest(f, List("--feelinglucky", "--library=no"), forError)(block)
mkTest(f, List("--codegen", "--evalground", "--feelinglucky", "--library=no"), forError)(block)
mkTest(f, List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky", "--library=no"), forError)(block)
- mkTest(f, List("--solvers=smt-z3", "--library=no"), forError)(block)
+ if (isZ3Available) {
+ mkTest(f, List("--solvers=smt-z3", "--feelinglucky", "--library=no"), forError)(block)
+ }
+ if (isCVC4Available) {
+ mkTest(f, List("--solvers=smt-cvc4", "--feelinglucky", "--library=no"), forError)(block)
+ }
}
}