From 74deb895e5e825b7a49973724712be51b91a6188 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 17 Jun 2015 17:24:49 +0200
Subject: [PATCH] Added quantification template instantiation
---
.../solvers/templates/QuantificationManager.scala | 12 ++++++------
.../scala/leon/solvers/templates/Templates.scala | 4 ++++
2 files changed, 10 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index 1bd5e3b51..a8c4f96c9 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -26,8 +26,8 @@ class QuantificationTemplate[T](
val applications: Map[T, Set[App[T]]],
val lambdas: Map[T, LambdaTemplate[T]]) {
- def instantiate(blocker: T): Instantiation[T] = {
- quantificationManager.instantiateQuantification(blocker, this)
+ def instantiate(substMap: Map[T, T]): Instantiation[T] = {
+ quantificationManager.instantiateQuantification(this, substMap)
}
}
@@ -234,7 +234,7 @@ trait QuantificationManager[T] { self : LambdaManager[T] =>
}
}
- def instantiateQuantification(blocker: T, template: QuantificationTemplate[T]): Instantiation[T] = {
+ def instantiateQuantification(template: QuantificationTemplate[T], substMap: Map[T, T]): Instantiation[T] = {
val quantification: Quantification = {
val quantified = template.quantifiers.map(_._2).toSet
@@ -260,9 +260,9 @@ trait QuantificationManager[T] { self : LambdaManager[T] =>
bindingApps
)
- val tpeCounts = template.quantifiers.groupBy(_._1.getType).mapValues(_.map(_._2).toSeq)
- val substMap = tpeCounts.flatMap { case (tpe, idTs) => idTs zip standardQuantifiers(tpe, idTs.size) }.toMap
- q.substitute(substMap + (template.start -> blocker))
+ val tpeCounts = template.quantifiers.groupBy(_._1.getType).mapValues(_.map(_._2).toSeq)
+ val qSubst = tpeCounts.flatMap { case (tpe, idTs) => idTs zip standardQuantifiers(tpe, idTs.size) }.toMap
+ q.substitute(substMap ++ qSubst)
}
val quantifierSubst: Map[T,T] = freshQuantifierSubst
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index cd0fe0e07..ae9e4e3e0 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -96,6 +96,10 @@ trait Template[T] { self =>
instantiation ++= lambdaManager.instantiateApp(b, app)
}
+ for (q <- quantifications) {
+ instantiation ++= q.instantiate(substMap)
+ }
+
instantiation
}
--
GitLab