diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index f5bd3b78e92e6a870212210d07f64fd60811e927..3249656efc6052635d74f79f3470f7e5a06d7f75 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -131,9 +131,9 @@ trait ChainBuilder extends RelationBuilder { self: TerminationChecker with Stren
def decreasing(relations: List[Relation]): Boolean = {
val constraints = relations.map(relation => relationConstraints.getOrElse(relation, {
val Relation(funDef, path, FunctionInvocation(_, args), _) = relation
- val (e1, e2) = (tupleWrap(funDef.params.map(_.toVariable)), tupleWrap(args))
- val constraint = if (solver.definitiveALL(implies(andJoin(path), self.softDecreasing(e1, e2)))) {
- if (solver.definitiveALL(implies(andJoin(path), self.sizeDecreasing(e1, e2)))) {
+ val args0 = funDef.params.map(_.toVariable)
+ val constraint = if (solver.definitiveALL(implies(andJoin(path), self.softDecreasing(args0, args)))) {
+ if (solver.definitiveALL(implies(andJoin(path), self.sizeDecreasing(args0, args)))) {
StrongDecreasing
} else {
WeakDecreasing
diff --git a/src/main/scala/leon/termination/RelationComparator.scala b/src/main/scala/leon/termination/RelationComparator.scala
index 90741fd6679581e0325c86b9d424ac8858ec7640..14121286b497355f7cd2479a2cb8dfea42ef76d7 100644
--- a/src/main/scala/leon/termination/RelationComparator.scala
+++ b/src/main/scala/leon/termination/RelationComparator.scala
@@ -4,12 +4,18 @@ package leon
package termination
import purescala.Expressions._
+import leon.purescala.Constructors._
trait RelationComparator { self : StructuralSize =>
- def sizeDecreasing(e1: Expr, e2: Expr) = GreaterThan(self.size(e1), self.size(e2))
+ def sizeDecreasing(args1: Seq[Expr], args2: Seq[Expr]): Expr = {
+ GreaterThan(self.size(tupleWrap(args1)), self.size(tupleWrap(args2)))
+ }
+
+ def softDecreasing(args1: Seq[Expr], args2: Seq[Expr]): Expr = {
+ GreaterEquals(self.size(tupleWrap(args1)), self.size(tupleWrap(args2)))
+ }
- def softDecreasing(e1: Expr, e2: Expr) = GreaterEquals(self.size(e1), self.size(e2))
}
// vim: set ts=4 sw=4 et:
diff --git a/src/main/scala/leon/termination/RelationProcessor.scala b/src/main/scala/leon/termination/RelationProcessor.scala
index d4d1aad73f1c17d9f9ff323f38e19707a7356ae2..91fdce46e7c10dbbef1554935c18fc44d4902015 100644
--- a/src/main/scala/leon/termination/RelationProcessor.scala
+++ b/src/main/scala/leon/termination/RelationProcessor.scala
@@ -27,10 +27,10 @@ class RelationProcessor(
val formulas = problem.funDefs.map({ funDef =>
funDef -> checker.getRelations(funDef).collect({
case Relation(_, path, FunctionInvocation(tfd, args), _) if problem.funSet(tfd.fd) =>
- val (e1, e2) = (tupleWrap(funDef.params.map(_.toVariable)), tupleWrap(args))
+ val args0 = funDef.params.map(_.toVariable)
def constraint(expr: Expr) = implies(andJoin(path.toSeq), expr)
- val greaterThan = checker.sizeDecreasing(e1, e2)
- val greaterEquals = checker.softDecreasing(e1, e2)
+ val greaterThan = checker.sizeDecreasing(args0, args)
+ val greaterEquals = checker.softDecreasing(args0, args)
(tfd.fd, (constraint(greaterThan), constraint(greaterEquals)))
})
})
diff --git a/src/main/scala/leon/termination/Strengthener.scala b/src/main/scala/leon/termination/Strengthener.scala
index bfe0c73a52b0a96a79379718eca4bead9bf62712..31ed7f002c962a6ca4dab1fc09be515eae1a9c37 100644
--- a/src/main/scala/leon/termination/Strengthener.scala
+++ b/src/main/scala/leon/termination/Strengthener.scala
@@ -22,12 +22,12 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
val sortedCallees : Seq[FunDef] = callees.toSeq.sortWith((fd1, fd2) => self.program.callGraph.transitivelyCalls(fd2, fd1))
for (funDef <- sortedCallees if !strengthenedPost(funDef) && funDef.hasBody && self.terminates(funDef).isGuaranteed) {
- def strengthen(cmp: (Expr, Expr) => Expr): Boolean = {
+ def strengthen(cmp: (Seq[Expr], Seq[Expr]) => Expr): Boolean = {
val old = funDef.postcondition
val postcondition = {
val res = FreshIdentifier("res", funDef.returnType, true)
val post = old.map{application(_, Seq(Variable(res)))}.getOrElse(BooleanLiteral(true))
- val sizePost = cmp(tupleWrap(funDef.params.map(_.toVariable)), res.toVariable)
+ val sizePost = cmp(funDef.params.map(_.toVariable), Seq(res.toVariable))
Lambda(Seq(ValDef(res)), and(post, sizePost))
}
@@ -71,8 +71,8 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
def applicationConstraint(fd: FunDef, id: Identifier, arg: Expr, args: Seq[Expr]): Expr = arg match {
case Lambda(fargs, body) => appConstraint.get(fd -> id) match {
- case Some(StrongDecreasing) => self.sizeDecreasing(tupleWrap(args), tupleWrap(fargs.map(_.toVariable)))
- case Some(WeakDecreasing) => self.softDecreasing(tupleWrap(args), tupleWrap(fargs.map(_.toVariable)))
+ case Some(StrongDecreasing) => self.sizeDecreasing(args, fargs.map(_.toVariable))
+ case Some(WeakDecreasing) => self.softDecreasing(args, fargs.map(_.toVariable))
case _ => BooleanLiteral(true)
}
case _ => BooleanLiteral(true)
@@ -84,20 +84,20 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
for (funDef <- sortedFunDefs if !strengthenedApp(funDef) && funDef.hasBody && self.terminates(funDef).isGuaranteed) {
- val appCollector = new CollectorWithPaths[(Identifier,Expr,Expr)] {
- def collect(e: Expr, path: Seq[Expr]): Option[(Identifier, Expr, Expr)] = e match {
- case Application(Variable(id), args) => Some((id, andJoin(path), tupleWrap(args)))
+ val appCollector = new CollectorWithPaths[(Identifier,Expr,Seq[Expr])] {
+ def collect(e: Expr, path: Seq[Expr]): Option[(Identifier, Expr, Seq[Expr])] = e match {
+ case Application(Variable(id), args) => Some((id, andJoin(path), args))
case _ => None
}
}
val applications = appCollector.traverse(funDef).distinct
- val funDefArgTuple = tupleWrap(funDef.params.map(_.toVariable))
+ val funDefArgs = funDef.params.map(_.toVariable)
val allFormulas = for ((id, path, appArgs) <- applications) yield {
- val soft = Implies(path, self.softDecreasing(funDefArgTuple, appArgs))
- val hard = Implies(path, self.sizeDecreasing(funDefArgTuple, appArgs))
+ val soft = Implies(path, self.softDecreasing(funDefArgs, appArgs))
+ val hard = Implies(path, self.sizeDecreasing(funDefArgs, appArgs))
id -> ((soft, hard))
}
@@ -117,10 +117,10 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
val funDefHOArgs = funDef.params.map(_.id).filter(_.getType.isInstanceOf[FunctionType]).toSet
- 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 {
+ val fiCollector = new CollectorWithPaths[(Expr, Seq[Expr], Seq[(Identifier,(FunDef, Identifier))])] {
+ def collect(e: Expr, path: Seq[Expr]): Option[(Expr, Seq[Expr], Seq[(Identifier,(FunDef, Identifier))])] = e match {
case FunctionInvocation(tfd, args) if (funDefHOArgs intersect args.collect({ case Variable(id) => id }).toSet).nonEmpty =>
- Some((andJoin(path), tupleWrap(args), (args zip tfd.fd.params).collect {
+ Some((andJoin(path), args, (args zip tfd.fd.params).collect {
case (Variable(id), vd) if funDefHOArgs(id) => id -> ((tfd.fd, vd.id))
}))
case _ => None
@@ -128,19 +128,19 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
}
val invocations = fiCollector.traverse(funDef)
- val id2invocations : Seq[(Identifier, ((FunDef, Identifier), Expr, Expr))] =
+ val id2invocations : Seq[(Identifier, ((FunDef, Identifier), Expr, Seq[Expr]))] =
invocations.flatMap(p => p._3.map(c => c._1 -> ((c._2, p._1, p._2))))
- val invocationMap : Map[Identifier, Seq[((FunDef, Identifier), Expr, Expr)]] =
+ val invocationMap : Map[Identifier, Seq[((FunDef, Identifier), Expr, Seq[Expr])]] =
id2invocations.groupBy(_._1).mapValues(_.map(_._2))
- def constraint(id: Identifier, passings: Seq[((FunDef, Identifier), Expr, Expr)]): SizeConstraint = {
+ def constraint(id: Identifier, passings: Seq[((FunDef, Identifier), Expr, Seq[Expr])]): SizeConstraint = {
if (constraints.get(id) == Some(NoConstraint)) NoConstraint
else if (passings.exists(p => appConstraint.get(p._1) == Some(NoConstraint))) NoConstraint
else passings.foldLeft[SizeConstraint](constraints.getOrElse(id, StrongDecreasing)) {
case (constraint, (key, path, args)) =>
- lazy val strongFormula = Implies(path, self.sizeDecreasing(funDefArgTuple, args))
- lazy val weakFormula = Implies(path, self.softDecreasing(funDefArgTuple, args))
+ lazy val strongFormula = Implies(path, self.sizeDecreasing(funDefArgs, args))
+ lazy val weakFormula = Implies(path, self.softDecreasing(funDefArgs, args))
(constraint, appConstraint.get(key)) match {
case (_, Some(NoConstraint)) => scala.sys.error("Whaaaat!?!? This shouldn't happen...")