From bfdb241c5ba0da6e0726bcede09071141e27b9b3 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 9 Mar 2016 16:11:40 +0100
Subject: [PATCH] Benchmark should use BigInts
---
testcases/synthesis/future/SortedList.scala | 43 +++++++++++----------
1 file changed, 23 insertions(+), 20 deletions(-)
diff --git a/testcases/synthesis/future/SortedList.scala b/testcases/synthesis/future/SortedList.scala
index b71f4f67e..973cd4b50 100644
--- a/testcases/synthesis/future/SortedList.scala
+++ b/testcases/synthesis/future/SortedList.scala
@@ -4,41 +4,44 @@ import leon.lang.synthesis._
object SortedList {
sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
+ case class Cons(head: BigInt, tail: List) extends List
case class Nil() extends List
// proved with unrolling=0
- def size(l: List) : Int = (l match {
- case Nil() => 0
- case Cons(_, t) => 1 + size(t)
- }) ensuring(res => res >= 0)
+ def size(l: List) : BigInt = (l match {
+ case Nil() => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= BigInt(0))
- //def sizeSynth(l: List): Int = choose{ (i: Int) => i >= 0 && sizeSynth(Cons(0, l)) == i + 1}
+ //def sizeSynth(l: List): BigInt = choose{ (i: BigInt) => i >= 0 && sizeSynth(Cons(0, l)) == i + 1}
- def content(l: List): Set[Int] = l match {
+ def content(l: List): Set[BigInt] = l match {
case Nil() => Set()
case Cons(i, t) => Set(i) ++ content(t)
}
def groundSynth() = choose{ (out: List) => size(out) == 5 }
- def insertSynth(in: List, v: Int) = choose{ (out: List) => content(out) == content(in) ++ Set(v) }
+ def insertSynth(in: List, v: BigInt) = choose{ (out: List) => content(out) == content(in) ++ Set(v) }
def tailSynth(in: List) = choose{out: List => size(out)+1 == size(in)}
def consSynth(in: List) = choose{out: List => size(out) == size(in)+1}
- def listOfSizeSynth(i: Int) = choose{out: List => size(out) == i }
+ def listOfSizeSynth(i: BigInt) = {
+ require(i >= 0)
+ choose { out: List => size(out) == i }
+ }
- def insert1(l: List, v: Int) = (
+ def insert1(l: List, v: BigInt) = (
Cons(v, l)
) ensuring(res => content(res) == content(l) ++ Set(v) && size(res) >= size(l))
- def insert2(l: List, v: Int): List = (l match {
+ def insert2(l: List, v: BigInt): List = (l match {
case Nil() => Cons(v, Nil())
case Cons(x, tail) => if (x == v) l else Cons(x, insert2(tail, v))
}) ensuring(res => content(res) == content(l) ++ Set(v) && size(res) >= size(l))
- def insert3(l: List, v: Int): List = {
+ def insert3(l: List, v: BigInt): List = {
require(isStrictlySorted(l))
l match {
@@ -54,14 +57,14 @@ object SortedList {
}
} ensuring(res => content(res) == content(l) ++ Set(v) && size(res) >= size(l))
- def deleteSynth(in: List, v: Int) = choose{ (out: List) => !(content(out) contains v) }
+ def deleteSynth(in: List, v: BigInt) = choose{ (out: List) => !(content(out) contains v) }
- def delete1(l: List, v: Int): List = (l match {
+ def delete1(l: List, v: BigInt): List = (l match {
case Nil() => Nil()
case Cons(x, tail) => if (x == v) delete1(tail, v) else Cons(x, delete1(tail, v))
}) ensuring(res => !(content(res) contains v) && size(res) <= size(l))
- //def delete2(l: List, v: Int): List = {
+ //def delete2(l: List, v: BigInt): List = {
// require(isStrictlySorted(l))
// l match {
@@ -75,19 +78,19 @@ object SortedList {
// }
//} ensuring(res => !(content(res) contains v) && size(res) <= size(l))
- def contains(list : List, elem : Int) : Boolean = (list match {
+ def contains(list : List, elem : BigInt) : Boolean = (list match {
case Nil() => false
case Cons(x, xs) => if(elem == x) true else contains(xs, elem)
}) ensuring(res => res == content(list).contains(elem))
- def deleteMagic(head: Int, tail: List, toDelete: Int): List = ({
+ def deleteMagic(head: BigInt, tail: List, toDelete: BigInt): List = ({
//require(isStrictlySorted(Cons(head, tail)) && toDelete < head);
require(isStrictlySorted(Cons(toDelete, Cons(head, tail))))
Cons(head, tail)
})ensuring(res => !(content(res) contains toDelete))
- def delete3(l: List, v: Int): List = {
+ def delete3(l: List, v: BigInt): List = {
require(isStrictlySorted(l))
l match {
@@ -119,7 +122,7 @@ object SortedList {
case Cons(x, xs) => lessThanAll(x, xs)
}))
- def lessThanAll(x : Int, l : List) : Boolean = (l match {
+ def lessThanAll(x : BigInt, l : List) : Boolean = (l match {
case Nil() => true
case Cons(y, ys) => if(x < y) lessThanAll(x, ys) else false
}) ensuring(res => !res || !contains(l, x))
@@ -127,7 +130,7 @@ object SortedList {
def discard(value : Boolean) = true
@induct
- def ltaLemma(x : Int, y : Int, l : List) : Boolean = {
+ def ltaLemma(x : BigInt, y : BigInt, l : List) : Boolean = {
require(lessThanAll(y, l) && x < y)
lessThanAll(x, Cons(y, l))
} holds
--
GitLab