From a679d54b7cf4634c9c0874f00fac82d3ead08b8b Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 17 May 2016 12:52:10 +0200
Subject: [PATCH] Fixed funDef ordering in Strengthener
---
src/main/scala/leon/termination/Strengthener.scala | 14 ++++++++++++--
1 file changed, 12 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/termination/Strengthener.scala b/src/main/scala/leon/termination/Strengthener.scala
index 2f17ae601..21b95787f 100644
--- a/src/main/scala/leon/termination/Strengthener.scala
+++ b/src/main/scala/leon/termination/Strengthener.scala
@@ -17,12 +17,22 @@ trait Strengthener { self : RelationComparator =>
val checker: TerminationChecker
+ implicit object CallGraphOrdering extends Ordering[FunDef] {
+ def compare(a: FunDef, b: FunDef): Int = {
+ val aCallsB = checker.program.callGraph.transitivelyCalls(a, b)
+ val bCallsA = checker.program.callGraph.transitivelyCalls(b, a)
+ if (aCallsB && !bCallsA) -1
+ else if (bCallsA && !aCallsB) 1
+ else 0
+ }
+ }
+
private val strengthenedPost : MutableSet[FunDef] = MutableSet.empty
def strengthenPostconditions(funDefs: Set[FunDef])(implicit solver: Processor with Solvable) {
// Strengthen postconditions on all accessible functions by adding size constraints
val callees : Set[FunDef] = funDefs.flatMap(fd => checker.program.callGraph.transitiveCallees(fd))
- val sortedCallees : Seq[FunDef] = callees.toSeq.sortWith((fd1, fd2) => checker.program.callGraph.transitivelyCalls(fd2, fd1))
+ val sortedCallees : Seq[FunDef] = callees.toSeq.sorted
for (funDef <- sortedCallees if !strengthenedPost(funDef) && funDef.hasBody && checker.terminates(funDef).isGuaranteed) {
def strengthen(cmp: (Seq[Expr], Seq[Expr]) => Expr): Boolean = {
@@ -85,7 +95,7 @@ trait Strengthener { self : RelationComparator =>
def strengthenApplications(funDefs: Set[FunDef])(implicit solver: Processor with Solvable) {
val transitiveFunDefs = funDefs ++ funDefs.flatMap(checker.program.callGraph.transitiveCallees)
- val sortedFunDefs = transitiveFunDefs.toSeq.sortWith((fd1, fd2) => checker.program.callGraph.transitivelyCalls(fd2, fd1))
+ val sortedFunDefs = transitiveFunDefs.toSeq.sorted
for (funDef <- sortedFunDefs if !strengthenedApp(funDef) && funDef.hasBody && checker.terminates(funDef).isGuaranteed) {
--
GitLab