diff --git a/library/lang/package.scala b/library/lang/package.scala
index df7c29d010d540b60e743c099a45ab6546b3791f..44351d02ca9328bbbf86063745d233f2db17cd7c 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -30,6 +30,12 @@ package object lang {
}
}
+ @ignore def forall[A](p: A => Boolean): Boolean = sys.error("Can't execute quantified proposition")
+ @ignore def forall[A,B](p: (A,B) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
+ @ignore def forall[A,B,C](p: (A,B,C) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
+ @ignore def forall[A,B,C,D](p: (A,B,C,D) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
+ @ignore def forall[A,B,C,D,E](p: (A,B,C,D,E) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
+
@ignore
object InvariantFunction {
def invariant(x: Boolean): Unit = ()
diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index 37de1a88284a5659953da4a6c3bc77cb8a833046..3b355a4b7a960279f4dfd9d65ebfbdec4337147e 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -11,31 +11,32 @@ import purescala.Types._
import Instantiation._
-class LambdaManager[T](encoder: TemplateEncoder[T]) {
- private type IdMap = Map[T, LambdaTemplate[T]]
+class LambdaManager[T](protected val encoder: TemplateEncoder[T]) {
+
+ protected type IdMap = Map[T, LambdaTemplate[T]]
+ protected def byID : IdMap = byIDStack.head
private var byIDStack : List[IdMap] = List(Map.empty)
- private def byID : IdMap = byIDStack.head
private def byID_=(map: IdMap) : Unit = {
byIDStack = map :: byIDStack.tail
}
- private type TypeMap = Map[TypeTree, Set[(T, LambdaTemplate[T])]]
+ protected type TypeMap = Map[FunctionType, Set[(T, LambdaTemplate[T])]]
+ protected def byType : TypeMap = byTypeStack.head
private var byTypeStack : List[TypeMap] = List(Map.empty.withDefaultValue(Set.empty))
- private def byType : TypeMap = byTypeStack.head
private def byType_=(map: TypeMap) : Unit = {
byTypeStack = map :: byTypeStack.tail
}
- private type ApplicationMap = Map[TypeTree, Set[(T, App[T])]]
+ protected type ApplicationMap = Map[FunctionType, Set[(T, App[T])]]
+ protected def applications : ApplicationMap = applicationsStack.head
private var applicationsStack : List[ApplicationMap] = List(Map.empty.withDefaultValue(Set.empty))
- private def applications : ApplicationMap = applicationsStack.head
private def applications_=(map: ApplicationMap) : Unit = {
applicationsStack = map :: applicationsStack.tail
}
- private type FreeMap = Map[TypeTree, Set[T]]
+ protected type FreeMap = Map[FunctionType, Set[T]]
+ protected def freeLambdas : FreeMap = freeLambdasStack.head
private var freeLambdasStack : List[FreeMap] = List(Map.empty.withDefaultValue(Set.empty))
- private def freeLambdas : FreeMap = freeLambdasStack.head
private def freeLambdas_=(map: FreeMap) : Unit = {
freeLambdasStack = map :: freeLambdasStack.tail
}
@@ -55,67 +56,61 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) {
}
def registerFree(lambdas: Seq[(TypeTree, T)]): Unit = {
- lambdas.foreach(p => freeLambdas += p._1 -> (freeLambdas(p._1) + p._2))
+ for ((tpe, idT) <- lambdas) tpe match {
+ case ft: FunctionType =>
+ freeLambdas += ft -> (freeLambdas(ft) + idT)
+ case _ =>
+ }
}
- private def instantiate(apps: Map[T, Set[App[T]]], lambdas: Map[T, LambdaTemplate[T]]) : Instantiation[T] = {
- var clauses : Clauses[T] = Seq.empty
- var callBlockers : CallBlockers[T] = Map.empty.withDefaultValue(Set.empty)
+ def instantiateLambda(idT: T, template: LambdaTemplate[T]): Instantiation[T] = {
+ var clauses : Clauses[T] = equalityClauses(idT, template)
var appBlockers : AppBlockers[T] = Map.empty.withDefaultValue(Set.empty)
- def mkBlocker(blockedApp: (T, App[T]), lambda: (T, LambdaTemplate[T])) : Unit = {
- val (_, App(caller, tpe, args)) = blockedApp
- val (idT, template) = lambda
+ // make sure the new lambda isn't equal to any free lambda var
+ clauses ++= freeLambdas(template.tpe).map(pIdT => encoder.mkNot(encoder.mkEquals(pIdT, idT)))
+ byID += idT -> template
+ byType += template.tpe -> (byType(template.tpe) + (idT -> template))
+
+ for (blockedApp @ (_, App(caller, tpe, args)) <- applications(template.tpe)) {
val equals = encoder.mkEquals(idT, caller)
appBlockers += (blockedApp -> (appBlockers(blockedApp) + TemplateAppInfo(template, equals, args)))
}
- for (lambda @ (idT, template) <- lambdas) {
- // make sure the new lambda isn't equal to any free lambda var
- clauses ++= freeLambdas(template.tpe).map(pIdT => encoder.mkNot(encoder.mkEquals(pIdT, idT)))
-
- byID += idT -> template
- byType += template.tpe -> (byType(template.tpe) + (idT -> template))
-
- for (guardedApp <- applications(template.tpe)) {
- mkBlocker(guardedApp, lambda)
- }
- }
+ (clauses, Map.empty, appBlockers)
+ }
- for ((b, fas) <- apps; app @ App(caller, tpe, args) <- fas) {
- if (byID contains caller) {
- val (newClauses, newCalls, newApps) = byID(caller).instantiate(b, args)
+ def instantiateApp(blocker: T, app: App[T]): Instantiation[T] = {
+ val App(caller, tpe, args) = app
+ var clauses : Clauses[T] = Seq.empty
+ var callBlockers : CallBlockers[T] = Map.empty.withDefaultValue(Set.empty)
+ var appBlockers : AppBlockers[T] = Map.empty.withDefaultValue(Set.empty)
- clauses ++= newClauses
- newCalls.foreach(p => callBlockers += p._1 -> (callBlockers(p._1) ++ p._2))
- newApps.foreach(p => appBlockers += p._1 -> (appBlockers(p._1) ++ p._2))
- } else if (!freeLambdas(tpe).contains(caller)) {
- val key = b -> app
+ if (byID contains caller) {
+ val (newClauses, newCalls, newApps) = byID(caller).instantiate(blocker, args)
- // make sure that even if byType(tpe) is empty, app is recorded in blockers
- // so that UnrollingBank will generate the initial block!
- if (!(appBlockers contains key)) appBlockers += key -> Set.empty
+ clauses ++= newClauses
+ newCalls.foreach(p => callBlockers += p._1 -> (callBlockers(p._1) ++ p._2))
+ newApps.foreach(p => appBlockers += p._1 -> (appBlockers(p._1) ++ p._2))
+ } else if (!freeLambdas(tpe).contains(caller)) {
+ val key = blocker -> app
- for (lambda <- byType(tpe)) {
- mkBlocker(key, lambda)
- }
+ // make sure that even if byType(tpe) is empty, app is recorded in blockers
+ // so that UnrollingBank will generate the initial block!
+ if (!(appBlockers contains key)) appBlockers += key -> Set.empty
- applications += tpe -> (applications(tpe) + key)
+ for ((idT,template) <- byType(tpe)) {
+ val equals = encoder.mkEquals(idT, caller)
+ appBlockers += (key -> (appBlockers(key) + TemplateAppInfo(template, equals, args)))
}
+
+ applications += tpe -> (applications(tpe) + key)
}
(clauses, callBlockers, appBlockers)
}
- def instantiateLambda(idT: T, template: LambdaTemplate[T]): Instantiation[T] = {
- val eqClauses = equalityClauses(idT, template)
- val (clauses, blockers, apps) = instantiate(Map.empty, Map(idT -> template))
- (eqClauses ++ clauses, blockers, apps)
- }
-
- def instantiateApps(apps: Map[T, Set[App[T]]]): Instantiation[T] = instantiate(apps, Map.empty)
-
private def equalityClauses(idT: T, template: LambdaTemplate[T]): Seq[T] = {
byType(template.tpe).map { case (thatIdT, that) =>
val equals = encoder.mkEquals(idT, thatIdT)
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3503033f577a4c19ddadc3dfea835d68aae81c4c
--- /dev/null
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -0,0 +1,210 @@
+package leon
+package solvers
+package templates
+
+import purescala.Common._
+import purescala.Extractors._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
+
+import Instantiation._
+
+trait QuantificationManager[T] { self : LambdaManager[T] =>
+
+ lazy val startId = FreshIdentifier("q", BooleanType)
+ lazy val start = encoder.encodeId(startId)
+
+ private class QuantificationScope(
+ val quantifiedApps: List[(T, App[T])],
+ val quantifiedID: Map[Identifier, 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 lambdas: Map[T, LambdaTemplate[T]]
+ ) {
+ def this() = this(Nil, Map.empty, Map.empty, Map.empty, Seq.empty, Map.empty, Map.empty, Map.empty)
+ lazy val quantified: Set[T] = quantifiedID.values.toSet
+ }
+
+ private var scopes: List[QuantificationScope] = List(new QuantificationScope)
+ private def scope: QuantificationScope = scopes.head
+
+ override def push(): Unit = {
+ self.push()
+
+ val currentScope = scope
+ scopes = new QuantificationScope(
+ currentScope.quantifiedApps,
+ currentScope.quantifiedID,
+ currentScope.condVars,
+ currentScope.exprVars,
+ currentScope.clauses,
+ currentScope.blockers,
+ currentScope.applications,
+ currentScope.lambdas
+ ) :: scopes.tail
+ }
+
+ override def pop(lvl: Int): Unit = {
+ self.pop(lvl)
+ scopes = scopes.drop(lvl)
+ }
+
+ def registerQuantified(start: T, condVars: Map[Identifier, T], exprVars: Map[Identifier, T], clauses: Seq[T], blockers: Map[T, Set[TemplateCallInfo[T]]], apps: Set[(T, App[T])], quantified: Set[T]): Unit = {
+
+ val bindingCalls: Set[App[T]] = apps.collect {
+ case (b, app @ App(caller, tpe, args)) if args exists quantified => app
+ }
+
+ // TODO: postcondition res ??
+ val argumentBindings: Set[(Option[T], FunctionType, Int, T)] = bindingCalls.flatMap {
+ case App(caller, tpe, args) => args.zipWithIndex.collect {
+ case (qid, idx) if quantified(qid) => (if (freeLambdas(tpe)(caller)) Some(caller) else None, tpe, idx, qid)
+ }
+ }
+
+ val (callerBindings, typeBindings) = argumentBindings.partition(_._1.isDefined)
+
+ val typeMap: Map[FunctionType, Set[(Int, T)]] = typeBindings.groupBy(_._2).mapValues(_.map(p => (p._3, p._4)))
+ val typePairs: Seq[(T, T)] = typeMap.toSeq.flatMap {
+ case (_, argBinds) => argBinds.groupBy(_._1).mapValues(_.map(_._2)).toSeq.flatMap {
+ case (_, options) => options.flatMap(o1 => options.map(o2 => o1 -> o2))
+ }
+ }
+
+ val callerPairs: Seq[(T, T)] = callerBindings.groupBy(p => (p._1.get, p._2)).toSeq.flatMap {
+ case ((freeFunction, tpe), arguments) =>
+ val callerIdentified: Set[(Int, T)] = arguments.map(p => (p._3, p._4))
+ val typeIdentified: Set[(Int, T)] = typeMap.getOrElse(tpe, Set.empty)
+
+ (callerIdentified ++ typeIdentified).groupBy(_._1).mapValues(_.map(_._2)).toSeq.flatMap {
+ case (_, options) => options.flatMap(o1 => options.map(o2 => o1 -> o2))
+ }
+ }
+
+ val filteredPairs: Set[(T, T)] = {
+ def rec(
+ mappings: Seq[(T, T)],
+ result: Set[(T, T)]
+ ): Set[(T, T)] = mappings match {
+ case (p @ (x, y)) +: tail if !result(p) && !result(y -> x) => rec(tail, result + p)
+ case p +: tail => rec(tail, result)
+ case Seq() => result
+ }
+
+ rec(callerPairs ++ typePairs, Set.empty)
+ }
+
+ val mappings: List[Map[T, T]] =
+ filteredPairs.groupBy(_._1).toSeq.foldLeft(List(Map.empty[T, T])) {
+ case (mappings, (_, pairs)) => pairs.toList.flatMap(p => mappings.map(mapping => mapping + p))
+ }
+
+ val expandedClauses = mappings.flatMap { mapping =>
+ val substituter = encoder.substitute(mapping)
+ clauses map substituter
+ }
+
+
+ }
+
+ override def instantiateApp(blocker: T, app: App[T]): Instantiation[T] = {
+ val App(caller, tpe, args) = app
+ val currentScope = scope
+ import currentScope._
+
+ // 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
+ // as other instantiations have been performed previously when the associated applications
+ // were first encountered.
+ val appMappings: List[List[((T, App[T]), (T, App[T]))]] = quantifiedApps
+ // 1. select an application in the quantified proposition for which the current app can
+ // be bound when generating the new constraints
+ .filter { case (qb, qapp) =>
+ qapp.caller == caller || (qapp.tpe == tpe && !freeLambdas(qapp.tpe)(qapp.caller))
+ }
+ // 2. build the instantiation mapping associated to the chosen current application binding
+ .flatMap { bindingApp => quantifiedApps
+ // 2.1. select all potential matches for each quantified application
+ .map { case qapp @ (qb, App(qcaller, qtpe, qargs)) =>
+ if (qapp == bindingApp) {
+ bindingApp -> Set(blocker -> app)
+ } else {
+ val instances = self.applications(qtpe).filter(p => qcaller == p._2.caller || !freeLambdas(qtpe)(p._2.caller))
+
+ // 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 withApp = if (qcaller == caller || !freeLambdas(tpe)(caller)) instances + (blocker -> app) else instances
+
+ // add quantified application to instances for constraints that depend on free variables
+ // this also make sure that constraints that don't depend on all variables will also be instantiated
+ val withAll = withApp + qapp
+
+ qapp -> withAll
+ }
+ }
+ // 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[List[List[((T, App[T]), (T, App[T]))]]] (List(Nil)) {
+ case (mappings, (qapp, instances)) =>
+ instances.toList.flatMap(app => mappings.map(mapping => mapping :+ (app -> qapp)))
+ }
+ }
+
+ var instantiation = Instantiation.empty[T]
+
+ for (mapping <- appMappings) {
+ var constraints: List[T] = Nil
+ var subst: Map[T, T] = Map.empty
+
+ for {
+ ((qb, App(qcaller, _, qargs)), (b, App(caller, _, args))) <- mapping
+ _ = constraints ++= Seq(qb, b)
+ _ = if (qcaller != caller) constraints :+= encoder.mkEquals(qcaller, caller)
+ (qarg, arg) <- (qargs zip args)
+ } if (subst.isDefinedAt(qarg) || !quantified(qarg)) {
+ constraints :+= encoder.mkEquals(qarg, arg)
+ } else {
+ subst += qarg -> arg
+ }
+
+ // make sure we freshen quantified variables that haven't been bound by concrete calls
+ subst ++= quantifiedID.collect {
+ case (id, idT) if !subst.isDefinedAt(idT) => idT -> encoder.encodeId(id)
+ }
+
+ val bp = encoder.encodeId(startId)
+ val enabler = encoder.mkEquals(bp, encoder.mkAnd(constraints : _*))
+
+ val lambdaSubstMap = lambdas.map { case (idT, lambda) => idT -> encoder.encodeId(lambda.id) }
+ val substMap = subst ++ lambdaSubstMap + (start -> enabler)
+ val substituter = encoder.substitute(subst)
+
+ val newClauses = clauses.map(substituter)
+ val newBlockers = blockers.map { case (b, fis) =>
+ substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
+ }
+
+ val newApplications = currentScope.applications.map { case (b, fas) =>
+ substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
+ }
+
+ instantiation ++= (newClauses, newBlockers, Map.empty)
+
+ for ((idT, lambda) <- lambdas) {
+ val newIdT = substituter(idT)
+ val newTemplate = lambda.substitute(substMap)
+ instantiation ++= instantiateLambda(newIdT, newTemplate)
+ }
+
+ for ((b, apps) <- newApplications; app <- apps) {
+ instantiation ++= instantiateApp(b, app)
+ }
+ }
+
+ instantiation
+ }
+}
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 0e0e7f063daebff985beda49f198deae8edbcde3..1eac5171272810efc23750e3745a7b03ce5fbf46 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -17,7 +17,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
private var cache = Map[TypedFunDef, FunctionTemplate[T]]()
private var cacheExpr = Map[Expr, FunctionTemplate[T]]()
- private val lambdaManager = new LambdaManager[T](encoder)
+ private val lambdaManager = new LambdaManager[T](encoder) with QuantificationManager[T]
def mkTemplate(body: Expr): FunctionTemplate[T] = {
if (cacheExpr contains body) {
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index 38821e2a0a73c98fe45c05df0ff37b265d307aa9..fddce8a08e50c3a6083edf0ae136aaf2b1b8fb3e 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -11,7 +11,7 @@ import purescala.ExprOps._
import purescala.Types._
import purescala.Definitions._
-case class App[T](caller: T, tpe: TypeTree, args: Seq[T]) {
+case class App[T](caller: T, tpe: FunctionType, args: Seq[T]) {
override def toString = {
"(" + caller + " : " + tpe + ")" + args.mkString("(", ",", ")")
}
@@ -26,7 +26,7 @@ object Instantiation {
def empty[T] = (Seq.empty[T], Map.empty[T, Set[TemplateCallInfo[T]]], Map.empty[(T, App[T]), Set[TemplateAppInfo[T]]])
implicit class InstantiationWrapper[T](i: Instantiation[T]) {
- def merge(that: Instantiation[T]): Instantiation[T] = {
+ def ++(that: Instantiation[T]): Instantiation[T] = {
val (thisClauses, thisBlockers, thisApps) = i
val (thatClauses, thatBlockers, thatApps) = that
@@ -81,17 +81,19 @@ trait Template[T] { self =>
substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
}
- val lambdaInstantiation = lambdas.foldLeft(Instantiation.empty[T]) {
- case (acc, (idT, lambda)) =>
- val newIdT = substituter(idT)
- val newTemplate = lambda.substitute(substMap)
- val instantiation = lambdaManager.instantiateLambda(newIdT, newTemplate)
- acc merge instantiation
+ var instantiation: Instantiation[T] = (newClauses, newBlockers, Map.empty)
+
+ for ((idT, lambda) <- lambdas) {
+ val newIdT = substituter(idT)
+ val newTemplate = lambda.substitute(substMap)
+ instantiation ++= lambdaManager.instantiateLambda(newIdT, newTemplate)
}
- val appInstantiation = lambdaManager.instantiateApps(newApplications)
+ for ((b,apps) <- newApplications; app <- apps) {
+ instantiation ++= lambdaManager.instantiateApp(b, app)
+ }
- (newClauses, newBlockers, Map.empty[(T, App[T]), Set[TemplateAppInfo[T]]]) merge lambdaInstantiation merge appInstantiation
+ instantiation
}
override def toString : String = "Instantiated template"
@@ -132,7 +134,7 @@ object Template {
val App(c, tpe, prevArgs) = applicationTemplate(caller)
App(c, tpe, prevArgs ++ args.map(encodeExpr))
case Application(c, args) =>
- App(encodeExpr(c), c.getType, args.map(encodeExpr))
+ App(encodeExpr(c), c.getType.asInstanceOf[FunctionType], args.map(encodeExpr))
case _ => scala.sys.error("Should never happen!")
}
@@ -151,7 +153,7 @@ object Template {
lambdas: Map[T, LambdaTemplate[T]],
substMap: Map[Identifier, T] = Map.empty[Identifier, T],
optCall: Option[TypedFunDef] = None,
- optApp: Option[(T, TypeTree)] = None
+ optApp: Option[(T, FunctionType)] = None
) : (Seq[T], Map[T, Set[TemplateCallInfo[T]]], Map[T, Set[App[T]]], () => String) = {
val idToTrId : Map[Identifier, T] = {
@@ -258,7 +260,6 @@ object FunctionTemplate {
funString
)
}
-
}
class FunctionTemplate[T] private(
@@ -344,7 +345,7 @@ object LambdaTemplate {
) : LambdaTemplate[T] = {
val id = ids._2
- val tpe = ids._1.getType
+ val tpe = ids._1.getType.asInstanceOf[FunctionType]
val (clauses, blockers, applications, templateString) =
Template.encode(encoder, pathVar, arguments, condVars, exprVars, guardedExprs, lambdas,
substMap = baseSubstMap + ids, optApp = Some(id -> tpe))
@@ -390,7 +391,7 @@ class LambdaTemplate[T] private (
private[templates] val structuralKey: Lambda,
stringRepr: () => String) extends Template[T] {
- val tpe = id.getType
+ val tpe = id.getType.asInstanceOf[FunctionType]
def substitute(substMap: Map[T,T]): LambdaTemplate[T] = {
val substituter : T => T = encoder.substitute(substMap)