From d318d306dc7af94d00b4cb22d34fbda55a692ef2 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 21 Jul 2015 16:45:31 +0200
Subject: [PATCH] fixpoint should not be in ExprOps
---
src/main/scala/leon/purescala/ExprOps.scala | 15 +----------
src/main/scala/leon/utils/GraphOps.scala | 2 +-
src/main/scala/leon/utils/package.scala | 28 +++++++++++++++++++++
3 files changed, 30 insertions(+), 15 deletions(-)
create mode 100644 src/main/scala/leon/utils/package.scala
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index a63cf2cdc..0be34a227 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -9,7 +9,7 @@ import Definitions._
import Expressions._
import Extractors._
import Constructors._
-import utils.Simplifiers
+import utils._
import solvers._
/** Provides functions to manipulate [[purescala.Expressions]].
@@ -189,19 +189,6 @@ object ExprOps {
}
- def fixpoint[T](f: T => T, limit: Int = -1)(e: T): T = {
- var v1 = e
- var v2 = f(v1)
- var lim = limit
- while(v2 != v1 && lim != 0) {
- v1 = v2
- lim -= 1
- v2 = f(v2)
- }
- v2
- }
-
-
/*
* =============
* Auxiliary API
diff --git a/src/main/scala/leon/utils/GraphOps.scala b/src/main/scala/leon/utils/GraphOps.scala
index 012abda64..3fede60e6 100644
--- a/src/main/scala/leon/utils/GraphOps.scala
+++ b/src/main/scala/leon/utils/GraphOps.scala
@@ -32,7 +32,7 @@ object GraphOps {
graph.getOrElse(v, Set())
}))
}
- leon.purescala.ExprOps.fixpoint(step, -1)(graph)
+ fixpoint(step, -1)(graph)
}
def sources[A](graph : Map[A,Set[A]]) = {
diff --git a/src/main/scala/leon/utils/package.scala b/src/main/scala/leon/utils/package.scala
new file mode 100644
index 000000000..2599fd069
--- /dev/null
+++ b/src/main/scala/leon/utils/package.scala
@@ -0,0 +1,28 @@
+package leon
+
+/** Various utilities used throughout the Leon system */
+package object utils {
+
+ /** compute the fixpoint of a function.
+ *
+ * Apply the input function on an expression as long as until
+ * it stays the same (value equality) or until a set limit.
+ *
+ * @param f
+ * @param limit
+ * @param e
+ * @return
+ */
+ def fixpoint[T](f: T => T, limit: Int = -1)(e: T): T = {
+ var v1 = e
+ var v2 = f(v1)
+ var lim = limit
+ while(v2 != v1 && lim != 0) {
+ v1 = v2
+ lim -= 1
+ v2 = f(v2)
+ }
+ v2
+ }
+
+}
--
GitLab