update testcases to bigint and fix readme instruction

README.md

@@ -29,31 +29,38 @@ To build, type this:
 
 Then you can try e.g.
 
-    $ ./leon ./testcases/sas2011-testcases/RedBlackTree.scala
+    $ ./leon ./testcases/verification/sas2011-testcases/RedBlackTree.scala
 
 and get something like this:
 
 <pre>
-    ┌─────────┐
-  ╔═╡ Summary ╞═══════════════════════════════════════════════════════════════════════╗
-  ║ └─────────┘                                                                       ║
-  ║ add                       postcond.           valid               Z3-f+t    0.314 ║
-  ║ add                       precond.    (82,14) valid               Z3-f+t    0.020 ║
-  ║ add                       precond.    (82,18) valid               Z3-f+t    0.005 ║
-  ║ balance                   postcond.           valid               Z3-f+t    0.409 ║
-  ║ balance                   match.      (91,19) valid               Z3-f+t    0.034 ║
-  ║ blackHeight               match.      (51,39) valid               Z3-f+t    0.004 ║
-  ║ buggyAdd                  postcond.           invalid             Z3-f+t    4.084 ║
-  ║ buggyAdd                  precond.     (87,8) invalid             Z3-f+t    0.111 ║
-  ║ buggyBalance              postcond.           invalid             Z3-f+t    0.055 ║
-  ║ buggyBalance              match.     (105,19) invalid             Z3-f+t    0.007 ║
-  ║ ins                       postcond.           valid               Z3-f+t    6.577 ║
-  ║ ins                       precond.    (63,40) valid               Z3-f+t    0.021 ║
-  ║ ins                       precond.    (65,43) valid               Z3-f+t    0.005 ║
-  ║ makeBlack                 postcond.           valid               Z3-f+t    0.007 ║
-  ║ redNodesHaveBlackChildren match.      (35,56) valid               Z3-f+t    0.003 ║
-  ║ size                      postcond.           valid               Z3-f+t    0.012 ║
-  ╚═══════════════════════════════════════════════════════════════════════════════════╝
+    ┌──────────────────────┐
+  ╔═╡ Verification Summary ╞═════════════════════════════════════════════════════════════════════╗
+  ║ └──────────────────────┘                                                                     ║
+  ║ add                            postcondition            83:22    valid        Z3-f     0.057 ║
+  ║ add                            precondition             82:5     valid        Z3-f     0.017 ║
+  ║ add                            precondition             82:15    valid        Z3-f     0.003 ║
+  ║ balance                        match exhaustiveness     91:5     valid        Z3-f     0.005 ║
+  ║ balance                        postcondition            102:22   valid        Z3-f     0.055 ║
+  ║ blackBalanced                  match exhaustiveness     46:43    valid        Z3-f     0.003 ║
+  ║ blackHeight                    match exhaustiveness     51:40    valid        Z3-f     0.004 ║
+  ║ buggyAdd                       postcondition            88:22    invalid      Z3-f     1.162 ║
+  ║ buggyAdd                       precondition             87:5     invalid      Z3-f     0.027 ║
+  ║ buggyBalance                   match exhaustiveness     105:5    invalid      Z3-f     0.007 ║
+  ║ buggyBalance                   postcondition            116:22   invalid      Z3-f     0.017 ║
+  ║ content                        match exhaustiveness     18:37    valid        Z3-f     0.034 ║
+  ║ ins                            match exhaustiveness     60:5     valid        Z3-f     0.003 ║
+  ║ ins                            postcondition            67:22    valid        Z3-f     1.753 ║
+  ║ ins                            precondition             63:37    valid        Z3-f     0.011 ║
+  ║ ins                            precondition             65:40    valid        Z3-f     0.012 ║
+  ║ makeBlack                      postcondition            78:21    valid        Z3-f     0.012 ║
+  ║ redDescHaveBlackChildren       match exhaustiveness     41:53    valid        Z3-f     0.003 ║
+  ║ redNodesHaveBlackChildren      match exhaustiveness     35:54    valid        Z3-f     0.004 ║
+  ║ size                           match exhaustiveness     23:33    valid        Z3-f     0.004 ║
+  ║ size                           postcondition            26:15    valid        Z3-f     0.043 ║
+  ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
+  ║ total: 21     valid: 17     invalid: 4      unknown 0                                  3.236 ║
+  ╚══════════════════════════════════════════════════════════════════════════════════════════════╝
 </pre>
 
 Building Leon

testcases/verification/sas2011-testcases/AmortizedQueue.scala

@@ -10,8 +10,8 @@ object AmortizedQueue {
   sealed abstract class AbsQueue
   case class Queue(front : List, rear : List) extends AbsQueue
 
-  def size(list : List) : Int = (list match {
-    case Nil() => 0
+  def size(list : List) : BigInt = (list match {
+    case Nil() => BigInt(0)
     case Cons(_, xs) => 1 + size(xs)
   }) ensuring(_ >= 0)
 

testcases/verification/sas2011-testcases/InsertionSort.scala

@@ -4,19 +4,19 @@ import leon.lang._
 
 object InsertionSort {
   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
 
   sealed abstract class OptInt
-  case class Some(value: Int) extends OptInt
+  case class Some(value: BigInt) extends OptInt
   case class None() extends OptInt
 
-  def size(l : List) : Int = (l match {
-    case Nil() => 0
+  def size(l : List) : BigInt = (l match {
+    case Nil() => BigInt(0)
     case Cons(_, xs) => 1 + size(xs)
   }) ensuring(_ >= 0)
 
-  def contents(l: List): Set[Int] = l match {
+  def contents(l: List): Set[BigInt] = l match {
     case Nil() => Set.empty
     case Cons(x,xs) => contents(xs) ++ Set(x)
   }
@@ -37,7 +37,7 @@ object InsertionSort {
 
   /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
    * the expected content and size */
-  def sortedIns(e: Int, l: List): List = {
+  def sortedIns(e: BigInt, l: List): List = {
     require(isSorted(l))
     l match {
       case Nil() => Cons(e,Nil())
@@ -50,7 +50,7 @@ object InsertionSort {
 
   /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
    * the expected content and size */
-  def buggySortedIns(e: Int, l: List): List = {
+  def buggySortedIns(e: BigInt, l: List): List = {
     // require(isSorted(l))
     l match {
       case Nil() => Cons(e,Nil())

testcases/verification/sas2011-testcases/ListOperations.scala

@@ -14,13 +14,13 @@ object ListOperations {
     sealed abstract class IntPair
     case class IP(fst: Int, snd: Int) extends IntPair
 
-    def size(l: List) : Int = (l match {
-        case Nil() => 0
+    def size(l: List) : BigInt = (l match {
+        case Nil() => BigInt(0)
         case Cons(_, t) => 1 + size(t)
     }) ensuring(res => res >= 0)
 
-    def iplSize(l: IntPairList) : Int = (l match {
-      case IPNil() => 0
+    def iplSize(l: IntPairList) : BigInt = (l match {
+      case IPNil() => BigInt(0)
       case IPCons(_, xs) => 1 + iplSize(xs)
     }) ensuring(_ >= 0)
 
@@ -37,8 +37,8 @@ object ListOperations {
       }
     } ensuring(iplSize(_) == size(l1))
 
-    def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0)
-    def sizeTailRecAcc(l: List, acc: Int) : Int = {
+    def sizeTailRec(l: List) : BigInt = sizeTailRecAcc(l, 0)
+    def sizeTailRecAcc(l: List, acc: BigInt) : BigInt = {
      require(acc >= 0)
      l match {
        case Nil() => acc

testcases/verification/sas2011-testcases/RedBlackTree.scala

@@ -20,8 +20,8 @@ object RedBlackTree {
     case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
   }
 
-  def size(t: Tree) : Int = (t match {
-    case Empty() => 0
+  def size(t: Tree) : BigInt = (t match {
+    case Empty() => BigInt(0)
     case Node(_, l, v, r) => size(l) + 1 + size(r)
   }) ensuring(_ >= 0)
 
@@ -48,8 +48,8 @@ object RedBlackTree {
     case Empty() => true
   }
 
-  def blackHeight(t : Tree) : Int = t match {
-    case Empty() => 1
+  def blackHeight(t : Tree) : BigInt = t match {
+    case Empty() => BigInt(1)
     case Node(Black(), l, _, _) => blackHeight(l) + 1
     case Node(Red(), l, _, _) => blackHeight(l)
   }

testcases/verification/sas2011-testcases/SearchLinkedList.scala

@@ -7,8 +7,8 @@ object SearchLinkedList {
   case class Cons(head : Int, tail : List) extends List
   case class Nil() extends List
 
-  def size(list : List) : Int = (list match {
-    case Nil() => 0
+  def size(list : List) : BigInt = (list match {
+    case Nil() => BigInt(0)
     case Cons(_, xs) => 1 + size(xs)
   }) ensuring(_ >= 0)
 
@@ -17,9 +17,9 @@ object SearchLinkedList {
     case Cons(x, xs) => x == elem || contains(xs, elem)
   })
 
-  def firstZero(list : List) : Int = (list match {
-    case Nil() => 0
-    case Cons(x, xs) => if (x == 0) 0 else firstZero(xs) + 1
+  def firstZero(list : List) : BigInt = (list match {
+    case Nil() => BigInt(0)
+    case Cons(x, xs) => if (x == 0) BigInt(0) else firstZero(xs) + 1
   }) ensuring (res =>
     res >= 0 && (if (contains(list, 0)) {
       firstZeroAtPos(list, res)
@@ -27,14 +27,14 @@ object SearchLinkedList {
       res == size(list)
     }))
 
-  def firstZeroAtPos(list : List, pos : Int) : Boolean = {
+  def firstZeroAtPos(list : List, pos : BigInt) : Boolean = {
     list match {
       case Nil() => false
       case Cons(x, xs) => if (pos == 0) x == 0 else x != 0 && firstZeroAtPos(xs, pos - 1)
     }
   } 
 
-  def goal(list : List, i : Int) : Boolean = {
+  def goal(list : List, i : BigInt) : Boolean = {
     if(firstZero(list) == i) {
       if(contains(list, 0)) {
         firstZeroAtPos(list, i)

testcases/verification/sas2011-testcases/SumAndMax.scala

@@ -3,10 +3,10 @@ import leon.annotation._
 
 object SumAndMax {
   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
 
-  def max(list : List) : Int = {
+  def max(list : List) : BigInt = {
     require(list != Nil())
     list match {
       case Cons(x, Nil()) => x
@@ -17,13 +17,13 @@ object SumAndMax {
     }
   }
 
-  def sum(list : List) : Int = list match {
-    case Nil() => 0
+  def sum(list : List) : BigInt = list match {
+    case Nil() => BigInt(0)
     case Cons(x, xs) => x + sum(xs)
   }
 
-  def size(list : List) : Int = (list match {
-    case Nil() => 0
+  def size(list : List) : BigInt = (list match {
+    case Nil() => BigInt(0)
     case Cons(_, xs) => 1 + size(xs)
   }) ensuring(_ >= 0)