Add current benchmarks, new benchmark List[T].indexOfOpt with variants

testcases/synthesis/current/AddressBook/Make.scala

+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object AddressBookMake {
+
+  case class Address[A](info: A, priv: Boolean)
+
+  sealed abstract class AddressList[A] {
+    def size: BigInt = {
+      this match {
+        case Nil() => BigInt(0)
+        case Cons(head, tail) => BigInt(1) + tail.size
+      }
+    } ensuring { res => res >= 0 }
+
+    def content: Set[Address[A]] = this match {
+      case Nil() => Set[Address[A]]()
+      case Cons(addr, l1) => Set(addr) ++ l1.content
+    }
+  }
+
+  case class Cons[A](a: Address[A], tail: AddressList[A]) extends AddressList[A]
+  case class Nil[A]() extends AddressList[A]
+
+  def allPersonal[A](l: AddressList[A]): Boolean = l match {
+    case Nil() => true
+    case Cons(a, l1) =>
+      if (a.priv) allPersonal(l1)
+      else false
+  }
+
+  def allBusiness[A](l: AddressList[A]): Boolean = l match {
+    case Nil() => true
+    case Cons(a, l1) =>
+      if (a.priv) false
+      else allBusiness(l1)
+  }
+
+  case class AddressBook[A](business: AddressList[A], personal: AddressList[A]) {
+    def size: BigInt = business.size + personal.size
+
+    def content: Set[Address[A]] = business.content ++ personal.content
+
+    def invariant = {
+      allPersonal(personal) && allBusiness(business)
+    }
+  }
+
+  def makeAddressBook[A](as: AddressList[A]): AddressBook[A] = {
+    choose( (res: AddressBook[A]) => res.content == as.content && res.invariant )
+
+ /*   as match {
+      case Nil() => AddressBook[A](Nil[A](), Nil[A]())
+      case Cons(x, xs) =>
+        val AddressBook(b, p) = makeAddressBook(xs)
+        if(x.priv) AddressBook(b, Cons(x, p))
+        else AddressBook(Cons(x, b), p)
+    }
+
+  } ensuring { 
+    res => res.content == as.content && res.invariant */
+  }
+
+
+}

testcases/synthesis/current/AddressBook/Merge.scala

+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object AddressBookMake {
+
+  case class Address[A](info: A, priv: Boolean)
+
+  sealed abstract class AddressList[A] {
+    def size: BigInt = {
+      this match {
+        case Nil() => BigInt(0)
+        case Cons(head, tail) => BigInt(1) + tail.size
+      }
+    } ensuring { res => res >= 0 }
+
+    def content: Set[Address[A]] = this match {
+      case Nil() => Set[Address[A]]()
+      case Cons(addr, l1) => Set(addr) ++ l1.content
+    }
+
+    def ++(that: AddressList[A]): AddressList[A] = {
+      this match {
+        case Cons(h, t) => Cons(h, t ++ that)
+        case Nil() => that
+      }
+    } ensuring {
+      res => res.content == this.content ++ that.content
+    }
+  }
+
+  case class Cons[A](a: Address[A], tail: AddressList[A]) extends AddressList[A]
+  case class Nil[A]() extends AddressList[A]
+
+  def allPersonal[A](l: AddressList[A]): Boolean = l match {
+    case Nil() => true
+    case Cons(a, l1) =>
+      if (a.priv) allPersonal(l1)
+      else false
+  }
+
+  def allBusiness[A](l: AddressList[A]): Boolean = l match {
+    case Nil() => true
+    case Cons(a, l1) =>
+      if (a.priv) false
+      else allBusiness(l1)
+  }
+
+  case class AddressBook[A](business: AddressList[A], personal: AddressList[A]) {
+    def size: BigInt = business.size + personal.size
+
+    def content: Set[Address[A]] = business.content ++ personal.content
+
+    @inline
+    def invariant = {
+      allPersonal(personal) && allBusiness(business)
+    }
+  }
+
+  def merge[A](a1: AddressBook[A], a2: AddressBook[A]): AddressBook[A] = {
+    require(a1.invariant && a2.invariant)
+
+    choose( (res: AddressBook[A]) =>
+      res.personal.content == (a1.personal.content ++ a2.personal.content) &&
+      res.business.content == (a1.business.content ++ a2.business.content) &&
+      res.invariant
+    )
+  }
+}

testcases/synthesis/current/BatchedQueue/Dequeue.scala

+import leon.lang._
+import leon.lang.synthesis._
+
+object BatchedQueue {
+  sealed abstract class List[T] {
+    def content: Set[T] = {
+      this match {
+        case Cons(h, t) => Set(h) ++ t.content
+        case Nil() => Set()
+      }
+    }
+
+    def size: BigInt = {
+      this match {
+        case Cons(h, t) => BigInt(1) + t.size
+        case Nil() => BigInt(0)
+      }
+    } ensuring { _ >= 0 }
+
+    def reverse: List[T] = {
+      this match {
+        case Cons(h, t) => t.reverse.append(Cons(h, Nil[T]()))
+        case Nil() => Nil[T]()
+      }
+    } ensuring { res =>
+      this.content == res.content
+    }
+
+    def append(r: List[T]): List[T] = {
+      this match {
+        case Cons(h, t) => Cons(h, t.append(r))
+        case Nil() => r
+      }
+    }
+
+    def isEmpty: Boolean = {
+      this == Nil[T]()
+    }
+
+    def tail: List[T] = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, t) => t
+      }
+    }
+
+    def head: T = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, t) => h
+      }
+    }
+  }
+
+  case class Cons[T](h: T, t: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+  case class Queue[T](f: List[T], r: List[T]) {
+    def content: Set[T] = f.content ++ r.content
+    def size: BigInt = f.size + r.size
+
+    def isEmpty: Boolean = f.isEmpty && r.isEmpty
+
+    def invariant: Boolean = {
+      (f.isEmpty) ==> (r.isEmpty)
+    }
+
+    def toList: List[T] = f.append(r.reverse)
+
+    def dequeue: Queue[T] = {
+      require(invariant && !isEmpty)
+
+      choose { (res: Queue[T]) =>
+        res.size == size-1 && res.toList == this.toList.tail && res.invariant
+      }
+    }
+  }
+
+  val test = Queue[BigInt](Cons(42, Nil()), Nil()).dequeue
+}

testcases/synthesis/current/BatchedQueue/Enqueue.scala

+import leon.lang._
+import leon.lang.synthesis._
+
+object BatchedQueue {
+  sealed abstract class List[T] {
+    def content: Set[T] = {
+      this match {
+        case Cons(h, t) => Set(h) ++ t.content
+        case Nil() => Set()
+      }
+    }
+
+    def size: BigInt = {
+      this match {
+        case Cons(h, t) => BigInt(1) + t.size
+        case Nil() => BigInt(0)
+      }
+    } ensuring { _ >= 0 }
+
+    def reverse: List[T] = {
+      this match {
+        case Cons(h, t) => t.reverse.append(Cons(h, Nil[T]()))
+        case Nil() => Nil[T]()
+      }
+    } ensuring { res =>
+      this.content == res.content
+    }
+
+    def append(r: List[T]): List[T] = {
+      this match {
+        case Cons(h, t) => Cons(h, t.append(r))
+        case Nil() => r
+      }
+    }
+
+    def tail: List[T] = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, t) => t
+      }
+    }
+
+    def head: T = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, t) => h
+      }
+    }
+
+    def last: T = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, Nil()) => h
+        case Cons(h, t) => t.last
+      }
+    }
+  }
+
+  case class Cons[T](h: T, t: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+  case class Queue[T](f: List[T], r: List[T]) {
+    def content: Set[T] = f.content ++ r.content
+    def size: BigInt = f.size + r.size
+
+    def invariant: Boolean = {
+      (f == Nil[T]()) ==> (r == Nil[T]())
+    }
+
+    def toList: List[T] = f.append(r.reverse)
+
+    def enqueue(v: T): Queue[T] = {
+      require(invariant)
+
+      ???[Queue[T]]
+    } ensuring { (res: Queue[T]) =>
+      res.invariant &&
+      res.toList.last == v &&
+      res.size == size + 1 &&
+      res.content == this.content ++ Set(v)
+    }
+  }
+}

testcases/synthesis/current/Compiler/Desugar.scala

+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+  abstract class Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr
+  case class UMinus(e: Expr) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class And(lhs: Expr, rhs: Expr) extends Expr
+  case class Implies(lhs: Expr, rhs: Expr) extends Expr
+  case class Or(lhs: Expr, rhs: Expr) extends Expr
+  case class Not(e : Expr) extends Expr
+  case class Eq(lhs: Expr, rhs: Expr) extends Expr
+  case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+  case class BoolLiteral(b : Boolean) extends Expr
+  case class IntLiteral(i: BigInt) extends Expr
+
+  abstract class Value
+  case class BoolValue(b: Boolean) extends Value
+  case class IntValue(i: BigInt) extends Value
+  case object Error extends Value
+
+  def eval(e: Expr): Value = e match {
+    case Plus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+        case _ => Error
+      }
+
+    case Minus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+        case _ => Error
+      }
+
+    case UMinus(l) =>
+      eval(l) match {
+        case IntValue(b) => IntValue(-b)
+        case _ => Error
+      }
+
+    case LessThan(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+        case _ => Error
+      }
+
+    case And(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(false) => b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Or(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Implies(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          eval(r)
+        case b @ BoolValue(false) =>
+          BoolValue(true)
+        case _ => Error
+      }
+
+    case Not(l) =>
+      eval(l) match {
+        case BoolValue(b) => BoolValue(!b)
+        case _ => Error
+      }
+
+    case Eq(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir))   => BoolValue(il == ir)
+        case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+        case _ => Error
+      }
+
+    case Ite(c, t, e) =>
+      eval(c) match {
+        case BoolValue(true) => eval(t)
+        case BoolValue(false) => eval(t)
+        case _ => Error
+      }
+
+    case IntLiteral(l)  => IntValue(l)
+    case BoolLiteral(b) => BoolValue(b)
+  }
+
+  def rewriteMinus(in: Minus): Expr = {
+    choose{ (out: Expr) =>
+      eval(in) == eval(out) && !(out.isInstanceOf[Minus])
+    }
+  }
+
+  def rewriteImplies(in: Implies): Expr = {
+    choose{ (out: Expr) =>
+      eval(in) == eval(out) && !(out.isInstanceOf[Implies])
+    }
+  }
+
+
+  def plop(x: Expr) = {
+    eval(x) == Error//eval(Not(IntLiteral(BigInt(2))))
+  }.holds
+}

testcases/synthesis/current/Compiler/DesugarImplies.scala

+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+  abstract class Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr
+  case class UMinus(e: Expr) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class And(lhs: Expr, rhs: Expr) extends Expr
+  case class Implies(lhs: Expr, rhs: Expr) extends Expr
+  case class Or(lhs: Expr, rhs: Expr) extends Expr
+  case class Not(e : Expr) extends Expr
+  case class Eq(lhs: Expr, rhs: Expr) extends Expr
+  case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+  case class BoolLiteral(b : Boolean) extends Expr
+  case class IntLiteral(i: BigInt) extends Expr
+
+  def exists(e: Expr, f: Expr => Boolean): Boolean = {
+    f(e) || (e match {
+      case Plus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Minus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case LessThan(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case And(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Or(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Implies(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Eq(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Ite(c, t, e) => exists(c, f) || exists(t, f) || exists(e, f)
+      case Not(e) => exists(e, f)
+      case UMinus(e) => exists(e, f)
+      case _ => false
+    })
+  }
+
+  abstract class Value
+  case class BoolValue(b: Boolean) extends Value
+  case class IntValue(i: BigInt) extends Value
+  case object Error extends Value
+
+  def eval(e: Expr): Value = e match {
+    case Plus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+        case _ => Error
+      }
+
+    case Minus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+        case _ => Error
+      }
+
+    case UMinus(l) =>
+      eval(l) match {
+        case IntValue(b) => IntValue(-b)
+        case _ => Error
+      }
+
+    case LessThan(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+        case _ => Error
+      }
+
+    case And(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(false) => b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Or(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Implies(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          eval(r)
+        case b @ BoolValue(false) =>
+          BoolValue(true)
+        case _ => Error
+      }
+
+    case Not(l) =>
+      eval(l) match {
+        case BoolValue(b) => BoolValue(!b)
+        case _ => Error
+      }
+
+    case Eq(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir))   => BoolValue(il == ir)
+        case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+        case _ => Error
+      }
+
+    case Ite(c, t, e) =>
+      eval(c) match {
+        case BoolValue(true) => eval(t)
+        case BoolValue(false) => eval(t)
+        case _ => Error
+      }
+
+    case IntLiteral(l)  => IntValue(l)
+    case BoolLiteral(b) => BoolValue(b)
+  }
+
+
+  //def desugar(e: Expr): Expr = {
+  //  choose{ (out: Expr) =>
+  //    eval(e) == eval(out) && !exists(out, f => f.isInstanceOf[Implies])
+  //  }
+  //}
+
+  def desugar(e: Expr): Expr = {
+    e match {
+      case Plus(lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+      case Minus(lhs, rhs) => Minus(desugar(lhs), desugar(rhs))
+      case LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+      case And(lhs, rhs) => And(desugar(lhs), desugar(rhs))
+      case Or(lhs, rhs) => Or(desugar(lhs), desugar(rhs))
+      case Implies(lhs, rhs) => //Implies(desugar(lhs), desugar(rhs))
+        Or(Not(desugar(lhs)), desugar(rhs))
+      case Eq(lhs, rhs) => Eq(desugar(lhs), desugar(rhs))
+      case Ite(c, t, e) => Ite(desugar(c), desugar(t), desugar(e))
+      case Not(e) => Not(desugar(e))
+      case UMinus(e) => UMinus(desugar(e))
+      case e => e
+    }
+  } ensuring { out =>
+    //eval(e) == eval(out) && 
+    !exists(out, f => f.isInstanceOf[Implies])
+  }
+}

testcases/synthesis/current/Compiler/RewriteImplies.scala

+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+  abstract class Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr
+  case class UMinus(e: Expr) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class And(lhs: Expr, rhs: Expr) extends Expr
+  case class Implies(lhs: Expr, rhs: Expr) extends Expr
+  case class Or(lhs: Expr, rhs: Expr) extends Expr
+  case class Not(e : Expr) extends Expr
+  case class Eq(lhs: Expr, rhs: Expr) extends Expr
+  case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+  case class BoolLiteral(b : Boolean) extends Expr
+  case class IntLiteral(i: BigInt) extends Expr
+
+  def exists(e: Expr, f: Expr => Boolean): Boolean = {
+    f(e) || (e match {
+      case Plus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Minus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case LessThan(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case And(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Or(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Implies(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Eq(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Ite(c, t, e) => exists(c, f) || exists(t, f) || exists(e, f)
+      case Not(e) => exists(e, f)
+      case UMinus(e) => exists(e, f)
+      case _ => false
+    })
+  }
+
+  abstract class Value
+  case class BoolValue(b: Boolean) extends Value
+  case class IntValue(i: BigInt) extends Value
+  case object Error extends Value
+
+  def eval(e: Expr): Value = e match {
+    case Plus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+        case _ => Error
+      }
+
+    case Minus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+        case _ => Error
+      }
+
+    case UMinus(l) =>
+      eval(l) match {
+        case IntValue(b) => IntValue(-b)
+        case _ => Error
+      }
+
+    case LessThan(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+        case _ => Error
+      }
+
+    case And(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(false) => b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Or(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Implies(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          eval(r)
+        case b @ BoolValue(false) =>
+          BoolValue(true)
+        case _ => Error
+      }
+
+    case Not(l) =>
+      eval(l) match {
+        case BoolValue(b) => BoolValue(!b)
+        case _ => Error
+      }
+
+    case Eq(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir))   => BoolValue(il == ir)
+        case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+        case _ => Error
+      }
+
+    case Ite(c, t, e) =>
+      eval(c) match {
+        case BoolValue(true) => eval(t)
+        case BoolValue(false) => eval(t)
+        case _ => Error
+      }
+
+    case IntLiteral(l)  => IntValue(l)
+    case BoolLiteral(b) => BoolValue(b)
+  }
+
+
+  def desugar(in: Expr): Expr = {
+    choose{ (out: Expr) =>
+      eval(in) == eval(out) && !(out.isInstanceOf[Implies])
+    }
+  }
+}

testcases/synthesis/current/Compiler/RewriteMinus.scala

+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+  abstract class Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr
+  case class UMinus(e: Expr) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class And(lhs: Expr, rhs: Expr) extends Expr
+  case class Implies(lhs: Expr, rhs: Expr) extends Expr
+  case class Or(lhs: Expr, rhs: Expr) extends Expr
+  case class Not(e : Expr) extends Expr
+  case class Eq(lhs: Expr, rhs: Expr) extends Expr
+  case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+  case class BoolLiteral(b : Boolean) extends Expr
+  case class IntLiteral(i: BigInt) extends Expr
+
+  abstract class Value
+  case class BoolValue(b: Boolean) extends Value
+  case class IntValue(i: BigInt) extends Value
+  case object Error extends Value
+
+  def eval(e: Expr): Value = e match {
+    case Plus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+        case _ => Error
+      }
+
+    case Minus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+        case _ => Error
+      }
+
+    case UMinus(l) =>
+      eval(l) match {
+        case IntValue(b) => IntValue(-b)
+        case _ => Error
+      }
+
+    case LessThan(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+        case _ => Error
+      }
+
+    case And(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(false) => b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Or(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Implies(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          eval(r)
+        case b @ BoolValue(false) =>
+          BoolValue(true)
+        case _ => Error
+      }
+
+    case Not(l) =>
+      eval(l) match {
+        case BoolValue(b) => BoolValue(!b)
+        case _ => Error
+      }
+
+    case Eq(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir))   => BoolValue(il == ir)
+        case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+        case _ => Error
+      }
+
+    case Ite(c, t, e) =>
+      eval(c) match {
+        case BoolValue(true) => eval(t)
+        case BoolValue(false) => eval(t)
+        case _ => Error
+      }
+
+    case IntLiteral(l)  => IntValue(l)
+    case BoolLiteral(b) => BoolValue(b)
+  }
+
+  def rewriteMinus(in: Minus): Expr = {
+    choose{ (out: Expr) =>
+      eval(in) == eval(out) && !(out.isInstanceOf[Minus])
+    }
+  }
+}

testcases/synthesis/current/List/Delete.scala

+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Delete {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def delete(in: List, v: BigInt) = {
+    ???[List]
+  } ensuring {
+    (out : List) =>
+      content(out) == content(in) -- Set(v)
+  }
+}

testcases/synthesis/current/List/Diff.scala

+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Diff {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def insert(in1: List, v: BigInt): List = {
+    Cons(v, in1)
+  } ensuring { content(_) == content(in1) ++ Set(v) }
+
+  def delete(in1: List, v: BigInt): List = {
+    in1 match {
+      case Cons(h,t) =>
+        if (h == v) {
+          delete(t, v)
+        } else {
+          Cons(h, delete(t, v))
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { content(_) == content(in1) -- Set(v) }
+
+  // def diff(in1: List, in2: List): List = {
+  //   in2 match {
+  //     case Nil =>
+  //       in1
+  //     case Cons(h, t) =>
+  //       diff(delete(in1, h), t)
+  //   }
+  // } ensuring { content(_) == content(in1) -- content(in2) }
+
+  def diff(in1: List, in2: List) = choose {
+    (out : List) =>
+      content(out) == content(in1) -- content(in2)
+  }
+}

testcases/synthesis/current/List/IndexOfInt.scala

+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object IndexOf {
+  sealed abstract class List[T] {
+    def size: BigInt = {
+      this match {
+        case Nil() => BigInt(0)
+        case Cons(_, t) => BigInt(1) + t.size
+      }
+    } ensuring {
+      res => res >= 0
+    }
+
+    def content: Set[T] = this match {
+      case Nil() => Set.empty[T]
+      case Cons(i, t) => Set(i) ++ t.content
+    }
+
+    def apply(i: BigInt): T = {
+      require(i >= 0 && i < size)
+      this match {
+        case Cons(h, t) =>
+          if (i == 0) {
+            h
+          } else {
+            t.apply(i-1)
+          }
+      }
+    } ensuring { e =>
+      content contains e
+    }
+
+    def indexOfInt(e: T): BigInt = {
+      ???[BigInt]
+      
+      //this match {
+      //  case Cons(h, t) =>
+      //    val r = t.indexOfInt(e)
+
+      //    if (e == h) {
+      //      BigInt(0)
+      //    } else {
+      //      if (r < 0) {
+      //        r
+      //      } else {
+      //        r + 1
+      //      }
+      //    }
+      //  case Nil() =>
+      //    BigInt(-1)
+      //}
+      
+    } ensuring { res =>
+      if (res < 0) {
+        !(content contains e)
+      } else {
+        res < size && apply(res) == e
+      }
+    }
+  }
+
+  case class Cons[T](head: T, tail: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+}

testcases/synthesis/current/List/IndexOfOpt.scala

+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object IndexOf {
+  sealed abstract class List[T] {
+    def size: BigInt = {
+      this match {
+        case Nil() => BigInt(0)
+        case Cons(_, t) => BigInt(1) + t.size
+      }
+    } ensuring {
+      res => res >= 0
+    }
+
+    def content: Set[T] = this match {
+      case Nil() => Set.empty[T]
+      case Cons(i, t) => Set(i) ++ t.content
+    }
+
+    def apply(i: BigInt): T = {
+      require(i >= 0 && i < size)
+      this match {
+        case Cons(h, t) =>
+          if (i == 0) {
+            h
+          } else {
+            t.apply(i-1)
+          }
+      }
+    } ensuring { e =>
+      content contains e
+    }
+
+    def indexOfOpt(e: T): Option[BigInt] = {
+      ???[Option[BigInt]]
+      /*
+      this match {
+        case Cons(h, t) =>
+          val r = t.indexOfOpt(e)
+
+          if (e == h) {
+            Some(BigInt(0))
+          } else {
+            r match {
+              case Some(i) => Some(i+1)
+              case None() => None[BigInt]()
+            }
+          }
+        case Nil() =>
+          None[BigInt]()
+      }
+      */
+    } ensuring { res =>
+      res match {
+        case None() => !(content contains e)
+        case Some(i) => i >= 0 && i < size && apply(i) == e
+      }
+    }
+  }
+
+  case class Cons[T](head: T, tail: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+}

testcases/synthesis/current/List/IndexOfOpt2.scala

+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object IndexOf {
+  sealed abstract class List[T] {
+    def size: BigInt = {
+      this match {
+        case Nil() => BigInt(0)
+        case Cons(_, t) => BigInt(1) + t.size
+      }
+    } ensuring {
+      res => res >= 0
+    }
+
+    def content: Set[T] = this match {
+      case Nil() => Set.empty[T]
+      case Cons(i, t) => Set(i) ++ t.content
+    }
+
+    def apply(i: BigInt): T = {
+      require(i >= 0 && i < size)
+      this match {
+        case Cons(h, t) =>
+          if (i == 0) {
+            h
+          } else {
+            t.apply(i-1)
+          }
+      }
+    } ensuring { e =>
+      content contains e
+    }
+
+    def indexOfOpt(e: T, offset: BigInt): Option[BigInt] = {
+      ???[Option[BigInt]]
+      /*
+      this match {
+        case Cons(h, t) =>
+          val r = t.indexOfOpt(e)
+
+          if (e == h) {
+            Some(BigInt(0))
+          } else {
+            r match {
+              case Some(i) => Some(i+1)
+              case None() => None[BigInt]()
+            }
+          }
+        case Nil() =>
+          None[BigInt]()
+      }
+      */
+    } ensuring { res =>
+      res match {
+        case None() => !(content contains e)
+        case Some(r) =>
+          val i = r - offset;
+          i >= 0 && i < size && apply(i) == e
+      }
+    }
+  }
+
+  case class Cons[T](head: T, tail: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+}

testcases/synthesis/current/List/Insert.scala

+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Insert {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  //def insert(in1: List, v: BigInt): List = {
+  //  Cons(v, in1)
+  //} ensuring { content(_) == content(in1) ++ Set(v) }
+
+  def insert(in1: List, v: BigInt) = choose {
+    (out : List) =>
+      content(out) == content(in1) ++ Set(v)
+  }
+}

testcases/synthesis/current/List/Split.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def splitSpec(list : List, res : (List,List)) : Boolean = {
+    val s1 = size(res._1)
+    val s2 = size(res._2)
+    abs(s1 - s2) <= 1 && s1 + s2 == size(list) &&
+    content(res._1) ++ content(res._2) == content(list) 
+  }
+
+  def abs(i : BigInt) : BigInt = {
+    if(i < 0) -i else i
+  } ensuring(_ >= 0)
+
+  def split(list : List) : (List,List) = {
+    choose { (res : (List,List)) => splitSpec(list, res) }
+  }
+
+}

testcases/synthesis/current/List/Union.scala

+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Union {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1)+ size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def insert(in1: List, v: BigInt): List = {
+    Cons(v, in1)
+  } ensuring { content(_) == content(in1) ++ Set(v) }
+
+  // def union(in1: List, in2: List): List = {
+  //   in1 match {
+  //     case Cons(h, t) =>
+  //       Cons(h, union(t, in2))
+  //     case Nil =>
+  //       in2
+  //   }
+  // } ensuring { content(_) == content(in1) ++ content(in2) }
+
+  def union(in1: List, in2: List) = choose {
+    (out : List) =>
+      content(out) == content(in1) ++ content(in2)
+  }
+}

testcases/synthesis/current/Parentheses/Par.scala

+import leon.lang._
+import leon.lang.synthesis._
+import leon.collection._
+
+
+object MatchPar {
+  abstract class AbsChar
+  case object OP extends AbsChar
+  case object CP extends AbsChar
+  case object NA extends AbsChar
+
+  def matchPar(l: List[AbsChar]): BigInt = {
+
+    ???[BigInt]
+    /*
+    l match {
+      case Nil() => 0
+      case Cons(h, t) =>
+        val rec = matchPar(t)
+        h match {
+          case OP => 1 + rec
+          case CP => if (rec <= 0) {
+            -1
+          } else {
+            rec - 1
+          }
+          case NA => rec
+        }
+    }*/
+  } ensuring { res =>
+    ((count(OP, l) != count(CP, l)) ==> (res != 0)) &&
+    ((l, res) passes {
+      case Nil() => 0
+      case Cons(OP, Cons(CP, Nil())) => 0
+      case Cons(CP, Cons(OP, _))     => -1
+      case Cons(OP, Cons(OP, Nil())) => 2
+      case Cons(OP, Cons(OP, Cons(CP, Cons(CP, Cons(OP, Cons(CP, Nil())))))) => 0
+    })
+  }
+
+  def count[T](a: T, l: List[T]): BigInt = {
+    l match {
+      case Cons(h, t) =>
+        if (h == a) {
+          1 + count(a, t)
+        } else {
+          count(a, t)
+        }
+      case Nil() => BigInt(0)
+    }
+  } ensuring { (res: BigInt) =>
+    res >= 0
+  }
+}

testcases/synthesis/current/SortedList/Delete.scala

+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListDelete {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def isSorted(list: List): Boolean = list match {
+    case Nil => true
+    case Cons(_, Nil) => true
+    case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+    case Cons(_, xs) => isSorted(xs)
+  }
+
+  def delete(in: List, v: BigInt) = {
+    require(isSorted(in))
+
+    choose( (res : List) =>
+        (content(res) == content(in) -- Set(v)) && isSorted(res)
+    )
+  }
+}