diff --git a/testcases/insynth-leon-tests/Arguments.scala b/testcases/insynth-leon-tests/Arguments.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cae6e5f9e77fb97aa52393ed4a62e40a9a07dae7
--- /dev/null
+++ b/testcases/insynth-leon-tests/Arguments.scala
@@ -0,0 +1,13 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Hole {
+
+ def method(t: Int, x: Boolean, y: Boolean) : Int = ({
+ if (t > 5)
+ hole(5)
+ else
+ t
+ }) ensuring ( _ > 0 )
+
+}
diff --git a/testcases/insynth-leon-tests/BubbleSortBug.scala b/testcases/insynth-leon-tests/BubbleSortBug.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4377e43994275a92de92a4a49f8f7bc5825675f2
--- /dev/null
+++ b/testcases/insynth-leon-tests/BubbleSortBug.scala
@@ -0,0 +1,30 @@
+import leon.Utils._
+
+/* The calculus of Computation textbook */
+
+object BubbleSortBug {
+
+ def sort(a: Array[Int]): Array[Int] = ({
+ require(a.length >= 1)
+ var i = a.length - 1
+ var j = 0
+ val sa = a.clone
+ (while(i > 0) {
+ j = 0
+ (while(j < i) {
+ if(sa(j) < sa(j+1)) {
+ val tmp = sa(j)
+ sa(j) = sa(j+1)
+
+ hole(0)
+
+ sa(j+1) = tmp
+ }
+ j = j + 1
+ }) invariant(j >= 0 && j <= i && i < sa.length)
+ i = i - 1
+ }) invariant(i >= 0 && i < sa.length)
+ sa
+ }) ensuring(res => true)
+
+}
diff --git a/testcases/insynth-leon-tests/CaseClassSelectExample.scala b/testcases/insynth-leon-tests/CaseClassSelectExample.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5239efa37de79807bbe50df7a0132cae72e6f7c5
--- /dev/null
+++ b/testcases/insynth-leon-tests/CaseClassSelectExample.scala
@@ -0,0 +1,24 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object CaseClassSelectExample {
+
+ sealed abstract class OptionInt
+ case class Some(v : Int) extends OptionInt
+ case class None() extends OptionInt
+
+ // this won't work
+// sealed abstract class AbsHasVal(v: Int)
+// case class Concrete(x: Int) extends AbsHasVal(x)
+
+ def selectIntFromSome(some: Some) = {
+ some.v
+ }
+
+ // this won't work
+// def selectIntFromSome(a: Concrete) = {
+// a.v
+// }
+
+}
diff --git a/testcases/insynth-leon-tests/Hole.scala b/testcases/insynth-leon-tests/Hole.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f860590f3ae0efcdf69797795deabfab2642289b
--- /dev/null
+++ b/testcases/insynth-leon-tests/Hole.scala
@@ -0,0 +1,13 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Hole {
+
+ def method(t: Int) : Int = ({
+ if (t > 5)
+ hole(5)
+ else
+ t
+ }) ensuring ( _ > 0 )
+
+}
diff --git a/testcases/insynth-leon-tests/ListOperationsHole.scala b/testcases/insynth-leon-tests/ListOperationsHole.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bd3cb28e6a2a6a9c19822f84562a82c62d0e3737
--- /dev/null
+++ b/testcases/insynth-leon-tests/ListOperationsHole.scala
@@ -0,0 +1,24 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+// def isEmpty(l: List) = l match {
+// case Nil() => true
+// case Cons(_, _) => false
+// }
+
+ def concat(l1: List, l2: List) : List = ({
+ hole(l1)
+ }) ensuring(res => content(res) == content(l1) ++ content(l2))
+
+}
diff --git a/testcases/insynth-leon-tests/RedBlackTreeFull.scala b/testcases/insynth-leon-tests/RedBlackTreeFull.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bc2de6ba96ee699736d4558932b752eea9ebba9f
--- /dev/null
+++ b/testcases/insynth-leon-tests/RedBlackTreeFull.scala
@@ -0,0 +1,117 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case class Red() extends Color
+ case class Black() extends Color
+
+ sealed abstract class Tree
+ case class Empty() extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ sealed abstract class OptionInt
+ case class Some(v : Int) extends OptionInt
+ case class None() extends OptionInt
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty() => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = (t match {
+ case Empty() => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }) ensuring(_ >= 0)
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(),_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty() => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty() => 1
+ case Node(Black(), l, _, _) => blackHeight(l) + 1
+ case Node(Red(), l, _, _) => blackHeight(l)
+ }
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ t match {
+ case Empty() => Node(Red(),Empty(),x,Empty())
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(x, a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(x, b))
+ }
+ } ensuring (res => content(res) == content(t) ++ Set(x)
+ && size(t) <= size(res) && size(res) <= size(t) + 1
+ && redDescHaveBlackChildren(res)
+ && blackBalanced(res))
+
+ def makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n) && blackBalanced(n))
+ n match {
+ case Node(Red(),l,v,r) => Node(Black(),l,v,r)
+ case _ => n
+ }
+ } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res))
+
+ def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res))
+
+ def buggyAdd(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t))
+ ins(x, t)
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
+
+ def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ // case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
+}
diff --git a/testcases/insynth-synthesis-tests/Hole.scala b/testcases/insynth-synthesis-tests/Hole.scala
new file mode 100644
index 0000000000000000000000000000000000000000..091afbdb46d9d6c19fab2b627617fe7468c803df
--- /dev/null
+++ b/testcases/insynth-synthesis-tests/Hole.scala
@@ -0,0 +1,13 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Hole {
+
+ def method(t: Int) : Int = ({
+ if (t > 5)
+ hole(5)
+ else
+ t
+ })// ensuring ( _ > 0 )
+
+}
diff --git a/testcases/insynth-synthesis-tests/LocalScope.scala b/testcases/insynth-synthesis-tests/LocalScope.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4d39693476d3cd55d7c419c5a090e0304cb69842
--- /dev/null
+++ b/testcases/insynth-synthesis-tests/LocalScope.scala
@@ -0,0 +1,31 @@
+import leon.Utils._
+
+object LocalScope {
+ sealed abstract class Color
+ case class Red() extends Color
+ case class Black() extends Color
+
+ sealed abstract class Tree
+ case class Empty() extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ sealed abstract class OptionInt
+ case class Some(v : Int) extends OptionInt
+ case class None() extends OptionInt
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_, l, v, r) => {
+ // hide r
+ val r: Int = 5
+ //val f: ((Int, Int) => Boolean) = (x: Int, y: Int) => false
+
+ Some(5) match {
+ case Some(newInt) => hole(0)
+ }
+
+ false
+ }
+
+ case Empty() => true
+ }
+}
\ No newline at end of file
diff --git a/testcases/lesynth-results/RedBlackTreeSynthResult.scala b/testcases/lesynth-results/RedBlackTreeSynthResult.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c1c1c46b3c70af522d42fc083da85299b51d2116
--- /dev/null
+++ b/testcases/lesynth-results/RedBlackTreeSynthResult.scala
@@ -0,0 +1,95 @@
+import leon.Annotations._
+import leon.Utils._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case class Red() extends Color
+ case class Black() extends Color
+
+ sealed abstract class Tree
+ case class Empty() extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty() => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = t match {
+ case Empty() => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(),_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty() => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty() => 1
+ case Node(Black(), l, _, _) => blackHeight(l) + 1
+ case Node(Red(), l, _, _) => blackHeight(l)
+ }
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+// t match {
+// case Empty() => Node(Red(),Empty(),x,Empty())
+// case Node(c,a,y,b) =>
+// if (x < y) balance(c, ins(x, a), y, b)
+// else if (x == y) Node(c,a,y,b)
+// else balance(c,a,y,ins(x, b))
+// }
+ if ((redNodesHaveBlackChildren(t) && blackBalanced(t))) {
+ (t match {
+ case Empty() =>
+ Node(Red(), Empty(), x, Empty())
+ case n: Node =>
+ if ((n.value == x)) {
+ balance(Black(), n.right, x, n.left)
+ } else {
+ balance(n.color, n.left, x, ins(n.value, n.right))
+ }
+ })
+ } else {
+ leon.Utils.error[Tree]("Precondition failed")
+ }
+ } ensuring (res => content(res) == content(t) ++ Set(x)
+ && size(t) <= size(res) && size(res) <= size(t) + 1
+ && redDescHaveBlackChildren(res)
+ && blackBalanced(res))
+
+}
diff --git a/testcases/lesynth-results/RedBlackTreeSynthResultBad.scala b/testcases/lesynth-results/RedBlackTreeSynthResultBad.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4be3aae0f689d119048297be1f7aac259271db29
--- /dev/null
+++ b/testcases/lesynth-results/RedBlackTreeSynthResultBad.scala
@@ -0,0 +1,95 @@
+import leon.Annotations._
+import leon.Utils._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case class Red() extends Color
+ case class Black() extends Color
+
+ sealed abstract class Tree
+ case class Empty() extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty() => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = t match {
+ case Empty() => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(),_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty() => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty() => 1
+ case Node(Black(), l, _, _) => blackHeight(l) + 1
+ case Node(Red(), l, _, _) => blackHeight(l)
+ }
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+// t match {
+// case Empty() => Node(Red(),Empty(),x,Empty())
+// case Node(c,a,y,b) =>
+// if (x < y) balance(c, ins(x, a), y, b)
+// else if (x == y) Node(c,a,y,b)
+// else balance(c,a,y,ins(x, b))
+// }
+ if ((redNodesHaveBlackChildren(t) && blackBalanced(t))) {
+ (t match {
+ case Empty() =>
+ Node(Red(), Empty(), x, Empty())
+ case n: Node =>
+ if ((n.value == x)) {
+ Node(n.color, n.left, x, n.right)
+ } else {
+ balance(n.color, n.right, n.value, ins(x, n.left))
+ }
+ })
+ } else {
+ leon.Utils.error[Tree]("Precondition failed")
+ }
+ } ensuring (res => content(res) == content(t) ++ Set(x)
+ && size(t) <= size(res) && size(res) <= size(t) + 1
+ && redDescHaveBlackChildren(res)
+ && blackBalanced(res))
+
+}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueue.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..941bbadf944b61b78878c2acb0bdb0576f038c26
--- /dev/null
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueue.scala
@@ -0,0 +1,76 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ def isEmpty(p: Queue): Boolean = p.f == Nil
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r)
+ }
+
+ def head(p: Queue): Set[Int] = (
+ p.f match {
+ case Nil => Set[Int]()
+ case Cons(x, xs) => Set(x)
+ }) ensuring (
+ res =>
+ if (isEmpty(p)) true
+ else content(p) == res ++ content(tail(p)))
+
+ def tail(p: Queue): Queue = {
+ require(!isEmpty(p))
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ }
+ //
+ // def last(p: Queue): Int = {
+ // require(!isEmpty(p))
+ // p.r match {
+ // case Nil => reverse(p.f).asInstanceOf[Cons].head
+ // case Cons(x, _) => x
+ // }
+ // }
+
+ def snoc(p: Queue, x: Int): Queue =
+ checkf(p.f, Cons(x, p.r)) ensuring (
+ res =>
+ content(res) == content(p) ++ Set(x) &&
+ (if (isEmpty(p)) true
+ else content(tail(res)) ++ Set(x) == content(tail(res))))
+
+ def main(args: Array[String]): Unit = {
+ val pair = Queue(Cons(4, Nil), Cons(3, Nil))
+
+ println(head(pair))
+ println(content(pair) == head(pair) ++ content(tail(pair)))
+
+ println(head(Queue(Nil, Nil)))
+ }
+}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4faa50286c879d90d3e9fe12db58856459ee8993
--- /dev/null
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala
@@ -0,0 +1,49 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = {
+ rev_append(q.f, q.r) == rev_append(f, r) &&
+ { if (q.f == Nil) q.r == Nil else true }
+ }
+
+ def tail(p: Queue): Queue = {
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ }
+
+//(f match {
+// case Nil => Queue(reverse(r), Nil)
+// case _ => Queue(f, r)
+ def checkf(f: List, r: List): Queue = {
+ choose {
+ (res: Queue) =>
+ invariantList(res, f, r)
+ }
+ }
+
+}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueFull.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueFull.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cc5f1f73a99da0f3f64b878e4f569b68ec430e14
--- /dev/null
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueFull.scala
@@ -0,0 +1,101 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def size(q: Queue) : Int =
+ size(q.f) + size(q.r)
+
+ def isEmpty(p: Queue): Boolean = p.f == Nil
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (
+ res =>
+ content(res) == content(aList) ++ content(bList) &&
+ size(res) == size(aList) + size(bList)
+ )
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = ({
+ rev_append(q.f, q.r) == rev_append(f, r)
+ }) ensuring (
+ res =>
+ true
+ )
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (
+ res =>
+ content(res) == content(list) && size(res) == size(list)
+ )
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r) &&
+ size(res) == size(f) + size(r) &&
+ invariantList(res, f, r)
+ }
+
+ def head(p: Queue): Set[Int] = (
+ p.f match {
+ case Nil => Set[Int]()
+ case Cons(x, xs) => Set(x)
+ }) ensuring (
+ res =>
+ if (isEmpty(p)) true
+ else content(p) == res ++ content(tail(p)))
+
+ def tail(p: Queue): Queue = {
+ require(!isEmpty(p))
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ } ensuring {
+ (res: Queue) => content(res) ++ head(p) == content(p) &&
+ (if (isEmpty(p)) true
+ else size(res) + 1 == size(p))
+ }
+ //
+ // def last(p: Queue): Int = {
+ // require(!isEmpty(p))
+ // p.r match {
+ // case Nil => reverse(p.f).asInstanceOf[Cons].head
+ // case Cons(x, _) => x
+ // }
+ // }
+
+ def snoc(p: Queue, x: Int): Queue =
+ checkf(p.f, Cons(x, p.r)) ensuring (
+ res =>
+ content(res) == content(p) ++ Set(x) &&
+ size(res) == size(p) + 1 &&
+ (
+ if (isEmpty(p)) true
+ else (content(tail(res)) ++ Set(x) == content(tail(res)) &&
+ size(res.f) == size(p.f))
+ )
+ )
+
+}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6541b33b5dbce7b126d0eeac8b46858d286fa59d
--- /dev/null
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala
@@ -0,0 +1,60 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = {
+ rev_append(q.f, q.r) == rev_append(f, r) &&
+ { if (q.f == Nil) q.r == Nil else true }
+ }
+
+ def tail(p: Queue): Queue = {
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ }
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r)
+ }
+ //
+ // def last(p: Queue): Int = {
+ // require(!isEmpty(p))
+ // p.r match {
+ // case Nil => reverse(p.f).asInstanceOf[Cons].head
+ // case Cons(x, _) => x
+ // }
+ // }
+
+ def snoc(p: Queue, x: Int): Queue =
+ choose { (res: Queue) =>
+ content(res) == content(p) ++ Set(x) &&
+ (p.f == Nil || content(tail(res)) ++
+ Set(x) == content(tail(res)))
+ }
+}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnocWeird.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnocWeird.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0b9eccfc3d71060b7b85cf204f3f34b742ce2758
--- /dev/null
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnocWeird.scala
@@ -0,0 +1,63 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ def isEmpty(p: Queue): Boolean = p.f == Nil
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def queueInvariant(q:Queue) = if (q.f == Nil) q.r == Nil else true
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = {
+ rev_append(q.f, q.r) == rev_append(f, r) &&
+ { if (q.f == Nil) q.r == Nil else true }
+ }
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r)
+ }
+ //
+ // def last(p: Queue): Int = {
+ // require(!isEmpty(p))
+ // p.r match {
+ // case Nil => reverse(p.f).asInstanceOf[Cons].head
+ // case Cons(x, _) => x
+ // }
+ // }
+
+ def snoc(p: Queue, x: Int): Queue = {
+ require(queueInvariant(p))
+ choose { (res: Queue) =>
+ content(res) == content(p) ++ Set(x) &&
+ {res.f match {
+ case Nil => content(res) ++ Set(x) == content(res)
+ case Cons(_, xs) =>
+ content(checkf(xs, p.r)) ++ Set(x) == content(checkf(xs, p.r))
+ }}
+
+ }
+ }
+}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d35737dab64b76701d1904aae49dd4bfdb188a27
--- /dev/null
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala
@@ -0,0 +1,56 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ def isEmpty(p: Queue): Boolean = p.f == Nil
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = {
+ rev_append(q.f, q.r) == rev_append(f, r) &&
+ { if (q.f == Nil) q.r == Nil else true }
+ }
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r)
+ }
+
+ def tail(p: Queue): Queue = {
+ require( if (p.f == Nil) p.r == Nil else true )
+// p.f match {
+// case Nil => p
+// case Cons(_, xs) => checkf(xs, p.r)
+// }
+ choose {
+ (res: Queue) =>
+ p.f match {
+ case Nil => isEmpty(res)
+ case Cons(x, xs) => content(res) ++ Set(x) == content(p) && content(res) != content(p)
+ }
+ }
+ }
+
+}
diff --git a/testcases/lesynth/synthesis/BinarySearch.scala b/testcases/lesynth/synthesis/BinarySearch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d35de5266876b9208d98a8fdb80c9f9976678e8c
--- /dev/null
+++ b/testcases/lesynth/synthesis/BinarySearch.scala
@@ -0,0 +1,42 @@
+import leon.Utils._
+
+object BinarySearch {
+
+ def binarySearch(a: Array[Int], key: Int): Int =
+ choose{ (res: Int) =>
+ res >= -1 &&
+ res < a.length &&
+ (if(res >= 0) a(res) == key else !occurs(a, 0, a.length, key))
+ }
+
+
+ def occurs(a: Array[Int], from: Int, to: Int, key: Int): Boolean = {
+ require(a.length >= 0 && to <= a.length && from >= 0)
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= to)
+ false
+ else {
+ if(a(i) == key) true else rec(i+1)
+ }
+ }
+ if(from >= to)
+ false
+ else
+ rec(from)
+ }
+
+
+ def sorted(a: Array[Int], l: Int, u: Int) : Boolean = {
+ require(a.length >= 0 && l >= 0 && l <= u && u < a.length)
+ val t = sortedWhile(true, l, l, u, a)
+ t._1
+ }
+
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Array[Int]): (Boolean, Int) = {
+ require(a.length >= 0 && l >= 0 && l <= u && u < a.length && k >= l && k <= u)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a)
+ } else (isSorted, k)
+ }
+}
diff --git a/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeFull.scala b/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeFull.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e454407409fa0b47f80914ec16b0770a6f7dcdcb
--- /dev/null
+++ b/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeFull.scala
@@ -0,0 +1,143 @@
+import scala.collection.immutable.Set
+
+import leon.Annotations._
+import leon.Utils._
+
+object BinarySearchTree {
+ sealed abstract class Tree
+ case class Node(left: Tree, value: Int, right: Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def contents(tree: Tree): Set[Int] = tree match {
+ case Leaf() => Set.empty[Int]
+ case Node(l, v, r) => contents(l) ++ Set(v) ++ contents(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 isSorted(tree: Tree): Boolean = tree match {
+// case Leaf() => true
+// case Node(Leaf(), v, Leaf()) => true
+// case Node(l @ Node(_, vIn, _), v, Leaf()) => v > vIn && isSorted(l)
+// case Node(Leaf(), v, r @ Node(_, vIn, _)) => v < vIn && isSorted(r)
+// case Node(l @ Node(_, vInLeft, _), v, r @ Node(_, vInRight, _)) =>
+// v > vInLeft && v < vInRight && isSorted(l) && isSorted(r)
+// }
+//
+// def isSorted(tree: Tree): Boolean = tree match {
+// case Leaf() => true
+// case Node(l, v, r) => isLowerThan(l, v) && isGreaterThan(r, v) && isSorted(l) && isSorted(r)
+// }
+//
+// def isLowerThan(tree: Tree, max: Int): Boolean = tree match {
+// case Leaf() => true
+// case Node(l, v, r) => v < max && isLowerThan(l, max) && isLowerThan(r, max)
+// }
+//
+// def isGreaterThan(tree: Tree, min: Int): Boolean = tree match {
+// case Leaf() => true
+// case Node(l, v, r) => v > min && isGreaterThan(r, min) && isGreaterThan(l, min)
+// }
+//
+// def isSorted(tree: Tree): Boolean = tree match {
+// case Leaf() => true
+// case Node(l, v, r) => isSorted(l) && isSorted(r) &&
+// contents(l).forall( v > _ ) && contents(r).forall( v < _ )
+// }
+
+ def member(tree: Tree, value: Int): Boolean = {
+ require(isSorted(tree))
+ tree match {
+ case Leaf() => false
+ case n @ Node(l, v, r) => if (v < value) {
+ member(r, value)
+ } else if (v > value) {
+ member(l, value)
+ } else {
+ true
+ }
+ }
+ } ensuring (res =>
+ (res && contents(tree).contains(value)) ||
+ (!res && !contents(tree).contains(value))
+ )
+
+// def insert(tree: Tree, value: Int): Node = {
+// require(isSorted(tree))
+// tree match {
+// case Leaf() => Node(Leaf(), value, Leaf())
+// case n @ Node(l, v, r) => if (v < value) {
+// Node(l, v, insert(r, value))
+// } else if (v > value) {
+// Node(insert(l, value), v, r)
+// } else {
+// n
+// }
+// }
+// } ensuring (res => contents(res) == contents(tree) ++ Set(value) && isSorted(res))
+
+// def treeMin(tree: Node): Int = {
+// require(isSorted(tree))
+// tree match {
+// case Node(left, v, _) => left match {
+// case Leaf() => v
+// case n @ Node(_, _, _) => treeMin(n)
+// }
+// }
+// }
+//
+// def treeMax(tree: Node): Int = {
+// require(isSorted(tree))
+// tree match {
+// case Node(_, v, right) => right match {
+// case Leaf() => v
+// case n @ Node(_, _, _) => treeMax(n)
+// }
+// }
+// }
+
+// def remove(tree: Tree, value: Int): Node = {
+// require(isSorted(tree))
+// tree match {
+// case l @ Leaf() => l
+// case n @ Node(l, v, r) => if (v < value) {
+// Node(l, v, insert(r, value))
+// } else if (v > value) {
+// Node(insert(l, value), v, r)
+// } else {
+// n
+// }
+// }
+// } ensuring (res => contents(res) == contents(tree) -- Set(value))
+
+}
+
diff --git a/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeMember.scala b/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeMember.scala
new file mode 100644
index 0000000000000000000000000000000000000000..416c6ef577cfb267df1d66c1a8a6f8d0f4ba141a
--- /dev/null
+++ b/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeMember.scala
@@ -0,0 +1,115 @@
+import scala.collection.immutable.Set
+
+import leon.Annotations._
+import leon.Utils._
+
+object BinarySearchTree {
+ sealed abstract class Tree
+ case class Node(left: Tree, value: Int, right: Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def contents(tree: Tree): Set[Int] = tree match {
+ case Leaf() => Set.empty[Int]
+ case Node(l, v, r) => contents(l) ++ Set(v) ++ contents(r)
+ }
+// def isSorted(tree: Tree): Boolean = tree match {
+// case Leaf() => true
+// case Node(Leaf(), v, Leaf()) => true
+// case Node(l@Node(_, vIn, _), v, Leaf()) => v > vIn && isSorted(l)
+// case Node(Leaf(), v, r@Node(_, vIn, _)) => v < vIn && isSorted(r)
+// case Node(l@Node(_, vInLeft, _), v, r@Node(_, vInRight, _)) =>
+// v > vInLeft && v < vInRight && isSorted(l) && isSorted(r)
+// }
+//
+
+ def isSorted(tree: Tree): Boolean =
+ isSortedMaxMin(tree, Int.MinValue, Int.MaxValue)
+
+ def max(a: Int, b: Int) = if (a < b) b else a
+
+ def min(a: Int, b: Int) = if (a > b) b else a
+
+ def isSortedMaxMin(tree: Tree, minVal: Int, maxVal: Int): Boolean = tree match {
+ case Leaf() => true
+ case Node(left, v, right) =>
+ minVal < v && v < maxVal &&
+ // go left, update upper bound
+ isSortedMaxMin(left, minVal, min(maxVal, v)) &&
+ isSortedMaxMin(right, max(minVal, v), maxVal)
+ }
+
+ def member(tree: Tree, value: Int): Boolean = {
+ require(isSorted(tree))
+ choose {
+ (res: Boolean) =>
+ (
+ if (res) (contents(tree) == contents(tree) ++ Set(value))
+ else !(contents(tree) == contents(tree) ++ Set(value))
+ )
+ }
+ }
+
+// def member(tree: Tree, value: Int): Boolean = {
+// require(isSorted(tree))
+// tree match {
+// case Leaf() => false
+// case n @ Node(l, v, r) => if (v < value) {
+// member(r, value)
+// } else if (v > value) {
+// member(l, value)
+// } else {
+// true
+// }
+// }
+// } ensuring (_ || !(contents(tree) == contents(tree) ++ Set(value)))
+//
+// def insert(tree: Tree, value: Int): Node = {
+// require(isSorted(tree))
+// tree match {
+// case Leaf() => Node(Leaf(), value, Leaf())
+// case n @ Node(l, v, r) => if (v < value) {
+// Node(l, v, insert(r, value))
+// } else if (v > value) {
+// Node(insert(l, value), v, r)
+// } else {
+// n
+// }
+// }
+// } ensuring (res => contents(res) == contents(tree) ++ Set(value) && isSorted(res))
+
+ // def treeMin(tree: Node): Int = {
+ // require(isSorted(tree).sorted)
+ // tree match {
+ // case Node(left, v, _) => left match {
+ // case Leaf() => v
+ // case n@Node(_, _, _) => treeMin(n)
+ // }
+ // }
+ // }
+ //
+ // def treeMax(tree: Node): Int = {
+ // require(isSorted(tree).sorted)
+ // tree match {
+ // case Node(_, v, right) => right match {
+ // case Leaf() => v
+ // case n@Node(_, _, _) => treeMax(n)
+ // }
+ // }
+ // }
+
+// def remove(tree: Tree, value: Int): Node = {
+// require(isSorted(tree))
+// tree match {
+// case l @ Leaf() => l
+// case n @ Node(l, v, r) => if (v < value) {
+// Node(l, v, insert(r, value))
+// } else if (v > value) {
+// Node(insert(l, value), v, r)
+// } else {
+// n
+// }
+// }
+// } ensuring (contents(_) == contents(tree) -- Set(value))
+
+}
+
diff --git a/testcases/lesynth/synthesis/InsertionSort/InsertionSortInsert.scala b/testcases/lesynth/synthesis/InsertionSort/InsertionSortInsert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ac832856ed117c3a7e68eabae2f5ab87b70ef3bb
--- /dev/null
+++ b/testcases/lesynth/synthesis/InsertionSort/InsertionSortInsert.scala
@@ -0,0 +1,61 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object InsertionSort {
+ 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(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ 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))
+ }
+
+ /* 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 = {
+ require(isSorted(l))
+ choose { (res : List) =>
+ (
+ contents(res) == contents(l) ++ Set(e) &&
+ isSorted(res) &&
+ size(res) == size(l) + 1
+ )
+ }
+// val cond1: Boolean = /*!*/
+// l match {
+// case Nil() => /*!*/ // Cons(e,Nil())
+// case Cons(x,xs) =>
+// val cond2: Boolean = /*!*/
+// if (x <= e) /*!*/ // Cons(x,sortedIns(e, xs))
+// else /*!*/ // Cons(e, l)
+// }
+ }
+// ensuring(res => contents(res) == contents(l) ++ Set(e)
+// && isSorted(res)
+// && size(res) == size(l) + 1
+// )
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def sort(l: List): List = (l match {
+ case Nil() => Nil()
+ case Cons(x,xs) => sortedIns(x, sort(xs))
+ }) ensuring(res => contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l)
+ )
+
+}
diff --git a/testcases/lesynth/synthesis/InsertionSort/InsertionSortSort.scala b/testcases/lesynth/synthesis/InsertionSort/InsertionSortSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7daae970332d41e0b971b32c8cc70b57aa9b69b5
--- /dev/null
+++ b/testcases/lesynth/synthesis/InsertionSort/InsertionSortSort.scala
@@ -0,0 +1,57 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object InsertionSort {
+ 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(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ 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))
+ }
+
+ /* 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 = {
+ require(isSorted(l))
+ l match {
+ case Nil() => Cons(e,Nil())
+ case Cons(x,xs) =>
+ if (x <= e) Cons(x,sortedIns(e, xs))
+ else Cons(e, l)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1
+)
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def xxsort(l: List): List = choose {
+ (res : List) =>
+ contents(res) == contents(l) &&
+ isSorted(res) &&
+ size(res) == size(l)
+// val cond: Boolean = /*!*/
+// case Nil() => /*!*/ // Nil()
+// case Cons(x,xs) => /*!*/ // sortedIns(x, sort(xs))
+ }
+// ensuring(res => contents(res) == contents(l)
+// && isSorted(res)
+// && size(res) == size(l)
+// )
+
+}
diff --git a/testcases/lesynth/synthesis/List/ListConcat.scala b/testcases/lesynth/synthesis/List/ListConcat.scala
new file mode 100644
index 0000000000000000000000000000000000000000..96a2d909ac25e11596ee86c63d884df08d5be7e3
--- /dev/null
+++ b/testcases/lesynth/synthesis/List/ListConcat.scala
@@ -0,0 +1,20 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def concat(l1: List, l2: List) : List = choose {
+ (out : List) =>
+ content(out) == content(l1) ++ content(l2)
+ }
+
+}
diff --git a/testcases/lesynth/synthesis/List/ListSearch.scala b/testcases/lesynth/synthesis/List/ListSearch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c70269a41016e45ce3edb968d07730a59aeb7c28
--- /dev/null
+++ b/testcases/lesynth/synthesis/List/ListSearch.scala
@@ -0,0 +1,50 @@
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class Option
+ case class Some(i: Int) extends Option
+ case object None extends Option
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil() => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+//
+// def isEmpty(l: List) = l match {
+// case Nil() => true
+// case Cons(_, _) => false
+// }
+
+
+ def linearSearch(l: List, c: Int): Option = {
+ l match {
+ case Nil() => None
+ case Cons(lHead, lTail) =>
+ if (lHead == c) Some(size(l))
+ else Some(linearSearch(lTail, c))
+ }
+ } ensuring(res => if(res > -1) atInd(l, size(l) - res) == c else !content(l).contains(c))
+
+ def atInd(l: List, ind: Int): Int = {
+ require(ind >= 0 && ind < size(l))
+
+ l match {
+ case Nil() => -1
+ case Cons(lHead, lTail) =>
+ if (ind == 0) lHead
+ else atInd(lTail, ind - 1)
+ }
+
+ } ensuring( res =>
+ if (size(l) == 0) res == -1 else content(l).contains(res)
+ )
+}
diff --git a/testcases/lesynth/synthesis/MergeSort/MergeSortMerge.scala b/testcases/lesynth/synthesis/MergeSort/MergeSortMerge.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8b25821929c319358ea948139245904b6f9e2a3b
--- /dev/null
+++ b/testcases/lesynth/synthesis/MergeSort/MergeSortMerge.scala
@@ -0,0 +1,55 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst : List, snd : List) extends PairAbs
+
+ def contents(l : List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l : List) : Boolean = l match {
+ case Nil() => true
+ case Cons(x,xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list : List) : Int = list match {
+ case Nil() => 0
+ case Cons(x,xs) => 1 + size(xs)
+ }
+
+ def merge(aList : List, bList : List) : List = {
+ require(isSorted(aList) && isSorted(bList))
+ choose( (res: List) =>
+ ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+ )
+ }
+
+// def merge(aList : List, bList : List) : List = {
+// require(isSorted(aList) && isSorted(bList))
+//
+// bList match {
+// case Nil() => aList
+// case Cons(x,xs) =>
+// aList match {
+// case Nil() => bList
+// case Cons(y,ys) =>
+// if (y < x)
+// Cons(y,merge(ys, bList))
+// else
+// Cons(x,merge(aList, xs))
+// }
+// }
+// } ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+
+}
diff --git a/testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala b/testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..987c538c4ab36dc9b378f03fc24592210bcbd62b
--- /dev/null
+++ b/testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala
@@ -0,0 +1,86 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst : List, snd : List) extends PairAbs
+
+ def contents(l : List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l : List) : Boolean = l match {
+ case Nil() => true
+ case Cons(x,xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list : List) : Int = list match {
+ case Nil() => 0
+ case Cons(x,xs) => 1 + size(xs)
+ }
+
+ def splithelper(aList : List, bList : List, n : Int) : Pair = {
+ if (n <= 0) Pair(aList,bList)
+ else
+ bList match {
+ case Nil() => Pair(aList,bList)
+ case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+ }
+ } ensuring(res => contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd))
+
+// def split(list : List, n : Int): Pair = {
+// splithelper(Nil(),list,n)
+// } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def split(list: List): Pair = {
+ splithelper(Nil(),list,size(list)/2)
+ } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def merge(aList : List, bList : List) : List = {
+ require(isSorted(aList) && isSorted(bList))
+ bList match {
+ case Nil() => aList
+ case Cons(x,xs) =>
+ aList match {
+ case Nil() => bList
+ case Cons(y,ys) =>
+ if (y < x)
+ Cons(y,merge(ys, bList))
+ else
+ Cons(x,merge(aList, xs))
+ }
+ }
+ } ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+
+ def isEmpty(list: List) : Boolean = list match {
+ case Nil() => true
+ case Cons(x,xs) => false
+ }
+
+ def sort(list : List) : List = choose {
+
+ (res : List) =>
+ contents(res) == contents(list) && isSorted(res)
+
+// list match {
+// case Nil() => list
+// case Cons(x,Nil()) => list
+// case _ =>
+// val p = split(list,size(list)/2)
+// merge(mergeSort(p.fst), mergeSort(p.snd))
+
+// merge(mergeSort(split(list).fst), mergeSort(split(list).snd))
+ }
+
+ //ensuring(res => contents(res) == contents(list) && isSorted(res))
+
+}
diff --git a/testcases/lesynth/synthesis/MergeSort/MergeSortSortWithVal.scala b/testcases/lesynth/synthesis/MergeSort/MergeSortSortWithVal.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2cccf5c98753a362235d4fb423e2621e84de534a
--- /dev/null
+++ b/testcases/lesynth/synthesis/MergeSort/MergeSortSortWithVal.scala
@@ -0,0 +1,85 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst : List, snd : List) extends PairAbs
+
+ def contents(l : List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l : List) : Boolean = l match {
+ case Nil() => true
+ case Cons(x,xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list : List) : Int = list match {
+ case Nil() => 0
+ case Cons(x,xs) => 1 + size(xs)
+ }
+
+ def splithelper(aList : List, bList : List, n : Int) : Pair = {
+ if (n <= 0) Pair(aList,bList)
+ else
+ bList match {
+ case Nil() => Pair(aList,bList)
+ case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+ }
+ } ensuring(res => contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd))
+
+// def split(list : List, n : Int): Pair = {
+// splithelper(Nil(),list,n)
+// } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def split(list: List): Pair = {
+ splithelper(Nil(),list,size(list)/2)
+ } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def merge(aList : List, bList : List) : List = {
+ require(isSorted(aList) && isSorted(bList))
+ bList match {
+ case Nil() => aList
+ case Cons(x,xs) =>
+ aList match {
+ case Nil() => bList
+ case Cons(y,ys) =>
+ if (y < x)
+ Cons(y,merge(ys, bList))
+ else
+ Cons(x,merge(aList, xs))
+ }
+ }
+ } ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+
+ def isEmpty(list: List) : Boolean = list match {
+ case Nil() => true
+ case Cons(x,xs) => false
+ }
+
+ def sort(list : List) : List =
+ list match {
+ case Nil() => list
+ case Cons(_,Nil()) => list
+ case _ => {
+ val p = split(list)
+ choose {(res : List) =>
+ contents(res) == contents(list) && isSorted(res)
+ }
+ }
+ }
+
+// merge(mergeSort(split(list).fst), mergeSort(split(list).snd))
+
+ //ensuring(res => contents(res) == contents(list) && isSorted(res))
+
+}
diff --git a/testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6b9a73a9c1290c626d03f8a8cad3ea8f49bc8598
--- /dev/null
+++ b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala
@@ -0,0 +1,103 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ local: Boolean
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def isEmpty(ab: AddressBook) = size(ab) == 0
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// !hasPrivate(res.business) &&
+// hasPrivate(res.pers)
+// }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+//
+// def makeAddressBook(l: List): AddressBook =
+// choose {
+// (res: AddressBook) =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+
+ def makeAddressBook(l: List): AddressBook =
+ choose {
+ (res: AddressBook) =>
+ size(res) == size(l) && addressBookInvariant(res)
+ }
+
+}
diff --git a/testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c22541f8c9649c1e5485a41d5ebe4ce093d68bf2
--- /dev/null
+++ b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala
@@ -0,0 +1,106 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+
+ case class Address(a: Int, b: Int, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+ def merge(l1: List, l2: List): List = l1 match {
+ case Nil => l2
+ case Cons(a, tail) => Cons(a, merge(tail, l2))
+ }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// !hasPrivate(res.business) &&
+// hasPrivate(res.pers)
+// }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+//
+// def makeAddressBook(l: List): AddressBook =
+// choose {
+// (res: AddressBook) =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+
+ def makeAddressBook(l: List): AddressBook =
+ choose {
+ (res: AddressBook) =>
+ size(res) == size(l) &&
+ allPrivate(res.pers) && allBusiness(res.business) &&
+ content(res) == content(l)
+ }
+
+}
diff --git a/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala b/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0d6d8c0677806c687186184aa929e80032b869a8
--- /dev/null
+++ b/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala
@@ -0,0 +1,81 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ phoneNumber: Int
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def isEmpty(ab: AddressBook) = size(ab) == 0
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+ def makeAddressBook(l: List): AddressBook = (l match {
+ case Nil => AddressBook(Nil, Nil)
+ case Cons(a, l1) => {
+ val res = makeAddressBook(l1)
+ if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+ else AddressBook(Cons(a, res.business), res.pers)
+ }
+ }) ensuring {
+ (res: AddressBook) =>
+ size(res) == size(l) && addressBookInvariant(res)
+ }
+
+ def merge(l1: List, l2: List): List = l1 match {
+ case Nil => l2
+ case Cons(a, tail) => Cons(a, merge(tail, l2))
+ }
+
+ def mergeAddressBooks(ab1: AddressBook, ab2: AddressBook) = {
+ require(addressBookInvariant(ab1) && addressBookInvariant(ab2))
+ choose {
+ (res: AddressBook) =>
+ (size(res) == size(ab1) + size(ab2)) && addressBookInvariant(res)
+ }
+ }
+
+}
diff --git a/testcases/lesynth/synthesis/RedBlackTree/RedBlackTree.scala b/testcases/lesynth/synthesis/RedBlackTree/RedBlackTree.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f72664258ebb5b329d61d0eb17c82c581b370d01
--- /dev/null
+++ b/testcases/lesynth/synthesis/RedBlackTree/RedBlackTree.scala
@@ -0,0 +1,81 @@
+import leon.Annotations._
+import leon.Utils._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case class Red() extends Color
+ case class Black() extends Color
+
+ sealed abstract class Tree
+ case class Empty() extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty() => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = t match {
+ case Empty() => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(),_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty() => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty() => 1
+ case Node(Black(), l, _, _) => blackHeight(l) + 1
+ case Node(Red(), l, _, _) => blackHeight(l)
+ }
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ t match {
+ case Empty() => Node(Red(),Empty(),x,Empty())
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(x, a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(x, b))
+ }
+ } ensuring (res => content(res) == content(t) ++ Set(x)
+ && size(t) <= size(res) && size(res) <= size(t) + 1
+ && redDescHaveBlackChildren(res)
+ && blackBalanced(res))
+
+}
diff --git a/testcases/lesynth/synthesis/RedBlackTree/RedBlackTreeInsert.scala b/testcases/lesynth/synthesis/RedBlackTree/RedBlackTreeInsert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e6413ffaf8278fdacb43372eb615ced566e60022
--- /dev/null
+++ b/testcases/lesynth/synthesis/RedBlackTree/RedBlackTreeInsert.scala
@@ -0,0 +1,77 @@
+import leon.Annotations._
+import leon.Utils._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case class Red() extends Color
+ case class Black() extends Color
+
+ sealed abstract class Tree
+ case class Empty() extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ def content(t: Tree): Set[Int] = t match {
+ case Empty() => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree): Int = t match {
+ case Empty() => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree): Boolean = t match {
+ case Empty() => true
+ case Node(Black(), _, _, _) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree): Boolean = t match {
+ case Empty() => true
+ case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree): Boolean = t match {
+ case Empty() => true
+ case Node(_, l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t: Tree): Boolean = t match {
+ case Node(_, l, _, r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty() => true
+ }
+
+ def blackHeight(t: Tree): Int = t match {
+ case Empty() => 1
+ case Node(Black(), l, _, _) => blackHeight(l) + 1
+ case Node(Red(), l, _, _) => blackHeight(l)
+ }
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c, a, x, b) match {
+ case Node(Black(), Node(Red(), Node(Red(), a, xV, b), yV, c), zV, d) =>
+ Node(Red(), Node(Black(), a, xV, b), yV, Node(Black(), c, zV, d))
+ case Node(Black(), Node(Red(), a, xV, Node(Red(), b, yV, c)), zV, d) =>
+ Node(Red(), Node(Black(), a, xV, b), yV, Node(Black(), c, zV, d))
+ case Node(Black(), a, xV, Node(Red(), Node(Red(), b, yV, c), zV, d)) =>
+ Node(Red(), Node(Black(), a, xV, b), yV, Node(Black(), c, zV, d))
+ case Node(Black(), a, xV, Node(Red(), b, yV, Node(Red(), c, zV, d))) =>
+ Node(Red(), Node(Black(), a, xV, b), yV, Node(Black(), c, zV, d))
+ case Node(c, a, xV, b) => Node(c, a, xV, b)
+ }
+ } ensuring (res => content(res) == content(Node(c, a, x, b)))
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ choose { (res: Tree) =>
+ content(res) == content(t) ++ Set(x) &&
+ size (t) <= size(res) && size(res) <= size(t) + 1 &&
+ redDescHaveBlackChildren (res) &&
+ blackBalanced (res)
+ }
+ }
+
+}
\ No newline at end of file
diff --git a/testcases/lesynth/test/Addresses.scala b/testcases/lesynth/test/Addresses.scala
new file mode 100644
index 0000000000000000000000000000000000000000..52260559cecdabef594aa208096cd9a05b93dbe5
--- /dev/null
+++ b/testcases/lesynth/test/Addresses.scala
@@ -0,0 +1,52 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+
+ case class Address(aComp: Int, bComp: Int, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def setA(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(a, l1) => Set(a) ++ setA(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def makeAddressBook(l: List): AddressBook =
+ choose {
+ (res: AddressBook) =>
+ size(res) == size(l) &&
+ allPrivate(res.pers) && allBusiness(res.business)
+ }
+
+}
diff --git a/testcases/lesynth/test/AddressesMergeAddressBooks.scala b/testcases/lesynth/test/AddressesMergeAddressBooks.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d308ac24746f388ab21c8f767bf5ffe1de215243
--- /dev/null
+++ b/testcases/lesynth/test/AddressesMergeAddressBooks.scala
@@ -0,0 +1,70 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+
+ case class Address(a: Int, b: Int, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def setA(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(a, l1) => Set(a) ++ setA(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def makeAddressBook(l: List): AddressBook = (l match {
+ case Nil => AddressBook(Nil, Nil)
+ case Cons(a, l1) => {
+ val res = makeAddressBook(l1)
+ if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+ else AddressBook(Cons(a, res.business), res.pers)
+ }
+ }) ensuring {
+ (res: AddressBook) =>
+ size(res) == size(l) &&
+ allPrivate(res.pers) && allBusiness(res.business)
+ }
+
+ def merge(l1: List, l2: List): List = l1 match {
+ case Nil => l2
+ case Cons(a, tail) => Cons(a, merge(tail, l2))
+ }
+
+ def mergeAddressBooks(ab1: AddressBook, ab2: AddressBook) =
+ choose {
+ (res: AddressBook) =>
+ size(res) == size(ab1) + size(ab2) &&
+ allPrivate(res.pers) && allBusiness(res.business)
+ }
+
+}
diff --git a/testcases/lesynth/test/refinement/ListConcat.scala b/testcases/lesynth/test/refinement/ListConcat.scala
new file mode 100644
index 0000000000000000000000000000000000000000..96a2d909ac25e11596ee86c63d884df08d5be7e3
--- /dev/null
+++ b/testcases/lesynth/test/refinement/ListConcat.scala
@@ -0,0 +1,20 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def concat(l1: List, l2: List) : List = choose {
+ (out : List) =>
+ content(out) == content(l1) ++ content(l2)
+ }
+
+}
diff --git a/testcases/lesynth/test/refinement/ListConcatWithEmpty.scala b/testcases/lesynth/test/refinement/ListConcatWithEmpty.scala
new file mode 100644
index 0000000000000000000000000000000000000000..336fd7e680ca29f30124947d10a1b7a9de8496b0
--- /dev/null
+++ b/testcases/lesynth/test/refinement/ListConcatWithEmpty.scala
@@ -0,0 +1,37 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def isEmpty(l: List) = l match {
+ case Nil() => true
+ case Cons(head, tail) => false
+ }
+
+ def isEmptyBad(l: List) = l match {
+ case Nil() => true
+ case Cons(head, tail) => true
+ }
+
+ def hasContent(l: List) = l match {
+ case Nil() => false
+ case Cons(head, tail) => true
+ }
+
+// !content(l).isEmpty
+
+ def concat(l1: List, l2: List) : List = choose {
+ (out : List) =>
+ content(out) == content(l1) ++ content(l2)
+ }
+
+}
diff --git a/testcases/lesynth/test/verifier/BinarySearchTree.scala b/testcases/lesynth/test/verifier/BinarySearchTree.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3ddc3fba824da29b9216cbeb60b931eb4e187136
--- /dev/null
+++ b/testcases/lesynth/test/verifier/BinarySearchTree.scala
@@ -0,0 +1,65 @@
+import scala.collection.immutable.Set
+
+import leon.Annotations._
+import leon.Utils._
+
+object BinarySearchTree {
+ sealed abstract class Tree
+ case class Node(left: Tree, value: Int, right: Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def contents(tree: Tree): Set[Int] = tree match {
+ case Leaf() => Set.empty[Int]
+ case Node(l, v, r) => contents(l) ++ Set(v) ++ contents(r)
+ }
+
+ def isSorted(tree: Tree): Boolean = tree match {
+ case Leaf() => true
+ case Node(Leaf(), v, Leaf()) => true
+ case Node(l@Node(_, vIn, _), v, Leaf()) => v > vIn && isSorted(l)
+ case Node(Leaf(), v, r@Node(_, vIn, _)) => v < vIn && isSorted(r)
+ case Node(l@Node(_, vInLeft, _), v, r@Node(_, vInRight, _)) =>
+ v > vInLeft && v < vInRight && isSorted(l) && isSorted(r)
+ }
+
+ def member(tree: Tree, value: Int): Boolean = {
+ require(isSorted(tree))
+ choose {
+ (res: Boolean) =>
+ (
+ if (res) (contents(tree) == contents(tree) ++ Set(value))
+ else !(contents(tree) == contents(tree) ++ Set(value))
+ )
+ }
+ }
+
+ def goodMember(tree: Tree, value: Int): Boolean = {
+ require(isSorted(tree))
+ tree match {
+ case Leaf() => false
+ case n @ Node(l, v, r) => if (v < value) {
+ member(r, value)
+ } else if (v > value) {
+ member(l, value)
+ } else {
+ true
+ }
+ }
+ } ensuring (_ || !(contents(tree) == contents(tree) ++ Set(value)))
+
+ def badMember(tree: Tree, value: Int): Boolean = {
+ require(isSorted(tree))
+ tree match {
+ case Leaf() => false
+ case n @ Node(l, v, r) => if (v <= value) {
+ member(r, value)
+ } else if (v > value) {
+ member(l, value)
+ } else {
+ true
+ }
+ }
+ } ensuring (_ || !(contents(tree) == contents(tree) ++ Set(value)))
+
+}
+
diff --git a/testcases/lesynth/test/verifier/ListConcat.scala b/testcases/lesynth/test/verifier/ListConcat.scala
new file mode 100644
index 0000000000000000000000000000000000000000..39b756d8424a66535cf9b4c331fdc7d66cff0bb2
--- /dev/null
+++ b/testcases/lesynth/test/verifier/ListConcat.scala
@@ -0,0 +1,44 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def concat(l1: List, l2: List) : List = choose {
+ (out : List) =>
+ content(out) == content(l1) ++ content(l2)
+ }
+
+ def goodConcat1(l1: List, l2: List) : List =
+ l1 match {
+ case Nil() => l2
+ case Cons(l1Head, l1Tail) =>
+ l1 match {
+ case Nil() => l2
+ case _ => Cons(l1Head, Cons(l1Head, concat(l1Tail, l2)))
+ }
+ }
+
+ def goodConcat2(l1: List, l2: List) : List =
+ l1 match {
+ case Nil() => l2
+ case Cons(l1Head, l1Tail) =>
+ Cons(l1Head, Cons(l1Head, concat(l1Tail, l2)))
+ }
+
+ def badConcat1(l1: List, l2: List) : List =
+ l1 match {
+ case Nil() => l1
+ case Cons(l1Head, l1Tail) =>
+ Cons(l1Head, Cons(l1Head, concat(l1Tail, l2)))
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
new file mode 100644
index 0000000000000000000000000000000000000000..027d90bcbc47dba08d0e4d8b5e4c55ade9fea82c
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
@@ -0,0 +1,103 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ local: Boolean
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def sizeA(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def isEmpty(ab: AddressBook) = sizeA(ab) == 0
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// !hasPrivate(res.business) &&
+// hasPrivate(res.pers)
+// }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+//
+// def makeAddressBook(l: List): AddressBook =
+// choose {
+// (res: AddressBook) =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+
+ def makeAddressBook(l: List): AddressBook =
+ choose {
+ (res: AddressBook) =>
+ sizeA(res) == size(l) && addressBookInvariant(res)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
new file mode 100644
index 0000000000000000000000000000000000000000..579c6d4b71b0fb5b063b3cec14f19f5cbf87ab1a
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
@@ -0,0 +1,129 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ local: Boolean
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def sizeA(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+// def isEmpty(ab: AddressBook) = sizeA(ab) == 0
+
+ def contentA(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// !hasPrivate(res.business) &&
+// hasPrivate(res.pers)
+// }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+//
+// def makeAddressBook(l: List): AddressBook =
+// choose {
+// (res: AddressBook) =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+
+/*
+ // MANUAL SOLUTION:
+ def makeAB(l:List) : AddressBook = {
+ l match {
+ case Nil => AddressBook(Nil,Nil)
+ case Cons(a,t) => {
+ val ab1 = makeAB(t)
+ if (a.priv) AddressBook(ab1.business, Cons(a,ab1.pers))
+ else AddressBook(Cons(a,ab1.business), ab1.pers)
+ }
+ }
+ } ensuring((res: AddressBook) =>
+ sizeA(res) == size(l) &&
+ addressBookInvariant(res) &&
+ contentA(res) == content(l))
+
+*/
+
+/* // Perhaps this can be useful?
+ def cond(b:Boolean, ab1: AddressBook, ab2: AddressBook) : AddressBook = {
+ if (b) ab1 else ab2
+ }
+*/
+
+ def makeAddressBook(l: List): AddressBook =
+ choose {
+ (res: AddressBook) =>
+ sizeA(res) == size(l) &&
+ addressBookInvariant(res) &&
+ contentA(res) == content(l)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e47b260075ca097290b0dc1489d603ff48a51223
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
@@ -0,0 +1,113 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ local: Boolean
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def sizeA(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def isEmpty(ab: AddressBook) = sizeA(ab) == 0
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// !hasPrivate(res.business) &&
+// hasPrivate(res.pers)
+// }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+//
+// def makeAddressBook(l: List): AddressBook =
+// choose {
+// (res: AddressBook) =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+
+ def makeAddressBook(l: List): AddressBook = {
+ l match {
+ case Nil => AddressBook(Nil,l)
+ case Cons(h,t) => {
+ if (allPrivate(t))
+ AddressBook(Nil, Cons(Address(h.info, allPrivate(t)), t))
+ else
+ AddressBook(Cons(Address(h.info, isEmpty(makeAddressBook(t))),
+ makeAddressBook(t).business),
+ makeAddressBook(t).pers)
+ }
+ }
+ } ensuring ((res: AddressBook) =>
+ sizeA(res) == size(l) && addressBookInvariant(res))
+
+}
+
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
new file mode 100644
index 0000000000000000000000000000000000000000..98bb95f59711ab5a212a1764223601bbb5c016c5
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
@@ -0,0 +1,106 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+
+ case class Address(a: Int, b: Int, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def contentA(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+ def merge(l1: List, l2: List): List = l1 match {
+ case Nil => l2
+ case Cons(a, tail) => Cons(a, merge(tail, l2))
+ }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// !hasPrivate(res.business) &&
+// hasPrivate(res.pers)
+// }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+//
+// def makeAddressBook(l: List): AddressBook =
+// choose {
+// (res: AddressBook) =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+
+ def makeAddressBook(l: List): AddressBook =
+ choose {
+ (res: AddressBook) =>
+ size(res) == size(l) &&
+ allPrivate(res.pers) && allBusiness(res.business) &&
+ contentA(res) == content(l)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8cb51d2483552623a9d3e329634968ccbd5b993b
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
@@ -0,0 +1,78 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ phoneNumber: Int
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def sizeA(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def addToPers(ab: AddressBook, adr: Address) = ({
+ require(addressBookInvariant(ab))
+ AddressBook(ab.business, Cons(adr, ab.pers))
+ }) ensuring(res => addressBookInvariant(res))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = ({
+ require(addressBookInvariant(ab))
+ AddressBook(Cons(adr, ab.business), ab.pers)
+ }) ensuring(res => addressBookInvariant(res))
+
+ def isEmpty(ab: AddressBook) = sizeA(ab) == 0
+
+ def contentA(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+ def merge(l1: List, l2: List): List = (l1 match {
+ case Nil => l2
+ case Cons(a, tail) => Cons(a, merge(tail, l2))
+ }) ensuring(res => size(res)==size(l1) + size(l2) &&
+ (!allPrivate(l1) || !allPrivate(l2) || allPrivate(res)) &&
+ (!allBusiness(l1) || !allBusiness(l2) || !allBusiness(res))
+ )
+
+ def mergeAddressBooks(ab1: AddressBook, ab2: AddressBook) = {
+ require(addressBookInvariant(ab1) && addressBookInvariant(ab2))
+ choose {
+ (res: AddressBook) =>
+ (sizeA(res) == sizeA(ab1) + sizeA(ab2)) && addressBookInvariant(res)
+ }
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e29c6dfc97fc2953b189bfd5deb58658423786e6
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
@@ -0,0 +1,73 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ phoneNumber: Int
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def isEmpty(ab: AddressBook) = size(ab) == 0
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+ def makeAddressBook(l: List): AddressBook = (l match {
+ case Nil => AddressBook(Nil, Nil)
+ case Cons(a, l1) => {
+ val res = makeAddressBook(l1)
+ if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+ else AddressBook(Cons(a, res.business), res.pers)
+ }
+ }) ensuring {
+ (res: AddressBook) =>
+ size(res) == size(l) && addressBookInvariant(res)
+ }
+
+ def merge(l1: List, l2: List): List = {
+ choose((res:List) => size(res) == size(l1) + size(l2) &&
+ (!allBusiness(l1) || !allBusiness(l2) ||allBusiness(res)) &&
+ (!allPrivate(l1) || !allPrivate(l2) ||allPrivate(res)))
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ddf3ca49b60afdb16894c93bda4d6cf4780615b5
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
@@ -0,0 +1,83 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ phoneNumber: Int
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def isEmpty(ab: AddressBook) = size(ab) == 0
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+ def makeAddressBook(l: List): AddressBook = (l match {
+ case Nil => AddressBook(Nil, Nil)
+ case Cons(a, l1) => {
+ val res = makeAddressBook(l1)
+ if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+ else AddressBook(Cons(a, res.business), res.pers)
+ }
+ }) ensuring {
+ (res: AddressBook) =>
+ size(res) == size(l) && addressBookInvariant(res)
+ }
+
+ def merge(l1: List, l2: List): List = (l1 match {
+ case Nil => l2
+ case Cons(a, tail) => Cons(a, merge(tail, l2))
+ }) ensuring(res => size(res) == size(l1) + size(l2) &&
+ (!allBusiness(l1) || !allBusiness(l2) ||allBusiness(res)) &&
+ (!allPrivate(l1) || !allPrivate(l2) ||allPrivate(res)))
+
+ def mergeAddressBooks(ab1: AddressBook, ab2: AddressBook) = {
+ require(addressBookInvariant(ab1) && addressBookInvariant(ab2))
+ choose {
+ (res: AddressBook) =>
+ (size(res) == size(ab1) + size(ab2)) && addressBookInvariant(res)
+ }
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4faa50286c879d90d3e9fe12db58856459ee8993
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala
@@ -0,0 +1,49 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = {
+ rev_append(q.f, q.r) == rev_append(f, r) &&
+ { if (q.f == Nil) q.r == Nil else true }
+ }
+
+ def tail(p: Queue): Queue = {
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ }
+
+//(f match {
+// case Nil => Queue(reverse(r), Nil)
+// case _ => Queue(f, r)
+ def checkf(f: List, r: List): Queue = {
+ choose {
+ (res: Queue) =>
+ invariantList(res, f, r)
+ }
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1ede1397ff8e041f160b7fa9cc14fcfaa7c6f687
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala
@@ -0,0 +1,91 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (
+ res =>
+ content(res) == content(aList) ++ content(bList) &&
+ size(res) == size(aList) + size(bList)
+ )
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = ({
+ rev_append(q.f, q.r) == rev_append(f, r)
+ }) ensuring (
+ res =>
+ true
+ )
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (
+ res =>
+ content(res) == content(list) && size(res) == size(list)
+ )
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r) &&
+ size(res) == size(f) + size(r) &&
+ invariantList(res, f, r)
+ }
+
+ def head(p: Queue): Set[Int] = (
+ p.f match {
+ case Nil => Set[Int]()
+ case Cons(x, xs) => Set(x)
+ }) ensuring (
+ res =>
+ if (isEmpty(p)) true
+ else content(p) == res ++ content(tail(p)))
+
+ def tail(p: Queue): Queue = {
+ require(!isEmpty(p))
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ } ensuring {
+ (res: Queue) => content(res) ++ head(p) == content(p) &&
+ (if (isEmpty(p)) true
+ else size(res) + 1 == size(p))
+ }
+ //
+ // def last(p: Queue): Int = {
+ // require(!isEmpty(p))
+ // p.r match {
+ // case Nil => reverse(p.f).asInstanceOf[Cons].head
+ // case Cons(x, _) => x
+ // }
+ // }
+
+ def snoc(p: Queue, x: Int): Queue =
+ checkf(p.f, Cons(x, p.r)) ensuring (
+ res =>
+ content(res) == content(p) ++ Set(x) &&
+ size(res) == size(p) + 1 &&
+ (
+ if (isEmpty(p)) true
+ else (content(tail(res)) ++ Set(x) == content(tail(res)) &&
+ size(res.f) == size(p.f))
+ )
+ )
+
+}
diff --git a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6541b33b5dbce7b126d0eeac8b46858d286fa59d
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala
@@ -0,0 +1,60 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = {
+ rev_append(q.f, q.r) == rev_append(f, r) &&
+ { if (q.f == Nil) q.r == Nil else true }
+ }
+
+ def tail(p: Queue): Queue = {
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ }
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r)
+ }
+ //
+ // def last(p: Queue): Int = {
+ // require(!isEmpty(p))
+ // p.r match {
+ // case Nil => reverse(p.f).asInstanceOf[Cons].head
+ // case Cons(x, _) => x
+ // }
+ // }
+
+ def snoc(p: Queue, x: Int): Queue =
+ choose { (res: Queue) =>
+ content(res) == content(p) ++ Set(x) &&
+ (p.f == Nil || content(tail(res)) ++
+ Set(x) == content(tail(res)))
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala b/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0a2fb81ef16751781c525e6981bb3106e07362cd
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala
@@ -0,0 +1,36 @@
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+ sealed abstract class Tree
+ case class Node(left : Tree, value : Int, right : Tree) extends Tree
+ case object Leaf extends Tree
+
+ def content(t : Tree): Set[Int] = t match {
+ case Leaf => Set()
+ case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree): Int = {
+ t match {
+ case Leaf => 0
+ case Node(l, v, r) => size(l) + size(r) + 1
+ }
+ } ensuring { _ >= 0 }
+
+ def insert(in: Tree, v: Int): Tree = choose {
+ (res: Tree) => content(res) == content(in) ++ Set(v)
+ }
+
+ def delete(in: Tree, v: Int): Tree = choose {
+ (res: Tree) => content(res) == content(in) -- Set(v)
+ }
+
+ def union(in1: Tree, in2: Tree): Tree = choose {
+ (res: Tree) => content(res) == content(in1) ++ content(in2)
+ }
+
+ def diff(in1: Tree, in2: Tree): Tree = choose {
+ (res: Tree) => content(res) == content(in1) -- content(in2)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/Church/Batch.scala b/testcases/synthesis/oopsla2013/Church/Batch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..491166f56533c308963396e5e16a5be177a10205
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/Church/Batch.scala
@@ -0,0 +1,25 @@
+import leon.Utils._
+object ChurchNumerals {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n:Num) : Int = {
+ n match {
+ case Z => 0
+ case S(p) => 1 + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) + value(y)
+ }
+ }
+
+ def distinct(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ r != x && r != y
+ }
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala b/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f741708ad50de666a76185664ddef9228e4ed56b
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala
@@ -0,0 +1,48 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object InsertionSort {
+ 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(_, xs) => 1 + size(xs)
+ }) ensuring (_ >= 0)
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x, xs) => contents(xs) ++ Set(x)
+ }
+
+ 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))
+ }
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def insert(e: Int, l: List): List = {
+ l match {
+ case Nil() => Cons(e, Nil())
+ case Cons(x, xs) =>
+ if (x <= e) Cons(x, sortedIns(e, xs))
+ else Cons(e, l)
+ }
+ } ensuring (res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1)
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def sort(l: List): List = (l match {
+ case Nil() => Nil()
+ case Cons(x, xs) => sortedIns(x, sort(xs))
+ }) ensuring (res => contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l))
+
+}
diff --git a/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala b/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c9402ee740fb0a48dcb16b56baf3c0bb3c984beb
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala
@@ -0,0 +1,53 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object InsertionSort {
+ 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(_, xs) => 1 + size(xs)
+ }) ensuring (_ >= 0)
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x, xs) => contents(xs) ++ Set(x)
+ }
+
+ 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))
+ }
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def insert(e: Int, l: List): List = {
+ require(isSorted(l))
+ choose { (res: List) =>
+ (
+ contents(res) == contents(l) ++ Set(e) &&
+ isSorted(res) &&
+ size(res) == size(l) + 1)
+ }
+ // l match {
+ // case Nil() => Cons(e, Nil())
+ // case Cons(x, xs) =>
+ // if (x <= e) Cons(x, sortedIns(e, xs))
+ // else Cons(e, l)
+ // }
+ }
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def sort(l: List): List = (l match {
+ case Nil() => Nil()
+ case Cons(x, xs) => insert(x, sort(xs))
+ }) ensuring (res => contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l))
+
+}
diff --git a/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala b/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e75c803ddf86ac9207e6a82273c49d08cc32df7d
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala
@@ -0,0 +1,52 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object InsertionSort {
+ 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(_, xs) => 1 + size(xs)
+ }) ensuring (_ >= 0)
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x, xs) => contents(xs) ++ Set(x)
+ }
+
+ 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))
+ }
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def insert(e: Int, l: List): List = {
+ require(isSorted(l))
+ l match {
+ case Nil() => Cons(e, Nil())
+ case Cons(x, xs) =>
+ if (x <= e) Cons(x, insert(e, xs))
+ else Cons(e, l)
+ }
+ } ensuring (res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1)
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def sort(l: List): List = {
+ choose { (res: List) =>
+ ( contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l))
+ }
+ }
+ // case Nil() => Nil()
+ // case Cons(x, xs) => sortedIns(x, sort(xs))
+
+}
\ No newline at end of file
diff --git a/testcases/synthesis/oopsla2013/List/Batch.scala b/testcases/synthesis/oopsla2013/List/Batch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f008b75755b461c01806245165a31ae8b4071347
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Batch.scala
@@ -0,0 +1,38 @@
+import leon.Annotations._
+import leon.Utils._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object 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 insert(in1: List, v: Int) = choose {
+ (out : List) =>
+ content(out) == content(in1) ++ Set(v)
+ }
+
+ def delete(in1: List, v: Int) = choose {
+ (out : List) =>
+ content(out) == content(in1) -- Set(v)
+ }
+
+ def union(in1: List, in2: List) = choose {
+ (out : List) =>
+ content(out) == content(in1) ++ content(in2)
+ }
+
+ def diff(in1: List, in2: List) = choose {
+ (out : List) =>
+ content(out) == content(in1) -- content(in2)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/List/Split.scala b/testcases/synthesis/oopsla2013/List/Split.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5aa4a8f1f309475a19eb466d0e871c72cab416fb
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Split.scala
@@ -0,0 +1,98 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object 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 insert(in1: List, v: Int): List = {
+ Cons(v, in1)
+ } ensuring { content(_) == content(in1) ++ Set(v) }
+
+ //def insert(in1: List, v: Int) = choose {
+ // (out : List) =>
+ // content(out) == content(in1) ++ Set(v)
+ //}
+
+ def delete(in1: List, v: Int): 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 delete(in1: List, v: Int) = choose {
+ // (out : List) =>
+ // content(out) == 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)
+ //}
+
+ 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)
+ //}
+
+ 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 : Int) : Int = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ // def split(list : List) : (List,List) = (list match {
+ // case Nil => (Nil, Nil)
+ // case Cons(x, Nil) => (Cons(x, Nil), Nil)
+ // case Cons(x1, Cons(x2, xs)) =>
+ // val (s1,s2) = split(xs)
+ // (Cons(x1, s1), Cons(x2, s2))
+ // }) ensuring(res => splitSpec(list, res))
+
+ def split(list : List) : (List,List) = {
+ choose { (res : (List,List)) => splitSpec(list, res) }
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/MergeSort/Complete.scala b/testcases/synthesis/oopsla2013/MergeSort/Complete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a373e82ca551da34c8b56a4f9fe64022da66e952
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/MergeSort/Complete.scala
@@ -0,0 +1,85 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst: List, snd: List) extends PairAbs
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x, xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x, xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list: List): Int = list match {
+ case Nil() => 0
+ case Cons(x, xs) => 1 + size(xs)
+ }
+
+ def splithelper(aList: List, bList: List, n: Int): Pair = {
+ if (n <= 0) Pair(aList, bList)
+ else
+ bList match {
+ case Nil() => Pair(aList, bList)
+ case Cons(x, xs) => splithelper(Cons(x, aList), xs, n - 1)
+ }
+ } ensuring (res =>
+ contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd)
+ &&
+ size(aList) + size(bList) == size(res.fst) + size(res.snd)
+ )
+
+ def split(list: List): Pair = {
+ splithelper(Nil(), list, 2)
+ } ensuring (res =>
+ contents(list) == contents(res.fst) ++ contents(res.snd)
+ &&
+ size(list) == size(res.fst) + size(res.snd)
+ )
+
+ def merge(aList: List, bList: List): List = {
+ require(isSorted(aList) && isSorted(bList))
+ bList match {
+ case Nil() => aList
+ case Cons(x, xs) =>
+ aList match {
+ case Nil() => bList
+ case Cons(y, ys) =>
+ if (y < x)
+ Cons(y, merge(ys, bList))
+ else
+ Cons(x, merge(aList, xs))
+ }
+ }
+ } ensuring (res => contents(res) ==
+ contents(aList) ++ contents(bList) && isSorted(res) &&
+ size(res) == size(aList) + size(bList)
+ )
+
+ def isEmpty(list: List): Boolean = list match {
+ case Nil() => true
+ case Cons(x, xs) => false
+ }
+
+ def sort(list: List): List = {
+ list match {
+ case Nil() => list
+ case Cons(x, Nil()) => list
+ case _ =>
+ merge(sort(split(list).fst), sort(split(list).snd))
+ }
+ } ensuring (res => contents(res) == contents(list) && isSorted(res) && size(res) == size(list))
+
+}
diff --git a/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..987c538c4ab36dc9b378f03fc24592210bcbd62b
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala
@@ -0,0 +1,86 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst : List, snd : List) extends PairAbs
+
+ def contents(l : List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l : List) : Boolean = l match {
+ case Nil() => true
+ case Cons(x,xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list : List) : Int = list match {
+ case Nil() => 0
+ case Cons(x,xs) => 1 + size(xs)
+ }
+
+ def splithelper(aList : List, bList : List, n : Int) : Pair = {
+ if (n <= 0) Pair(aList,bList)
+ else
+ bList match {
+ case Nil() => Pair(aList,bList)
+ case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+ }
+ } ensuring(res => contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd))
+
+// def split(list : List, n : Int): Pair = {
+// splithelper(Nil(),list,n)
+// } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def split(list: List): Pair = {
+ splithelper(Nil(),list,size(list)/2)
+ } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def merge(aList : List, bList : List) : List = {
+ require(isSorted(aList) && isSorted(bList))
+ bList match {
+ case Nil() => aList
+ case Cons(x,xs) =>
+ aList match {
+ case Nil() => bList
+ case Cons(y,ys) =>
+ if (y < x)
+ Cons(y,merge(ys, bList))
+ else
+ Cons(x,merge(aList, xs))
+ }
+ }
+ } ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+
+ def isEmpty(list: List) : Boolean = list match {
+ case Nil() => true
+ case Cons(x,xs) => false
+ }
+
+ def sort(list : List) : List = choose {
+
+ (res : List) =>
+ contents(res) == contents(list) && isSorted(res)
+
+// list match {
+// case Nil() => list
+// case Cons(x,Nil()) => list
+// case _ =>
+// val p = split(list,size(list)/2)
+// merge(mergeSort(p.fst), mergeSort(p.snd))
+
+// merge(mergeSort(split(list).fst), mergeSort(split(list).snd))
+ }
+
+ //ensuring(res => contents(res) == contents(list) && isSorted(res))
+
+}
diff --git a/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2cccf5c98753a362235d4fb423e2621e84de534a
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala
@@ -0,0 +1,85 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst : List, snd : List) extends PairAbs
+
+ def contents(l : List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l : List) : Boolean = l match {
+ case Nil() => true
+ case Cons(x,xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list : List) : Int = list match {
+ case Nil() => 0
+ case Cons(x,xs) => 1 + size(xs)
+ }
+
+ def splithelper(aList : List, bList : List, n : Int) : Pair = {
+ if (n <= 0) Pair(aList,bList)
+ else
+ bList match {
+ case Nil() => Pair(aList,bList)
+ case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+ }
+ } ensuring(res => contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd))
+
+// def split(list : List, n : Int): Pair = {
+// splithelper(Nil(),list,n)
+// } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def split(list: List): Pair = {
+ splithelper(Nil(),list,size(list)/2)
+ } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def merge(aList : List, bList : List) : List = {
+ require(isSorted(aList) && isSorted(bList))
+ bList match {
+ case Nil() => aList
+ case Cons(x,xs) =>
+ aList match {
+ case Nil() => bList
+ case Cons(y,ys) =>
+ if (y < x)
+ Cons(y,merge(ys, bList))
+ else
+ Cons(x,merge(aList, xs))
+ }
+ }
+ } ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+
+ def isEmpty(list: List) : Boolean = list match {
+ case Nil() => true
+ case Cons(x,xs) => false
+ }
+
+ def sort(list : List) : List =
+ list match {
+ case Nil() => list
+ case Cons(_,Nil()) => list
+ case _ => {
+ val p = split(list)
+ choose {(res : List) =>
+ contents(res) == contents(list) && isSorted(res)
+ }
+ }
+ }
+
+// merge(mergeSort(split(list).fst), mergeSort(split(list).snd))
+
+ //ensuring(res => contents(res) == contents(list) && isSorted(res))
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Batch.scala b/testcases/synthesis/oopsla2013/SortedList/Batch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..adb1f6de92b69e8aa80c56076fa69113b82dce83
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Batch.scala
@@ -0,0 +1,89 @@
+import leon.Annotations._
+import leon.Utils._
+
+object SortedList {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object 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(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 insert(in1: List, v: Int) = {
+ require(isSorted(in1))
+
+ choose {
+ (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+ }
+
+ def delete(in1: List, v: Int) = {
+ require(isSorted(in1))
+
+ choose {
+ (out : List) =>
+ isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ }
+ }
+
+ def union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+
+ choose {
+ (out : List) =>
+ && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+ }
+
+ def diff(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+
+ choose {
+ (out : List) =>
+ && (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ }
+ }
+
+ // ***********************
+ // Sorting algorithms
+ // ***********************
+
+ 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 : Int) : Int = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def sortSpec(in : List, out : List) : Boolean = {
+ content(out) == content(in) && isSorted(out)
+ }
+
+ def split(list : List) : (List,List) = {
+ choose { (res : (List,List)) => splitSpec(list, res) }
+ }
+
+ def sort(list: List): List = choose {
+ (res: List) => sortSpec(list, res)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Complete.scala b/testcases/synthesis/oopsla2013/SortedList/Complete.scala
index b83a876a3ef6e16c9c707e8dddfd94fcf83a332c..ca1086c4c92a5bbbd71027cc80fe848f2f027be2 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Complete.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Complete.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,7 +40,7 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- //def insert1(in1: List, v: Int) = choose {
+ //def insert(in1: List, v: Int) = choose {
// (out : List) =>
// isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
//}
@@ -92,7 +92,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- union(t1, insert1(in2, h1))
+ union(t1, insert(in2, h1))
case Nil =>
in2
}
@@ -152,7 +152,7 @@ object Complete {
def sort1(in : List) : List = (in match {
case Nil => Nil
- case Cons(x, xs) => insert1(sort1(xs), x)
+ case Cons(x, xs) => insert(sort1(xs), x)
}) ensuring(res => sortSpec(in, res))
// Not really quicksort, neither mergesort.
diff --git a/testcases/synthesis/oopsla2013/SortedList/Delete.scala b/testcases/synthesis/oopsla2013/SortedList/Delete.scala
index 1b99aeb00e24864515d72b8844b94043ae9cba4c..c3ebd3f787f8b0a83d491017903d341431f5c1d7 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Delete.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Delete.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
// def delete(in1: List, v: Int): List = {
// require(isSorted(in1))
// in1 match {
@@ -73,8 +56,12 @@ object Complete {
// }
// } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
- def delete(in1: List, v: Int) = choose {
- (out : List) =>
- isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ def delete(in1: List, v: Int) = {
+ require(isSorted(in1))
+
+ choose {
+ (out : List) =>
+ (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ }
}
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Diff.scala b/testcases/synthesis/oopsla2013/SortedList/Diff.scala
index 4dd0df64f5833882470f8301505a4e034b9f4173..e4fa1dca9968a64e12e7e1264a3c495cca0341f9 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Diff.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Diff.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -77,7 +60,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- union(t1, insert1(in2, h1))
+ union(t1, insert(in2, h1))
case Nil =>
in2
}
@@ -93,9 +76,13 @@ object Complete {
// }
// } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
- def diff(in1: List, in2: List) = choose {
- (out : List) =>
- isSorted(in1) && isSorted(in2) && (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ def diff(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+
+ choose {
+ (out : List) =>
+ (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ }
}
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Insert1.scala b/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
index 1b93466404a5e4ab840a16bfaaf85c1841ee72ba..f790fd50c074ca8b96175d30ff88d50dfeffbe98 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- // def insert1(in1: List, v: Int): List = {
+ // def insert(in1: List, v: Int): List = {
// require(isSorted(in1))
// in1 match {
// case Cons(h, t) =>
@@ -32,16 +32,17 @@ object Complete {
// } else if (v == h) {
// in1
// } else {
- // Cons(h, insert1(t, v))
+ // Cons(h, insert(t, v))
// }
// case Nil =>
// Cons(v, Nil)
// }
// } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert1(in1: List, v: Int) = choose {
- (out : List) =>
- isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
- }
+ def insert(in1: List, v: Int) = {
+ require(isSorted(in1))
+ choose { (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out) }
+ }
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Insert2.scala b/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
index 98c7331e9271dcc8b5dd9a30474ffdb2ea9a0050..14556e667609a3b7846400a8d9c5851be91eb5df 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
@@ -39,9 +39,13 @@ object Complete {
// }
// } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
- def insert2(in1: List, v: Int) = choose {
- (out : List) =>
- isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out) && size(out) == size(in1) + 1
+ def insert2(in1: List, v: Int) = {
+ require(isSorted(in1))
+
+ choose {
+ (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out) && size(out) == size(in1) + 1
+ }
}
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Sort.scala b/testcases/synthesis/oopsla2013/SortedList/Sort.scala
index 03619f39ede7c65f87d535d85d0f90fd601ad4ff..721ea6fa94324be438c7df7386803723c5b06e4b 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Sort.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Sort.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -77,7 +60,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- insert1(union(t1, in2), h1)
+ insert(union(t1, in2), h1)
case Nil =>
in2
}
@@ -123,7 +106,7 @@ object Complete {
// def sort1(in : List) : List = (in match {
// case Nil => Nil
- // case Cons(x, xs) => insert1(sort1(xs), x)
+ // case Cons(x, xs) => insert(sort1(xs), x)
// }) ensuring(res => sortSpec(in, res))
// // Not really quicksort, neither mergesort.
diff --git a/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala b/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d3bf0090d78d199001e03a2e113d5734ef1f8908
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala
@@ -0,0 +1,105 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object 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(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 insert(in1: List, v: Int): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h, t) =>
+ if (v < h) {
+ Cons(v, in1)
+ } else if (v == h) {
+ in1
+ } else {
+ Cons(h, insert(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+
+ def delete(in1: List, v: Int): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h,t) =>
+ if (h < v) {
+ Cons(h, delete(t, v))
+ } else if (h == v) {
+ delete(t, v)
+ } else {
+ in1
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+ def union(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2))
+ in1 match {
+ case Cons(h1, t1) =>
+ insert(union(t1, in2), h1)
+ case Nil =>
+ in2
+ }
+ } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+ def diff(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2))
+ in2 match {
+ case Cons(h2, t2) =>
+ diff(delete(in1, h2), t2)
+ case Nil =>
+ in1
+ }
+ } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+ // ***********************
+ // Sorting algorithms
+ // ***********************
+ def sortSpec(in : List, out : List) : Boolean = {
+ content(out) == content(in) && isSorted(out)
+ }
+
+ // def sort1(in : List) : List = (in match {
+ // case Nil => Nil
+ // case Cons(x, xs) => insert(sort1(xs), x)
+ // }) ensuring(res => sortSpec(in, res))
+
+ // // Not really quicksort, neither mergesort.
+ // def sort2(in : List) : List = (in match {
+ // case Nil => Nil
+ // case Cons(x, Nil) => Cons(x, Nil)
+ // case _ =>
+ // val (s1,s2) = split(in)
+ // union(sort2(s1), sort2(s2))
+ // }) ensuring(res => sortSpec(in, res))
+
+ def sort(list: List): List = choose {
+ (res: List) => sortSpec(list, res)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala b/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bf0794fe7da0fe43d24f32bd401cec2040973f5a
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala
@@ -0,0 +1,114 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def abs(i : Int) : Int = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ 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(in1: List, v: Int): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h,t) =>
+ if (h < v) {
+ Cons(h, delete(t, v))
+ } else if (h == v) {
+ delete(t, v)
+ } else {
+ in1
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+ def union(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2) && abs(size(in1)-size(in2)) <= 1)
+ (in1, in2) match {
+ case (Cons(h1, t1), Cons(h2, t2)) =>
+ if (h1 < h2) {
+ Cons(h1, union(t1, Cons(h2, t2)))
+ } else {
+ Cons(h2, union(Cons(h1, t1), t2))
+ }
+ case (Nil, l2) =>
+ l2
+ case (l1, Nil) =>
+ l1
+ }
+ } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+ def diff(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2))
+ in2 match {
+ case Cons(h2, t2) =>
+ diff(delete(in1, h2), t2)
+ case Nil =>
+ in1
+ }
+ } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+ // ***********************
+ // Sorting algorithms
+ // ***********************
+
+ 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 sortSpec(in : List, out : List) : Boolean = {
+ content(out) == content(in) && isSorted(out)
+ }
+
+
+ def split(list : List) : (List,List) = (list match {
+ case Nil => (Nil, Nil)
+ case Cons(x, Nil) => (Cons(x, Nil), Nil)
+ case Cons(x1, Cons(x2, xs)) =>
+ val (s1,s2) = split(xs)
+ (Cons(x1, s1), Cons(x2, s2))
+ }) ensuring(res => splitSpec(list, res))
+
+ // def sort1(in : List) : List = (in match {
+ // case Nil => Nil
+ // case Cons(x, xs) => insert(sort1(xs), x)
+ // }) ensuring(res => sortSpec(in, res))
+
+ // // Not really quicksort, neither mergesort.
+ // def sort2(in : List) : List = (in match {
+ // case Nil => Nil
+ // case Cons(x, Nil) => Cons(x, Nil)
+ // case _ =>
+ // val (s1,s2) = split(in)
+ // union(sort2(s1), sort2(s2))
+ // }) ensuring(res => sortSpec(in, res))
+
+ def sort(list: List): List = choose {
+ (res: List) => sortSpec(list, res)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala b/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala
new file mode 100644
index 0000000000000000000000000000000000000000..daff218c9e334f496621dce2db05128d9338017f
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala
@@ -0,0 +1,124 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def abs(i : Int) : Int = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ 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(in1: List, v: Int): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h,t) =>
+ if (h < v) {
+ Cons(h, delete(t, v))
+ } else if (h == v) {
+ delete(t, v)
+ } else {
+ in1
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+ def union(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2) && abs(size(in1)-size(in2)) <= 1)
+ (in1, in2) match {
+ case (Cons(h1, t1), Cons(h2, t2)) =>
+ if (h1 < h2) {
+ Cons(h1, union(t1, Cons(h2, t2)))
+ } else {
+ Cons(h2, union(Cons(h1, t1), t2))
+ }
+ case (Nil, l2) =>
+ l2
+ case (l1, Nil) =>
+ l1
+ }
+ } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+ def diff(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2))
+ in2 match {
+ case Cons(h2, t2) =>
+ diff(delete(in1, h2), t2)
+ case Nil =>
+ in1
+ }
+ } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+ // ***********************
+ // Sorting algorithms
+ // ***********************
+
+ 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 sortSpec(in : List, out : List) : Boolean = {
+ content(out) == content(in) && isSorted(out)
+ }
+
+
+ def split(list : List) : (List,List) = (list match {
+ case Nil => (Nil, Nil)
+ case Cons(x, Nil) => (Cons(x, Nil), Nil)
+ case Cons(x1, Cons(x2, xs)) =>
+ val (s1,s2) = split(xs)
+ (Cons(x1, s1), Cons(x2, s2))
+ }) ensuring(res => splitSpec(list, res))
+
+ // def sort1(in : List) : List = (in match {
+ // case Nil => Nil
+ // case Cons(x, xs) => insert(sort1(xs), x)
+ // }) ensuring(res => sortSpec(in, res))
+
+ // // Not really quicksort, neither mergesort.
+ // def sort2(in : List) : List = (in match {
+ // case Nil => Nil
+ // case Cons(x, Nil) => Cons(x, Nil)
+ // case _ =>
+ // val (s1,s2) = split(in)
+ // union(sort2(s1), sort2(s2))
+ // }) ensuring(res => sortSpec(in, res))
+
+ def sort(list: List): List = (list match {
+ case Nil => Nil
+ case Cons(_, Nil) => list
+ case _ => split(list) match {
+ case (l1, l2) =>
+ val r1 = sort(l1)
+ val r2 = sort(l2)
+
+ choose {
+ (res: List) => sortSpec(list, res)
+ }
+ }
+ }) ensuring { res => size(res) == size(list) && sortSpec(list, res) }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split.scala b/testcases/synthesis/oopsla2013/SortedList/Split.scala
index 5d28846ea8e278912fbd0a801830def580d58234..485146c3cccb22decb7341bd71107df7868d8ddb 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -77,7 +60,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- union(t1, insert1(in2, h1))
+ union(t1, insert(in2, h1))
case Nil =>
in2
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split1.scala b/testcases/synthesis/oopsla2013/SortedList/Split1.scala
index daa3b9deb6d493b320a152578832670481a44ccc..ef2090109ac1a0e33d3157b9013d5ca92bb431b4 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split1.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split1.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -77,7 +60,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- union(t1, insert1(in2, h1))
+ union(t1, insert(in2, h1))
case Nil =>
in2
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split2.scala b/testcases/synthesis/oopsla2013/SortedList/Split2.scala
index fcdcf7b68abc51190d2568ec4217b555c14f70f7..37192748ca474c4711ac0b39b01f0ca0523ee0c0 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split2.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split2.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -77,7 +60,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- union(t1, insert1(in2, h1))
+ union(t1, insert(in2, h1))
case Nil =>
in2
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split3.scala b/testcases/synthesis/oopsla2013/SortedList/Split3.scala
index 1042be56e875482207c585ac820bb4cb0c8b952a..f764e19e9d4fbfb6bdfb45eef0815f8b77c3d818 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split3.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split3.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -77,7 +60,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- union(t1, insert1(in2, h1))
+ union(t1, insert(in2, h1))
case Nil =>
in2
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Union.scala b/testcases/synthesis/oopsla2013/SortedList/Union.scala
index 394ca3a7a82a4e541838f8df725abb9e10770da3..5d8767c31ca795cf2d7c9b3ccc79f0e4673213f1 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Union.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Union.scala
@@ -24,7 +24,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -33,7 +33,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -41,23 +41,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -78,7 +61,7 @@ object Complete {
// require(isSorted(in1) && isSorted(in2))
// in1 match {
// case Cons(h1, t1) =>
- // union(t1, insert1(in2, h1))
+ // union(t1, insert(in2, h1))
// case Nil =>
// in2
// }
diff --git a/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala b/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ffaf5f1d14fda31062d75de13f7e7fea7f51b42c
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala
@@ -0,0 +1,52 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object 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(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 union(in1: List, in2: List): List = {
+ // require(isSorted(in1) && isSorted(in2))
+ // in1 match {
+ // case Cons(h1, t1) =>
+ // union(t1, insert(in2, h1))
+ // case Nil =>
+ // in2
+ // }
+ // } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+/*
+ def union(in1: List, in2: List) = choose {
+ (out : List) =>
+ isSorted(in1) && isSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+*/
+
+ def union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose { (out : List) =>
+ (in1!= Cons(10,Cons(20,Cons(30,Cons(40,Nil)))) ||
+ in2!= Cons(11,Cons(13,Cons(25,Cons(45,Cons(48,Cons(60,Nil)))))) ||
+ out == Cons(10,Cons(11,Cons(13,Cons(20,Cons(25,Cons(30,Cons(40,Cons(45,Cons(48,Cons(60,Nil))))))))))) &&
+ (content(out) == content(in1) ++ content(in2)) && isSorted(out) }
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Batch.scala b/testcases/synthesis/oopsla2013/SparseVector/Batch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..230aa7ff234d92d2d16c1ec6685b2218b1eab85e
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SparseVector/Batch.scala
@@ -0,0 +1,63 @@
+import leon.Annotations._
+import leon.Utils._
+
+object SparseVector {
+ sealed abstract class SparseVector
+ case class Cons(index: Int, value : Int, tail: SparseVector) extends SparseVector
+ case object Nil extends SparseVector
+
+ sealed abstract class Option
+ case class Some(v: Int) extends Option
+ case object None extends Option
+
+ def size(sv: SparseVector): Int = {
+ sv match {
+ case Cons(i, v, t) =>
+ 1 + size(t)
+ case Nil =>
+ 0
+ }
+ } ensuring { _ >= 0 }
+
+ def isDefined(o: Option) = o match {
+ case Some(v) => true
+ case None => false
+ }
+
+ def valueOf(o: Option) = o match {
+ case Some(v) => v
+ case None => -42
+ }
+
+ def values(sv: SparseVector): Set[Int] = sv match {
+ case Cons(i, v, t) =>
+ values(t) ++ Set(v)
+ case Nil =>
+ Set()
+ }
+
+ def indices(sv: SparseVector): Set[Int] = sv match {
+ case Cons(i, v, t) =>
+ indices(t) ++ Set(i)
+ case Nil =>
+ Set()
+ }
+
+ def invariant(sv: SparseVector): Boolean = sv match {
+ case Cons(i1, v1, t1 @ Cons(i2, v2, t2)) =>
+ (i1 < i2) && invariant(t1)
+ case _ => true
+ }
+
+ def set(sv: SparseVector, at: Int, newV: Int): SparseVector = choose {
+ (res: SparseVector) => invariant(sv) && (values(res) contains newV) && invariant(res) && (indices(res) == indices(sv) ++ Set(at))
+ }
+
+ def delete(sv: SparseVector, at: Int): SparseVector = choose {
+ (res: SparseVector) => invariant(sv) && (size(res) <= size(sv)) && invariant(res) && (indices(res) == indices(sv) -- Set(at))
+ }
+
+ def get(sv: SparseVector, at: Int): Option = choose {
+ (res: Option) => invariant(sv) && ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res)))
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0be1a7af69055152efe5155bb1af3d72cf56057b
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala
@@ -0,0 +1,46 @@
+import leon.Annotations._
+import leon.Utils._
+
+object StrictSortedList {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object 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(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 insert(in1: List, v: Int) = choose {
+ (out : List) =>
+ isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+
+ def delete(in1: List, v: Int) = choose {
+ (out : List) =>
+ isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ }
+
+ def union(in1: List, in2: List) = choose {
+ (out : List) =>
+ isSorted(in1) && isSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+
+ def diff(in1: List, in2: List) = choose {
+ (out : List) =>
+ isSorted(in1) && isSorted(in2) && (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
index a0b56fa9da45474b70a1af440932ad26fe931aa3..4b04ae60de3a718d5a83329573d2730c7e3d2cc0 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
@@ -56,8 +56,9 @@ object Delete {
// }
// } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
- def delete(in1: List, v: Int) = choose {
- (out : List) =>
- isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ def delete(in1: List, v: Int) = {
+ require(isSorted(in1))
+ choose {(out : List) => content(out) == content(in1) -- Set(v) &&
+ isSorted(out) }
}
}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
index eea2a1eac8c87156e7a90df8510275bc4b2dff02..aa38b4ca139c7315657d0d4593673394df6c5683 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
@@ -76,9 +76,9 @@ object Complete {
// }
// } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
- def diff(in1: List, in2: List) = choose {
- (out : List) =>
- isSorted(in1) && isSorted(in2) && (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ def diff(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose((out : List) =>
+ content(out) == content(in1) -- content(in2) && isSorted(out))
}
-
}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
index 31344aec35684ccb34b5cbcce1f1f32e52f2c035..cac8b1551cfe361b443668b46b2840d7defabaf2 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
@@ -39,9 +39,10 @@ object Complete {
// }
// } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert(in1: List, v: Int) = choose {
- (out : List) =>
- isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ def insert(in1: List, v: Int) = {
+ require(isSorted(in1))
+ choose((out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out))
}
}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
index e44158330eba8111f27db44aa32d703a7ba87d4d..c990996b415fbee85b97a01b9fc3e012f74f5f65 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
@@ -66,8 +66,10 @@ object Complete {
// }
//} ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
- def union(in1: List, in2: List) = choose {
- (out : List) =>
- isSorted(in1) && isSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ def union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose( (out : List) => (content(out) == content(in1) ++ content(in2)) &&
+ isSorted(out)
+ )
}
}