Add various benchmarks

New Verification Benchmarks:
    - Addresses
    - AmortizedQueue
    - TreeListSet

New Synthesis Benchmarks:
    - List
    - BinaryTree
    - AVLTree (incomplete)

testcases/Addresses.scala

+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+  // list of integers
+  sealed abstract class List
+  case class Cons(a:Int,b:Int,c:Int, tail:List) extends List
+  case class Nil() extends List
+
+  def empty() = Set.empty[Int]
+
+  def setA(l:List) : Set[Int] = l match {
+    case Nil() => empty
+    case Cons(a,b,c,l1) => Set(a) ++ setA(l1)
+  }
+
+  def containsA(x:Int,l:List) : Boolean = (l match {
+    case Nil() => false
+    case Cons(a,b,c,t) => a==x || containsA(x,t)
+  }) ensuring (res => res == (setA(l) contains x))
+
+  def theseAunique1(as:Set[Int],l:List) : Boolean = l match {
+    case Nil() => true
+    case Cons(a,b,c,l1) => 
+      theseAunique1(as,l1) && !(as contains a) && (setA(l1) contains a)
+  }
+
+  def theseAunique2(as:Set[Int],l:List) : Boolean = (l match {
+    case Nil() => true
+    case Cons(a,b,c,l1) => 
+      theseAunique2(as,l1) && !(as contains a) && containsA(a,l1)
+  }) ensuring (res => res==theseAunique1(as,l))
+
+  def disjoint(x:Set[Int],y:Set[Int]):Boolean =
+    x.intersect(y).isEmpty
+
+  def uniqueAbsentAs(unique:Set[Int],absent:Set[Int],l:List) : Boolean = (l match {
+    case Nil() => true
+    case Cons(a,b,c,l1) => {
+      !(absent contains a) &&
+      (if (unique contains a) uniqueAbsentAs(unique -- Set(a), absent ++ Set(a), l1)
+       else uniqueAbsentAs(unique, absent, l1))
+    }
+  }) ensuring (res => theseAunique1(unique,l) && disjoint(setA(l),absent))
+
+  def allPos(l:List) : Boolean = l match {
+    case Nil() => true
+    case Cons(a,b,c,l1) => 0 <= a && 0 <= b && 0 <= c && allPos(l1)
+  }
+
+  def max(x:Int,y:Int) = if (x <= y) x else y
+
+  def collectA(x:Int,l:List) : (Int,Int,List) = (l match {
+    case Nil() => (0,0,Nil())
+    case Cons(a,b,c,l1) if (a==x) => {
+      val (b2,c2,l2) = collectA(x,l1)
+      (max(b,b2),max(c,c2),l2)
+    }
+    case Cons(a,b,c,l1) if (a!=x) => {
+      val (b2,c2,l2) = collectA(x,l1)
+      (b2,c2,Cons(a,b,c,l2))
+    }
+  }) ensuring (res => {
+    val (b,c,l1) = res
+    !setA(l1).contains(x)
+  })
+
+  def makeUniqueA(x:Int,l:List) : List = {
+    require(allPos(l))
+    val (b,c,l1) = collectA(x,l)
+    Cons(x,b,c,l1)
+  } ensuring(res => theseAunique1(Set(x),res))
+}

testcases/AmortizedQueueStrongSpec.scala

+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+object AmortizedQueue {
+  sealed abstract class List
+  case class Cons(head : Int, tail : List) extends List
+  case class Nil() extends List
+
+  sealed abstract class AbsQueue
+  case class Queue(front : List, rear : List) extends AbsQueue
+
+  def size(list : List) : Int = (list match {
+    case Nil() => 0
+    case Cons(_, xs) => 1 + size(xs)
+  }) ensuring(_ >= 0)
+
+  def content(l: List) : Set[Int] = l match {
+    case Nil() => Set.empty[Int]
+    case Cons(x, xs) => Set(x) ++ content(xs)
+  }
+  
+  def q2l(queue : AbsQueue) : List = queue match {
+    case Queue(front, rear) => concat(front, reverse(rear))
+  }
+
+  def nth(l:List, n:Int) : Int = {
+    require(0 <= n && n < size(l))
+    l match {
+      case Cons(x,xs) => 
+	if (n==0) x else nth(xs, n-1)
+    }
+  }
+
+  def l2mFrom(k:Int, l:List) : Map[Int,Int] = (l match {
+    case Nil() => Map[Int,Int]()
+    case Cons(x,xs) => l2mFrom(k+1,xs).updated(k,x)
+  })
+
+  def l2m(l:List) : Map[Int,Int] = l2mFrom(0,l)
+
+  def concat(l1 : List, l2 : List) : List = (l1 match {
+    case Nil() => l2
+    case Cons(x,xs) => Cons(x, concat(xs, l2))
+  }) ensuring (res => size(res) == size(l1) + size(l2) && content(res) == content(l1) ++ content(l2))
+
+  def concatTest(l1 : List, l2 : List, i:Int) : List = ({
+    require(0 <= i && i < size(l1) + size(l2))
+    l1 match {
+      case Nil() => l2
+      case Cons(x,xs) => Cons(x, 
+			      if (i == 0) concat(xs, l2)
+			      else concatTest(xs, l2, i-1))
+    }
+  }) ensuring (res => size(res) == size(l1) + size(l2) && 
+	       content(res) == content(l1) ++ content(l2) &&
+	       nth(res,i) == (if (i < size(l1)) nth(l1,i) else nth(l2,i-size(l1))) &&
+	       res == concat(l1,l2))
+
+  def nthConcat(l1:List, l2:List, i:Int) : Boolean = {
+    require(0 <= i && i < size(l1) + size(l2))
+    concatTest(l1, l2, i) == concatTest(l1, l2, i) &&
+    nth(concat(l1,l2), i) == (if (i < size(l1)) nth(l1,i) else nth(l2,i-size(l1)))
+  } holds
+
+  def sameUpto(l1:List, l2:List, k:Int) : Boolean = {
+    require(0 <= k)
+    (l1,l2) match {
+      case (Nil(),Nil()) => true
+      case (Nil(),_) => false
+      case (_,Nil()) => false
+      case (Cons(x,xs),Cons(y,ys)) => {
+	x==y && (if (k==0) true else sameUpto(xs,ys,k-1))
+      }
+    }
+  } ensuring(res => !(size(l1)==k && size(l2)==k && res) || l1==l2)
+
+  @induct
+  def concatAssoc(l1:List, l2:List, l3:List) : Boolean = {
+    concat(l1, concat(l2,l3)) == concat(concat(l1,l2), l3)
+  } holds
+
+  def concatCons(x:Int, l2:List, l3:List) : Boolean = {
+    Cons(x, concat(l2,l3)) == concat(Cons(x,l2), l3)
+  } holds
+
+  def isAmortized(queue : AbsQueue) : Boolean = queue match {
+    case Queue(front, rear) => size(front) >= size(rear)
+  }
+
+  def reverse(l : List) : List = (l match {
+    case Nil() => Nil()
+    case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil()))
+  }) ensuring (res => content(res) == content(l))
+
+  def revConcatNth(l1:List, l2:List, i:Int) : Boolean = {
+    require(0 <= i && i < size(l1)+size(l2))
+    nth(reverse(concat(l1,l2)),i) == nth(concat(reverse(l2), reverse(l1)),i)
+  } holds
+
+  def revrev(l:List) : Boolean = {
+    reverse(reverse(l)) == l
+  } holds
+
+  def amortizedQueue(front : List, rear : List) : AbsQueue = {
+    if (size(rear) <= size(front))
+      Queue(front, rear)
+    else
+      Queue(concat(front, reverse(rear)), Nil())
+  } ensuring(res => isAmortized(res) && q2l(Queue(front, rear)) == q2l(res))
+
+  def isEmpty(queue : AbsQueue) : Boolean = (queue match {
+      case Queue(Nil(), Nil()) => true
+      case _ => false
+  }) ensuring(res => (res == (q2l(queue) == Nil())))
+
+  def enqueue(queue : AbsQueue, elem : Int) : AbsQueue = (queue match {
+    case Queue(front, rear) => amortizedQueue(front, Cons(elem, rear))
+  }) ensuring(res => isAmortized(res) && q2l(res) == concat(q2l(queue), Cons(elem, Nil())))
+    // this did not find a counterexample:
+    // ensuring(res => isAmortized(res) && q2l(res) == Cons(elem, q2l(queue)))
+
+  def push(queue : AbsQueue, elem : Int) : AbsQueue = (queue match {
+    case Queue(front, rear) => amortizedQueue(Cons(elem,front), rear)
+  }) ensuring(res => isAmortized(res) && q2l(res) == Cons(elem, q2l(queue)))
+
+
+ // I did not know why this does not type check
+  def matchQ(queue : AbsQueue) : (Int, AbsQueue) = ({
+    require(isAmortized(queue) && !isEmpty(queue))
+    queue match {
+      case Queue(Cons(f, fs), rear) => (f, amortizedQueue(fs, rear))
+    }
+  }) ensuring(res => {
+    val (f,q) = res
+    q2l(queue) == Cons(f, q2l(q))
+  })
+
+  def tail(queue : AbsQueue) : AbsQueue = ({
+    require(isAmortized(queue) && !isEmpty(queue))
+    queue match {
+      case Queue(Cons(f, fs), rear) => amortizedQueue(fs, rear)
+    }
+  }) ensuring(res => isAmortized(res) && (q2l(queue) match { 
+    case Nil() => false
+    case Cons(_,xs) => q2l(res)==xs
+  }))
+
+  def front(queue : AbsQueue) : Int = ({
+    require(isAmortized(queue) && !isEmpty(queue))
+    queue match {
+      case Queue(Cons(f, _), _) => f
+    }
+  }) ensuring(res => q2l(queue) match { 
+    case Nil() => false
+    case Cons(x,_) => x==res
+  })
+
+  // @induct
+  // def propEnqueue(rear : List, front : List, list : List, elem : Int) : Boolean = {
+  //   require(isAmortized(Queue(front, rear)))
+  //   val queue = Queue(front, rear)
+  //   if (q2l(queue) == list) {
+  //     q2l(enqueue(queue, elem)) == concat(list, Cons(elem, Nil()))
+  //   } else
+  //     true
+  // } holds
+
+  @induct
+  def propFront(queue : AbsQueue, list : List, elem : Int) : Boolean = {
+    require(!isEmpty(queue) && isAmortized(queue))
+    if (q2l(queue) == list) {
+      list match {
+        case Cons(x, _) => front(queue) == x
+      }
+    } else
+      true
+  } holds
+
+  @induct
+  def propTail(rear : List, front : List, list : List, elem : Int) : Boolean = {
+    require(!isEmpty(Queue(front, rear)) && isAmortized(Queue(front, rear)))
+    if (q2l(Queue(front, rear)) == list) {
+      list match {
+        case Cons(_, xs) => q2l(tail(Queue(front, rear))) == xs
+      }
+    } else
+      true
+  } // holds
+
+  def enqueueAndFront(queue : AbsQueue, elem : Int) : Boolean = {
+    if (isEmpty(queue))
+      front(enqueue(queue, elem)) == elem
+    else
+      true
+  } holds
+
+  def enqueueDequeueThrice(queue : AbsQueue, e1 : Int, e2 : Int, e3 : Int) : Boolean = {
+    if (isEmpty(queue)) {
+      val q1 = enqueue(queue, e1)
+      val q2 = enqueue(q1, e2)
+      val q3 = enqueue(q2, e3)
+      val e1prime = front(q3)
+      val q4 = tail(q3)
+      val e2prime = front(q4)
+      val q5 = tail(q4)
+      val e3prime = front(q5)
+      e1 == e1prime && e2 == e2prime && e3 == e3prime
+    } else
+      true
+  } holds
+}

testcases/TreeListSetNoDup.scala

+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+  // list of integers
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case class Nil() extends List
+
+  // set of elements from l
+  def l2s(l: List): Set[Int] = l match {
+    case Nil() => Set()
+    case Cons(i, t) => Set(i) ++ l2s(t)
+  }
+
+  // list of t, in order, in from of l0
+  def seqWith(t:Tree,l0:List) : List = (t match {
+    case Leaf() => l0
+    case Node(l, v, r) => seqWith(l,Cons(v,seqWith(r,l0)))
+  }) ensuring (res => l2s(res) == t2s(t) ++ l2s(l0))
+
+  // list of tree t
+  def t2l(t:Tree) : List = seqWith(t,Nil())
+
+  // l has no duplicates, nor elements from s
+  def noDupWith(l:List,s:Set[Int]) : Boolean = l match {
+    case Nil() => true
+    case Cons(h,l1) => !s.contains(h) && noDupWith(l1,Set(h) ++ s)
+  }
+
+  // l has no duplicates
+  def noDup(l:List): Boolean = noDupWith(l,Set.empty[Int])
+
+  // removing duplicates from l1 gives l2
+  def removeDupGives(l1:List,l2:List) : Boolean = 
+    l2s(l1)==l2s(l2) && noDup(l2)
+
+  def removeDupAnd(l:List,s0:Set[Int]) : List = (l match {
+    case Nil() => Nil()
+    case Cons(h,l1) => {
+      if (s0.contains(h)) removeDupAnd(l1,s0)
+      else Cons(h,removeDupAnd(l1,Set(h)++s0))
+    }
+  }) ensuring (res => noDupWith(res,s0) && l2s(l) ++ s0 == l2s(res) ++ s0)
+
+  def removeDup(l:List) : List = ({
+    removeDupAnd(l,Set.empty[Int])
+  }) ensuring (res => removeDupGives(l,res))
+
+  def revRemoveDupAnd(l:List,s0:Set[Int],l0:List) : List = ({
+    require(l2s(l0).subsetOf(s0) && noDup(l0))
+    l match {
+      case Nil() => l0
+      case Cons(h,l1) => {
+	if (s0.contains(h)) revRemoveDupAnd(l1,s0,l0)
+	else revRemoveDupAnd(l1,Set(h)++s0,Cons(h,l0))
+      }
+    }
+  }) ensuring (res => noDupWith(res,s0) && l2s(l) ++l2s(l0) ++ s0 == l2s(res) ++ s0)
+
+  def revRemoveDup(l:List) : List = ({
+    revRemoveDupAnd(
+      revRemoveDupAnd(l,Set.empty[Int],Nil()),
+      Set.empty[Int],Nil())
+  }) ensuring (res => removeDupGives(l,res))
+
+  // tree of integers
+  sealed abstract class Tree
+  case class Node(left : Tree, value : Int, right : Tree) extends Tree
+  case class Leaf() extends Tree
+
+  // set of elements from t
+  def t2s(t : Tree): Set[Int] = t match {
+    case Leaf() => Set.empty[Int]
+    case Node(l, v, r) => t2s(l) ++ Set(v) ++ t2s(r)
+  }
+
+  // list of elements of t, in order, without duplicates, in front of l0
+  def seqNoDup(t:Tree,l0:List,s0:Set[Int]) : (List,Set[Int]) = ({
+    require(l2s(l0).subsetOf(s0) && noDup(l0))
+    t match {
+      case Leaf() => (l0,s0)
+      case Node(l, v, r) => {
+	val (rl,rs) = seqNoDup(r,l0,s0)
+	val (l1,s1) = if (rs.contains(v)) (rl,rs) else (Cons(v,rl),Set(v)++rs)
+	seqNoDup(l,l1,s1)
+      }
+    }
+  }) ensuring (res => {
+    val (lres,sres) = res
+    l2s(lres).subsetOf(sres) &&
+    removeDupGives(t2l(t), lres)
+  })
+
+  // list of elements of t, without duplicates
+  def t2lNoDup(t:Tree) : List = ({
+    seqNoDup(t,Nil(),Set.empty[Int])._1
+  }) ensuring (res => removeDupGives(t2l(t), res))
+}

testcases/synthesis/cav2013/AVLTree.scala

+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object AVLTree {
+  sealed abstract class Tree
+  case class Node(left : Tree, value : Int, right : Tree) extends Tree
+  case class Leaf() extends Tree
+
+  def content(t : Tree): Set[Int] = t match {
+    case Leaf() => Set.empty[Int]
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def height(t: Tree): Int = t match {
+    case Leaf() => 0
+    case Node(l, _, r) =>
+      val lh = height(l)
+      val rh = height(r)
+      if (rh > lh) {
+        rh+1
+      } else {
+        lh+1
+      }
+  }
+
+  def isSortedMinMax(t: Tree, min: Int, max: Int): Boolean = t match {
+    case Node(l, v, r) =>
+      isSortedMinMax(l, min, v) &&
+      isSortedMinMax(r, v, max) &&
+      v < max && v > min
+    case _ => true
+  }
+
+  def isSortedMin(t: Tree, min: Int): Boolean = t match {
+    case Node(l, v, r) =>
+      isSortedMinMax(l, min, v) &&
+      isSortedMin(r, v) &&
+      v > min
+    case _ => true
+  }
+
+  def isSortedMax(t: Tree, max: Int): Boolean = t match {
+    case Node(l, v, r) =>
+      isSortedMax(l, v) &&
+      isSortedMinMax(r, v, max) &&
+      v < max
+    case _ => true
+  }
+
+  def isBalanced(t: Tree): Boolean = t match {
+    case Node(l, v, r) =>
+      val diff = height(l)-height(r)
+
+      !(diff > 1 || diff < -1) && isBalanced(l) && isBalanced(r)
+    case Leaf() =>
+      true
+  }
+
+  def isSorted(t: Tree): Boolean = t match {
+    case Node(l, v, r) =>
+      isSortedMin(r, v) &&
+      isSortedMax(l, v)
+    case _ => true
+  }
+
+  def deleteSynth(in : Tree, v : Int) = choose {
+    (out : Tree) => content(out) == (content(in) -- Set(v))
+  }
+
+  def insertSynth(in : Tree, v : Int) = choose {
+    (out : Tree) => content(out) == (content(in) ++ Set(v))
+  }
+
+  def insertBalancedSynth(in: Tree, v: Int) = choose {
+    (out : Tree) => isBalanced(in) && (content(out) == (content(in) ++ Set(v))) && isBalanced(out)
+  }
+
+  def insertSortedSynth(in : Tree, v : Int) = choose {
+    (out : Tree) => isSorted(in) && (content(out) == (content(in) ++ Set(v))) && isSorted(out)
+  }
+
+  def deleteSortedSynth(in : Tree, v : Int) = choose {
+    (out : Tree) => isSorted(in) && (content(out) == (content(in) -- Set(v))) && isSorted(out)
+  }
+
+  def deleteBalancedSynth(in: Tree, v: Int) = choose {
+    (out : Tree) => isBalanced(in) && (content(out) == (content(in) -- Set(v))) && isBalanced(out)
+  }
+}

testcases/synthesis/cav2013/BinaryTree.scala

+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+  sealed abstract class Tree
+  case class Node(left : Tree, value : Int, right : Tree) extends Tree
+  case class Leaf() extends Tree
+
+  def content(t : Tree): Set[Int] = t match {
+    case Leaf() => Set.empty[Int]
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def isSortedMinMax(t: Tree, min: Int, max: Int): Boolean = t match {
+    case Node(l, v, r) =>
+      isSortedMinMax(l, min, v) &&
+      isSortedMinMax(r, v, max) &&
+      v < max && v > min
+    case _ => true
+  }
+
+  def isSortedMin(t: Tree, min: Int): Boolean = t match {
+    case Node(l, v, r) =>
+      isSortedMinMax(l, min, v) &&
+      isSortedMin(r, v) &&
+      v > min
+    case _ => true
+  }
+
+  def isSortedMax(t: Tree, max: Int): Boolean = t match {
+    case Node(l, v, r) =>
+      isSortedMax(l, v) &&
+      isSortedMinMax(r, v, max) &&
+      v < max
+    case _ => true
+  }
+
+  def isSorted(t: Tree): Boolean = t match {
+    case Node(l, v, r) =>
+      isSortedMin(r, v) &&
+      isSortedMax(l, v)
+    case _ => true
+  }
+
+  def deleteSynth(in : Tree, v : Int) = choose {
+    (out : Tree) => content(out) == (content(in) -- Set(v))
+  }
+
+  def insertSynth(in : Tree, v : Int) = choose {
+    (out : Tree) => content(out) == (content(in) ++ Set(v))
+  }
+
+  def insertSortedSynth(in : Tree, v : Int) = choose {
+    (out : Tree) => isSorted(in) && (content(out) == (content(in) ++ Set(v))) && isSorted(out)
+  }
+
+  def deleteSortedSynth(in : Tree, v : Int) = choose {
+    (out : Tree) => isSorted(in) && (content(out) == (content(in) -- Set(v))) && isSorted(out)
+  }
+}

testcases/synthesis/cav2013/List.scala

+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object List {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case class Nil() extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil() => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil() => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def isSorted(l: List): Boolean = l match {
+    case Nil() => true
+    case Cons(x, Nil()) => true
+    case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
+  }
+
+  def isStrictSorted(l: List): Boolean = l match {
+    case Nil() => true
+    case Cons(x, Nil()) => true
+    case Cons(x, Cons(y, ys)) => x < y && isSorted(Cons(y, ys))
+  }
+
+  def deleteSynth(in: List, v: Int) = choose {
+    (out: List) => (content(out) == (content(in) -- Set(v)))
+  }
+
+  def deleteSortedSynth(in: List, v: Int) = choose {
+    (out: List) => isSorted(in) && (content(out) == (content(in) -- Set(v))) && isSorted(out)
+  }
+
+  def insertSynth(in: List, v: Int) = choose {
+    (out: List) => (content(out) == (content(in) ++ Set(v)))
+  }
+
+  def insertSortedSynth(in: List, v: Int) = choose {
+    (out: List) => isSorted(in) && (content(out) == (content(in) ++ Set(v))) && isSorted(out)
+  }
+
+  def insertStrictSortedSynth(in: List, v: Int) = choose {
+    (out: List) => isStrictSorted(in) && (content(out) == (content(in) ++ Set(v))) && isStrictSorted(out)
+  }
+
+  def concatSynth(in1: List, in2: List) = choose {
+    (out : List) => content(out) == content(in1) ++ content(in2)
+  }
+
+  def mergeSynth(in1: List, in2: List) = choose {
+    (out : List) => isSorted(in1) && isSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+  }
+
+  def mergeStrictSynth(in1: List, in2: List) = choose {
+    (out : List) => isStrictSorted(in1) && isStrictSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isStrictSorted(out)
+  }
+
+}