From 2628128f0fd6ae2ebb01d2f0c828110992542c74 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sat, 29 Oct 2016 14:35:31 +0200
Subject: [PATCH] Added call-graph based orderings
---
src/main/scala/inox/ast/CallGraph.scala | 24 ++++++++++++++++++++++++
1 file changed, 24 insertions(+)
diff --git a/src/main/scala/inox/ast/CallGraph.scala b/src/main/scala/inox/ast/CallGraph.scala
index 047ac4151..12d68dd0f 100644
--- a/src/main/scala/inox/ast/CallGraph.scala
+++ b/src/main/scala/inox/ast/CallGraph.scala
@@ -77,4 +77,28 @@ trait CallGraph {
}
lazy val stronglyConnectedComponents = graph.stronglyConnectedComponents.N
+
+ lazy val functionComponent: Map[FunDef, Set[FunDef]] = {
+ val inComponents = stronglyConnectedComponents.flatMap(fds => fds.map(_ -> fds)).toMap
+ inComponents ++ symbols.functions.values.filterNot(inComponents.isDefinedAt).map(_ -> Set.empty[FunDef])
+ }
+
+ object CallGraphOrderings {
+ implicit object componentOrdering extends Ordering[Set[FunDef]] {
+ private val components = graph.stronglyConnectedComponents.topSort
+ def compare(a: Set[FunDef], b: Set[FunDef]): Int = {
+ components.indexOf(a).compare(components.indexOf(b))
+ }
+ }
+
+ implicit object functionOrdering extends Ordering[FunDef] {
+ def compare(a: FunDef, b: FunDef): Int = {
+ val (c1, c2) = (functionComponent(a), functionComponent(b))
+ if (c1.isEmpty && c2.isEmpty) a.id.uniqueName.compare(b.id.uniqueName)
+ else if (c1.isEmpty) -1
+ else if (c2.isEmpty) -1
+ else componentOrdering.compare(c1, c2)
+ }
+ }
+ }
}
--
GitLab