Benchmark should use BigInts

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