diff --git a/testcases/synthesis/FastExp.scala b/testcases/synthesis/FastExp.scala index 9ea39a1d660d4c8b34ee41cb2d242ea6e065c27f..4d094d500f73fd4a077e78ce2f836f92f125c3f0 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) + //} }