diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala index 369ac9e718c5785b1efbade3e58fffe4e1a36c84..0766f017f34ba5f3421ce0f25d228c189d236391 100644 --- a/src/main/scala/leon/purescala/ExprOps.scala +++ b/src/main/scala/leon/purescala/ExprOps.scala @@ -1245,12 +1245,7 @@ object ExprOps { case e => e }).copiedFrom(expr) - def fix[A](f: (A) => A)(a: A): A = { - val na = f(a) - if(a == na) a else fix(f)(na) - } - - fix(simplePostTransform(simplify0))(expr) + fixpoint(simplePostTransform(simplify0))(expr) } /** Checks whether a predicate is inductive on a certain identfier. diff --git a/src/unit-test/scala/leon/utils/UtilsPackageSuite.scala b/src/unit-test/scala/leon/utils/UtilsPackageSuite.scala new file mode 100644 index 0000000000000000000000000000000000000000..77bf111afb1e96f9c28819ed7445effbea822ee7 --- /dev/null +++ b/src/unit-test/scala/leon/utils/UtilsPackageSuite.scala @@ -0,0 +1,32 @@ +/* Copyright 2009-2015 EPFL, Lausanne */ + +package leon +package utils + +class ExprOpsSuite extends LeonTestSuite { + + test("fixpoint computes correct fixpoint of function that increments up to a max") { + def f(x: Int): Int = if(x < 10) x + 1 else 10 + assert(f(10) === 10) + assert(fixpoint(f)(1) === 10) + } + + test("fixpoint computes correct fixpoint with a large limit") { + def f(x: Int): Int = if(x < 100) x + 1 else 100 + assert(f(100) === 100) + assert(fixpoint(f)(-1) === 100) + } + + test("fixpoint finds the fixpoint in small number of iteration") { + def f(x: Int): Int = if(x < 10) x + 1 else 10 + assert(f(10) === 10) + assert(fixpoint(f, 15)(1) === 10) + } + + test("fixpoint of id is the starting expression") { + def id(x: Int): Int = x + assert(fixpoint(id)(1) === 1) + assert(fixpoint(id)(42) === 42) + } + +}