From f8a8d62f672e4170f004b7489ddb688303bae0a5 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 26 Jan 2015 10:26:07 +0100
Subject: [PATCH] Fixed issue with freshened ids in lambda strengthener
---
src/main/scala/leon/purescala/TreeOps.scala | 2 +-
.../leon/termination/RelationBuilder.scala | 24 +++++++++++++------
.../scala/leon/termination/Strengthener.scala | 6 ++---
3 files changed, 21 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index f1ce4fffd..b4ed90a7b 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1247,7 +1247,7 @@ object TreeOps {
def walk(e: Expr, path: Seq[Expr]): Option[Expr] = None
- override final def rec(e: Expr, path: Seq[Expr]) = {
+ override def rec(e: Expr, path: Seq[Expr]) = {
collect(e, path).foreach { results :+= _ }
walk(e, path) match {
case Some(r) => r
diff --git a/src/main/scala/leon/termination/RelationBuilder.scala b/src/main/scala/leon/termination/RelationBuilder.scala
index c9acd8ccf..0e910e99f 100644
--- a/src/main/scala/leon/termination/RelationBuilder.scala
+++ b/src/main/scala/leon/termination/RelationBuilder.scala
@@ -20,7 +20,7 @@ trait RelationBuilder { self: TerminationChecker with Strengthener =>
protected type RelationSignature = (FunDef, Option[Expr], Option[Expr], Option[Expr], Boolean, Set[(FunDef, Boolean)])
protected def funDefRelationSignature(fd: FunDef): RelationSignature = {
- val strengthenedCallees = Set.empty[(FunDef, Boolean)] // self.program.callGraph.callees(fd).map(fd => fd -> strengthened(fd))
+ val strengthenedCallees = self.program.callGraph.callees(fd).map(fd => fd -> strengthened(fd))
(fd, fd.precondition, fd.body, fd.postcondition.map(_._2), self.terminates(fd).isGuaranteed, strengthenedCallees)
}
@@ -31,19 +31,29 @@ trait RelationBuilder { self: TerminationChecker with Strengthener =>
case _ => {
val collector = new CollectorWithPaths[Relation] {
var inLambda: Boolean = false
+
+ override def rec(e: Expr, path: Seq[Expr]): Expr = e match {
+ case l : Lambda =>
+ val old = inLambda
+ inLambda = true
+ val res = super.rec(e, path)
+ inLambda = old
+ res
+ case _ =>
+ super.rec(e, path)
+ }
+
def collect(e: Expr, path: Seq[Expr]): Option[Relation] = e match {
case fi @ FunctionInvocation(f, args) if self.functions(f.fd) =>
Some(Relation(funDef, path, fi, inLambda))
- case l @ Lambda(args, body) =>
- inLambda = true
- None
case _ => None
}
override def walk(e: Expr, path: Seq[Expr]) = e match {
- case FunctionInvocation(fd, args) =>
- Some(FunctionInvocation(fd, (fd.params.map(_.id) zip args) map { case (id, arg) =>
- rec(arg, /* register(self.applicationConstraint(fd, id, arg, args), path) */ path)
+ case FunctionInvocation(tfd, args) =>
+ val funDef = tfd.fd
+ Some(FunctionInvocation(tfd, (funDef.params.map(_.id) zip args) map { case (id, arg) =>
+ rec(arg, register(self.applicationConstraint(funDef, id, arg, args), path))
}))
case _ => None
}
diff --git a/src/main/scala/leon/termination/Strengthener.scala b/src/main/scala/leon/termination/Strengthener.scala
index a827162ca..2357cea33 100644
--- a/src/main/scala/leon/termination/Strengthener.scala
+++ b/src/main/scala/leon/termination/Strengthener.scala
@@ -116,9 +116,9 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
val fiCollector = new CollectorWithPaths[(Expr, Expr, Seq[(Identifier,(FunDef, Identifier))])] {
def collect(e: Expr, path: Seq[Expr]): Option[(Expr, Expr, Seq[(Identifier,(FunDef, Identifier))])] = e match {
- case FunctionInvocation(fd, args) if (funDefHOArgs intersect args.collect({ case Variable(id) => id }).toSet).nonEmpty =>
- Some((And(path), Tuple(args), (args zip fd.params).collect {
- case (Variable(id), vd) if funDefHOArgs(id) => id -> ((fd.fd, vd.id))
+ case FunctionInvocation(tfd, args) if (funDefHOArgs intersect args.collect({ case Variable(id) => id }).toSet).nonEmpty =>
+ Some((And(path), Tuple(args), (args zip tfd.fd.params).collect {
+ case (Variable(id), vd) if funDefHOArgs(id) => id -> ((tfd.fd, vd.id))
}))
case _ => None
}
--
GitLab