diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala index a63cf2cdc155ba4c8d45a2247002f958720ee89a..0be34a227e952eb5876440a21c388a78ba4b23aa 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 012abda64dc15821774b5fe49e4aa07b3c0ccd5f..3fede60e6035f55dc33b7274e272641c4ef73834 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 0000000000000000000000000000000000000000..2599fd069c068da547fc06a6edec050925e04521 --- /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 + } + +}