diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 7330ca605f4c478c9e4aa025e727fc465f46b333..ff376b905e0dafd5fe9c944f607930f0bc082053 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -49,12 +49,14 @@ abstract class Reporter(val debugSections: Set[DebugSection]) {
emit(account(Message(FATAL, pos, msg)))
onFatal()
}
+
final def internalError(pos: Position, msg : Any) : Nothing = {
emit(account(Message(INTERNAL, pos, msg.toString +
"\nPlease inform the authors of Leon about this message"
)))
onFatal()
}
+
final def internalAssertion(cond : Boolean, pos: Position, msg : Any) : Unit = {
if (!cond) internalError(pos,msg)
}
@@ -86,14 +88,12 @@ abstract class Reporter(val debugSections: Set[DebugSection]) {
}
}
-
def debug(pos: Position, msg: => Any)(implicit section: DebugSection): Unit = {
ifDebug(pos, debug =>
debug(msg)
)(section)
}
-
// No-position alternatives
final def info(msg: Any): Unit = info(NoPosition, msg)
final def warning(msg: Any): Unit = warning(NoPosition, msg)
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index d197872cfa889880e5a3c1f2e1b9420746d38d50..7e1a3ad8cae3e932fee8d9172a72949a842c573c 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -237,22 +237,18 @@ trait CodeGeneration {
private[codegen] val classToLambda = scala.collection.mutable.Map.empty[String, Lambda]
protected def compileLambda(l: Lambda): (String, Seq[(Identifier, String)], Seq[TypeParameter], String) = {
- val (normalized, structSubst) = purescala.ExprOps.normalizeStructure(matchToIfThenElse(l))
- val reverseSubst = structSubst.map(p => p._2 -> p._1)
- val nl = normalized.asInstanceOf[Lambda]
+ val tparams: Seq[TypeParameter] = typeParamsOf(l).toSeq.sortBy(_.id.uniqueName)
- val tparams: Seq[TypeParameter] = typeParamsOf(nl).toSeq.sortBy(_.id.uniqueName)
-
- val closedVars = purescala.ExprOps.variablesOf(nl).toSeq.sortBy(_.uniqueName)
+ val closedVars = purescala.ExprOps.variablesOf(l).toSeq.sortBy(_.uniqueName)
val closuresWithoutMonitor = closedVars.map(id => id -> typeToJVM(id.getType))
val closures = (monitorID -> s"L$MonitorClass;") +:
((if (tparams.nonEmpty) Seq(tpsID -> "[I") else Seq.empty) ++ closuresWithoutMonitor)
- val afName = lambdaToClass.getOrElse(nl, {
+ val afName = lambdaToClass.getOrElse(l, {
val afId = FreshIdentifier("Leon$CodeGen$Lambda$")
val afName = afId.uniqueName
- lambdaToClass += nl -> afName
- classToLambda += afName -> nl
+ lambdaToClass += l -> afName
+ classToLambda += afName -> l
val cf = new ClassFile(afName, Some(LambdaClass))
@@ -293,7 +289,7 @@ trait CodeGeneration {
cch.freeze
}
- val argMapping = nl.args.map(_.id).zipWithIndex.toMap
+ val argMapping = l.args.map(_.id).zipWithIndex.toMap
val closureMapping = closures.map { case (id, jvmt) => id -> (afName, id.uniqueName, jvmt) }.toMap
val newLocals = NoLocals.withArgs(argMapping).withFields(closureMapping).withTypes(tparams)
@@ -307,7 +303,7 @@ trait CodeGeneration {
val apch = apm.codeHandler
- mkBoxedExpr(nl.body, apch)(newLocals)
+ mkBoxedExpr(l.body, apch)(newLocals)
apch << ARETURN
@@ -395,7 +391,7 @@ trait CodeGeneration {
})
(afName, closures.map { case p @ (id, jvmt) =>
- if (id == monitorID || id == tpsID) p else (reverseSubst(id) -> jvmt)
+ if (id == monitorID || id == tpsID) p else (id -> jvmt)
}, tparams, "(" + closures.map(_._2).mkString("") + ")V")
}
@@ -1786,12 +1782,23 @@ trait CodeGeneration {
// Finally check invariant (if it exists)
if (params.checkContracts && ccd.hasInvariant) {
+ val skip = cch.getFreshLabel("skip_invariant")
+ load(monitorID, cch)(newLocs)
+ cch << ALoad(0)
+ cch << Ldc(registerType(cct))
+
+ cch << InvokeVirtual(MonitorClass, "invariantCheck", s"(L$ObjectClass;I)Z")
+ cch << IfEq(skip)
+
+ load(monitorID, cch)(newLocs)
+ cch << ALoad(0)
+ cch << Ldc(registerType(cct))
+
val thisId = FreshIdentifier("this", cct, true)
val invLocals = newLocs.withVar(thisId -> 0)
- mkExpr(IfExpr(FunctionInvocation(cct.invariant.get, Seq(Variable(thisId))),
- BooleanLiteral(true),
- Error(BooleanType, "ADT Invariant failed @" + ccd.invariant.get.getPos)), cch)(invLocals)
- cch << POP
+ mkExpr(FunctionInvocation(cct.invariant.get, Seq(Variable(thisId))), cch)(invLocals)
+ cch << InvokeVirtual(MonitorClass, "invariantResult", s"(L$ObjectClass;IZ)V")
+ cch << Label(skip)
}
cch << RETURN
diff --git a/src/main/scala/leon/codegen/runtime/Monitor.scala b/src/main/scala/leon/codegen/runtime/Monitor.scala
index 07b5e665a1abaf65142877674c785c6c5d02d0f2..e4a0afa66a578cd19bce0e83e66c626d9399c5a6 100644
--- a/src/main/scala/leon/codegen/runtime/Monitor.scala
+++ b/src/main/scala/leon/codegen/runtime/Monitor.scala
@@ -4,7 +4,7 @@ package leon
package codegen.runtime
import utils._
-import purescala.Expressions._
+import purescala.Expressions.{CaseClass => LeonCaseClass, _}
import purescala.Constructors._
import purescala.Definitions._
import purescala.Common._
@@ -29,6 +29,10 @@ abstract class Monitor {
def typeParams(params: Array[Int], tps: Array[Int], newTps: Array[Int]): Array[Int]
+ def invariantCheck(obj: AnyRef, tpeIdx: Int): Boolean
+
+ def invariantResult(obj: AnyRef, tpeIdx: Int, result: Boolean): Unit
+
def onAbstractInvocation(id: Int, tps: Array[Int], args: Array[AnyRef]): AnyRef
def onChooseInvocation(id: Int, tps: Array[Int], args: Array[AnyRef]): AnyRef
@@ -43,6 +47,14 @@ class NoMonitor extends Monitor {
throw new LeonCodeGenEvaluationException("No monitor available.")
}
+ def invariantCheck(obj: AnyRef, tpeIdx: Int): Boolean = {
+ throw new LeonCodeGenEvaluationException("No monitor available.")
+ }
+
+ def invariantResult(obj: AnyRef, tpeIdx: Int, result: Boolean): Unit = {
+ throw new LeonCodeGenEvaluationException("No monitor available.")
+ }
+
def onAbstractInvocation(id: Int, tps: Array[Int], args: Array[AnyRef]): AnyRef = {
throw new LeonCodeGenEvaluationException("No monitor available.")
}
@@ -70,6 +82,21 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
}
}
+ def invariantCheck(obj: AnyRef, tpeIdx: Int): Boolean = {
+ val tpe = unit.runtimeIdToTypeMap(tpeIdx)
+ val cc = unit.jvmToValue(obj, tpe).asInstanceOf[LeonCaseClass]
+ val result = evaluators.Evaluator.invariantCheck(cc)
+ if (result.isFailure) throw new LeonCodeGenRuntimeException("ADT invariant failed @" + cc.ct.classDef.invariant.get.getPos)
+ else result.isRequired
+ }
+
+ def invariantResult(obj: AnyRef, tpeIdx: Int, result: Boolean): Unit = {
+ val tpe = unit.runtimeIdToTypeMap(tpeIdx)
+ val cc = unit.jvmToValue(obj, tpe).asInstanceOf[LeonCaseClass]
+ evaluators.Evaluator.invariantResult(cc, result)
+ if (!result) throw new LeonCodeGenRuntimeException("ADT invariant failed @" + cc.ct.classDef.invariant.get.getPos)
+ }
+
def typeParams(params: Array[Int], tps: Array[Int], newTps: Array[Int]): Array[Int] = {
val tparams = params.toSeq.map(unit.runtimeIdToTypeMap(_).asInstanceOf[TypeParameter])
val static = tps.toSeq.map(unit.runtimeIdToTypeMap(_))
@@ -110,7 +137,7 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
} else {
val tStart = System.currentTimeMillis
- val solverf = SolverFactory.default(ctx, program).withTimeout(10.second)
+ val solverf = SolverFactory.getFromSettings(ctx, program).withTimeout(10.second)
val solver = solverf.getNewSolver()
val newTypes = tps.toSeq.map(unit.runtimeIdToTypeMap(_))
@@ -176,11 +203,16 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
val (tparams, f) = unit.runtimeForallMap(id)
val program = unit.program
- val ctx = unit.ctx.copy(options = unit.ctx.options.map {
- case LeonOption(optDef, value) if optDef == UnrollingProcedure.optFeelingLucky =>
- LeonOption(optDef)(false)
- case opt => opt
- })
+
+ val newOptions = Seq(
+ LeonOption(UnrollingProcedure.optFeelingLucky)(false),
+ LeonOption(UnrollingProcedure.optSilentErrors)(true),
+ LeonOption(UnrollingProcedure.optCheckModels)(true)
+ )
+
+ val ctx = unit.ctx.copy(options = unit.ctx.options.filterNot { opt =>
+ newOptions.exists(no => opt.optionDef == no.optionDef)
+ } ++ newOptions)
ctx.reporter.debug("Executing forall (codegen)!")
val argsSeq = args.toSeq
@@ -190,7 +222,7 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
} else {
val tStart = System.currentTimeMillis
- val solverf = SolverFactory.default(ctx, program).withTimeout(1.second)
+ val solverf = SolverFactory.getFromSettings(ctx, program).withTimeout(.5.second)
val solver = solverf.getNewSolver()
val newTypes = tps.toSeq.map(unit.runtimeIdToTypeMap(_))
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index c308c5e347e859bc192833bf015e4c2013dc26b9..5ae1a57a6f5475c772b0fc950aac9bff7e5a76ea 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -9,6 +9,8 @@ import purescala.Expressions._
import solvers.Model
+import scala.collection.mutable.{Map => MutableMap}
+
abstract class Evaluator(val context: LeonContext, val program: Program) extends LeonComponent {
/** The type of value that this [[Evaluator]] calculates
@@ -104,3 +106,47 @@ trait DeterministicEvaluator extends Evaluator {
trait NDEvaluator extends Evaluator {
type Value = Stream[Expr]
}
+
+object Evaluator {
+
+ /* Global set that tracks checked case-class invariants
+ *
+ * Checking case-class invariants can require invoking a solver
+ * on a ground formula that contains a reference to `this` (the
+ * current case class). If we then wish to check the model
+ * returned by the solver, the expression given to the evaluator
+ * will again contain the constructor for the current case-class.
+ * This will create an invariant-checking loop.
+ *
+ * To avoid this problem, we introduce a global set of invariants
+ * that have already been checked. This set is used by all
+ * evaluators to determine whether the invariant of a given case
+ * class should be checked.
+ */
+ private val checkCache: MutableMap[CaseClass, CheckStatus] = MutableMap.empty
+
+ sealed abstract class CheckStatus {
+ def isFailure: Boolean = this match {
+ case Complete(status) => !status
+ case _ => false
+ }
+
+ def isRequired: Boolean = this == NoCheck
+ }
+
+ case class Complete(success: Boolean) extends CheckStatus
+ case object Pending extends CheckStatus
+ case object NoCheck extends CheckStatus
+
+ def invariantCheck(cc: CaseClass): CheckStatus =
+ if (!cc.ct.classDef.hasInvariant) Complete(true)
+ else checkCache.get(cc).getOrElse {
+ checkCache(cc) = Pending
+ NoCheck
+ }
+
+ def invariantResult(cc: CaseClass, success: Boolean): Unit = {
+ checkCache(cc) = Complete(success)
+ }
+
+}
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 10351213546db205fc52e1fc83d817315de81119..75194a83ff93a26a13839b6bdf30af5f12d85a56 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -22,7 +22,7 @@ import org.apache.commons.lang3.StringEscapeUtils
abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int)
extends ContextualEvaluator(ctx, prog, maxSteps)
- with DeterministicEvaluator {
+ with DeterministicEvaluator {
val name = "evaluator"
val description = "Recursive interpreter for PureScala expressions"
@@ -74,7 +74,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case Assert(cond, oerr, body) =>
e(IfExpr(Not(cond), Error(expr.getType, oerr.getOrElse("Assertion failed @"+expr.getPos)), body))
- case en@Ensuring(body, post) =>
+ case en @ Ensuring(body, post) =>
e(en.toAssert)
case Error(tpe, desc) =>
@@ -210,12 +210,15 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case CaseClass(cct, args) =>
val cc = CaseClass(cct, args.map(e))
- if (cct.classDef.hasInvariant) {
- val i = FreshIdentifier("i", cct)
- e(FunctionInvocation(cct.invariant.get, Seq(Variable(i))))(rctx.withNewVar(i, cc), gctx) match {
- case BooleanLiteral(true) =>
- case BooleanLiteral(false) =>
- throw RuntimeError("ADT invariant violation for " + cct.classDef.id.asString + " reached in evaluation.: " + cct.invariant.get.asString)
+ val check = Evaluator.invariantCheck(cc)
+ if (check.isFailure) {
+ throw RuntimeError("ADT invariant violation for " + cct.classDef.id.asString + " reached in evaluation.: " + cct.invariant.get.asString)
+ } else if (check.isRequired) {
+ e(FunctionInvocation(cct.invariant.get, Seq(cc))) match {
+ case BooleanLiteral(success) =>
+ Evaluator.invariantResult(cc, success)
+ if (!success)
+ throw RuntimeError("ADT invariant violation for " + cct.classDef.id.asString + " reached in evaluation.: " + cct.invariant.get.asString)
case other =>
throw RuntimeError(typeErrorMsg(other, BooleanType))
}
@@ -585,14 +588,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case l @ Lambda(_, _) =>
val mapping = variablesOf(l).map(id => id -> e(Variable(id))).toMap
- val newLambda = replaceFromIDs(mapping, l).asInstanceOf[Lambda]
- val (normalized, _) = normalizeStructure(matchToIfThenElse(newLambda))
- val nl = normalized.asInstanceOf[Lambda]
- if (!gctx.lambdas.isDefinedAt(nl)) {
- val (norm, _) = normalizeStructure(matchToIfThenElse(l))
- gctx.lambdas += (nl -> norm.asInstanceOf[Lambda])
- }
- nl
+ replaceFromIDs(mapping, l).asInstanceOf[Lambda]
case FiniteLambda(mapping, dflt, tpe) =>
FiniteLambda(mapping.map(p => p._1.map(e) -> e(p._2)), e(dflt), tpe)
@@ -609,11 +605,15 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
frlCache.getOrElse((f, context), {
val tStart = System.currentTimeMillis
- val newCtx = ctx.copy(options = ctx.options.map {
- case LeonOption(optDef, value) if optDef == UnrollingProcedure.optFeelingLucky =>
- LeonOption(optDef)(false)
- case opt => opt
- })
+ val newOptions = Seq(
+ LeonOption(UnrollingProcedure.optFeelingLucky)(false),
+ LeonOption(UnrollingProcedure.optSilentErrors)(true),
+ LeonOption(UnrollingProcedure.optCheckModels)(true)
+ )
+
+ val newCtx = ctx.copy(options = ctx.options.filterNot { opt =>
+ newOptions.exists(no => opt.optionDef == no.optionDef)
+ } ++ newOptions)
val solverf = SolverFactory.getFromSettings(newCtx, program).withTimeout(1.second)
val solver = solverf.getNewSolver()
@@ -629,12 +629,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
val domainCnstr = orJoin(quorums.map { quorum =>
val quantifierDomains = quorum.flatMap { case (path, caller, args) =>
- val matcher = e(caller) match {
- case l: Lambda => gctx.lambdas.getOrElse(l, l)
- case ev => ev
- }
-
- val domain = pm.domains.get(matcher)
+ val domain = pm.domains.get(e(caller))
args.zipWithIndex.flatMap {
case (Variable(id),idx) if quantifiers(id) =>
Some(id -> domain.map(cargs => path -> cargs(idx)))
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
index c211ba70677291b3136a8ed28eb3ee04a8d025dc..7058c9ba1a42e9001d463e58ea63f6fe1cb2ed67 100644
--- a/src/main/scala/leon/evaluators/StreamEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -101,6 +101,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
case And(args) if args.isEmpty =>
Stream(BooleanLiteral(true))
+
case And(args) =>
e(args.head).distinct.flatMap {
case BooleanLiteral(false) => Stream(BooleanLiteral(false))
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index f3a9a94caaabf7e5d2c104439f041de680c54f53..7da928faf68b71bdb48068e77f3f3c42018d678a 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -287,51 +287,57 @@ object ExprOps extends GenTreeOps[Expr] {
* This function relies on the static map `typedIds` to ensure identical
* structures and must therefore be synchronized.
*/
- def normalizeStructure(expr: Expr): (Expr, Map[Identifier, Identifier]) = synchronized {
- val allVars : Seq[Identifier] = fold[Seq[Identifier]] {
- (expr, idSeqs) => idSeqs.foldLeft(expr match {
- case Lambda(args, _) => args.map(_.id)
- case Forall(args, _) => args.map(_.id)
- case LetDef(fds, _) => fds.flatMap(_.paramIds)
- case Let(i, _, _) => Seq(i)
- case MatchExpr(_, cses) => cses.flatMap(_.pattern.binders)
- case Passes(_, _, cses) => cses.flatMap(_.pattern.binders)
- case Variable(id) => Seq(id)
- case _ => Seq.empty[Identifier]
- })((acc, seq) => acc ++ seq)
- } (expr).distinct
-
- val grouped : Map[TypeTree, Seq[Identifier]] = allVars.groupBy(_.getType)
- val subst = grouped.foldLeft(Map.empty[Identifier, Identifier]) { case (subst, (tpe, ids)) =>
- val currentVars = typedIds(tpe)
-
- val freshCount = ids.size - currentVars.size
- val typedVars = if (freshCount > 0) {
- val allIds = currentVars ++ List.range(0, freshCount).map(_ => FreshIdentifier("x", tpe, true))
- typedIds += tpe -> allIds
- allIds
- } else {
- currentVars
+ def normalizeStructure(args: Seq[Identifier], expr: Expr): (Seq[Identifier], Expr, Map[Identifier, Expr]) = synchronized {
+ val vars = args.toSet
+
+ class Normalizer extends TreeTransformer {
+ var subst: Map[Identifier, Expr] = Map.empty
+ var remainingIds: Map[TypeTree, List[Identifier]] = typedIds.toMap
+
+ def getId(e: Expr): Identifier = {
+ val newId = remainingIds.get(e.getType) match {
+ case Some(x :: xs) =>
+ remainingIds += e.getType -> xs
+ x
+ case _ =>
+ val x = FreshIdentifier("x", e.getType, true)
+ typedIds(e.getType) = typedIds(e.getType) :+ x
+ x
+ }
+ subst += newId -> e
+ newId
}
- subst ++ (ids zip typedVars)
+ override def transform(id: Identifier): Identifier = subst.get(id) match {
+ case Some(Variable(newId)) => newId
+ case Some(_) => scala.sys.error("Should never happen!")
+ case None => getId(id.toVariable)
+ }
+
+ override def transform(e: Expr)(implicit bindings: Map[Identifier, Identifier]): Expr = e match {
+ case expr if isSimple(expr) && (variablesOf(expr) & vars).isEmpty => getId(expr).toVariable
+ case _ => super.transform(e)
+ }
}
- val normalized = postMap {
- case Lambda(args, body) => Some(Lambda(args.map(vd => vd.copy(id = subst(vd.id))), body))
- case Forall(args, body) => Some(Forall(args.map(vd => vd.copy(id = subst(vd.id))), body))
- case Let(i, e, b) => Some(Let(subst(i), e, b))
- case m@MatchExpr(scrut, cses) => Some(MatchExpr(scrut, cses.map { cse =>
- cse.copy(pattern = replacePatternBinders(cse.pattern, subst))
- }).copiedFrom(m))
- case Passes(in, out, cses) => Some(Passes(in, out, cses.map { cse =>
- cse.copy(pattern = replacePatternBinders(cse.pattern, subst))
- }))
- case Variable(id) => Some(Variable(subst(id)))
- case _ => None
- } (expr)
+ val n = new Normalizer
+ val bindings = args.map(id => id -> n.getId(id.toVariable)).toMap
+ val normalized = n.transform(matchToIfThenElse(expr))(bindings)
+
+ val argsImgSet = bindings.map(_._2).toSet
+ val bodySubst = n.subst.filter(p => !argsImgSet(p._1))
+
+ (args.map(bindings), normalized, bodySubst)
+ }
+
+ def normalizeStructure(lambda: Lambda): (Lambda, Map[Identifier, Expr]) = {
+ val (args, body, subst) = normalizeStructure(lambda.args.map(_.id), lambda.body)
+ (Lambda(args.map(ValDef(_)), body), subst)
+ }
- (normalized, subst)
+ def normalizeStructure(forall: Forall): (Forall, Map[Identifier, Expr]) = {
+ val (args, body, subst) = normalizeStructure(forall.args.map(_.id), forall.body)
+ (Forall(args.map(ValDef(_)), body), subst)
}
/** Returns '''true''' if the formula is Ground,
diff --git a/src/main/scala/leon/purescala/Quantification.scala b/src/main/scala/leon/purescala/Quantification.scala
index 5e10ace6b3246056c26074f6bd8cf701fc2f13ec..82558fe87e2ccdf0966f124fbf0cc3a4e76833f0 100644
--- a/src/main/scala/leon/purescala/Quantification.scala
+++ b/src/main/scala/leon/purescala/Quantification.scala
@@ -79,11 +79,18 @@ object Quantification {
def empty = new Domains(Map.empty, Map.empty)
}
- class Domains (val lambdas: Map[Lambda, Set[Seq[Expr]]], val tpes: Map[TypeTree, Set[Seq[Expr]]]) {
+ class Domains (_lambdas: Map[Lambda, Set[Seq[Expr]]], val tpes: Map[TypeTree, Set[Seq[Expr]]]) {
+ val lambdas = _lambdas.map { case (lambda, domain) =>
+ val (nl, _) = normalizeStructure(lambda)
+ nl -> domain
+ }
+
def get(e: Expr): Set[Seq[Expr]] = {
val specialized: Set[Seq[Expr]] = e match {
case FiniteLambda(mapping, _, _) => mapping.map(_._1).toSet
- case l: Lambda => lambdas.getOrElse(l, Set.empty)
+ case l: Lambda =>
+ val (nl, _) = normalizeStructure(l)
+ lambdas.getOrElse(nl, Set.empty)
case _ => Set.empty
}
specialized ++ tpes.getOrElse(e.getType, Set.empty)
diff --git a/src/main/scala/leon/solvers/unrolling/LambdaManager.scala b/src/main/scala/leon/solvers/unrolling/LambdaManager.scala
index ecc7843f7cb5dd2e755c3a12527269ca4abe8443..775fcc2671f7c108fab00a30de2a039d6eda1298 100644
--- a/src/main/scala/leon/solvers/unrolling/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/unrolling/LambdaManager.scala
@@ -60,9 +60,8 @@ object LambdaTemplate {
"Template for lambda " + ids._1 + ": " + lambda + " is :\n" + templateString()
}
- val (structuralLambda, structSubst) = normalizeStructure(lambda)
- val keyDeps = dependencies.map { case (id, idT) => structSubst(id) -> idT }
- val key = structuralLambda.asInstanceOf[Lambda]
+ val (structuralLambda, deps) = normalizeStructure(lambda)
+ val keyDeps = deps.map { case (id, dep) => id -> encoder.encodeExpr(dependencies)(dep) }
new LambdaTemplate[T](
ids,
@@ -79,8 +78,9 @@ object LambdaTemplate {
lambdas,
matchers,
quantifications,
+ structuralLambda,
keyDeps,
- key -> structSubst,
+ lambda,
lambdaString
)
}
@@ -123,14 +123,14 @@ class LambdaTemplate[T] private (
val lambdas: Seq[LambdaTemplate[T]],
val matchers: Map[T, Set[Matcher[T]]],
val quantifications: Seq[QuantificationTemplate[T]],
+ val structure: Lambda,
val dependencies: Map[Identifier, T],
- val struct: (Lambda, Map[Identifier, Identifier]),
+ val lambda: Lambda,
stringRepr: () => String) extends Template[T] with KeyedTemplate[T, Lambda] {
val args = arguments.map(_._2)
val tpe = bestRealType(ids._1.getType).asInstanceOf[FunctionType]
val functions: Set[(T, FunctionType, T)] = Set.empty
- val (structure, structSubst) = struct
def substitute(substituter: T => T, matcherSubst: Map[T, Matcher[T]]): LambdaTemplate[T] = {
val newStart = substituter(start)
@@ -176,8 +176,9 @@ class LambdaTemplate[T] private (
newLambdas,
newMatchers,
newQuantifications,
+ structure,
newDependencies,
- struct,
+ lambda,
stringRepr
)
}
@@ -188,7 +189,7 @@ class LambdaTemplate[T] private (
ids._1 -> idT, encoder, manager, pathVar, arguments, condVars, exprVars, condTree,
clauses map substituter, // make sure the body-defining clause is inlined!
blockers, applications, lambdas, matchers, quantifications,
- dependencies, struct, stringRepr
+ structure, dependencies, lambda, stringRepr
)
}
diff --git a/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala b/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
index af31e6543edc4ca06bf58648f37412bb9cf6b22d..70f0ee251e055137acd25cf1bb68bf325736c477 100644
--- a/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
@@ -57,11 +57,11 @@ class QuantificationTemplate[T](
val applications: Map[T, Set[App[T]]],
val matchers: Map[T, Set[Matcher[T]]],
val lambdas: Seq[LambdaTemplate[T]],
+ val structure: Forall,
val dependencies: Map[Identifier, T],
- val struct: (Forall, Map[Identifier, Identifier]),
+ val forall: Forall,
stringRepr: () => String) extends KeyedTemplate[T, Forall] {
- val structure = struct._1
lazy val start = pathVar._2
def substitute(substituter: T => T, matcherSubst: Map[T, Matcher[T]]): QuantificationTemplate[T] = {
@@ -92,8 +92,9 @@ class QuantificationTemplate[T](
substituter(b) -> ms.map(_.substitute(substituter, matcherSubst))
},
lambdas.map(_.substitute(substituter, matcherSubst)),
+ structure,
dependencies.map { case (id, value) => id -> substituter(value) },
- struct,
+ forall,
stringRepr
)
}
@@ -130,13 +131,12 @@ object QuantificationTemplate {
Template.encode(encoder, pathVar, quantifiers, condVars, exprVars, guardedExprs, lambdas, Seq.empty,
substMap = baseSubstMap + q2s + insts + guards + qs)
- val (structuralQuant, structSubst) = normalizeStructure(proposition)
- val keyDeps = dependencies.map { case (id, idT) => structSubst(id) -> idT }
- val key = structuralQuant.asInstanceOf[Forall]
+ val (structuralQuant, deps) = normalizeStructure(proposition)
+ val keyDeps = deps.map { case (id, dep) => id -> encoder.encodeExpr(dependencies)(dep) }
new QuantificationTemplate[T](quantificationManager,
pathVar, qs, q2s, insts, guards._2, quantifiers, condVars, exprVars, condTree,
- clauses, blockers, applications, matchers, lambdas, keyDeps, key -> structSubst,
+ clauses, blockers, applications, matchers, lambdas, structuralQuant, keyDeps, proposition,
() => "Template for " + proposition + " is :\n" + templateString())
}
}
@@ -551,11 +551,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
private var _currentQ2Var: T = qs._2
def currentQ2Var = _currentQ2Var
val holds = qs._2
- val body = {
- val quantified = quantifiers.map(_._1).toSet
- val mapping = template.struct._2.map(p => p._2 -> p._1.toVariable)
- replaceFromIDs(mapping, template.structure.body)
- }
+ val body = template.forall.body
private var _currentInsts: Map[T, Set[T]] = Map.empty
def currentInsts = _currentInsts
@@ -618,12 +614,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val template: LambdaTemplate[T]) extends MatcherQuantification {
val holds = start
-
- val body = {
- val quantified = quantifiers.map(_._1).toSet
- val mapping = template.structSubst.map(p => p._2 -> p._1.toVariable)
- replaceFromIDs(mapping, template.structure)
- }
+ val body = template.lambda.body
protected def instanceSubst(enabler: T): Map[T, T] = {
Map(guardVar -> start, blocker -> enabler)
diff --git a/src/main/scala/leon/solvers/unrolling/TemplateManager.scala b/src/main/scala/leon/solvers/unrolling/TemplateManager.scala
index d1da0d8f17f0d32f7fa343d0d5e8155529fe6dd0..2857a0cbb6188efb3d82690c588400d886f79b7f 100644
--- a/src/main/scala/leon/solvers/unrolling/TemplateManager.scala
+++ b/src/main/scala/leon/solvers/unrolling/TemplateManager.scala
@@ -304,6 +304,7 @@ object Template {
pathVar: Identifier,
aVar: T
): (Map[T, Arg[T]], Instantiation[T]) = {
+
val freshSubst = exprVars.map { case (id, idT) => idT -> encoder.encodeId(id) } ++
manager.freshConds(pathVar -> aVar, condVars, condTree)
val matcherSubst = baseSubst.collect { case (c, Right(m)) => c -> m }
@@ -322,7 +323,7 @@ object Template {
// We have to be wary while computing the lambda subst map since lambdas can
// depend on each other. However, these dependencies cannot be cyclic so it
// suffices to make sure the traversal order is correct.
- var seen : Set[LambdaTemplate[T]] = Set.empty
+ var seen : Set[LambdaTemplate[T]] = Set.empty
val lambdaKeys = lambdas.map(lambda => lambda.ids._1 -> lambda).toMap
def extractSubst(lambda: LambdaTemplate[T]): Unit = {
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index b7aa7dc664c80941d8fcd23e7e5f807aead28174..03431b57720647b4017c3857d6146a615cc679b4 100644
--- a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
@@ -30,6 +30,7 @@ trait UnrollingProcedure extends LeonComponent {
val optUseCodeGen = LeonFlagOptionDef("codegen", "Use compiled evaluator instead of interpreter", false)
val optAssumePre = LeonFlagOptionDef("assumepre", "Assume precondition holds (pre && f(x) = body) when unfolding", false)
val optPartialModels = LeonFlagOptionDef("partialmodels", "Extract domains for quantifiers and bounded first-class functions", false)
+ val optSilentErrors = LeonFlagOptionDef("silenterrors", "Fail silently into UNKNOWN when encountering an error", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
Set(optCheckModels, optFeelingLucky, optUseCodeGen, optUnrollCores, optAssumePre, optUnrollFactor, optPartialModels)
@@ -49,6 +50,7 @@ trait AbstractUnrollingSolver[T]
val unrollUnsatCores = context.findOptionOrDefault(optUnrollCores)
val assumePreHolds = context.findOptionOrDefault(optAssumePre)
val partialModels = context.findOptionOrDefault(optPartialModels)
+ val silentErrors = context.findOptionOrDefault(optSilentErrors)
protected var foundDefinitiveAnswer = false
protected var definitiveAnswer : Option[Boolean] = None
@@ -325,10 +327,12 @@ trait AbstractUnrollingSolver[T]
quantify = true
}
} else {
- val valid = !checkModels || validateModel(model, assumptionsSeq, silenceErrors = false)
+ val valid = !checkModels || validateModel(model, assumptionsSeq, silenceErrors = silentErrors)
if (valid) {
foundAnswer(Some(true), model)
+ } else if (silentErrors) {
+ foundAnswer(None, model)
} else {
reporter.error(
"Something went wrong. The model should have been valid, yet we got this: " +
@@ -437,7 +441,9 @@ trait AbstractUnrollingSolver[T]
reporter.debug(" - more unrollings")
+ val timer = context.timers.solvers.unroll.start()
val newClauses = unrollingBank.unrollBehind(toRelease)
+ timer.stop()
for (ncl <- newClauses) {
solverAssert(ncl)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 1036643df0bc92de9772597af9d26f156c0ebb97..ee54fc9f2dc0cd9739da6686ea19f1b1821a3aa5 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -47,11 +47,16 @@ trait AbstractZ3Solver extends Solver {
}
}
- toggleWarningMessages(true)
+ protected var z3 : Z3Context = new Z3Context(
+ "MODEL" -> true,
+ "TYPE_CHECK" -> true,
+ "WELL_SORTED_CHECK" -> true
+ )
- protected[leon] var z3 : Z3Context = null
+ // @nv: This MUST take place AFTER Z3Context was created!!
+ toggleWarningMessages(true)
- lazy protected val solver = z3.mkSolver()
+ protected var solver : Z3Solver = null
override def free(): Unit = {
freed = true
@@ -95,13 +100,7 @@ trait AbstractZ3Solver extends Solver {
var isInitialized = false
protected[leon] def initZ3(): Unit = {
if (!isInitialized) {
- val timer = context.timers.solvers.z3.init.start()
-
- z3 = new Z3Context(
- "MODEL" -> true,
- "TYPE_CHECK" -> true,
- "WELL_SORTED_CHECK" -> true
- )
+ solver = z3.mkSolver()
functions.clear()
lambdas.clear()
@@ -114,8 +113,6 @@ trait AbstractZ3Solver extends Solver {
prepareSorts()
isInitialized = true
-
- timer.stop()
}
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 815f79750f01c06ab6e0c4b2ccf18e912f36564a..414d3185a8af4a449ed88ce389e2b4bff1cf9ed1 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -53,7 +53,7 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
}
def solverGetModel: ModelWrapper = new ModelWrapper {
- val model = solver.getModel
+ val model: Z3Model = solver.getModel
/*
val functionsModel: Map[Z3FuncDecl, (Seq[(Seq[Z3AST], Z3AST)], Z3AST)] = model.getModelFuncInterpretations.map(i => (i._1, (i._2, i._3))).toMap
@@ -84,16 +84,21 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
val fullModel = leonModel ++ (functionsAsMap ++ constantFunctionsAsMap)
*/
- def modelEval(elem: Z3AST, tpe: TypeTree): Option[Expr] = tpe match {
- case BooleanType => model.evalAs[Boolean](elem).map(BooleanLiteral)
- case Int32Type => model.evalAs[Int](elem).map(IntLiteral).orElse {
- model.eval(elem).flatMap(t => softFromZ3Formula(model, t, Int32Type))
- }
- case IntegerType => model.evalAs[Int](elem).map(InfiniteIntegerLiteral(_))
- case other => model.eval(elem) match {
- case None => None
- case Some(t) => softFromZ3Formula(model, t, other)
+ def modelEval(elem: Z3AST, tpe: TypeTree): Option[Expr] = {
+ val timer = context.timers.solvers.z3.eval.start()
+ val res = tpe match {
+ case BooleanType => model.evalAs[Boolean](elem).map(BooleanLiteral)
+ case Int32Type => model.evalAs[Int](elem).map(IntLiteral).orElse {
+ model.eval(elem).flatMap(t => softFromZ3Formula(model, t, Int32Type))
+ }
+ case IntegerType => model.evalAs[Int](elem).map(InfiniteIntegerLiteral(_))
+ case other => model.eval(elem) match {
+ case None => None
+ case Some(t) => softFromZ3Formula(model, t, other)
+ }
}
+ timer.stop()
+ res
}
override def toString = model.toString
@@ -179,7 +184,9 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
}
def solverAssert(cnstr: Z3AST): Unit = {
+ val timer = context.timers.solvers.z3.assert.start()
solver.assertCnstr(cnstr)
+ timer.stop()
}
def solverUnsatCore = Some(solver.getUnsatCore)
diff --git a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
index a1ed39dfe442044be38be88dac287cfd34aca391..fba5f0b100181f385496e0ace906d3252e110f1d 100644
--- a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
@@ -10,4 +10,4 @@ import unrolling._
import theories._
class Z3UnrollingSolver(context: LeonContext, program: Program, underlying: Solver)
- extends UnrollingSolver(context, program, underlying, new StringEncoder(context, program))
+ extends UnrollingSolver(context, program, underlying, new StringEncoder(context, program) >> new BagEncoder(context, program))