From 7159d3a29f997d5452ea82ab63dfc8d342cef718 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sat, 12 Dec 2015 18:22:46 +0100
Subject: [PATCH] Fix for functions with no pathVars
---
.../solvers/templates/LambdaManager.scala | 6 ++---
.../templates/QuantificationManager.scala | 26 +++++++++++--------
.../solvers/templates/TemplateManager.scala | 15 ++++++-----
3 files changed, 26 insertions(+), 21 deletions(-)
diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index 74bfe2fd4..75d163815 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -54,7 +54,7 @@ object LambdaTemplate {
ids,
encoder,
manager,
- pathVar._2,
+ pathVar,
arguments,
condVars,
exprVars,
@@ -76,7 +76,7 @@ class LambdaTemplate[T] private (
val ids: (Identifier, T),
val encoder: TemplateEncoder[T],
val manager: QuantificationManager[T],
- val start: T,
+ val pathVar: (Identifier, T),
val arguments: Seq[(Identifier, T)],
val condVars: Map[Identifier, T],
val exprVars: Map[Identifier, T],
@@ -122,7 +122,7 @@ class LambdaTemplate[T] private (
ids._1 -> substituter(ids._2),
encoder,
manager,
- newStart,
+ pathVar._1 -> newStart,
arguments,
condVars,
exprVars,
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index 9bc278f09..c7f715b5e 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -45,7 +45,7 @@ case class Matcher[T](caller: T, tpe: TypeTree, args: Seq[Either[T, Matcher[T]]]
class QuantificationTemplate[T](
val quantificationManager: QuantificationManager[T],
- val start: T,
+ val pathVar: (Identifier, T),
val qs: (Identifier, T),
val q2s: (Identifier, T),
val insts: (Identifier, T),
@@ -60,10 +60,12 @@ class QuantificationTemplate[T](
val matchers: Map[T, Set[Matcher[T]]],
val lambdas: Seq[LambdaTemplate[T]]) {
+ lazy val start = pathVar._2
+
def substitute(substituter: T => T): QuantificationTemplate[T] = {
new QuantificationTemplate[T](
quantificationManager,
- substituter(start),
+ pathVar._1 -> substituter(start),
qs,
q2s,
insts,
@@ -114,7 +116,7 @@ object QuantificationTemplate {
substMap = subst + q2s + insts + guards + qs)
new QuantificationTemplate[T](quantificationManager,
- pathVar._2, qs, q2s, insts, guards._2, quantifiers,
+ pathVar, qs, q2s, insts, guards._2, quantifiers,
condVars, exprVars, condTree, clauses, blockers, applications, matchers, lambdas)
}
}
@@ -328,7 +330,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
private trait MatcherQuantification {
- val start: T
+ val pathVar: (Identifier, T)
val quantified: Set[T]
val matchers: Set[Matcher[T]]
val allMatchers: Map[T, Set[Matcher[T]]]
@@ -340,6 +342,8 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val applications: Map[T, Set[App[T]]]
val lambdas: Seq[LambdaTemplate[T]]
+ lazy val start = pathVar._2
+
private lazy val depth = matchers.map(matcherDepth).max
private lazy val transMatchers: Set[Matcher[T]] = (for {
(b, ms) <- allMatchers.toSeq
@@ -438,7 +442,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
val baseSubstMap = exprVars.map { case (id, idT) => idT -> encoder.encodeId(id) } ++
- freshConds(enabler, condVars, condTree)
+ freshConds(pathVar._1 -> enabler, condVars, condTree)
val lambdaSubstMap = lambdas map (lambda => lambda.ids._2 -> encoder.encodeId(lambda.ids._1))
val substMap = subst.mapValues(Matcher.argValue) ++ baseSubstMap ++ lambdaSubstMap ++ instanceSubst(enablers)
@@ -473,7 +477,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
private class Quantification (
- val start: T,
+ val pathVar: (Identifier, T),
val qs: (Identifier, T),
val q2s: (Identifier, T),
val insts: (Identifier, T),
@@ -520,7 +524,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
private class LambdaAxiom (
- val start: T,
+ val pathVar: (Identifier, T),
val blocker: T,
val guardVar: T,
val quantified: Set[T],
@@ -599,7 +603,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val enablingClause = encoder.mkImplies(guardT, blockerT)
instantiateAxiom(
- substMap(template.start),
+ template.pathVar._1 -> substMap(template.start),
blockerT,
guardT,
quantifiers,
@@ -621,7 +625,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
def instantiateAxiom(
- start: T,
+ pathVar: (Identifier, T),
blocker: T,
guardVar: T,
quantifiers: Seq[(Identifier, T)],
@@ -641,7 +645,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
var instantiation = Instantiation.empty[T]
for (matchers <- matchQuorums) {
- val axiom = new LambdaAxiom(start, blocker, guardVar, quantified,
+ val axiom = new LambdaAxiom(pathVar, blocker, guardVar, quantified,
matchers, allMatchers, condVars, exprVars, condTree,
clauses, blockers, applications, lambdas
)
@@ -679,7 +683,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val substituter = encoder.substitute(subst)
val quantification = new Quantification(
- substituter(template.start),
+ template.pathVar._1 -> substituter(template.start),
template.qs._1 -> newQ,
template.q2s, template.insts, template.guardVar,
quantified,
diff --git a/src/main/scala/leon/solvers/templates/TemplateManager.scala b/src/main/scala/leon/solvers/templates/TemplateManager.scala
index 618a23c3a..bb6629ec1 100644
--- a/src/main/scala/leon/solvers/templates/TemplateManager.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateManager.scala
@@ -62,7 +62,7 @@ trait Template[T] { self =>
val encoder : TemplateEncoder[T]
val manager : QuantificationManager[T]
- val start : T
+ val pathVar: (Identifier, T)
val args : Seq[T]
val condVars : Map[Identifier, T]
val exprVars : Map[Identifier, T]
@@ -74,6 +74,8 @@ trait Template[T] { self =>
val matchers : Map[T, Set[Matcher[T]]]
val lambdas : Seq[LambdaTemplate[T]]
+ lazy val start = pathVar._2
+
private var substCache : Map[Seq[T],Map[T,T]] = Map.empty
def instantiate(aVar: T, args: Seq[T]): Instantiation[T] = {
@@ -82,7 +84,7 @@ trait Template[T] { self =>
case Some(subst) => subst
case None =>
val subst = exprVars.map { case (id, idT) => idT -> encoder.encodeId(id) } ++
- manager.freshConds(aVar, condVars, condTree) ++
+ manager.freshConds(pathVar._1 -> aVar, condVars, condTree) ++
(this.args zip args)
substCache += args -> subst
subst
@@ -303,7 +305,7 @@ object FunctionTemplate {
tfd,
encoder,
manager,
- pathVar._2,
+ pathVar,
arguments.map(_._2),
condVars,
exprVars,
@@ -324,7 +326,7 @@ class FunctionTemplate[T] private(
val tfd: TypedFunDef,
val encoder: TemplateEncoder[T],
val manager: QuantificationManager[T],
- val start: T,
+ val pathVar: (Identifier, T),
val args: Seq[T],
val condVars: Map[Identifier, T],
val exprVars: Map[Identifier, T],
@@ -358,10 +360,9 @@ class TemplateManager[T](protected[templates] val encoder: TemplateEncoder[T]) e
def push(): Unit = incrementals.foreach(_.push())
def pop(): Unit = incrementals.foreach(_.pop())
- def freshConds(path: T, condVars: Map[Identifier, T], tree: Map[Identifier, Set[Identifier]]): Map[T, T] = {
+ def freshConds(path: (Identifier, T), condVars: Map[Identifier, T], tree: Map[Identifier, Set[Identifier]]): Map[T, T] = {
val subst = condVars.map { case (id, idT) => idT -> encoder.encodeId(id) }
- val pathVar = tree.keys.filter(id => !condVars.isDefinedAt(id)).head
- val mapping = condVars.mapValues(subst) + (pathVar -> path)
+ val mapping = condVars.mapValues(subst) + path
for ((parent, children) <- tree; ep = mapping(parent); child <- children) {
val ec = mapping(child)
--
GitLab