diff --git a/src/test/resources/regression/synthesis/Church/Add.scala b/src/test/resources/regression/synthesis/Church/Add.scala
index d060360c201b590095b5bac16a6a2e8218a4352f..694f76a15a00b1fc666b372336f3d7baaa6b77d7 100644
--- a/src/test/resources/regression/synthesis/Church/Add.scala
+++ b/src/test/resources/regression/synthesis/Church/Add.scala
@@ -1,27 +1,21 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
-object ChurchNumerals {
+object Numerals {
sealed abstract class Num
case object Z extends Num
case class S(pred: Num) extends Num
- def value(n:Num) : Int = {
+ def value(n: Num): BigInt = {
n match {
case Z => 0
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
- // def add(x : Num, y : Num) : Num = (x match {
- // case Z => y
- // case S(p) => add(p, S(y))
- // }) ensuring (value(_) == value(x) + value(y))
-
def add(x: Num, y: Num): Num = {
- choose { (r : Num) =>
+ choose { (r: Num) =>
value(r) == value(x) + value(y)
}
}
diff --git a/src/test/resources/regression/synthesis/Church/Distinct.scala b/src/test/resources/regression/synthesis/Church/Distinct.scala
index 3e503f4ab896d5632d8f9ea2e5f1a5a8d1203625..827d8d70f8f5a860447897e86f62d5f5f19d529d 100644
--- a/src/test/resources/regression/synthesis/Church/Distinct.scala
+++ b/src/test/resources/regression/synthesis/Church/Distinct.scala
@@ -1,37 +1,24 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
import leon.lang._
import leon.lang.synthesis._
-object ChurchNumerals {
+import leon.annotation._
+
+object Numerals {
sealed abstract class Num
case object Z extends Num
case class S(pred: Num) extends Num
- def value(n:Num) : Int = {
+ def value(n: Num): BigInt = {
n match {
case Z => 0
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
- def add(x : Num, y : Num) : Num = (x match {
+ def add(x: Num, y: Num): Num = (x match {
case Z => y
case S(p) => add(p, S(y))
}) ensuring (value(_) == value(x) + value(y))
- //def distinct(x : Num, y : Num) : Num = (x match {
- // case Z =>
- // S(y)
-
- // case S(p) =>
- // y match {
- // case Z =>
- // S(x)
- // case S(p) =>
- // Z
- // }
- //}) ensuring (res => res != x && res != y)
-
def distinct(x: Num, y: Num): Num = {
choose { (r : Num) =>
r != x && r != y
diff --git a/src/test/resources/regression/synthesis/Church/Mult.scala b/src/test/resources/regression/synthesis/Church/Mult.scala
index 39c0286d08edb25a8c3e737da5f9175dd5202c1d..1e58606d07d6bb78de617fa90d6129052007624b 100644
--- a/src/test/resources/regression/synthesis/Church/Mult.scala
+++ b/src/test/resources/regression/synthesis/Church/Mult.scala
@@ -1,40 +1,26 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
-object ChurchNumerals {
+object Numerals {
sealed abstract class Num
case object Z extends Num
case class S(pred: Num) extends Num
- def value(n:Num) : Int = {
+ def value(n: Num): BigInt = {
n match {
case Z => 0
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
- def add(x : Num, y : Num) : Num = (x match {
+ def add(x: Num, y: Num): Num = (x match {
case Z => y
case S(p) => add(p, S(y))
}) ensuring (value(_) == value(x) + value(y))
- //def distinct(x : Num, y : Num) : Num = (x match {
- // case Z =>
- // S(y)
-
- // case S(p) =>
- // y match {
- // case Z =>
- // S(x)
- // case S(p) =>
- // Z
- // }
- //}) ensuring (res => res != x && res != y)
-
def mult(x: Num, y: Num): Num = {
- choose { (r : Num) =>
+ choose { (r: Num) =>
value(r) == value(x) * value(y)
}
}
diff --git a/src/test/resources/regression/synthesis/Church/Squared.scala b/src/test/resources/regression/synthesis/Church/Squared.scala
index 9328e70ff65874a445d41f2c01635f3d9ca2311a..32b05900f7c4527287b5f92f24bb8c053899b484 100644
--- a/src/test/resources/regression/synthesis/Church/Squared.scala
+++ b/src/test/resources/regression/synthesis/Church/Squared.scala
@@ -1,38 +1,19 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
-object ChurchNumerals {
+object Numerals {
sealed abstract class Num
case object Z extends Num
case class S(pred: Num) extends Num
- def value(n:Num) : Int = {
+ def value(n:Num) : BigInt = {
n match {
case Z => 0
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
- def add(x : Num, y : Num) : Num = (x match {
- case Z => y
- case S(p) => add(p, S(y))
- }) ensuring (value(_) == value(x) + value(y))
-
- //def distinct(x : Num, y : Num) : Num = (x match {
- // case Z =>
- // S(y)
-
- // case S(p) =>
- // y match {
- // case Z =>
- // S(x)
- // case S(p) =>
- // Z
- // }
- //}) ensuring (res => res != x && res != y)
-
def mult(x: Num, y: Num): Num = (y match {
case S(p) =>
add(mult(x, p), x)
@@ -41,7 +22,7 @@ object ChurchNumerals {
}) ensuring { value(_) == value(x) * value(y) }
def squared(x: Num): Num = {
- choose { (r : Num) =>
+ choose { (r: Num) =>
value(r) == value(x) * value(x)
}
}
diff --git a/src/test/resources/regression/synthesis/List/Delete.scala b/src/test/resources/regression/synthesis/List/Delete.scala
index 02f13ec3837b5b96b2ace88269ecede8fd7744d2..a548f46e2507bc4e95754bd1d512175260af1a49 100644
--- a/src/test/resources/regression/synthesis/List/Delete.scala
+++ b/src/test/resources/regression/synthesis/List/Delete.scala
@@ -1,43 +1,25 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.annotation._
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
object Delete {
sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
+ case class Cons(head: BigInt, tail: List) extends List
case object Nil extends List
- def size(l: List) : Int = (l match {
+ def size(l: List) : BigInt = (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]
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
case Cons(i, t) => Set(i) ++ content(t)
}
- def insert(in1: List, v: Int): List = {
- Cons(v, in1)
- } ensuring { content(_) == 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) =>
+ def delete(in1: List, v: BigInt) = {
+ choose { (out : List) =>
content(out) == content(in1) -- Set(v)
+ }
}
}
diff --git a/src/test/resources/regression/synthesis/List/Diff.scala b/src/test/resources/regression/synthesis/List/Diff.scala
index 5ae469ea7c04e6373707ad9d6083798f2d5fe16a..0943955b170124ef788132a529ae0dd7ee9b55bb 100644
--- a/src/test/resources/regression/synthesis/List/Diff.scala
+++ b/src/test/resources/regression/synthesis/List/Diff.scala
@@ -1,29 +1,23 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.annotation._
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
object Diff {
sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
+ case class Cons(head: BigInt, tail: List) extends List
case object Nil extends List
- def size(l: List) : Int = (l match {
+ def size(l: List) : BigInt = (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]
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
case Cons(i, t) => Set(i) ++ content(t)
}
- def insert(in1: List, v: Int): List = {
- Cons(v, in1)
- } ensuring { content(_) == content(in1) ++ Set(v) }
-
- def delete(in1: List, v: Int): List = {
+ def delete(in1: List, v: BigInt): List = {
in1 match {
case Cons(h,t) =>
if (h == v) {
@@ -36,26 +30,9 @@ object Diff {
}
} ensuring { content(_) == content(in1) -- Set(v) }
- def union(in1: List, in2: List): List = {
- in1 match {
- case Cons(h, t) =>
- Cons(h, union(t, in2))
- case Nil =>
- in2
- }
- } ensuring { content(_) == content(in1) ++ content(in2) }
-
- // def 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) =>
+ def diff(in1: List, in2: List) = {
+ choose { (out : List) =>
content(out) == content(in1) -- content(in2)
+ }
}
}
diff --git a/src/test/resources/regression/synthesis/List/Insert.scala b/src/test/resources/regression/synthesis/List/Insert.scala
index 0a2cb88b0efa17ab1498b71bac764c55504c1f96..62e91d9b92c1d87008d1192f2f9e5c68580ef1ec 100644
--- a/src/test/resources/regression/synthesis/List/Insert.scala
+++ b/src/test/resources/regression/synthesis/List/Insert.scala
@@ -1,30 +1,25 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.annotation._
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
object Insert {
sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
+ case class Cons(head: BigInt, tail: List) extends List
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => BigInt(0)
- case Cons(_, t) => size(t) + 1
+ 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]
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
case Cons(i, t) => Set(i) ++ content(t)
}
- //def insert(in1: List, v: Int): List = {
- // Cons(v, in1)
- //} ensuring { content(_) == content(in1) ++ Set(v) }
-
- def insert(in1: List, v: Int) = choose {
- (out : List) =>
+ def insert(in1: List, v: BigInt) = {
+ choose { (out : List) =>
content(out) == content(in1) ++ Set(v)
+ }
}
}
diff --git a/src/test/resources/regression/synthesis/List/Split.scala b/src/test/resources/regression/synthesis/List/Split.scala
deleted file mode 100644
index 989d509da8018aca3f96be9834275796258887f3..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/synthesis/List/Split.scala
+++ /dev/null
@@ -1,101 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.annotation._
-import leon.lang._
-import leon.lang.synthesis._
-
-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/src/test/resources/regression/synthesis/List/Split1.scala b/src/test/resources/regression/synthesis/List/Split1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..facbda843c5a6349cc6efca052bf104ec63f7156
--- /dev/null
+++ b/src/test/resources/regression/synthesis/List/Split1.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def abs(i: BigInt) : BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def split(list: List): (List, List) = {
+ choose { (res: (List, List)) =>
+ (content(res._1) ++ content(res._2) == content(list))
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/List/Split2.scala b/src/test/resources/regression/synthesis/List/Split2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..38c07caf52566eb6f599e2557900b1ed83a53c37
--- /dev/null
+++ b/src/test/resources/regression/synthesis/List/Split2.scala
@@ -0,0 +1,31 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def abs(i: BigInt) : BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def split(list: List): (List, List) = {
+ choose { (res : (List, List)) =>
+ (content(res._1) ++ content(res._2) == content(list)) &&
+ (abs(size(res._1) - size(res._2)) <= 1)
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/List/Split3.scala b/src/test/resources/regression/synthesis/List/Split3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..15c74190e1839abb484b375b28fea1582d8d58ea
--- /dev/null
+++ b/src/test/resources/regression/synthesis/List/Split3.scala
@@ -0,0 +1,36 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def abs(i: BigInt): BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def tcons(h1: BigInt, h2: BigInt, tl: (List, List)) = {
+ (Cons(h1, tl._1), Cons(h2, tl._2))
+ }
+
+ def split(list : List): (List,List) = {
+ choose { (res: (List,List)) =>
+ (content(res._1) ++ content(res._2) == content(list)) &&
+ (abs(size(res._1) - size(res._2)) <= 1) &&
+ (size(res._1) + size(res._2) == size(list))
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/List/Union.scala b/src/test/resources/regression/synthesis/List/Union.scala
index a4acf629b8a4ec2bbb22e7f95a46af965b18fd63..0b21dc0375c63b438f810acb9bdcd4f04ef25b36 100644
--- a/src/test/resources/regression/synthesis/List/Union.scala
+++ b/src/test/resources/regression/synthesis/List/Union.scala
@@ -1,52 +1,25 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.annotation._
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
object Union {
sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
+ case class Cons(head: BigInt, tail: List) extends List
case object Nil extends List
- def size(l: List) : Int = (l match {
+ def size(l: List) : BigInt = (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]
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
case Cons(i, t) => Set(i) ++ content(t)
}
- def insert(in1: List, v: Int): List = {
- Cons(v, in1)
- } ensuring { content(_) == 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 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) =>
+ def union(in1: List, in2: List) = {
+ choose { (out : List) =>
content(out) == content(in1) ++ content(in2)
+ }
}
}
diff --git a/src/test/resources/regression/synthesis/SortedList/Delete.scala b/src/test/resources/regression/synthesis/SortedList/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..31305ca094ec78fa6896985fad04729879839baf
--- /dev/null
+++ b/src/test/resources/regression/synthesis/SortedList/Delete.scala
@@ -0,0 +1,33 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def delete(in1: List, v: BigInt) = {
+ require(isSorted(in1))
+ choose { (out: List) =>
+ (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ }
+ }
+}
diff --git a/src/test/resources/regression/synthesis/SortedList/Diff.scala b/src/test/resources/regression/synthesis/SortedList/Diff.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9e4e32baeebb42ca25bd4dfec41e7b0303c80f53
--- /dev/null
+++ b/src/test/resources/regression/synthesis/SortedList/Diff.scala
@@ -0,0 +1,50 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def delete(in1: List, v: BigInt): 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 diff(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose { (out: List) =>
+ (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/SortedList/Insert1.scala b/src/test/resources/regression/synthesis/SortedList/Insert1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..affc5b45512a0383b49d11ca2c008df3d28b8d06
--- /dev/null
+++ b/src/test/resources/regression/synthesis/SortedList/Insert1.scala
@@ -0,0 +1,34 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt) = {
+ require(isSorted(in1))
+ choose { (out: List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/SortedList/Insert2.scala b/src/test/resources/regression/synthesis/SortedList/Insert2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e44eac286849ac69c19991168398ffad67726f5d
--- /dev/null
+++ b/src/test/resources/regression/synthesis/SortedList/Insert2.scala
@@ -0,0 +1,34 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt) = {
+ require(isSorted(in1))
+ choose { (out: List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out) && size(out) == size(in1) + 1
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/SortedList/InsertSort.scala b/src/test/resources/regression/synthesis/SortedList/InsertSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8f5b78247b9877952f9a7e17cdf507f424d16b05
--- /dev/null
+++ b/src/test/resources/regression/synthesis/SortedList/InsertSort.scala
@@ -0,0 +1,51 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt): 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 sort(list: List): List = {
+ choose { (res: List) =>
+ isSorted(res) &&
+ content(list) == content(res)
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/SortedList/Union.scala b/src/test/resources/regression/synthesis/SortedList/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..95d17bb61bb48927a2d189ccecf1b7330b4bb46e
--- /dev/null
+++ b/src/test/resources/regression/synthesis/SortedList/Union.scala
@@ -0,0 +1,50 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt): 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 union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose { (out: List) =>
+ (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+ }
+}
diff --git a/src/test/resources/regression/synthesis/StrictSortedList/Delete.scala b/src/test/resources/regression/synthesis/StrictSortedList/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..81827ed03b80beddf664e2b0c2beb62a43dad078
--- /dev/null
+++ b/src/test/resources/regression/synthesis/StrictSortedList/Delete.scala
@@ -0,0 +1,33 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Delete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def delete(in1: List, v: BigInt) = {
+ require(isSorted(in1))
+ choose { (out : List) =>
+ (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ }
+ }
+}
diff --git a/src/test/resources/regression/synthesis/StrictSortedList/Insert.scala b/src/test/resources/regression/synthesis/StrictSortedList/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6c7543ad3847671bfc8657dc5c99e2bbd236ed93
--- /dev/null
+++ b/src/test/resources/regression/synthesis/StrictSortedList/Insert.scala
@@ -0,0 +1,34 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt) = {
+ require(isSorted(in1))
+ choose { (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/StrictSortedList/Union.scala b/src/test/resources/regression/synthesis/StrictSortedList/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cf2fcd727323d6b5c705522f3d37b884bdfd896d
--- /dev/null
+++ b/src/test/resources/regression/synthesis/StrictSortedList/Union.scala
@@ -0,0 +1,50 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt): 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 union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose { (out : List) =>
+ (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+ }
+}