From bff35e416406569072d84d53666a65c73d10bacd Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 24 Jul 2015 17:43:08 +0200
Subject: [PATCH] Finished transitivity of propositions
---
.../codegen/runtime/SolverEntryPoint.scala | 149 ++++++++
.../leon/frontends/scalac/ASTExtractors.scala | 1 -
.../frontends/scalac/CodeExtraction.scala | 3 +
.../scala/leon/purescala/Expressions.scala | 6 +-
.../leon/purescala/FunctionClosure.scala | 4 +-
.../templates/QuantificationManager.scala | 355 +++++++++++-------
.../solvers/templates/TemplateGenerator.scala | 21 +-
.../leon/solvers/templates/Templates.scala | 135 ++++---
.../solvers/templates/UnrollingBank.scala | 4 +-
.../leon/solvers/z3/AbstractZ3Solver.scala | 2 +-
.../solvers/z3/Z3ModelReconstruction.scala | 2 +
11 files changed, 480 insertions(+), 202 deletions(-)
create mode 100644 src/main/scala/leon/codegen/runtime/SolverEntryPoint.scala
diff --git a/src/main/scala/leon/codegen/runtime/SolverEntryPoint.scala b/src/main/scala/leon/codegen/runtime/SolverEntryPoint.scala
new file mode 100644
index 000000000..e36f8aef0
--- /dev/null
+++ b/src/main/scala/leon/codegen/runtime/SolverEntryPoint.scala
@@ -0,0 +1,149 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package codegen.runtime
+
+import utils._
+import purescala.Common._
+import purescala.Expressions._
+import purescala.ExprOps.valuateWithModel
+import purescala.Constructors._
+import solvers.SolverFactory
+
+import java.util.WeakHashMap
+import java.lang.ref.WeakReference
+import scala.collection.mutable.{HashMap => MutableMap}
+import scala.concurrent.duration._
+
+import codegen.CompilationUnit
+
+import synthesis._
+
+object SolverEntryPoint {
+ implicit val debugSection = DebugSectionSolver
+
+ private case class ExprId(id: Int)
+ private case class SolverProblem(args: Seq[Identifier], problem: Expr)
+
+ private[this] val context = new WeakHashMap[ExprId, (WeakReference[CompilationUnit], SolverProblem)]()
+ private[this] val cache = new WeakHashMap[ExprId, MutableMap[Seq[AnyRef], Option[java.lang.Object]]]()
+
+ private[this] val ids = new WeakHashMap[CompilationUnit, MutableMap[SolverProblem, ExprId]]()
+
+ private[this] var _next = 0
+ private[this] def nextInt(): Int = {
+ _next += 1
+ _next
+ }
+
+ private def getUniqueId(unit: CompilationUnit, p: SolverProblem): ExprId = {
+ if (!ids.containsKey(unit)) {
+ ids.put(unit, new MutableMap())
+ }
+
+ if (ids.get(unit) contains p) {
+ ids.get(unit)(p)
+ } else {
+ val cid = new ExprId(nextInt())
+ ids.get(unit) += p -> cid
+ cid
+ }
+ }
+
+ def register(args: Seq[Identifier], expr: Expr, unit: CompilationUnit): Int = {
+ val p = SolverProblem(args, expr)
+ val cid = getUniqueId(unit, p)
+
+ context.put(cid, new WeakReference(unit) -> p)
+
+ cid.id
+ }
+
+ def check(i: Int, inputs: Array[AnyRef]): Boolean = {
+ val id = ExprId(i)
+ val (ur, p) = context.get(id)
+ val unit = ur.get
+
+ val program = unit.program
+ val ctx = unit.ctx
+
+ ctx.reporter.debug("Executing SAT problem (codegen)!")
+ val is = inputs.toSeq
+
+ if (!cache.containsKey(id)) {
+ cache.put(id, new MutableMap())
+ }
+
+ val resultCache = cache.get(id)
+
+ if (resultCache contains is) {
+ resultCache(is).isDefined
+ } else {
+ val tStart = System.currentTimeMillis
+
+ val solverf = SolverFactory.default(ctx, program).withTimeout(10.second)
+ val solver = solverf.getNewSolver()
+
+ val bindingCnstrs = (p.args zip inputs).flatMap { case (id, jvmExpr) =>
+ val v = Variable(id)
+ val expr = unit.jvmToExpr(jvmExpr, id.getType)
+
+ val inputCnstr = expr match {
+ case purescala.Extractors.FiniteLambda(default, mapping) =>
+ Some(ElementOfSet(v, FiniteSet(mapping.map(_._1).toSet, id.getType)))
+ case _ => None
+ }
+
+ Seq(Equals(v, expr)) ++ inputCnstr
+ }
+
+ solver.assertCnstr(andJoin(p.problem +: bindingCnstrs))
+
+ try {
+ solver.check match {
+ case Some(true) =>
+ val model = solver.getModel
+ val valModel = valuateWithModel(model) _
+ val res = p.args.map(valModel)
+ val leonRes = tupleWrap(res)
+
+ val total = System.currentTimeMillis-tStart
+
+ ctx.reporter.debug("Constraint \"execution\" took "+total+"ms")
+ ctx.reporter.debug("SAT with model "+leonRes.asString(ctx))
+
+ val obj = unit.exprToJVM(leonRes)(new LeonCodeGenRuntimeMonitor(unit.params.maxFunctionInvocations))
+ resultCache += is -> Some(obj)
+ true
+
+ case Some(false) =>
+ resultCache += is -> None
+ false
+
+ case _ =>
+ throw new LeonCodeGenRuntimeException("Timeout exceeded")
+ }
+ } finally {
+ solver.free()
+ solverf.shutdown()
+ }
+ }
+ }
+
+ def getModel(i: Int, inputs: Array[AnyRef]): java.lang.Object = {
+ val id = ExprId(i)
+ if (!cache.containsKey(id)) {
+ throw new LeonCodeGenRuntimeException("Problem was not checked before model query")
+ }
+
+ cache.get(id).get(inputs.toSeq) match {
+ case Some(Some(obj)) =>
+ obj
+ case Some(None) =>
+ throw new LeonCodeGenRuntimeException("Problem was UNSAT")
+ case None =>
+ throw new LeonCodeGenRuntimeException("Problem was not checked before model query")
+ }
+ }
+}
+
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 066955731..db477ec49 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -1036,6 +1036,5 @@ trait ASTExtractors {
case _ => None
}
}
-
}
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 34d781046..da0a83066 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1634,6 +1634,9 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, at: ArrayType), "updated", List(k, v)) =>
ArrayUpdated(a1, k, v)
+ case (IsTyped(a1, at: ArrayType), "clone", Nil) =>
+ a1
+
// Map methods
case (IsTyped(a1, MapType(_, vt)), "apply", List(a2)) =>
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index b44a4b9f8..720024b4f 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -95,6 +95,8 @@ object Expressions {
* @param pred The predicate to satisfy. It should be a function whose argument's type can handle the type of the body
*/
case class Ensuring(body: Expr, pred: Expr) extends Expr {
+ require(pred.isInstanceOf[Lambda])
+
val getType = pred.getType match {
case FunctionType(Seq(bodyType), BooleanType) if isSubtypeOf(body.getType, bodyType) =>
body.getType
@@ -833,8 +835,8 @@ object Expressions {
* with a default value (as genereted with `Array.fill` in Scala).
*/
case class NonemptyArray(elems: Map[Int, Expr], defaultLength: Option[(Expr, Expr)]) extends Expr {
- private val elements = elems.values.toList ++ defaultLength.map{_._1}
- val getType = ArrayType(optionToType(leastUpperBound(elements map { _.getType}))).unveilUntyped
+ private val elements = elems.values.toList ++ defaultLength.map(_._1)
+ val getType = ArrayType(optionToType(leastUpperBound(elements map { _.getType }))).unveilUntyped
}
/** $encodingof `Array[tpe]()` */
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 4ac11044d..607e9aeb4 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -77,7 +77,9 @@ class FunctionClosure extends TransformationPhase {
val newPrecondition = simplifyLets(introduceLets(and((capturedConstraints ++ fd.precondition).toSeq :_*), fd2FreshFd))
newFunDef.precondition = if(newPrecondition == BooleanLiteral(true)) None else Some(newPrecondition)
- val freshPostcondition = fd.postcondition.map{ post => introduceLets(post, fd2FreshFd).setPos(post) }
+ val freshPostcondition = fd.postcondition.map { case post @ Lambda(args, body) =>
+ Lambda(args, introduceLets(body, fd2FreshFd).setPos(body)).setPos(post)
+ }
newFunDef.postcondition = freshPostcondition
pathConstraints = fd.precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index d5bec5c31..a420b817b 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -14,8 +14,21 @@ import Instantiation._
import scala.collection.mutable.{Map => MutableMap, Set => MutableSet}
-case class Matcher[T](caller: T, tpe: TypeTree, args: Seq[T]) {
- override def toString = "M(" + caller + " : " + tpe + ", " + args.mkString("(",",",")") + ")"
+object Matcher {
+ def argValue[T](arg: Either[T, Matcher[T]]): T = arg match {
+ case Left(value) => value
+ case Right(matcher) => matcher.encoded
+ }
+}
+
+case class Matcher[T](caller: T, tpe: TypeTree, args: Seq[Either[T, Matcher[T]]], encoded: T) {
+ override def toString = "M(" + caller + " : " + tpe + ", " + args.map(Matcher.argValue).mkString("(",",",")") + ")"
+
+ def substitute(substituter: T => T): Matcher[T] = copy(
+ caller = substituter(caller),
+ args = args.map { arg => arg.left.map(substituter).right.map(_.substitute(substituter)) },
+ encoded = substituter(encoded)
+ )
}
case class IllegalQuantificationException(expr: Expr, msg: String)
@@ -25,7 +38,8 @@ class QuantificationTemplate[T](
val quantificationManager: QuantificationManager[T],
val start: T,
val qs: (Identifier, T),
- val holdVar: T,
+ val q2s: (Identifier, T),
+ val insts: (Identifier, T),
val guardVar: T,
val quantifiers: Seq[(Identifier, T)],
val condVars: Map[Identifier, T],
@@ -47,7 +61,8 @@ object QuantificationTemplate {
quantificationManager: QuantificationManager[T],
pathVar: (Identifier, T),
qs: (Identifier, T),
- holder: Identifier,
+ q2: Identifier,
+ inst: Identifier,
guard: Identifier,
quantifiers: Seq[(Identifier, T)],
condVars: Map[Identifier, T],
@@ -57,28 +72,24 @@ object QuantificationTemplate {
subst: Map[Identifier, T]
): QuantificationTemplate[T] = {
- val holders: (Identifier, T) = holder -> encoder.encodeId(holder)
+ val q2s: (Identifier, T) = q2 -> encoder.encodeId(q2)
+ val insts: (Identifier, T) = inst -> encoder.encodeId(inst)
val guards: (Identifier, T) = guard -> encoder.encodeId(guard)
val (clauses, blockers, applications, matchers, _) =
Template.encode(encoder, pathVar, quantifiers, condVars, exprVars, guardedExprs, lambdas,
- substMap = subst + holders + guards + qs)
+ substMap = subst + q2s + insts + guards + qs)
new QuantificationTemplate[T](quantificationManager,
- pathVar._2, qs, holders._2, guards._2, quantifiers,
+ pathVar._2, qs, q2s, insts, guards._2, quantifiers,
condVars, exprVars, clauses, blockers, applications, matchers, lambdas)
}
}
class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManager[T](encoder) {
- private val nextHolder: () => T = {
- val id: Identifier = FreshIdentifier("ph", BooleanType)
- () => encoder.encodeId(id)
- }
-
private val nextQ: () => T = {
- val id: Identifier = FreshIdentifier("q", BooleanType)
+ val id: Identifier = FreshIdentifier("q", BooleanType, true)
() => encoder.encodeId(id)
}
@@ -113,7 +124,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
knownStack = knownStack.drop(lvl)
}
- def blockers: Seq[T] = quantifications.map(_.holdVar)
+ def assumptions: Seq[T] = quantifications.map(_.currentQ2Var)
override def registerFree(ids: Seq[(TypeTree, T)]): Unit = {
super.registerFree(ids)
@@ -121,47 +132,24 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
private class Quantification (
- val qVar: T,
- val holdVar: T,
+ val qs: (Identifier, T),
+ val q2s: (Identifier, T),
+ val insts: (Identifier, T),
val guardVar: T,
- var currentHolder: T,
val quantified: Set[T],
+ val matchers: Set[Matcher[T]],
+ val allMatchers: Map[T, Set[Matcher[T]]],
val condVars: Map[Identifier, T],
val exprVars: Map[Identifier, T],
val clauses: Seq[T],
val blockers: Map[T, Set[TemplateCallInfo[T]]],
val applications: Map[T, Set[App[T]]],
- val matchers: Set[Matcher[T]],
val lambdas: Map[T, LambdaTemplate[T]]) {
- def this(
- qVar: T, holdVar: T, guardVar: T, quantified: Set[T],
- condVars: Map[Identifier, T], exprVars: Map[Identifier, T],
- clauses: Seq[T], blockers: Map[T, Set[TemplateCallInfo[T]]], applications: Map[T, Set[App[T]]],
- matchers: Set[Matcher[T]], lambdas: Map[T, LambdaTemplate[T]]) = {
- this(qVar, holdVar, guardVar, nextHolder(), quantified,
- condVars, exprVars, clauses, blockers, applications, matchers, lambdas)
- }
-
- def substitute(subst: Map[T, T]) = {
- val substituter = encoder.substitute(subst)
-
- new Quantification (
- qVar, holdVar, guardVar, currentHolder,
- quantified, condVars, exprVars,
- clauses map substituter,
- blockers map { case (b, fis) =>
- substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
- },
- applications map { case (b, fas) =>
- substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
- },
- matchers map (m => m.copy(caller = substituter(m.caller), args = m.args.map(substituter))),
- lambdas map { case (idT, template) => substituter(idT) -> template.substitute(subst) }
- )
- }
+ var currentQ2Var: T = qs._2
+ private var slaves: Seq[(T, Map[T,T], Quantification)] = Nil
- def instantiate(blocker: T, matcher: Matcher[T]): Instantiation[T] = {
+ private def mappings(blocker: T, matcher: Matcher[T]): Set[(T, Map[T, T])] = {
// Build a mapping from applications in the quantified statement to all potential concrete
// applications previously encountered. Also make sure the current `app` is in the mapping
@@ -172,136 +160,251 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
// be bound when generating the new constraints
.filter(qm => correspond(qm, matcher))
// 2. build the instantiation mapping associated to the chosen current application binding
- .flatMap { bindingMatcher => matchers
+ .flatMap { bindingMatcher =>
+
// 2.1. select all potential matches for each quantified application
- .map(qm => if (qm == bindingMatcher) {
- bindingMatcher -> Set(blocker -> matcher)
- } else {
- val instances: Set[(T, Matcher[T])] = instantiated.filter { case (b, m) => correspond(qm, m) }
+ val matcherToInstances = matchers
+ .map(qm => if (qm == bindingMatcher) {
+ bindingMatcher -> Set(blocker -> matcher)
+ } else {
+ val instances: Set[(T, Matcher[T])] = instantiated.filter { case (b, m) => correspond(qm, m) }
+
+ // concrete applications can appear multiple times in the constraint, and this is also the case
+ // for the current application for which we are generating the constraints
+ val withCurrent = if (correspond(qm, matcher)) instances + (blocker -> matcher) else instances
- // concrete applications can appear multiple times in the constraint, and this is also the case
- // for the current application for which we are generating the constraints
- val withCurrent = if (correspond(qm, matcher)) instances + (blocker -> matcher) else instances
+ qm -> withCurrent
+ }).toMap
- qm -> withCurrent
- })
// 2.2. based on the possible bindings for each quantified application, build a set of
// instantiation mappings that can be used to instantiate all necessary constraints
- .foldLeft[Set[Set[(T, Matcher[T], Matcher[T])]]] (Set(Set.empty)) {
- case (mappings, (qm, instances)) => Set(instances.toSeq.flatMap {
- case (b, m) => mappings.map(mapping => mapping + ((b, qm, m)))
- } : _*)
- }
+ extractMappings(matcherToInstances)
}
- var instantiation = Instantiation.empty[T]
-
- for (mapping <- matcherMappings) {
- var constraints: List[T] = Nil
- var subst: Map[T, T] = Map.empty
+ for (mapping <- matcherMappings) yield extractSubst(quantified, mapping)
+ }
- for {
- (b, Matcher(qcaller, _, qargs), Matcher(caller, _, args)) <- mapping
- _ = constraints :+= b
- (qarg, arg) <- (qargs zip args)
- } if (subst.isDefinedAt(qarg)) {
- constraints :+= encoder.mkEquals(subst(qarg), arg)
- } else if (!quantified(qarg)) {
- constraints :+= encoder.mkEquals(qarg, arg)
- } else {
- subst += qarg -> arg
- }
+ private def extractSlaveInfo(enabler: T, senabler: T, subst: Map[T,T], ssubst: Map[T,T]): (T, Map[T,T]) = {
+ val substituter = encoder.substitute(subst)
+ val slaveEnabler = encoder.mkAnd(enabler, substituter(senabler))
+ val slaveSubst = ssubst.map(p => p._1 -> substituter(p._2))
+ (slaveEnabler, slaveSubst)
+ }
- val enabler = if (constraints.size == 1) constraints.head else encoder.mkAnd(constraints : _*)
- val newHolder = nextHolder()
+ private def instantiate(enabler: T, subst: Map[T, T], seen: Set[Quantification]): Instantiation[T] = {
+ if (seen(this)) {
+ Instantiation.empty[T]
+ } else {
+ val nextQ2Var = encoder.encodeId(q2s._1)
val baseSubstMap = (condVars ++ exprVars).map { case (id, idT) => idT -> encoder.encodeId(id) }
val lambdaSubstMap = lambdas map { case (idT, lambda) => idT -> encoder.encodeId(lambda.id) }
val substMap = subst ++ baseSubstMap ++ lambdaSubstMap +
- (qVar -> currentHolder) + (guardVar -> enabler) + (holdVar -> newHolder)
+ (qs._2 -> currentQ2Var) + (guardVar -> enabler) + (q2s._2 -> nextQ2Var) +
+ (insts._2 -> encoder.encodeId(insts._1))
+
+ var instantiation = Template.instantiate(encoder, QuantificationManager.this,
+ clauses, blockers, applications, Seq.empty, Map.empty[T, Set[Matcher[T]]], lambdas, substMap)
+
+ for {
+ (senabler, ssubst, slave) <- slaves
+ (slaveEnabler, slaveSubst) = extractSlaveInfo(enabler, senabler, subst, ssubst)
+ } instantiation ++= slave.instantiate(slaveEnabler, slaveSubst, seen + this)
+
+ currentQ2Var = nextQ2Var
+ instantiation
+ }
+ }
+
+ def register(senabler: T, ssubst: Map[T, T], slave: Quantification): Instantiation[T] = {
+ var instantiation = Instantiation.empty[T]
+
+ for {
+ (blocker, matcher) <- instantiated
+ (enabler, subst) <- mappings(blocker, matcher)
+ (slaveEnabler, slaveSubst) = extractSlaveInfo(enabler, senabler, subst, ssubst)
+ } instantiation ++= slave.instantiate(slaveEnabler, slaveSubst, Set(this))
+
+ slaves :+= (senabler, ssubst, slave)
- instantiation ++= Template.instantiate(encoder, QuantificationManager.this,
- clauses, blockers, applications, Seq.empty, Map.empty, lambdas, substMap)
- currentHolder = newHolder
+ instantiation
+ }
+
+ def instantiate(blocker: T, matcher: Matcher[T]): Instantiation[T] = {
+ var instantiation = Instantiation.empty[T]
+
+ for ((enabler, subst) <- mappings(blocker, matcher)) {
+ instantiation ++= instantiate(enabler, subst, Set.empty)
}
instantiation
}
}
- def instantiateQuantification(template: QuantificationTemplate[T], substMap: Map[T, T]): Instantiation[T] = {
- val trueT = encoder.encodeExpr(Map.empty)(BooleanLiteral(true))
- val instantiationSubst: Map[T, T] = substMap + (template.guardVar -> trueT)
+ private def extractMappings(
+ bindings: Map[Matcher[T], Set[(T, Matcher[T])]]
+ ): Set[Set[(T, Matcher[T], Matcher[T])]] = {
+ val allMappings = bindings.foldLeft[Set[Set[(T, Matcher[T], Matcher[T])]]](Set(Set.empty)) {
+ case (mappings, (qm, instances)) => Set(instances.toSeq.flatMap {
+ case (b, m) => mappings.map(mapping => mapping + ((b, qm, m)))
+ } : _*)
+ }
+
+ def subBindings(b: T, sm: Matcher[T], m: Matcher[T]): Set[(T, Matcher[T], Matcher[T])] = {
+ (for ((sarg, arg) <- sm.args zip m.args) yield {
+ (sarg, arg) match {
+ case (Right(sargm), Right(argm)) => Set((b, sargm, argm)) ++ subBindings(b, sargm, argm)
+ case _ => Set.empty[(T, Matcher[T], Matcher[T])]
+ }
+ }).flatten.toSet
+ }
- val substituter = encoder.substitute(instantiationSubst)
- val matchers = template.matchers.map { case (b, ms) =>
- substituter(b) -> ms.map(m => m.copy(caller = substituter(m.caller), args = m.args.map(substituter)))
+ allMappings.filter { s =>
+ val withSubs = s ++ s.flatMap { case (b, sm, m) => subBindings(b, sm, m) }
+ withSubs.groupBy(_._2).forall(_._2.size == 1)
}
+ }
+
+ private def extractSubst(quantified: Set[T], mapping: Set[(T, Matcher[T], Matcher[T])]): (T, Map[T,T]) = {
+ var constraints: List[T] = Nil
+ var subst: Map[T, T] = Map.empty
+
+ for {
+ (b, Matcher(qcaller, _, qargs, _), Matcher(caller, _, args, _)) <- mapping
+ _ = constraints :+= b
+ (qarg, arg) <- (qargs zip args)
+ argVal = Matcher.argValue(arg)
+ } qarg match {
+ case Left(quant) if subst.isDefinedAt(quant) =>
+ constraints :+= encoder.mkEquals(quant, argVal)
+ case Left(quant) if quantified(quant) =>
+ subst += quant -> argVal
+ case _ =>
+ constraints :+= encoder.mkEquals(Matcher.argValue(qarg), argVal)
+ }
+
+ val enabler =
+ if (constraints.isEmpty) encoder.encodeExpr(Map.empty)(BooleanLiteral(true))
+ else if (constraints.size == 1) constraints.head
+ else encoder.mkAnd(constraints : _*)
- var instantiation: Instantiation[T] = Template.instantiate(encoder, this,
- template.clauses, template.blockers, template.applications,
- Seq.empty, Map.empty, template.lambdas, instantiationSubst)
+ (encoder.substitute(subst)(enabler), subst)
+ }
+ def instantiateQuantification(template: QuantificationTemplate[T], substMap: Map[T, T]): Instantiation[T] = {
val quantified = template.quantifiers.map(_._2).toSet
- val allMatchers: Set[Matcher[T]] = {
- def rec(templates: Map[T, LambdaTemplate[T]]): Set[Matcher[T]] = templates.flatMap {
- case (_, template) => template.matchers.flatMap(_._2).toSet ++ rec(template.lambdas)
- }.toSet
+ val allMatchers: Map[T, Set[Matcher[T]]] = {
+ def rec(templates: Map[T, LambdaTemplate[T]]): Map[T, Set[Matcher[T]]] =
+ templates.foldLeft(Map.empty[T, Set[Matcher[T]]]) {
+ case (matchers, (_, template)) => matchers merge template.matchers merge rec(template.lambdas)
+ }
- val allMatchers = template.matchers.flatMap(_._2).toSet ++ rec(template.lambdas)
- for (m @ Matcher(caller, tpe, args) <- allMatchers if args exists quantified) yield m
+ template.matchers merge rec(template.lambdas)
}
- val matchQuorums: Seq[Set[Matcher[T]]] = allMatchers.subsets.filter { ms =>
+ val quantifiedMatchers = for {
+ (_, ms) <- allMatchers
+ m @ Matcher(_, _, args, _) <- ms
+ if args exists (_.left.exists(quantified))
+ } yield m
+
+ val matchQuorums: Seq[Set[Matcher[T]]] = quantifiedMatchers.toSet.subsets.filter { ms =>
var doubled: Boolean = false
var qs: Set[T] = Set.empty
- for (m @ Matcher(_, _, args) <- ms) {
- val qargs = (args filter quantified).toSet
+ for (m @ Matcher(_, _, args, _) <- ms) {
+ val qargs = (args collect { case Left(a) if quantified(a) => a }).toSet
if ((qs & qargs).nonEmpty) doubled = true
qs ++= qargs
}
!doubled && (qs == quantified)
- }.toSeq
+ }.toList
+
+ var instantiation = Instantiation.empty[T]
- val newQuantifications = for (matchers <- matchQuorums) yield {
- val newQ = nextQ()
+ val qs = for (matchers <- matchQuorums) yield {
+ val newQ = encoder.encodeId(template.qs._1)
+ val subst = substMap + (template.qs._2 -> newQ)
- new Quantification(newQ,
- template.holdVar, template.guardVar,
- newQ, // set template `qVar` as `currentHolder` to ensure blocking before first unfolding
+ val substituter = encoder.substitute(substMap + (template.qs._2 -> newQ))
+ val quantification = new Quantification(template.qs._1 -> newQ,
+ template.q2s, template.insts, template.guardVar,
quantified,
+ matchers map (m => m.substitute(substituter)),
+ allMatchers map { case (b, ms) => substituter(b) -> ms.map(_.substitute(substituter)) },
template.condVars,
template.exprVars,
- template.clauses,
- template.blockers,
- template.applications,
- matchers,
- template.lambdas
- ).substitute(substMap)
- }
+ template.clauses map substituter,
+ template.blockers map { case (b, fis) =>
+ substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
+ },
+ template.applications map { case (b, fas) =>
+ substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
+ },
+ template.lambdas map { case (idT, template) => substituter(idT) -> template.substitute(subst) }
+ )
- val eqClause = {
- val qs = newQuantifications.map(_.qVar)
- val newQs = if (qs.isEmpty) trueT else if (qs.size == 1) qs.head else encoder.mkAnd(qs : _*)
- encoder.mkImplies(substMap(template.start), encoder.mkEquals(template.holdVar, newQs))
- }
+ def extendClauses(master: Quantification, slave: Quantification): Instantiation[T] = {
+ val bindingsMap: Map[Matcher[T], Set[(T, Matcher[T])]] = slave.matchers.map { sm =>
+ val instances = master.allMatchers.toSeq.flatMap { case (b, ms) => ms.map(b -> _) }
+ sm -> instances.filter(p => correspond(p._2, sm)).toSet
+ }.toMap
+
+ val allMappings = extractMappings(bindingsMap)
+ val filteredMappings = allMappings.filter { s =>
+ s.exists { case (b, sm, m) => !master.matchers(m) } &&
+ s.exists { case (b, sm, m) => sm != m } &&
+ s.forall { case (b, sm, m) =>
+ (sm.args zip m.args).forall {
+ case (Right(_), Left(_)) => false
+ case _ => true
+ }
+ }
+ }
+
+ var instantiation = Instantiation.empty[T]
- instantiation = (instantiation._1 :+ eqClause, instantiation._2, instantiation._3)
+ for (mapping <- filteredMappings) {
+ val (enabler, subst) = extractSubst(slave.quantified, mapping)
+ instantiation ++= master.register(enabler, subst, slave)
+ }
+
+ instantiation
+ }
+
+ val allSet = quantification.allMatchers.flatMap(_._2).toSet
+ for (q <- quantifications) {
+ val allQSet = q.allMatchers.flatMap(_._2).toSet
+ if (quantification.matchers.forall(m => allQSet.exists(qm => correspond(qm, m))))
+ instantiation ++= extendClauses(q, quantification)
- val saved = instantiated
+ if (q.matchers.forall(qm => allSet.exists(m => correspond(qm, m))))
+ instantiation ++= extendClauses(quantification, q)
+ }
+
+ for ((b, m) <- instantiated) {
+ instantiation ++= quantification.instantiate(b, m)
+ }
- for ((b, ms) <- matchers; bp = substituter(b); m <- ms) {
- val newM = m.copy(caller = substituter(m.caller), args = m.args.map(substituter))
- instantiation ++= instantiateMatcher(bp, newM)
+ quantifications :+= quantification
+ quantification.qs._2
}
- for ((b, m) <- saved; q <- newQuantifications) {
- instantiation ++= q.instantiate(b, m)
+ instantiation = instantiation withClause {
+ val newQs =
+ if (qs.isEmpty) encoder.encodeExpr(Map.empty)(BooleanLiteral(true))
+ else if (qs.size == 1) qs.head
+ else encoder.mkAnd(qs : _*)
+ encoder.mkImplies(substMap(template.start), encoder.mkEquals(substMap(template.qs._2), newQs))
}
- quantifications ++= newQuantifications
+ val quantifierSubst = substMap ++ template.quantifiers.map { case (id, idT) => idT -> encoder.encodeId(id) }
+ val substituter = encoder.substitute(quantifierSubst)
+
+ for ((b, ms) <- template.matchers; m <- ms) {
+ instantiation ++= instantiateMatcher(substMap(template.start), m.substitute(substituter))
+ }
instantiation
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 4c49c3101..ac155c710 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -170,9 +170,8 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
def rec(pathVar: Identifier, expr: Expr): Expr = {
expr match {
- case a @ Assert(cond, _, body) =>
- storeGuarded(pathVar, rec(pathVar, cond))
- rec(pathVar, body)
+ case a @ Assert(cond, err, body) =>
+ rec(pathVar, IfExpr(cond, body, Error(body.getType, err getOrElse "assertion failed")))
case e @ Ensuring(_, _) =>
rec(pathVar, e.toAssert)
@@ -272,7 +271,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val localSubst: Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
val clauseSubst: Map[Identifier, T] = localSubst ++ (idArgs zip trArgs)
val (lambdaConds, lambdaExprs, lambdaGuarded, lambdaTemplates, lambdaQuants) = mkClauses(pathVar, clause, clauseSubst)
- assert(lambdaQuants.isEmpty, "Unhandled quantification in lambdas in " + clause)
+ assert(lambdaQuants.isEmpty, "Unhandled quantification in lambdas in " + l)
val ids: (Identifier, T) = lid -> storeLambda(lid)
val dependencies: Map[Identifier, T] = variablesOf(l).map(id => id -> localSubst(id)).toMap
@@ -292,11 +291,12 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val idQuantifiers : Seq[Identifier] = quantifiers.toSeq
val trQuantifiers : Seq[T] = idQuantifiers.map(encoder.encodeId)
- val q: Identifier = FreshIdentifier("q", BooleanType)
- val ph: Identifier = FreshIdentifier("ph", BooleanType)
- val guard: Identifier = FreshIdentifier("guard", BooleanType)
+ val q: Identifier = FreshIdentifier("q", BooleanType, true)
+ val q2: Identifier = FreshIdentifier("qo", BooleanType, true)
+ val inst: Identifier = FreshIdentifier("inst", BooleanType, true)
+ val guard: Identifier = FreshIdentifier("guard", BooleanType, true)
- val clause = Equals(Variable(q), And(Variable(ph), Implies(Variable(guard), conjunct)))
+ val clause = Equals(Variable(inst), Implies(Variable(guard), conjunct))
val qs: (Identifier, T) = q -> encoder.encodeId(q)
val localSubst: Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
@@ -304,8 +304,11 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val (qConds, qExprs, qGuarded, qTemplates, qQuants) = mkClauses(pathVar, clause, clauseSubst)
assert(qQuants.isEmpty, "Unhandled nested quantification in "+clause)
+ val binder = Equals(Variable(q), And(Variable(q2), Variable(inst)))
+ val allQGuarded = qGuarded + (pathVar -> (binder +: qGuarded.getOrElse(pathVar, Seq.empty)))
+
val template = QuantificationTemplate[T](encoder, manager, pathVar -> encodedCond(pathVar),
- qs, ph, guard, idQuantifiers zip trQuantifiers, qConds, qExprs, qGuarded, qTemplates, localSubst)
+ qs, q2, inst, guard, idQuantifiers zip trQuantifiers, qConds, qExprs, allQGuarded, qTemplates, localSubst)
registerQuantification(template)
Variable(q)
}
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index d14a294c0..678050fa1 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -36,6 +36,9 @@ object Instantiation {
(thisClauses ++ thatClauses, thisBlockers merge thatBlockers, thisApps merge thatApps)
}
+
+ def withClause(cl: T): Instantiation[T] = (i._1 :+ cl, i._2, i._3)
+ def withClauses(cls: Seq[T]): Instantiation[T] = (i._1 ++ cls, i._2, i._3)
}
}
@@ -82,56 +85,50 @@ trait Template[T] { self =>
object Template {
- private def functionCallInfos[T](encodeExpr: Expr => T)(expr: Expr): (Set[TemplateCallInfo[T]], Set[App[T]]) = {
- def invocationCaller(expr: Expr): Boolean = expr match {
- case fi: FunctionInvocation => true
- case Application(caller, _) => invocationCaller(caller)
- case _ => false
+ private object InvocationExtractor {
+ private def flatInvocation(expr: Expr): Option[(TypedFunDef, Seq[Expr])] = expr match {
+ case fi @ FunctionInvocation(tfd, args) => Some((tfd, args))
+ case Application(caller, args) => flatInvocation(caller) match {
+ case Some((tfd, prevArgs)) => Some((tfd, prevArgs ++ args))
+ case None => None
+ }
+ case _ => None
}
- val calls = collect[Expr] {
- case IsTyped(f: FunctionInvocation, ft: FunctionType) => Set.empty
- case IsTyped(f: Application, ft: FunctionType) => Set.empty
- case f: FunctionInvocation => Set(f)
- case f: Application => Set(f)
- case _ => Set.empty
- }(expr)
-
- val (functionCalls, appCalls) = calls partition invocationCaller
-
- def functionTemplate(expr: Expr): TemplateCallInfo[T] = expr match {
- case FunctionInvocation(tfd, args) =>
- TemplateCallInfo(tfd, args.map(encodeExpr))
- case Application(caller, args) =>
- val TemplateCallInfo(tfd, prevArgs) = functionTemplate(caller)
- TemplateCallInfo(tfd, prevArgs ++ args.map(encodeExpr))
- case _ => scala.sys.error("Should never happen!")
+ def unapply(expr: Expr): Option[(TypedFunDef, Seq[Expr])] = expr match {
+ case IsTyped(f: FunctionInvocation, ft: FunctionType) => None
+ case IsTyped(f: Application, ft: FunctionType) => None
+ case FunctionInvocation(tfd, args) => Some(tfd -> args)
+ case f: Application => flatInvocation(f)
+ case _ => None
}
+ }
- val templates : Set[TemplateCallInfo[T]] = functionCalls map functionTemplate
-
- def applicationTemplate(expr: Expr): App[T] = expr match {
- case Application(caller : Application, args) =>
- val App(c, tpe, prevArgs) = applicationTemplate(caller)
- App(c, tpe, prevArgs ++ args.map(encodeExpr))
- case Application(c, args) =>
- App(encodeExpr(c), c.getType.asInstanceOf[FunctionType], args.map(encodeExpr))
- case _ => scala.sys.error("Should never happen!")
+ private object ApplicationExtractor {
+ private def flatApplication(expr: Expr): Option[(Expr, Seq[Expr])] = expr match {
+ case Application(fi: FunctionInvocation, _) => None
+ case Application(caller: Application, args) => flatApplication(caller) match {
+ case Some((c, prevArgs)) => Some((c, prevArgs ++ args))
+ case None => None
+ }
+ case Application(caller, args) => Some((caller, args))
+ case _ => None
}
- val apps : Set[App[T]] = appCalls map applicationTemplate
-
- (templates, apps)
+ def unapply(expr: Expr): Option[(Expr, Seq[Expr])] = expr match {
+ case IsTyped(f: Application, ft: FunctionType) => None
+ case f: Application => flatApplication(f)
+ case _ => None
+ }
}
- private def selectMatchInfos[T](encodeExpr: Expr => T)(expr: Expr): Set[Matcher[T]] = {
- collect[Matcher[T]] {
- case ArraySelect(arr, index) =>
- Set(Matcher(encodeExpr(arr), arr.getType, Seq(encodeExpr(index))))
- case MapGet(map, key) =>
- Set(Matcher(encodeExpr(map), map.getType, Seq(encodeExpr(key))))
- case _ => Set.empty
- }(expr)
+ private object MatchExtractor {
+ def unapply(expr: Expr): Option[(Expr, Seq[Expr])] = expr match {
+ case ApplicationExtractor(caller, args) => Some(caller -> args)
+ case ArraySelect(arr, index) => Some(arr -> Seq(index))
+ case MapGet(map, key) => Some(map -> Seq(key))
+ case _ => None
+ }
}
private def invocationMatcher[T](encodeExpr: Expr => T)(tfd: TypedFunDef, args: Seq[Expr]): Matcher[T] = {
@@ -146,8 +143,8 @@ object Template {
}
val (fiArgs, appArgs) = args.splitAt(tfd.params.size)
- val Application(caller, arguments) = rec(FunctionInvocation(tfd, fiArgs), appArgs)
- Matcher(encodeExpr(caller), caller.getType, arguments.map(encodeExpr))
+ val app @ Application(caller, arguments) = rec(FunctionInvocation(tfd, fiArgs), appArgs)
+ Matcher(encodeExpr(caller), caller.getType, arguments.map(arg => Left(encodeExpr(arg))), encodeExpr(app))
}
def encode[T](
@@ -174,9 +171,6 @@ object Template {
encodeExpr(Implies(Variable(b), e))
}).toSeq
- val extractInfos : Expr => (Set[TemplateCallInfo[T]], Set[App[T]]) = functionCallInfos(encodeExpr)
- val extractMatchers : Expr => Set[Matcher[T]] = selectMatchInfos(encodeExpr)
-
val optIdCall = optCall.map(tfd => TemplateCallInfo[T](tfd, arguments.map(_._2)))
val optIdApp = optApp.map { case (idT, tpe) => App(idT, tpe, arguments.map(_._2)) }
@@ -194,10 +188,34 @@ object Template {
var matchInfos : Set[Matcher[T]] = Set.empty
for (e <- es) {
- val (newFunInfos, newAppInfos) = extractInfos(e)
- funInfos ++= newFunInfos
- appInfos ++= newAppInfos
- matchInfos ++= extractMatchers(e)
+ funInfos ++= collect[TemplateCallInfo[T]] {
+ case InvocationExtractor(tfd, args) =>
+ Set(TemplateCallInfo(tfd, args.map(encodeExpr)))
+ case _ => Set.empty
+ }(e)
+
+ appInfos ++= collect[App[T]] {
+ case ApplicationExtractor(c, args) =>
+ Set(App(encodeExpr(c), c.getType.asInstanceOf[FunctionType], args.map(encodeExpr)))
+ case _ => Set.empty
+ }(e)
+
+ matchInfos ++= foldRight[Map[Expr, Matcher[T]]] { (expr, res) =>
+ val result = res.flatten.toMap
+
+ result ++ (expr match {
+ case MatchExtractor(c, args) =>
+ // Note that we rely here on the fact that foldRight visits the matcher's arguments first,
+ // so any Matcher in arguments will belong to the `result` map
+ val encodedArgs = args.map(arg => result.get(arg) match {
+ case Some(matcher) => Right(matcher)
+ case None => Left(encodeExpr(arg))
+ })
+
+ Some(expr -> Matcher(encodeExpr(c), c.getType, encodedArgs, encodeExpr(expr)))
+ case _ => None
+ })
+ }(e).values
}
val calls = funInfos -- optIdCall
@@ -206,13 +224,11 @@ object Template {
val apps = appInfos -- optIdApp
if (apps.nonEmpty) applications += b -> apps
- val matchs = matchInfos ++
- apps.map(app => Matcher(app.caller, app.tpe, app.args)) ++
- funInfos.flatMap {
- case info @ TemplateCallInfo(tfd, args) if Some(info) == optIdCall =>
- invocMatcher
- case _ => None
+ val matchs = matchInfos.filter { case m @ Matcher(mc, mtpe, margs, _) =>
+ !optIdApp.exists { case App(ac, atpe, aargs) =>
+ mc == ac && mtpe == atpe && margs.map(Matcher.argValue) == aargs
}
+ } ++ (if (funInfos.exists(info => Some(info) == optIdCall)) invocMatcher else None)
if (matchs.nonEmpty) matchers += b -> matchs
}
@@ -280,8 +296,7 @@ object Template {
}
for ((b, matchs) <- matchers; bp = substituter(b); m <- matchs) {
- val newM = m.copy(caller = substituter(m.caller), args = m.args.map(substituter))
- instantiation ++= manager.instantiateMatcher(bp, newM)
+ instantiation ++= manager.instantiateMatcher(bp, m.substitute(substituter))
}
for (q <- quantifications) {
@@ -494,7 +509,7 @@ class LambdaTemplate[T] private (
val newMatchers = matchers.map { case (b, ms) =>
val bp = if (b == start) newStart else b
- bp -> ms.map(m => m.copy(caller = substituter(m.caller), args = m.args.map(substituter)))
+ bp -> ms.map(_.substitute(substituter))
}
val newLambdas = lambdas.map { case (idT, template) => idT -> template.substitute(substMap) }
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index c1912d9d5..617f1c5f4 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -93,7 +93,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
def currentBlockers = callInfo.map(_._2._3).toSeq ++ appInfo.map(_._2._4).toSeq
- def quantificationAssumptions = manager.blockers
+ def quantificationAssumptions = manager.assumptions
def getBlockersToUnlock: Seq[T] = {
if (callInfo.isEmpty && appInfo.isEmpty) {
@@ -265,7 +265,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
defBlockers += info -> defBlocker
val template = templateGenerator.mkTemplate(tfd)
- reporter.debug(template)
+ //reporter.debug(template)
val (newExprs, callBlocks, appBlocks) = template.instantiate(defBlocker, args)
val blockExprs = freshAppBlocks(appBlocks.keys)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index bfa1d9c16..d2dc57f50 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -637,7 +637,7 @@ trait AbstractZ3Solver extends Solver {
case _ => reporter.fatalError("Translation from Z3 to Array failed")
}
- finiteArray(entries, Some(s, default), to)
+ finiteArray(entries, Some(default, s), to)
case _ =>
reporter.fatalError("Translation from Z3 to Array failed")
}
diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index 62f43d736..5b9d6be13 100644
--- a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
@@ -38,6 +38,8 @@ trait Z3ModelReconstruction {
def modelToMap(model: Z3Model, ids: Iterable[Identifier]) : Map[Identifier,Expr] = {
var asMap = Map.empty[Identifier,Expr]
+ println(model)
+
def completeID(id : Identifier) : Unit = {
asMap = asMap + (id -> simplestValue(id.getType))
reporter.debug("Completing variable '" + id + "' to simplest value")
--
GitLab