From b0984a4358a961e3248d804187e01993a7cdfd27 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 9 Dec 2015 17:18:59 +0100
Subject: [PATCH] Fixed lambda and matcher type indexing issue
---
.../leon/solvers/templates/TemplateGenerator.scala | 11 ++---------
.../leon/solvers/templates/TemplateManager.scala | 11 +++++++----
.../scala/leon/solvers/templates/UnrollingBank.scala | 6 ++++++
3 files changed, 15 insertions(+), 13 deletions(-)
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 665242433..60ddb1450 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -9,6 +9,7 @@ import purescala.Expressions._
import purescala.Extractors._
import purescala.ExprOps._
import purescala.Types._
+import purescala.TypeOps._
import purescala.Definitions._
import purescala.Constructors._
import purescala.Quantification._
@@ -253,14 +254,6 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
res
}
- def liftToIfExpr(pathVar: Identifier, parts: Seq[Expr], join: Seq[Expr] => Expr, recons: (Expr, Expr) => Expr): Expr = {
- val partitions = groupWhile(parts)(!requireDecomposition(_))
- partitions.map(join) match {
- case Seq(e) => e
- case seq => rec(pathVar, seq.reduceRight(recons))
- }
- }
-
def rec(pathVar: Identifier, expr: Expr): Expr = {
expr match {
case a @ Assert(cond, err, body) =>
@@ -416,7 +409,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val idArgs : Seq[Identifier] = lambdaArgs(l)
val trArgs : Seq[T] = idArgs.map(id => substMap.getOrElse(id, encoder.encodeId(id)))
- val lid = FreshIdentifier("lambda", l.getType, true)
+ val lid = FreshIdentifier("lambda", bestRealType(l.getType), true)
val clause = liftedEquals(Variable(lid), l, idArgs, inlineFirst = true)
val localSubst: Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
diff --git a/src/main/scala/leon/solvers/templates/TemplateManager.scala b/src/main/scala/leon/solvers/templates/TemplateManager.scala
index 07019aefd..618a23c3a 100644
--- a/src/main/scala/leon/solvers/templates/TemplateManager.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateManager.scala
@@ -11,6 +11,7 @@ import purescala.Quantification._
import purescala.Extractors._
import purescala.ExprOps._
import purescala.Types._
+import purescala.TypeOps._
import utils._
@@ -116,7 +117,7 @@ object Template {
val (fiArgs, appArgs) = args.splitAt(tfd.params.size)
val app @ Application(caller, arguments) = rec(FunctionInvocation(tfd, fiArgs), appArgs)
- Matcher(encodeExpr(caller), caller.getType, arguments.map(arg => Left(encodeExpr(arg))), encodeExpr(app))
+ Matcher(encodeExpr(caller), bestRealType(caller.getType), arguments.map(arg => Left(encodeExpr(arg))), encodeExpr(app))
}
def encode[T](
@@ -142,7 +143,9 @@ object Template {
}).toSeq
val optIdCall = optCall.map(tfd => TemplateCallInfo[T](tfd, arguments.map(_._2)))
- val optIdApp = optApp.map { case (idT, tpe) => App(idT, tpe, arguments.map(_._2)) }
+ val optIdApp = optApp.map { case (idT, tpe) =>
+ App(idT, bestRealType(tpe).asInstanceOf[FunctionType], arguments.map(_._2))
+ }
lazy val invocMatcher = optCall.filter(_.returnType.isInstanceOf[FunctionType])
.map(tfd => invocationMatcher(encodeExpr)(tfd, arguments.map(_._1.toVariable)))
@@ -160,7 +163,7 @@ object Template {
for (e <- es) {
funInfos ++= firstOrderCallsOf(e).map(p => TemplateCallInfo(p._1, p._2.map(encodeExpr)))
appInfos ++= firstOrderAppsOf(e).map { case (c, args) =>
- App(encodeExpr(c), c.getType.asInstanceOf[FunctionType], args.map(encodeExpr))
+ App(encodeExpr(c), bestRealType(c.getType).asInstanceOf[FunctionType], args.map(encodeExpr))
}
matchInfos ++= fold[Map[Expr, Matcher[T]]] { (expr, res) =>
@@ -175,7 +178,7 @@ object Template {
case None => Left(encodeExpr(arg))
})
- Some(expr -> Matcher(encodeExpr(c), c.getType, encodedArgs, encodeExpr(expr)))
+ Some(expr -> Matcher(encodeExpr(c), bestRealType(c.getType), encodedArgs, encodeExpr(expr)))
case _ => None
})
}(e).values
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index e6e5cd223..d1c4432a3 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -334,6 +334,12 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
newClauses ++= newCls
}
+ /*
+ for ((app @ (b, _), (gen, _, _, _, infos)) <- thisAppInfos if infos.isEmpty) {
+ registerAppBlocker(nextGeneration(gen), app, infos)
+ }
+ */
+
reporter.debug(s" - ${newClauses.size} new clauses")
//context.reporter.ifDebug { debug =>
// debug(s" - new clauses:")
--
GitLab