From a6259e94c5cd154b440a2e8bf248d855306520be Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 10 Dec 2015 16:44:49 +0100
Subject: [PATCH] Introduce new synthesis rules (InputSplit & IndependentSplit)
- InputSplit splits by a boolean input variable
- IndependentSplit splits output variables that are unrelated
---
.../leon/synthesis/ConversionPhase.scala | 2 +
src/main/scala/leon/synthesis/Rules.scala | 2 +
.../synthesis/rules/IndependentSplit.scala | 80 ++++++++++++++++++
.../leon/synthesis/rules/InputSplit.scala | 49 +++++++++++
.../invalid/PropositionalLogic.scala | 46 +----------
.../etienne-thesis/AddressBook/Make.scala | 53 ++++++++++++
.../etienne-thesis/AddressBook/Merge.scala | 69 ++++++++++++++++
.../etienne-thesis/BatchedQueue/Dequeue.scala | 80 ++++++++++++++++++
.../etienne-thesis/BatchedQueue/Enqueue.scala | 82 +++++++++++++++++++
.../etienne-thesis/List/Delete.scala | 25 ++----
.../etienne-thesis/SortedList/Delete.scala | 34 ++++++++
.../etienne-thesis/SortedList/Diff.scala | 53 ++++++++++++
.../etienne-thesis/SortedList/Insert.scala | 34 ++++++++
.../SortedList/InsertAlways.scala | 34 ++++++++
.../SortedList/InsertionSort.scala | 49 +++++++++++
.../etienne-thesis/SortedList/Union.scala | 51 ++++++++++++
.../StrictSortedList/Delete.scala | 34 ++++++++
.../StrictSortedList/Insert.scala | 34 ++++++++
.../StrictSortedList/Union.scala | 51 ++++++++++++
.../etienne-thesis/UnaryNumerals/Add.scala | 21 +++++
.../UnaryNumerals/Distinct.scala | 30 +++++++
.../etienne-thesis/UnaryNumerals/Mult.scala | 30 +++++++
testcases/synthesis/etienne-thesis/run.sh | 43 ++++++++++
23 files changed, 923 insertions(+), 63 deletions(-)
create mode 100644 src/main/scala/leon/synthesis/rules/IndependentSplit.scala
create mode 100644 src/main/scala/leon/synthesis/rules/InputSplit.scala
create mode 100644 testcases/synthesis/etienne-thesis/AddressBook/Make.scala
create mode 100644 testcases/synthesis/etienne-thesis/AddressBook/Merge.scala
create mode 100644 testcases/synthesis/etienne-thesis/BatchedQueue/Dequeue.scala
create mode 100644 testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
create mode 100644 testcases/synthesis/etienne-thesis/SortedList/Delete.scala
create mode 100644 testcases/synthesis/etienne-thesis/SortedList/Diff.scala
create mode 100644 testcases/synthesis/etienne-thesis/SortedList/Insert.scala
create mode 100644 testcases/synthesis/etienne-thesis/SortedList/InsertAlways.scala
create mode 100644 testcases/synthesis/etienne-thesis/SortedList/InsertionSort.scala
create mode 100644 testcases/synthesis/etienne-thesis/SortedList/Union.scala
create mode 100644 testcases/synthesis/etienne-thesis/StrictSortedList/Delete.scala
create mode 100644 testcases/synthesis/etienne-thesis/StrictSortedList/Insert.scala
create mode 100644 testcases/synthesis/etienne-thesis/StrictSortedList/Union.scala
create mode 100644 testcases/synthesis/etienne-thesis/UnaryNumerals/Add.scala
create mode 100644 testcases/synthesis/etienne-thesis/UnaryNumerals/Distinct.scala
create mode 100644 testcases/synthesis/etienne-thesis/UnaryNumerals/Mult.scala
create mode 100755 testcases/synthesis/etienne-thesis/run.sh
diff --git a/src/main/scala/leon/synthesis/ConversionPhase.scala b/src/main/scala/leon/synthesis/ConversionPhase.scala
index d5f4e842f..a2fa94ea9 100644
--- a/src/main/scala/leon/synthesis/ConversionPhase.scala
+++ b/src/main/scala/leon/synthesis/ConversionPhase.scala
@@ -188,6 +188,8 @@ object ConversionPhase extends UnitPhase[Program] {
// extract spec from chooses at the top-level
fullBody match {
+ case Require(_, Choose(spec)) =>
+ withPostcondition(fullBody, Some(spec))
case Choose(spec) =>
withPostcondition(fullBody, Some(spec))
case _ =>
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 51a5a15ec..02a04e270 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -44,7 +44,9 @@ object Rules {
//OnePoint,
Ground,
CaseSplit,
+ IndependentSplit,
IfSplit,
+ InputSplit,
UnusedInput,
EquivalentInputs,
UnconstrainedOutput,
diff --git a/src/main/scala/leon/synthesis/rules/IndependentSplit.scala b/src/main/scala/leon/synthesis/rules/IndependentSplit.scala
new file mode 100644
index 000000000..72be06b9c
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/IndependentSplit.scala
@@ -0,0 +1,80 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import leon.utils._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Extractors._
+import purescala.Constructors._
+import purescala.Common._
+import purescala.Types.CaseClassType
+
+case object IndependentSplit extends NormalizingRule("IndependentSplit") {
+ def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
+ val TopLevelAnds(clauses) = and(p.pc, p.phi)
+
+ var independentClasses = Set[Set[Identifier]]()
+
+ // We group connect variables together
+ for(c <- clauses) {
+ val vs = variablesOf(c)
+
+ var newClasses = Set[Set[Identifier]]()
+
+ var thisClass = vs
+
+ for (cl <- independentClasses) {
+ if ((cl & vs).nonEmpty) {
+ thisClass ++= cl
+ } else {
+ newClasses += cl
+ }
+ }
+
+ independentClasses = newClasses + thisClass
+ }
+
+ val outClasses = independentClasses.map(cl => cl & p.xs.toSet).filter(_.nonEmpty)
+
+ if (outClasses.size > 1) {
+
+ val TopLevelAnds(phiClauses) = p.phi
+
+ val subs = (for (cl <- outClasses.toList) yield {
+ val xs = p.xs.filter(cl)
+
+ if (xs.nonEmpty) {
+ val phi = andJoin(phiClauses.filter(c => (variablesOf(c) & cl).nonEmpty))
+
+ val xsToRemove = p.xs.filterNot(cl).toSet
+
+ val eb = p.qeb.removeOuts(xsToRemove)
+
+ Some(p.copy(phi = phi, xs = xs, eb = eb))
+ } else {
+ None
+ }
+ }).flatten
+
+ val onSuccess: List[Solution] => Option[Solution] = { sols =>
+
+ val infos = subs.map(_.xs).zip(sols.map(_.term))
+
+ val term = infos.foldLeft(tupleWrap(p.xs.map(_.toVariable))) {
+ case (expr, (xs, term)) =>
+ letTuple(xs, term, expr)
+ }
+
+ Some(Solution(andJoin(sols.map(_.pre)), sols.map(_.defs).flatten.toSet, term, sols.forall(_.isTrusted)))
+ }
+
+
+ List(decomp(subs, onSuccess, "Independent Clusters"))
+ } else {
+ Nil
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/rules/InputSplit.scala b/src/main/scala/leon/synthesis/rules/InputSplit.scala
new file mode 100644
index 000000000..4b9ffef53
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/InputSplit.scala
@@ -0,0 +1,49 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import leon.purescala.Common.Identifier
+import purescala.Expressions._
+import purescala.Extractors._
+import purescala.ExprOps._
+import purescala.Constructors._
+import purescala.Types._
+
+import solvers._
+
+import scala.concurrent.duration._
+
+case object InputSplit extends Rule("In. Split") {
+ def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
+ p.as.filter(_.getType == BooleanType).flatMap { a =>
+ def getProblem(v: Boolean): Problem = {
+ def replaceA(e: Expr) = replaceFromIDs(Map(a -> BooleanLiteral(v)), e)
+
+ p.copy(
+ as = p.as.filterNot(_ == a),
+ ws = replaceA(p.ws),
+ pc = replaceA(p.pc),
+ phi = replaceA(p.phi),
+ eb = p.qeb.removeIns(Set(a))
+ )
+ }
+
+ val sub1 = getProblem(true)
+ val sub2 = getProblem(false)
+
+ val onSuccess: List[Solution] => Option[Solution] = {
+ case List(s1, s2) =>
+ Some(Solution(or(and(Equals(Variable(a), BooleanLiteral(true)), s1.pre),
+ and(Equals(Variable(a), BooleanLiteral(false)), s2.pre)),
+ s1.defs ++ s2.defs,
+ IfExpr(Variable(a), s1.term, s2.term), s1.isTrusted && s2.isTrusted))
+ case _ =>
+ None
+ }
+
+ Some(decomp(List(sub1, sub2), onSuccess, s"Split on '$a'"))
+ }
+ }
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
index a8927f360..aa00e12d4 100644
--- a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
@@ -10,14 +10,11 @@ object PropositionalLogic {
case class Or(lhs: Formula, rhs: Formula) extends Formula
case class Implies(lhs: Formula, rhs: Formula) extends Formula
case class Not(f: Formula) extends Formula
- case class Literal(id: Int) extends Formula
+ case class Literal(id: BigInt) extends Formula
def simplify(f: Formula): Formula = (f match {
- case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
- case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
- case Not(f) => Not(simplify(f))
- case Literal(_) => f
+ case _ => f
}) ensuring(isSimplified(_))
def isSimplified(f: Formula): Boolean = f match {
@@ -28,18 +25,6 @@ object PropositionalLogic {
case Literal(_) => true
}
- def nnf(formula: Formula): Formula = (formula match {
- case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
- case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
- case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
- case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
- case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
- case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
- case Not(Not(f)) => nnf(f)
- case Not(Literal(_)) => formula
- case Literal(_) => formula
- }) ensuring(isNNF(_))
-
def isNNF(f: Formula): Boolean = f match {
case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
@@ -49,39 +34,14 @@ object PropositionalLogic {
case Literal(_) => true
}
- def vars(f: Formula): Set[Int] = {
- require(isNNF(f))
- f match {
- case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Not(Literal(i)) => Set[Int](i)
- case Literal(i) => Set[Int](i)
- }
- }
-
- def fv(f : Formula) = { vars(nnf(f)) }
// @induct
// def wrongCommutative(f: Formula) : Boolean = {
// nnf(simplify(f)) == simplify(nnf(f))
// }.holds
- @induct
- def simplifyBreaksNNF(f: Formula) : Boolean = {
+ def simplifyBreaksNNF(f: Formula) : Boolean = {
require(isNNF(f))
isNNF(simplify(f))
}.holds
-
- @induct
- def nnfIsStable(f: Formula) : Boolean = {
- require(isNNF(f))
- nnf(f) == f
- }.holds
-
- @induct
- def simplifyIsStable(f: Formula) : Boolean = {
- require(isSimplified(f))
- simplify(f) == f
- }.holds
}
diff --git a/testcases/synthesis/etienne-thesis/AddressBook/Make.scala b/testcases/synthesis/etienne-thesis/AddressBook/Make.scala
new file mode 100644
index 000000000..1fd12466c
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/AddressBook/Make.scala
@@ -0,0 +1,53 @@
+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 )
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/AddressBook/Merge.scala b/testcases/synthesis/etienne-thesis/AddressBook/Merge.scala
new file mode 100644
index 000000000..92a5b5bfe
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/BatchedQueue/Dequeue.scala b/testcases/synthesis/etienne-thesis/BatchedQueue/Dequeue.scala
new file mode 100644
index 000000000..c44fc0628
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/BatchedQueue/Enqueue.scala b/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
new file mode 100644
index 000000000..87e030915
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
@@ -0,0 +1,82 @@
+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)
+
+ choose { (res: Queue[T]) =>
+ res.invariant &&
+ res.toList.last == v &&
+ res.content == this.content ++ Set(v)
+ }
+ }
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/List/Delete.scala b/testcases/synthesis/etienne-thesis/List/Delete.scala
index 46f071087..30716c591 100644
--- a/testcases/synthesis/etienne-thesis/List/Delete.scala
+++ b/testcases/synthesis/etienne-thesis/List/Delete.scala
@@ -7,7 +7,7 @@ object Delete {
case class Cons(head: BigInt, tail: List) extends List
case object Nil extends List
- def size(l: List) : BigInt = (l match {
+ def size(l: List): BigInt = (l match {
case Nil => BigInt(0)
case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
@@ -17,25 +17,10 @@ object Delete {
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 delete(in1: List, v: BigInt) = choose {
+ def delete(in: List, v: BigInt) = {
+ ???[List]
+ } ensuring {
(out : List) =>
- content(out) == content(in1) -- Set(v)
+ content(out) == content(in) -- Set(v)
}
}
diff --git a/testcases/synthesis/etienne-thesis/SortedList/Delete.scala b/testcases/synthesis/etienne-thesis/SortedList/Delete.scala
new file mode 100644
index 000000000..788f232d3
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/SortedList/Diff.scala b/testcases/synthesis/etienne-thesis/SortedList/Diff.scala
new file mode 100644
index 000000000..d391b85ba
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/SortedList/Insert.scala b/testcases/synthesis/etienne-thesis/SortedList/Insert.scala
new file mode 100644
index 000000000..0bf80d1e9
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/SortedList/InsertAlways.scala b/testcases/synthesis/etienne-thesis/SortedList/InsertAlways.scala
new file mode 100644
index 000000000..73e0b240d
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/SortedList/InsertionSort.scala b/testcases/synthesis/etienne-thesis/SortedList/InsertionSort.scala
new file mode 100644
index 000000000..0752ad33f
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/SortedList/Union.scala b/testcases/synthesis/etienne-thesis/SortedList/Union.scala
new file mode 100644
index 000000000..d3f11adcc
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/StrictSortedList/Delete.scala b/testcases/synthesis/etienne-thesis/StrictSortedList/Delete.scala
new file mode 100644
index 000000000..23999d96c
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/StrictSortedList/Insert.scala b/testcases/synthesis/etienne-thesis/StrictSortedList/Insert.scala
new file mode 100644
index 000000000..65f3c01f9
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/StrictSortedList/Union.scala b/testcases/synthesis/etienne-thesis/StrictSortedList/Union.scala
new file mode 100644
index 000000000..c10ed419d
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/UnaryNumerals/Add.scala b/testcases/synthesis/etienne-thesis/UnaryNumerals/Add.scala
new file mode 100644
index 000000000..a34d1834f
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/UnaryNumerals/Distinct.scala b/testcases/synthesis/etienne-thesis/UnaryNumerals/Distinct.scala
new file mode 100644
index 000000000..4287378d1
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/UnaryNumerals/Mult.scala b/testcases/synthesis/etienne-thesis/UnaryNumerals/Mult.scala
new file mode 100644
index 000000000..bfa39365e
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/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/etienne-thesis/run.sh b/testcases/synthesis/etienne-thesis/run.sh
new file mode 100755
index 000000000..ee64d8670
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/run.sh
@@ -0,0 +1,43 @@
+#!/bin/bash
+
+function run {
+ cmd="./leon --debug=report --timeout=30 --synthesis $1"
+ echo "Running " $cmd
+ echo "------------------------------------------------------------------------------------------------------------------"
+ $cmd;
+}
+
+echo "==================================================================================================================" >> synthesis-report.txt
+# These are all the benchmarks included in my thesis
+# List
+run testcases/synthesis/etienne-thesis/List/Insert.scala
+run testcases/synthesis/etienne-thesis/List/Delete.scala
+run testcases/synthesis/etienne-thesis/List/Union.scala
+run testcases/synthesis/etienne-thesis/List/Diff.scala
+run testcases/synthesis/etienne-thesis/List/Split.scala
+
+# SortedList
+run testcases/synthesis/etienne-thesis/SortedList/Insert.scala
+run testcases/synthesis/etienne-thesis/SortedList/InsertAlways.scala
+run testcases/synthesis/etienne-thesis/SortedList/Delete.scala
+run testcases/synthesis/etienne-thesis/SortedList/Union.scala
+run testcases/synthesis/etienne-thesis/SortedList/Diff.scala
+run testcases/synthesis/etienne-thesis/SortedList/InsertionSort.scala
+
+# StrictSortedList
+run testcases/synthesis/etienne-thesis/StrictSortedList/Insert.scala
+run testcases/synthesis/etienne-thesis/StrictSortedList/Delete.scala
+run testcases/synthesis/etienne-thesis/StrictSortedList/Union.scala
+
+# UnaryNumerals
+run testcases/synthesis/etienne-thesis/UnaryNumerals/Add.scala
+run testcases/synthesis/etienne-thesis/UnaryNumerals/Distinct.scala
+run testcases/synthesis/etienne-thesis/UnaryNumerals/Mult.scala
+
+# BatchedQueue
+#run testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
+run testcases/synthesis/etienne-thesis/BatchedQueue/Dequeue.scala
+
+# AddressBook
+#run testcases/synthesis/etienne-thesis/AddressBook/Make.scala
+run testcases/synthesis/etienne-thesis/AddressBook/Merge.scala
--
GitLab