From 018e2a8af8bf8ecc40254d6ecab45583aea8ee94 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 12 Feb 2016 18:36:15 +0100
Subject: [PATCH] Add current benchmarks, new benchmark List[T].indexOfOpt with
variants
---
testcases/synthesis/PrimeHeuristic.scala.off | 11 --
.../{ => archives}/ADTInduction.scala | 0
.../synthesis/{ => archives}/BinaryTree.scala | 0
.../{ => archives}/CegisExamples.scala | 0
.../{ => archives}/CegisFunctions.scala | 0
.../{ => archives}/ChooseArith.scala | 0
.../synthesis/{ => archives}/ChooseIneq.scala | 0
.../synthesis/{ => archives}/ChoosePos.scala | 0
.../{ => archives}/ChurchNumerals.scala | 0
.../synthesis/{ => archives}/DrSuter.scala | 0
.../synthesis/{ => archives}/FastExp.scala | 0
.../synthesis/{ => archives}/FiniteSort.scala | 0
.../synthesis/{ => archives}/Injection.scala | 0
.../synthesis/{ => archives}/InnerSplit.scala | 0
.../synthesis/{ => archives}/Justify.scala | 0
.../synthesis/{ => archives}/Matching.scala | 0
.../{ => archives}/ScaleWeight.scala | 0
.../synthesis/{ => archives}/Sec2Time.scala | 0
.../{ => archives}/SimplestCegis.scala | 0
testcases/synthesis/{ => archives}/Spt.scala | 0
.../{ => archives}/Unification.scala | 0
.../synthesis/{ => archives}/ZuneBug.scala | 0
.../synthesis/current/AddressBook/Make.scala | 66 ++++++++
.../synthesis/current/AddressBook/Merge.scala | 69 +++++++++
.../current/BatchedQueue/Dequeue.scala | 80 ++++++++++
.../current/BatchedQueue/Enqueue.scala | 83 ++++++++++
.../synthesis/current/Compiler/Desugar.scala | 118 ++++++++++++++
.../current/Compiler/DesugarImplies.scala | 144 ++++++++++++++++++
.../current/Compiler/RewriteImplies.scala | 124 +++++++++++++++
.../current/Compiler/RewriteMinus.scala | 107 +++++++++++++
testcases/synthesis/current/List/Delete.scala | 26 ++++
testcases/synthesis/current/List/Diff.scala | 50 ++++++
.../synthesis/current/List/IndexOfInt.scala | 67 ++++++++
.../synthesis/current/List/IndexOfOpt.scala | 65 ++++++++
.../synthesis/current/List/IndexOfOpt2.scala | 67 ++++++++
testcases/synthesis/current/List/Insert.scala | 28 ++++
testcases/synthesis/current/List/Split.scala | 37 +++++
testcases/synthesis/current/List/Union.scala | 37 +++++
.../synthesis/current/Parentheses/Par.scala | 54 +++++++
.../synthesis/current/SortedList/Delete.scala | 34 +++++
.../synthesis/current/SortedList/Diff.scala | 53 +++++++
.../synthesis/current/SortedList/Insert.scala | 34 +++++
.../current/SortedList/InsertAlways.scala | 34 +++++
.../current/SortedList/InsertionSort.scala | 49 ++++++
.../current/SortedList/MergeSort.scala | 62 ++++++++
.../current/SortedList/MergeSortGuided.scala | 68 +++++++++
.../synthesis/current/SortedList/Union.scala | 51 +++++++
.../current/StrictSortedList/Delete.scala | 34 +++++
.../current/StrictSortedList/Insert.scala | 34 +++++
.../current/StrictSortedList/Union.scala | 51 +++++++
.../synthesis/current/UnaryNumerals/Add.scala | 21 +++
.../current/UnaryNumerals/Distinct.scala | 30 ++++
.../current/UnaryNumerals/Mult.scala | 30 ++++
testcases/synthesis/current/run.sh | 43 ++++++
54 files changed, 1850 insertions(+), 11 deletions(-)
delete mode 100644 testcases/synthesis/PrimeHeuristic.scala.off
rename testcases/synthesis/{ => archives}/ADTInduction.scala (100%)
rename testcases/synthesis/{ => archives}/BinaryTree.scala (100%)
rename testcases/synthesis/{ => archives}/CegisExamples.scala (100%)
rename testcases/synthesis/{ => archives}/CegisFunctions.scala (100%)
rename testcases/synthesis/{ => archives}/ChooseArith.scala (100%)
rename testcases/synthesis/{ => archives}/ChooseIneq.scala (100%)
rename testcases/synthesis/{ => archives}/ChoosePos.scala (100%)
rename testcases/synthesis/{ => archives}/ChurchNumerals.scala (100%)
rename testcases/synthesis/{ => archives}/DrSuter.scala (100%)
rename testcases/synthesis/{ => archives}/FastExp.scala (100%)
rename testcases/synthesis/{ => archives}/FiniteSort.scala (100%)
rename testcases/synthesis/{ => archives}/Injection.scala (100%)
rename testcases/synthesis/{ => archives}/InnerSplit.scala (100%)
rename testcases/synthesis/{ => archives}/Justify.scala (100%)
rename testcases/synthesis/{ => archives}/Matching.scala (100%)
rename testcases/synthesis/{ => archives}/ScaleWeight.scala (100%)
rename testcases/synthesis/{ => archives}/Sec2Time.scala (100%)
rename testcases/synthesis/{ => archives}/SimplestCegis.scala (100%)
rename testcases/synthesis/{ => archives}/Spt.scala (100%)
rename testcases/synthesis/{ => archives}/Unification.scala (100%)
rename testcases/synthesis/{ => archives}/ZuneBug.scala (100%)
create mode 100644 testcases/synthesis/current/AddressBook/Make.scala
create mode 100644 testcases/synthesis/current/AddressBook/Merge.scala
create mode 100644 testcases/synthesis/current/BatchedQueue/Dequeue.scala
create mode 100644 testcases/synthesis/current/BatchedQueue/Enqueue.scala
create mode 100644 testcases/synthesis/current/Compiler/Desugar.scala
create mode 100644 testcases/synthesis/current/Compiler/DesugarImplies.scala
create mode 100644 testcases/synthesis/current/Compiler/RewriteImplies.scala
create mode 100644 testcases/synthesis/current/Compiler/RewriteMinus.scala
create mode 100644 testcases/synthesis/current/List/Delete.scala
create mode 100644 testcases/synthesis/current/List/Diff.scala
create mode 100644 testcases/synthesis/current/List/IndexOfInt.scala
create mode 100644 testcases/synthesis/current/List/IndexOfOpt.scala
create mode 100644 testcases/synthesis/current/List/IndexOfOpt2.scala
create mode 100644 testcases/synthesis/current/List/Insert.scala
create mode 100644 testcases/synthesis/current/List/Split.scala
create mode 100644 testcases/synthesis/current/List/Union.scala
create mode 100644 testcases/synthesis/current/Parentheses/Par.scala
create mode 100644 testcases/synthesis/current/SortedList/Delete.scala
create mode 100644 testcases/synthesis/current/SortedList/Diff.scala
create mode 100644 testcases/synthesis/current/SortedList/Insert.scala
create mode 100644 testcases/synthesis/current/SortedList/InsertAlways.scala
create mode 100644 testcases/synthesis/current/SortedList/InsertionSort.scala
create mode 100644 testcases/synthesis/current/SortedList/MergeSort.scala
create mode 100644 testcases/synthesis/current/SortedList/MergeSortGuided.scala
create mode 100644 testcases/synthesis/current/SortedList/Union.scala
create mode 100644 testcases/synthesis/current/StrictSortedList/Delete.scala
create mode 100644 testcases/synthesis/current/StrictSortedList/Insert.scala
create mode 100644 testcases/synthesis/current/StrictSortedList/Union.scala
create mode 100644 testcases/synthesis/current/UnaryNumerals/Add.scala
create mode 100644 testcases/synthesis/current/UnaryNumerals/Distinct.scala
create mode 100644 testcases/synthesis/current/UnaryNumerals/Mult.scala
create mode 100755 testcases/synthesis/current/run.sh
diff --git a/testcases/synthesis/PrimeHeuristic.scala.off b/testcases/synthesis/PrimeHeuristic.scala.off
deleted file mode 100644
index 31a689935..000000000
--- a/testcases/synthesis/PrimeHeuristic.scala.off
+++ /dev/null
@@ -1,11 +0,0 @@
-import leon.lang._
-
-object PrimeHeuristic {
- def maybePrime(n: Int): Boolean = n match {
- case 2 * k => false
- case 3 * k => false
- case 6 * k - 1 => true
- case 6 * k + 1 => true
- }
-
-}
diff --git a/testcases/synthesis/ADTInduction.scala b/testcases/synthesis/archives/ADTInduction.scala
similarity index 100%
rename from testcases/synthesis/ADTInduction.scala
rename to testcases/synthesis/archives/ADTInduction.scala
diff --git a/testcases/synthesis/BinaryTree.scala b/testcases/synthesis/archives/BinaryTree.scala
similarity index 100%
rename from testcases/synthesis/BinaryTree.scala
rename to testcases/synthesis/archives/BinaryTree.scala
diff --git a/testcases/synthesis/CegisExamples.scala b/testcases/synthesis/archives/CegisExamples.scala
similarity index 100%
rename from testcases/synthesis/CegisExamples.scala
rename to testcases/synthesis/archives/CegisExamples.scala
diff --git a/testcases/synthesis/CegisFunctions.scala b/testcases/synthesis/archives/CegisFunctions.scala
similarity index 100%
rename from testcases/synthesis/CegisFunctions.scala
rename to testcases/synthesis/archives/CegisFunctions.scala
diff --git a/testcases/synthesis/ChooseArith.scala b/testcases/synthesis/archives/ChooseArith.scala
similarity index 100%
rename from testcases/synthesis/ChooseArith.scala
rename to testcases/synthesis/archives/ChooseArith.scala
diff --git a/testcases/synthesis/ChooseIneq.scala b/testcases/synthesis/archives/ChooseIneq.scala
similarity index 100%
rename from testcases/synthesis/ChooseIneq.scala
rename to testcases/synthesis/archives/ChooseIneq.scala
diff --git a/testcases/synthesis/ChoosePos.scala b/testcases/synthesis/archives/ChoosePos.scala
similarity index 100%
rename from testcases/synthesis/ChoosePos.scala
rename to testcases/synthesis/archives/ChoosePos.scala
diff --git a/testcases/synthesis/ChurchNumerals.scala b/testcases/synthesis/archives/ChurchNumerals.scala
similarity index 100%
rename from testcases/synthesis/ChurchNumerals.scala
rename to testcases/synthesis/archives/ChurchNumerals.scala
diff --git a/testcases/synthesis/DrSuter.scala b/testcases/synthesis/archives/DrSuter.scala
similarity index 100%
rename from testcases/synthesis/DrSuter.scala
rename to testcases/synthesis/archives/DrSuter.scala
diff --git a/testcases/synthesis/FastExp.scala b/testcases/synthesis/archives/FastExp.scala
similarity index 100%
rename from testcases/synthesis/FastExp.scala
rename to testcases/synthesis/archives/FastExp.scala
diff --git a/testcases/synthesis/FiniteSort.scala b/testcases/synthesis/archives/FiniteSort.scala
similarity index 100%
rename from testcases/synthesis/FiniteSort.scala
rename to testcases/synthesis/archives/FiniteSort.scala
diff --git a/testcases/synthesis/Injection.scala b/testcases/synthesis/archives/Injection.scala
similarity index 100%
rename from testcases/synthesis/Injection.scala
rename to testcases/synthesis/archives/Injection.scala
diff --git a/testcases/synthesis/InnerSplit.scala b/testcases/synthesis/archives/InnerSplit.scala
similarity index 100%
rename from testcases/synthesis/InnerSplit.scala
rename to testcases/synthesis/archives/InnerSplit.scala
diff --git a/testcases/synthesis/Justify.scala b/testcases/synthesis/archives/Justify.scala
similarity index 100%
rename from testcases/synthesis/Justify.scala
rename to testcases/synthesis/archives/Justify.scala
diff --git a/testcases/synthesis/Matching.scala b/testcases/synthesis/archives/Matching.scala
similarity index 100%
rename from testcases/synthesis/Matching.scala
rename to testcases/synthesis/archives/Matching.scala
diff --git a/testcases/synthesis/ScaleWeight.scala b/testcases/synthesis/archives/ScaleWeight.scala
similarity index 100%
rename from testcases/synthesis/ScaleWeight.scala
rename to testcases/synthesis/archives/ScaleWeight.scala
diff --git a/testcases/synthesis/Sec2Time.scala b/testcases/synthesis/archives/Sec2Time.scala
similarity index 100%
rename from testcases/synthesis/Sec2Time.scala
rename to testcases/synthesis/archives/Sec2Time.scala
diff --git a/testcases/synthesis/SimplestCegis.scala b/testcases/synthesis/archives/SimplestCegis.scala
similarity index 100%
rename from testcases/synthesis/SimplestCegis.scala
rename to testcases/synthesis/archives/SimplestCegis.scala
diff --git a/testcases/synthesis/Spt.scala b/testcases/synthesis/archives/Spt.scala
similarity index 100%
rename from testcases/synthesis/Spt.scala
rename to testcases/synthesis/archives/Spt.scala
diff --git a/testcases/synthesis/Unification.scala b/testcases/synthesis/archives/Unification.scala
similarity index 100%
rename from testcases/synthesis/Unification.scala
rename to testcases/synthesis/archives/Unification.scala
diff --git a/testcases/synthesis/ZuneBug.scala b/testcases/synthesis/archives/ZuneBug.scala
similarity index 100%
rename from testcases/synthesis/ZuneBug.scala
rename to testcases/synthesis/archives/ZuneBug.scala
diff --git a/testcases/synthesis/current/AddressBook/Make.scala b/testcases/synthesis/current/AddressBook/Make.scala
new file mode 100644
index 000000000..612effe38
--- /dev/null
+++ b/testcases/synthesis/current/AddressBook/Make.scala
@@ -0,0 +1,66 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object AddressBookMake {
+
+ case class Address[A](info: A, priv: Boolean)
+
+ sealed abstract class AddressList[A] {
+ def size: BigInt = {
+ this match {
+ case Nil() => BigInt(0)
+ case Cons(head, tail) => BigInt(1) + tail.size
+ }
+ } ensuring { res => res >= 0 }
+
+ def content: Set[Address[A]] = this match {
+ case Nil() => Set[Address[A]]()
+ case Cons(addr, l1) => Set(addr) ++ l1.content
+ }
+ }
+
+ case class Cons[A](a: Address[A], tail: AddressList[A]) extends AddressList[A]
+ case class Nil[A]() extends AddressList[A]
+
+ def allPersonal[A](l: AddressList[A]): Boolean = l match {
+ case Nil() => true
+ case Cons(a, l1) =>
+ if (a.priv) allPersonal(l1)
+ else false
+ }
+
+ def allBusiness[A](l: AddressList[A]): Boolean = l match {
+ case Nil() => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook[A](business: AddressList[A], personal: AddressList[A]) {
+ def size: BigInt = business.size + personal.size
+
+ def content: Set[Address[A]] = business.content ++ personal.content
+
+ def invariant = {
+ allPersonal(personal) && allBusiness(business)
+ }
+ }
+
+ def makeAddressBook[A](as: AddressList[A]): AddressBook[A] = {
+ choose( (res: AddressBook[A]) => res.content == as.content && res.invariant )
+
+ /* as match {
+ case Nil() => AddressBook[A](Nil[A](), Nil[A]())
+ case Cons(x, xs) =>
+ val AddressBook(b, p) = makeAddressBook(xs)
+ if(x.priv) AddressBook(b, Cons(x, p))
+ else AddressBook(Cons(x, b), p)
+ }
+
+ } ensuring {
+ res => res.content == as.content && res.invariant */
+ }
+
+
+}
diff --git a/testcases/synthesis/current/AddressBook/Merge.scala b/testcases/synthesis/current/AddressBook/Merge.scala
new file mode 100644
index 000000000..92a5b5bfe
--- /dev/null
+++ b/testcases/synthesis/current/AddressBook/Merge.scala
@@ -0,0 +1,69 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object AddressBookMake {
+
+ case class Address[A](info: A, priv: Boolean)
+
+ sealed abstract class AddressList[A] {
+ def size: BigInt = {
+ this match {
+ case Nil() => BigInt(0)
+ case Cons(head, tail) => BigInt(1) + tail.size
+ }
+ } ensuring { res => res >= 0 }
+
+ def content: Set[Address[A]] = this match {
+ case Nil() => Set[Address[A]]()
+ case Cons(addr, l1) => Set(addr) ++ l1.content
+ }
+
+ def ++(that: AddressList[A]): AddressList[A] = {
+ this match {
+ case Cons(h, t) => Cons(h, t ++ that)
+ case Nil() => that
+ }
+ } ensuring {
+ res => res.content == this.content ++ that.content
+ }
+ }
+
+ case class Cons[A](a: Address[A], tail: AddressList[A]) extends AddressList[A]
+ case class Nil[A]() extends AddressList[A]
+
+ def allPersonal[A](l: AddressList[A]): Boolean = l match {
+ case Nil() => true
+ case Cons(a, l1) =>
+ if (a.priv) allPersonal(l1)
+ else false
+ }
+
+ def allBusiness[A](l: AddressList[A]): Boolean = l match {
+ case Nil() => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook[A](business: AddressList[A], personal: AddressList[A]) {
+ def size: BigInt = business.size + personal.size
+
+ def content: Set[Address[A]] = business.content ++ personal.content
+
+ @inline
+ def invariant = {
+ allPersonal(personal) && allBusiness(business)
+ }
+ }
+
+ def merge[A](a1: AddressBook[A], a2: AddressBook[A]): AddressBook[A] = {
+ require(a1.invariant && a2.invariant)
+
+ choose( (res: AddressBook[A]) =>
+ res.personal.content == (a1.personal.content ++ a2.personal.content) &&
+ res.business.content == (a1.business.content ++ a2.business.content) &&
+ res.invariant
+ )
+ }
+}
diff --git a/testcases/synthesis/current/BatchedQueue/Dequeue.scala b/testcases/synthesis/current/BatchedQueue/Dequeue.scala
new file mode 100644
index 000000000..c44fc0628
--- /dev/null
+++ b/testcases/synthesis/current/BatchedQueue/Dequeue.scala
@@ -0,0 +1,80 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object BatchedQueue {
+ sealed abstract class List[T] {
+ def content: Set[T] = {
+ this match {
+ case Cons(h, t) => Set(h) ++ t.content
+ case Nil() => Set()
+ }
+ }
+
+ def size: BigInt = {
+ this match {
+ case Cons(h, t) => BigInt(1) + t.size
+ case Nil() => BigInt(0)
+ }
+ } ensuring { _ >= 0 }
+
+ def reverse: List[T] = {
+ this match {
+ case Cons(h, t) => t.reverse.append(Cons(h, Nil[T]()))
+ case Nil() => Nil[T]()
+ }
+ } ensuring { res =>
+ this.content == res.content
+ }
+
+ def append(r: List[T]): List[T] = {
+ this match {
+ case Cons(h, t) => Cons(h, t.append(r))
+ case Nil() => r
+ }
+ }
+
+ def isEmpty: Boolean = {
+ this == Nil[T]()
+ }
+
+ def tail: List[T] = {
+ require(this != Nil[T]())
+ this match {
+ case Cons(h, t) => t
+ }
+ }
+
+ def head: T = {
+ require(this != Nil[T]())
+ this match {
+ case Cons(h, t) => h
+ }
+ }
+ }
+
+ case class Cons[T](h: T, t: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+ case class Queue[T](f: List[T], r: List[T]) {
+ def content: Set[T] = f.content ++ r.content
+ def size: BigInt = f.size + r.size
+
+ def isEmpty: Boolean = f.isEmpty && r.isEmpty
+
+ def invariant: Boolean = {
+ (f.isEmpty) ==> (r.isEmpty)
+ }
+
+ def toList: List[T] = f.append(r.reverse)
+
+ def dequeue: Queue[T] = {
+ require(invariant && !isEmpty)
+
+ choose { (res: Queue[T]) =>
+ res.size == size-1 && res.toList == this.toList.tail && res.invariant
+ }
+ }
+ }
+
+ val test = Queue[BigInt](Cons(42, Nil()), Nil()).dequeue
+}
diff --git a/testcases/synthesis/current/BatchedQueue/Enqueue.scala b/testcases/synthesis/current/BatchedQueue/Enqueue.scala
new file mode 100644
index 000000000..0f30a5ba1
--- /dev/null
+++ b/testcases/synthesis/current/BatchedQueue/Enqueue.scala
@@ -0,0 +1,83 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object BatchedQueue {
+ sealed abstract class List[T] {
+ def content: Set[T] = {
+ this match {
+ case Cons(h, t) => Set(h) ++ t.content
+ case Nil() => Set()
+ }
+ }
+
+ def size: BigInt = {
+ this match {
+ case Cons(h, t) => BigInt(1) + t.size
+ case Nil() => BigInt(0)
+ }
+ } ensuring { _ >= 0 }
+
+ def reverse: List[T] = {
+ this match {
+ case Cons(h, t) => t.reverse.append(Cons(h, Nil[T]()))
+ case Nil() => Nil[T]()
+ }
+ } ensuring { res =>
+ this.content == res.content
+ }
+
+ def append(r: List[T]): List[T] = {
+ this match {
+ case Cons(h, t) => Cons(h, t.append(r))
+ case Nil() => r
+ }
+ }
+
+ def tail: List[T] = {
+ require(this != Nil[T]())
+ this match {
+ case Cons(h, t) => t
+ }
+ }
+
+ def head: T = {
+ require(this != Nil[T]())
+ this match {
+ case Cons(h, t) => h
+ }
+ }
+
+ def last: T = {
+ require(this != Nil[T]())
+ this match {
+ case Cons(h, Nil()) => h
+ case Cons(h, t) => t.last
+ }
+ }
+ }
+
+ case class Cons[T](h: T, t: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+ case class Queue[T](f: List[T], r: List[T]) {
+ def content: Set[T] = f.content ++ r.content
+ def size: BigInt = f.size + r.size
+
+ def invariant: Boolean = {
+ (f == Nil[T]()) ==> (r == Nil[T]())
+ }
+
+ def toList: List[T] = f.append(r.reverse)
+
+ def enqueue(v: T): Queue[T] = {
+ require(invariant)
+
+ ???[Queue[T]]
+ } ensuring { (res: Queue[T]) =>
+ res.invariant &&
+ res.toList.last == v &&
+ res.size == size + 1 &&
+ res.content == this.content ++ Set(v)
+ }
+ }
+}
diff --git a/testcases/synthesis/current/Compiler/Desugar.scala b/testcases/synthesis/current/Compiler/Desugar.scala
new file mode 100644
index 000000000..2684c71b2
--- /dev/null
+++ b/testcases/synthesis/current/Compiler/Desugar.scala
@@ -0,0 +1,118 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class UMinus(e: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Implies(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+ case class IntLiteral(i: BigInt) extends Expr
+
+ abstract class Value
+ case class BoolValue(b: Boolean) extends Value
+ case class IntValue(i: BigInt) extends Value
+ case object Error extends Value
+
+ def eval(e: Expr): Value = e match {
+ case Plus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+ case _ => Error
+ }
+
+ case Minus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+ case _ => Error
+ }
+
+ case UMinus(l) =>
+ eval(l) match {
+ case IntValue(b) => IntValue(-b)
+ case _ => Error
+ }
+
+ case LessThan(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+ case _ => Error
+ }
+
+ case And(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(false) => b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Or(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Implies(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ eval(r)
+ case b @ BoolValue(false) =>
+ BoolValue(true)
+ case _ => Error
+ }
+
+ case Not(l) =>
+ eval(l) match {
+ case BoolValue(b) => BoolValue(!b)
+ case _ => Error
+ }
+
+ case Eq(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il == ir)
+ case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+ case _ => Error
+ }
+
+ case Ite(c, t, e) =>
+ eval(c) match {
+ case BoolValue(true) => eval(t)
+ case BoolValue(false) => eval(t)
+ case _ => Error
+ }
+
+ case IntLiteral(l) => IntValue(l)
+ case BoolLiteral(b) => BoolValue(b)
+ }
+
+ def rewriteMinus(in: Minus): Expr = {
+ choose{ (out: Expr) =>
+ eval(in) == eval(out) && !(out.isInstanceOf[Minus])
+ }
+ }
+
+ def rewriteImplies(in: Implies): Expr = {
+ choose{ (out: Expr) =>
+ eval(in) == eval(out) && !(out.isInstanceOf[Implies])
+ }
+ }
+
+
+ def plop(x: Expr) = {
+ eval(x) == Error//eval(Not(IntLiteral(BigInt(2))))
+ }.holds
+}
diff --git a/testcases/synthesis/current/Compiler/DesugarImplies.scala b/testcases/synthesis/current/Compiler/DesugarImplies.scala
new file mode 100644
index 000000000..de5c544ff
--- /dev/null
+++ b/testcases/synthesis/current/Compiler/DesugarImplies.scala
@@ -0,0 +1,144 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class UMinus(e: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Implies(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+ case class IntLiteral(i: BigInt) extends Expr
+
+ def exists(e: Expr, f: Expr => Boolean): Boolean = {
+ f(e) || (e match {
+ case Plus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Minus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case LessThan(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case And(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Or(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Implies(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Eq(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Ite(c, t, e) => exists(c, f) || exists(t, f) || exists(e, f)
+ case Not(e) => exists(e, f)
+ case UMinus(e) => exists(e, f)
+ case _ => false
+ })
+ }
+
+ abstract class Value
+ case class BoolValue(b: Boolean) extends Value
+ case class IntValue(i: BigInt) extends Value
+ case object Error extends Value
+
+ def eval(e: Expr): Value = e match {
+ case Plus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+ case _ => Error
+ }
+
+ case Minus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+ case _ => Error
+ }
+
+ case UMinus(l) =>
+ eval(l) match {
+ case IntValue(b) => IntValue(-b)
+ case _ => Error
+ }
+
+ case LessThan(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+ case _ => Error
+ }
+
+ case And(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(false) => b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Or(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Implies(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ eval(r)
+ case b @ BoolValue(false) =>
+ BoolValue(true)
+ case _ => Error
+ }
+
+ case Not(l) =>
+ eval(l) match {
+ case BoolValue(b) => BoolValue(!b)
+ case _ => Error
+ }
+
+ case Eq(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il == ir)
+ case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+ case _ => Error
+ }
+
+ case Ite(c, t, e) =>
+ eval(c) match {
+ case BoolValue(true) => eval(t)
+ case BoolValue(false) => eval(t)
+ case _ => Error
+ }
+
+ case IntLiteral(l) => IntValue(l)
+ case BoolLiteral(b) => BoolValue(b)
+ }
+
+
+ //def desugar(e: Expr): Expr = {
+ // choose{ (out: Expr) =>
+ // eval(e) == eval(out) && !exists(out, f => f.isInstanceOf[Implies])
+ // }
+ //}
+
+ def desugar(e: Expr): Expr = {
+ e match {
+ case Plus(lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Minus(lhs, rhs) => Minus(desugar(lhs), desugar(rhs))
+ case LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case And(lhs, rhs) => And(desugar(lhs), desugar(rhs))
+ case Or(lhs, rhs) => Or(desugar(lhs), desugar(rhs))
+ case Implies(lhs, rhs) => //Implies(desugar(lhs), desugar(rhs))
+ Or(Not(desugar(lhs)), desugar(rhs))
+ case Eq(lhs, rhs) => Eq(desugar(lhs), desugar(rhs))
+ case Ite(c, t, e) => Ite(desugar(c), desugar(t), desugar(e))
+ case Not(e) => Not(desugar(e))
+ case UMinus(e) => UMinus(desugar(e))
+ case e => e
+ }
+ } ensuring { out =>
+ //eval(e) == eval(out) &&
+ !exists(out, f => f.isInstanceOf[Implies])
+ }
+}
diff --git a/testcases/synthesis/current/Compiler/RewriteImplies.scala b/testcases/synthesis/current/Compiler/RewriteImplies.scala
new file mode 100644
index 000000000..4b50b9cbe
--- /dev/null
+++ b/testcases/synthesis/current/Compiler/RewriteImplies.scala
@@ -0,0 +1,124 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class UMinus(e: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Implies(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+ case class IntLiteral(i: BigInt) extends Expr
+
+ def exists(e: Expr, f: Expr => Boolean): Boolean = {
+ f(e) || (e match {
+ case Plus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Minus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case LessThan(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case And(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Or(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Implies(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Eq(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Ite(c, t, e) => exists(c, f) || exists(t, f) || exists(e, f)
+ case Not(e) => exists(e, f)
+ case UMinus(e) => exists(e, f)
+ case _ => false
+ })
+ }
+
+ abstract class Value
+ case class BoolValue(b: Boolean) extends Value
+ case class IntValue(i: BigInt) extends Value
+ case object Error extends Value
+
+ def eval(e: Expr): Value = e match {
+ case Plus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+ case _ => Error
+ }
+
+ case Minus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+ case _ => Error
+ }
+
+ case UMinus(l) =>
+ eval(l) match {
+ case IntValue(b) => IntValue(-b)
+ case _ => Error
+ }
+
+ case LessThan(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+ case _ => Error
+ }
+
+ case And(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(false) => b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Or(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Implies(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ eval(r)
+ case b @ BoolValue(false) =>
+ BoolValue(true)
+ case _ => Error
+ }
+
+ case Not(l) =>
+ eval(l) match {
+ case BoolValue(b) => BoolValue(!b)
+ case _ => Error
+ }
+
+ case Eq(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il == ir)
+ case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+ case _ => Error
+ }
+
+ case Ite(c, t, e) =>
+ eval(c) match {
+ case BoolValue(true) => eval(t)
+ case BoolValue(false) => eval(t)
+ case _ => Error
+ }
+
+ case IntLiteral(l) => IntValue(l)
+ case BoolLiteral(b) => BoolValue(b)
+ }
+
+
+ def desugar(in: Expr): Expr = {
+ choose{ (out: Expr) =>
+ eval(in) == eval(out) && !(out.isInstanceOf[Implies])
+ }
+ }
+}
diff --git a/testcases/synthesis/current/Compiler/RewriteMinus.scala b/testcases/synthesis/current/Compiler/RewriteMinus.scala
new file mode 100644
index 000000000..de2fa4360
--- /dev/null
+++ b/testcases/synthesis/current/Compiler/RewriteMinus.scala
@@ -0,0 +1,107 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class UMinus(e: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Implies(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+ case class IntLiteral(i: BigInt) extends Expr
+
+ abstract class Value
+ case class BoolValue(b: Boolean) extends Value
+ case class IntValue(i: BigInt) extends Value
+ case object Error extends Value
+
+ def eval(e: Expr): Value = e match {
+ case Plus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+ case _ => Error
+ }
+
+ case Minus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+ case _ => Error
+ }
+
+ case UMinus(l) =>
+ eval(l) match {
+ case IntValue(b) => IntValue(-b)
+ case _ => Error
+ }
+
+ case LessThan(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+ case _ => Error
+ }
+
+ case And(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(false) => b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Or(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Implies(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ eval(r)
+ case b @ BoolValue(false) =>
+ BoolValue(true)
+ case _ => Error
+ }
+
+ case Not(l) =>
+ eval(l) match {
+ case BoolValue(b) => BoolValue(!b)
+ case _ => Error
+ }
+
+ case Eq(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il == ir)
+ case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+ case _ => Error
+ }
+
+ case Ite(c, t, e) =>
+ eval(c) match {
+ case BoolValue(true) => eval(t)
+ case BoolValue(false) => eval(t)
+ case _ => Error
+ }
+
+ case IntLiteral(l) => IntValue(l)
+ case BoolLiteral(b) => BoolValue(b)
+ }
+
+ def rewriteMinus(in: Minus): Expr = {
+ choose{ (out: Expr) =>
+ eval(in) == eval(out) && !(out.isInstanceOf[Minus])
+ }
+ }
+}
diff --git a/testcases/synthesis/current/List/Delete.scala b/testcases/synthesis/current/List/Delete.scala
new file mode 100644
index 000000000..30716c591
--- /dev/null
+++ b/testcases/synthesis/current/List/Delete.scala
@@ -0,0 +1,26 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Delete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def delete(in: List, v: BigInt) = {
+ ???[List]
+ } ensuring {
+ (out : List) =>
+ content(out) == content(in) -- Set(v)
+ }
+}
diff --git a/testcases/synthesis/current/List/Diff.scala b/testcases/synthesis/current/List/Diff.scala
new file mode 100644
index 000000000..9fb3ade95
--- /dev/null
+++ b/testcases/synthesis/current/List/Diff.scala
@@ -0,0 +1,50 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Diff {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ Cons(v, in1)
+ } ensuring { content(_) == content(in1) ++ Set(v) }
+
+ def delete(in1: List, v: BigInt): List = {
+ in1 match {
+ case Cons(h,t) =>
+ if (h == v) {
+ delete(t, v)
+ } else {
+ Cons(h, delete(t, v))
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { content(_) == content(in1) -- Set(v) }
+
+ // def diff(in1: List, in2: List): List = {
+ // in2 match {
+ // case Nil =>
+ // in1
+ // case Cons(h, t) =>
+ // diff(delete(in1, h), t)
+ // }
+ // } ensuring { content(_) == content(in1) -- content(in2) }
+
+ def diff(in1: List, in2: List) = choose {
+ (out : List) =>
+ content(out) == content(in1) -- content(in2)
+ }
+}
diff --git a/testcases/synthesis/current/List/IndexOfInt.scala b/testcases/synthesis/current/List/IndexOfInt.scala
new file mode 100644
index 000000000..595d40cf3
--- /dev/null
+++ b/testcases/synthesis/current/List/IndexOfInt.scala
@@ -0,0 +1,67 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object IndexOf {
+ sealed abstract class List[T] {
+ def size: BigInt = {
+ this match {
+ case Nil() => BigInt(0)
+ case Cons(_, t) => BigInt(1) + t.size
+ }
+ } ensuring {
+ res => res >= 0
+ }
+
+ def content: Set[T] = this match {
+ case Nil() => Set.empty[T]
+ case Cons(i, t) => Set(i) ++ t.content
+ }
+
+ def apply(i: BigInt): T = {
+ require(i >= 0 && i < size)
+ this match {
+ case Cons(h, t) =>
+ if (i == 0) {
+ h
+ } else {
+ t.apply(i-1)
+ }
+ }
+ } ensuring { e =>
+ content contains e
+ }
+
+ def indexOfInt(e: T): BigInt = {
+ ???[BigInt]
+
+ //this match {
+ // case Cons(h, t) =>
+ // val r = t.indexOfInt(e)
+
+ // if (e == h) {
+ // BigInt(0)
+ // } else {
+ // if (r < 0) {
+ // r
+ // } else {
+ // r + 1
+ // }
+ // }
+ // case Nil() =>
+ // BigInt(-1)
+ //}
+
+ } ensuring { res =>
+ if (res < 0) {
+ !(content contains e)
+ } else {
+ res < size && apply(res) == e
+ }
+ }
+ }
+
+ case class Cons[T](head: T, tail: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+}
diff --git a/testcases/synthesis/current/List/IndexOfOpt.scala b/testcases/synthesis/current/List/IndexOfOpt.scala
new file mode 100644
index 000000000..6738e5c23
--- /dev/null
+++ b/testcases/synthesis/current/List/IndexOfOpt.scala
@@ -0,0 +1,65 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object IndexOf {
+ sealed abstract class List[T] {
+ def size: BigInt = {
+ this match {
+ case Nil() => BigInt(0)
+ case Cons(_, t) => BigInt(1) + t.size
+ }
+ } ensuring {
+ res => res >= 0
+ }
+
+ def content: Set[T] = this match {
+ case Nil() => Set.empty[T]
+ case Cons(i, t) => Set(i) ++ t.content
+ }
+
+ def apply(i: BigInt): T = {
+ require(i >= 0 && i < size)
+ this match {
+ case Cons(h, t) =>
+ if (i == 0) {
+ h
+ } else {
+ t.apply(i-1)
+ }
+ }
+ } ensuring { e =>
+ content contains e
+ }
+
+ def indexOfOpt(e: T): Option[BigInt] = {
+ ???[Option[BigInt]]
+ /*
+ this match {
+ case Cons(h, t) =>
+ val r = t.indexOfOpt(e)
+
+ if (e == h) {
+ Some(BigInt(0))
+ } else {
+ r match {
+ case Some(i) => Some(i+1)
+ case None() => None[BigInt]()
+ }
+ }
+ case Nil() =>
+ None[BigInt]()
+ }
+ */
+ } ensuring { res =>
+ res match {
+ case None() => !(content contains e)
+ case Some(i) => i >= 0 && i < size && apply(i) == e
+ }
+ }
+ }
+
+ case class Cons[T](head: T, tail: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+}
diff --git a/testcases/synthesis/current/List/IndexOfOpt2.scala b/testcases/synthesis/current/List/IndexOfOpt2.scala
new file mode 100644
index 000000000..ff85f7a1c
--- /dev/null
+++ b/testcases/synthesis/current/List/IndexOfOpt2.scala
@@ -0,0 +1,67 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object IndexOf {
+ sealed abstract class List[T] {
+ def size: BigInt = {
+ this match {
+ case Nil() => BigInt(0)
+ case Cons(_, t) => BigInt(1) + t.size
+ }
+ } ensuring {
+ res => res >= 0
+ }
+
+ def content: Set[T] = this match {
+ case Nil() => Set.empty[T]
+ case Cons(i, t) => Set(i) ++ t.content
+ }
+
+ def apply(i: BigInt): T = {
+ require(i >= 0 && i < size)
+ this match {
+ case Cons(h, t) =>
+ if (i == 0) {
+ h
+ } else {
+ t.apply(i-1)
+ }
+ }
+ } ensuring { e =>
+ content contains e
+ }
+
+ def indexOfOpt(e: T, offset: BigInt): Option[BigInt] = {
+ ???[Option[BigInt]]
+ /*
+ this match {
+ case Cons(h, t) =>
+ val r = t.indexOfOpt(e)
+
+ if (e == h) {
+ Some(BigInt(0))
+ } else {
+ r match {
+ case Some(i) => Some(i+1)
+ case None() => None[BigInt]()
+ }
+ }
+ case Nil() =>
+ None[BigInt]()
+ }
+ */
+ } ensuring { res =>
+ res match {
+ case None() => !(content contains e)
+ case Some(r) =>
+ val i = r - offset;
+ i >= 0 && i < size && apply(i) == e
+ }
+ }
+ }
+
+ case class Cons[T](head: T, tail: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+}
diff --git a/testcases/synthesis/current/List/Insert.scala b/testcases/synthesis/current/List/Insert.scala
new file mode 100644
index 000000000..48c38f4df
--- /dev/null
+++ b/testcases/synthesis/current/List/Insert.scala
@@ -0,0 +1,28 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Insert {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ //def insert(in1: List, v: BigInt): List = {
+ // Cons(v, in1)
+ //} ensuring { content(_) == content(in1) ++ Set(v) }
+
+ def insert(in1: List, v: BigInt) = choose {
+ (out : List) =>
+ content(out) == content(in1) ++ Set(v)
+ }
+}
diff --git a/testcases/synthesis/current/List/Split.scala b/testcases/synthesis/current/List/Split.scala
new file mode 100644
index 000000000..f37e68264
--- /dev/null
+++ b/testcases/synthesis/current/List/Split.scala
@@ -0,0 +1,37 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def splitSpec(list : List, res : (List,List)) : Boolean = {
+ val s1 = size(res._1)
+ val s2 = size(res._2)
+ abs(s1 - s2) <= 1 && s1 + s2 == size(list) &&
+ content(res._1) ++ content(res._2) == content(list)
+ }
+
+ def abs(i : BigInt) : BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def split(list : List) : (List,List) = {
+ choose { (res : (List,List)) => splitSpec(list, res) }
+ }
+
+}
diff --git a/testcases/synthesis/current/List/Union.scala b/testcases/synthesis/current/List/Union.scala
new file mode 100644
index 000000000..d6a5fa579
--- /dev/null
+++ b/testcases/synthesis/current/List/Union.scala
@@ -0,0 +1,37 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Union {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1)+ size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ Cons(v, in1)
+ } ensuring { content(_) == content(in1) ++ Set(v) }
+
+ // def union(in1: List, in2: List): List = {
+ // in1 match {
+ // case Cons(h, t) =>
+ // Cons(h, union(t, in2))
+ // case Nil =>
+ // in2
+ // }
+ // } ensuring { content(_) == content(in1) ++ content(in2) }
+
+ def union(in1: List, in2: List) = choose {
+ (out : List) =>
+ content(out) == content(in1) ++ content(in2)
+ }
+}
diff --git a/testcases/synthesis/current/Parentheses/Par.scala b/testcases/synthesis/current/Parentheses/Par.scala
new file mode 100644
index 000000000..b91213086
--- /dev/null
+++ b/testcases/synthesis/current/Parentheses/Par.scala
@@ -0,0 +1,54 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.collection._
+
+
+object MatchPar {
+ abstract class AbsChar
+ case object OP extends AbsChar
+ case object CP extends AbsChar
+ case object NA extends AbsChar
+
+ def matchPar(l: List[AbsChar]): BigInt = {
+
+ ???[BigInt]
+ /*
+ l match {
+ case Nil() => 0
+ case Cons(h, t) =>
+ val rec = matchPar(t)
+ h match {
+ case OP => 1 + rec
+ case CP => if (rec <= 0) {
+ -1
+ } else {
+ rec - 1
+ }
+ case NA => rec
+ }
+ }*/
+ } ensuring { res =>
+ ((count(OP, l) != count(CP, l)) ==> (res != 0)) &&
+ ((l, res) passes {
+ case Nil() => 0
+ case Cons(OP, Cons(CP, Nil())) => 0
+ case Cons(CP, Cons(OP, _)) => -1
+ case Cons(OP, Cons(OP, Nil())) => 2
+ case Cons(OP, Cons(OP, Cons(CP, Cons(CP, Cons(OP, Cons(CP, Nil())))))) => 0
+ })
+ }
+
+ def count[T](a: T, l: List[T]): BigInt = {
+ l match {
+ case Cons(h, t) =>
+ if (h == a) {
+ 1 + count(a, t)
+ } else {
+ count(a, t)
+ }
+ case Nil() => BigInt(0)
+ }
+ } ensuring { (res: BigInt) =>
+ res >= 0
+ }
+}
diff --git a/testcases/synthesis/current/SortedList/Delete.scala b/testcases/synthesis/current/SortedList/Delete.scala
new file mode 100644
index 000000000..788f232d3
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/Delete.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListDelete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def delete(in: List, v: BigInt) = {
+ require(isSorted(in))
+
+ choose( (res : List) =>
+ (content(res) == content(in) -- Set(v)) && isSorted(res)
+ )
+ }
+}
diff --git a/testcases/synthesis/current/SortedList/Diff.scala b/testcases/synthesis/current/SortedList/Diff.scala
new file mode 100644
index 000000000..d391b85ba
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/Diff.scala
@@ -0,0 +1,53 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListDiff {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def delete(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/testcases/synthesis/current/SortedList/Insert.scala b/testcases/synthesis/current/SortedList/Insert.scala
new file mode 100644
index 000000000..0bf80d1e9
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/Insert.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListInsert {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ require(isSorted(in1))
+
+ choose { (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+ }
+}
diff --git a/testcases/synthesis/current/SortedList/InsertAlways.scala b/testcases/synthesis/current/SortedList/InsertAlways.scala
new file mode 100644
index 000000000..73e0b240d
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/InsertAlways.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListInsertAlways {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insertAlways(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/testcases/synthesis/current/SortedList/InsertionSort.scala b/testcases/synthesis/current/SortedList/InsertionSort.scala
new file mode 100644
index 000000000..0752ad33f
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/InsertionSort.scala
@@ -0,0 +1,49 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListInsertionSort {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def 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 insertionSort(in1: List): List = {
+ choose { (out: List) =>
+ content(out) == content(in1) && isSorted(out)
+ }
+ }
+}
diff --git a/testcases/synthesis/current/SortedList/MergeSort.scala b/testcases/synthesis/current/SortedList/MergeSort.scala
new file mode 100644
index 000000000..7a285c146
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/MergeSort.scala
@@ -0,0 +1,62 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListUnion {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def split(in: List): (List, List) = {
+ in match {
+ case Cons(h1, Cons(h2, t)) =>
+ val r = split(t)
+ (Cons(h1, r._1), Cons(h2, r._2))
+ case Cons(h1, Nil) =>
+ (in, Nil)
+ case Nil =>
+ (Nil, Nil)
+ }
+ }
+
+ def merge(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2))
+ (in1, in2) match {
+ case (Cons(h1, t1), Cons(h2, t2)) =>
+ if (h1 < h2) {
+ Cons(h1, merge(t1, in2))
+ } else {
+ Cons(h2, merge(in1, t2))
+ }
+ case (l, Nil) => l
+ case (Nil, l) => l
+ }
+ } ensuring {
+ (out : List) =>
+ (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+
+ def sort(in: List): List = {
+ ???[List]
+ } ensuring {
+ (out : List) =>
+ content(out) == content(in) && isSorted(out)
+ }
+}
diff --git a/testcases/synthesis/current/SortedList/MergeSortGuided.scala b/testcases/synthesis/current/SortedList/MergeSortGuided.scala
new file mode 100644
index 000000000..0035eceea
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/MergeSortGuided.scala
@@ -0,0 +1,68 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListUnion {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def split(in: List): (List, List) = {
+ in match {
+ case Cons(h1, Cons(h2, t)) =>
+ val r = split(t)
+ (Cons(h1, r._1), Cons(h2, r._2))
+ case Cons(h1, Nil) =>
+ (in, Nil)
+ case Nil =>
+ (Nil, Nil)
+ }
+ }
+
+ def merge(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2))
+ (in1, in2) match {
+ case (Cons(h1, t1), Cons(h2, t2)) =>
+ if (h1 < h2) {
+ Cons(h1, merge(t1, in2))
+ } else {
+ Cons(h2, merge(in1, t2))
+ }
+ case (l, Nil) => l
+ case (Nil, l) => l
+ }
+ } ensuring {
+ (out : List) =>
+ (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+
+ def sort(in: List): List = {
+ in match {
+ case Cons(h1, Cons(h2, t)) =>
+ val s = split(in)
+ merge(sort(s._1), sort(s._2))
+ case _ =>
+ ???[List]
+ }
+ } ensuring {
+ (out : List) =>
+ content(out) == content(in) && isSorted(out)
+ }
+}
diff --git a/testcases/synthesis/current/SortedList/Union.scala b/testcases/synthesis/current/SortedList/Union.scala
new file mode 100644
index 000000000..d3f11adcc
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/Union.scala
@@ -0,0 +1,51 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListUnion {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def 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/testcases/synthesis/current/StrictSortedList/Delete.scala b/testcases/synthesis/current/StrictSortedList/Delete.scala
new file mode 100644
index 000000000..23999d96c
--- /dev/null
+++ b/testcases/synthesis/current/StrictSortedList/Delete.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object StrictSortedListDelete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def delete(in: List, v: BigInt) = {
+ require(isSorted(in))
+
+ choose( (res : List) =>
+ (content(res) == content(in) -- Set(v)) && isSorted(res)
+ )
+ }
+}
diff --git a/testcases/synthesis/current/StrictSortedList/Insert.scala b/testcases/synthesis/current/StrictSortedList/Insert.scala
new file mode 100644
index 000000000..65f3c01f9
--- /dev/null
+++ b/testcases/synthesis/current/StrictSortedList/Insert.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object StrictSortedListInsert {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ require(isSorted(in1))
+
+ choose { (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+ }
+}
diff --git a/testcases/synthesis/current/StrictSortedList/Union.scala b/testcases/synthesis/current/StrictSortedList/Union.scala
new file mode 100644
index 000000000..c10ed419d
--- /dev/null
+++ b/testcases/synthesis/current/StrictSortedList/Union.scala
@@ -0,0 +1,51 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object StrictSortedListUnion {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def 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/testcases/synthesis/current/UnaryNumerals/Add.scala b/testcases/synthesis/current/UnaryNumerals/Add.scala
new file mode 100644
index 000000000..a34d1834f
--- /dev/null
+++ b/testcases/synthesis/current/UnaryNumerals/Add.scala
@@ -0,0 +1,21 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object UnaryNumeralsAdd {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n: Num): BigInt = {
+ n match {
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) + value(y)
+ }
+ }
+}
diff --git a/testcases/synthesis/current/UnaryNumerals/Distinct.scala b/testcases/synthesis/current/UnaryNumerals/Distinct.scala
new file mode 100644
index 000000000..4287378d1
--- /dev/null
+++ b/testcases/synthesis/current/UnaryNumerals/Distinct.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object UnaryNumeralsDistinct {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n: Num): BigInt = {
+ n match {
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x: Num, y: Num): Num = {
+ x match {
+ case S(p) => S(add(p, y))
+ case Z => y
+ }
+ } ensuring { (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/current/UnaryNumerals/Mult.scala b/testcases/synthesis/current/UnaryNumerals/Mult.scala
new file mode 100644
index 000000000..bfa39365e
--- /dev/null
+++ b/testcases/synthesis/current/UnaryNumerals/Mult.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object UnaryNumeralsMult {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n: Num): BigInt = {
+ n match {
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x: Num, y: Num): Num = {
+ x match {
+ case S(p) => S(add(p, y))
+ case Z => y
+ }
+ } ensuring { (r : Num) =>
+ value(r) == value(x) + value(y)
+ }
+
+ def mult(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) * value(y)
+ }
+ }
+}
diff --git a/testcases/synthesis/current/run.sh b/testcases/synthesis/current/run.sh
new file mode 100755
index 000000000..522e432df
--- /dev/null
+++ b/testcases/synthesis/current/run.sh
@@ -0,0 +1,43 @@
+#!/bin/bash
+
+function run {
+ cmd="./leon --debug=report --timeout=30 --synthesis --cegis:maxsize=7 $1"
+ echo "Running " $cmd
+ echo "------------------------------------------------------------------------------------------------------------------"
+ $cmd;
+}
+
+echo "==================================================================================================================" >> synthesis-report.txt
+# These are all the benchmarks included in my thesis
+# List
+run testcases/synthesis/current/List/Insert.scala
+run testcases/synthesis/current/List/Delete.scala
+run testcases/synthesis/current/List/Union.scala
+run testcases/synthesis/current/List/Diff.scala
+run testcases/synthesis/current/List/Split.scala
+
+# SortedList
+run testcases/synthesis/current/SortedList/Insert.scala
+run testcases/synthesis/current/SortedList/InsertAlways.scala
+run testcases/synthesis/current/SortedList/Delete.scala
+run testcases/synthesis/current/SortedList/Union.scala
+run testcases/synthesis/current/SortedList/Diff.scala
+run testcases/synthesis/current/SortedList/InsertionSort.scala
+
+# StrictSortedList
+run testcases/synthesis/current/StrictSortedList/Insert.scala
+run testcases/synthesis/current/StrictSortedList/Delete.scala
+run testcases/synthesis/current/StrictSortedList/Union.scala
+
+# UnaryNumerals
+run testcases/synthesis/current/UnaryNumerals/Add.scala
+run testcases/synthesis/current/UnaryNumerals/Distinct.scala
+run testcases/synthesis/current/UnaryNumerals/Mult.scala
+
+# BatchedQueue
+run testcases/synthesis/current/BatchedQueue/Enqueue.scala
+run testcases/synthesis/current/BatchedQueue/Dequeue.scala
+
+# AddressBook
+run testcases/synthesis/current/AddressBook/Make.scala
+run testcases/synthesis/current/AddressBook/Merge.scala
--
GitLab