From fe63cdcbb56ab68e895bf3abb227585147fb452e Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 23 Jul 2015 14:25:55 +0200
Subject: [PATCH] test and use fixpoint
---
src/main/scala/leon/purescala/ExprOps.scala | 7 +---
.../scala/leon/utils/UtilsPackageSuite.scala | 32 +++++++++++++++++++
2 files changed, 33 insertions(+), 6 deletions(-)
create mode 100644 src/unit-test/scala/leon/utils/UtilsPackageSuite.scala
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 369ac9e71..0766f017f 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 000000000..77bf111af
--- /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)
+ }
+
+}
--
GitLab