From 3b9caaf23538a77130d60d693c1d3a03a6997dc2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 29 Nov 2012 18:44:14 +0100
Subject: [PATCH] explicit FastExp
---
testcases/synthesis/FastExp.scala | 21 ++++++++++++++-------
1 file changed, 14 insertions(+), 7 deletions(-)
diff --git a/testcases/synthesis/FastExp.scala b/testcases/synthesis/FastExp.scala
index 9ea39a1d6..4d094d500 100644
--- a/testcases/synthesis/FastExp.scala
+++ b/testcases/synthesis/FastExp.scala
@@ -1,15 +1,22 @@
+import leon.Annotations._
import leon.Utils._
object FastExp {
- def fp(m : Int, b : Int, i : Int) : Int = i match {
- case 0 => m
- case 2 * j => fp(m, b*b, j)
- case 2 * j + 1 => fp(m*b, b*b, j)
+ def test(a : Int) : Int = {
+ val j1 = choose((k: Int) => 2*k == a)
+ val j2 = choose((k: Int) => 2*k + 1 == a)
+ j1 + j2
}
- def pow(base: Int, p: Int) = {
- fp(1, base, p)
- }
+ //def fp(m : Int, b : Int, i : Int) : Int = i match {
+ // case 0 => m
+ // case 2 * j => fp(m, b*b, j)
+ // case 2 * j + 1 => fp(m*b, b*b, j)
+ //}
+
+ //def pow(base: Int, p: Int) = {
+ // fp(1, base, p)
+ //}
}
--
GitLab