Merge pull request #1 from psuter/viktor/benchmark-updates

Updates on benchmarks from Viktor

testcases/SimpInterpret.scala

+//import scala.collection.immutable.Set
+//import leon.Annotations._
+import leon.Utils._
+
+object Interpret {
+  abstract class BoolTree 
+  case class Eq(t1 : IntTree, t2 : IntTree) extends BoolTree
+  case class And(t1 : BoolTree, t2 : BoolTree) extends BoolTree
+  case class Not(t : BoolTree) extends BoolTree
+
+  abstract class IntTree 
+  case class Const(c:Int) extends IntTree
+  case class Var() extends IntTree
+  case class Plus(t1 : IntTree, t2 : IntTree) extends IntTree
+  case class Minus(t1 : IntTree, t2 : IntTree) extends IntTree
+  case class Less(t1 : IntTree, t2 : IntTree) extends BoolTree
+  case class If(cond : BoolTree, t : IntTree, e : IntTree) extends IntTree
+
+  def repOk(t : IntTree) : Boolean = {
+    true
+  }
+
+  def beval(t:BoolTree, x0 : Int) : Boolean = {
+    t match {   
+      case Less(t1, t2) => ieval(t1,x0) < ieval(t2,x0)
+      case Eq(t1, t2) => ieval(t1,x0) == ieval(t2,x0)
+      case And(t1, t2) => beval(t1,x0) && beval(t2,x0)
+      case Not(t1) => !beval(t1,x0)
+    }
+  }
+
+  def ieval(t:IntTree, x0 : Int) : Int = {
+    t match {
+      case Const(c) => c
+      case Var() => x0
+      case Plus(t1,t2) => ieval(t1,x0) + ieval(t2,x0)
+      case Minus(t1, t2) => ieval(t1,x0) - ieval(t2,x0)
+      case If(c,t1,t2) => if (beval(c,x0)) ieval(t1,x0) else ieval(t2,x0)
+    }
+  }
+  def computesPositive(t : IntTree) : Boolean = {
+    ieval(t,0) >= 0 &&
+    ieval(t,1) >= 0 &&
+    ieval(t,-1) >= 0 &&
+    ieval(t,-2) >= 0 &&
+    ieval(t,2) >= 0
+  }
+  def identityForPositive(t : IntTree) : Boolean = {
+    ieval(t, 5) == 5 &&
+    ieval(t, 33) == 33 &&
+    ieval(t, 0) == 0 &&
+    ieval(t, -1) == 1 &&
+    ieval(t, -2) == 2
+  }
+
+  def treeBad(t : IntTree) : Boolean = {
+    !(repOk(t) && computesPositive(t) && identityForPositive(t))
+  } holds
+
+  def thereIsGoodTree() : Boolean = {
+    !treeBad(If(Less(Const(0),Var()), Var(), Minus(Const(0),Var())))
+  } holds
+
+  def main(args : Array[String]) {
+    thereIsGoodTree()
+  }
+}

testcases/synthesis/cav2013/ListByExample.scala

+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Lists {
+  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(h,t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def listUp(a:Int,b:Int) : List = {
+    require(a <= b)
+    if (a == b) Cons(a,Nil())
+    else Cons(a, listUp(a+1,b))
+  } ensuring (res => size(res)==1+b-a)
+
+  def listUp_syn(a:Int,b:Int) : List = {
+    require(a <= b)
+    choose((res:List) => 
+    size(res)==1+b-a &&
+    (!(a==5 && b==9) || res==Cons(5,Cons(6,Cons(7,Cons(8,Cons(9,Nil())))))) &&
+    (!(a==100 && b==105) || 
+      res==Cons(100,Cons(101,Cons(102,Cons(103,Cons(104,Cons(105,Nil())))))))
+	 )
+  }
+
+  def listDown(a:Int,b:Int) : List = {
+    require(a >= b)
+    if (a == b) Cons(a,Nil())
+    else Cons(a, listUp(a-1,b))
+  } ensuring (res => size(res)==1+b-a)
+
+  def listDown_syn(a:Int,b:Int) : List = {
+    require(a >= b)
+    choose((res:List) => 
+    size(res)==1+b-a &&
+    (!(a==9 && b==5) || res==Cons(9,Cons(8,Cons(7,Cons(6,Cons(5,Nil())))))) &&
+    (!(a==105 && b==100) || 
+      res==Cons(105,Cons(104,Cons(103,Cons(102,Cons(101,Cons(100,Nil())))))))
+	 )
+  }
+
+  def concat_syn(a:List, b:List) : List = {
+    choose((res:List) =>
+      size(res) == size(a) + size(b) &&
+      (!(a==listUp(1,5) && b==listUp(6,9)) || 
+         res==listUp(1,9)) &&
+      (!(a==listUp(101,105) && b==listUp(106,109)) || 
+         res==listUp(101,109)) &&
+      (!(a==listUp(201,205) && b==listUp(206,209)) || 
+         res==listUp(201,209)) &&
+      (!(a==listUp(301,304) && b==listUp(304,310)) || 
+         res==listUp(301,310))
+     )
+  }
+
+}

testcases/synthesis/cav2013/SynTreeListSet.scala

@@ -30,15 +30,28 @@ object BinaryTree {
       case Cons(i, t) => Set(i) ++ l2s(t)
   }
 
-  def l2s_syn(l:List):Set[Int] = {
+  def listFrom(k:Int) : List = {
+    require(0 <= k)
+    if (k==0) Nil()
+    else Cons(k, listFrom(k-1))
+  }
+  def setFrom(k:Int) : Set[Int] = {
+    require(0 <= k)
+    if (k==0) Set.empty[Int]
+    else Set(k) ++ setFrom(k-1)
+  }
+
+  def l2s_syn(l:List,k:Int):Set[Int] = {
+    require(0 <= k)
     choose((res:Set[Int]) =>
-      l match {
+      (l!=listFrom(k) || res==setFrom(k)) &&
+      (l match {
 	case Nil() => (res==Set.empty[Int])
 	case Cons(x,Nil()) => res==Set(x)
 	case Cons(x,Cons(y,Nil())) => res==Set(x,y)
 	case Cons(x1,Cons(x2,Cons(x3,Cons(x4,Nil())))) => res==Set(x1,x2,x3,x4)
 	case _ => true
-      }
+      })
    )
   }