From e3e4260fe5940c93c8cc2921dee8ef2cb7ae3694 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Mon, 15 Dec 2014 18:14:54 +0100
Subject: [PATCH] Refactor some benchmarks
---
.../repair/DaysToYears/DaysToYears3.scala | 36 ------
.../synthesis/repair/HeapSort/HeapSort2.scala | 2 +-
.../synthesis/repair/HeapSort/HeapSort4.scala | 4 +-
.../synthesis/repair/HeapSort/HeapSort6.scala | 113 ------------------
.../synthesis/repair/HeapSort/HeapSort7.scala | 113 ------------------
.../repair/SortedList/SortedList1.scala | 2 +-
6 files changed, 4 insertions(+), 266 deletions(-)
delete mode 100644 testcases/synthesis/repair/DaysToYears/DaysToYears3.scala
delete mode 100644 testcases/synthesis/repair/HeapSort/HeapSort6.scala
delete mode 100644 testcases/synthesis/repair/HeapSort/HeapSort7.scala
diff --git a/testcases/synthesis/repair/DaysToYears/DaysToYears3.scala b/testcases/synthesis/repair/DaysToYears/DaysToYears3.scala
deleted file mode 100644
index bb6c518b3..000000000
--- a/testcases/synthesis/repair/DaysToYears/DaysToYears3.scala
+++ /dev/null
@@ -1,36 +0,0 @@
-import leon.lang._
-
-object DaysToYears {
- val base : Int = 1980
-
- def isLeapYear(y : Int): Boolean = y % 4 == 0
-
- def daysToYears(days : Int): Int = {
- require(days > 0)
- daysToYears1(base, days)._1
- }
-
- def daysToYears1(year : Int, days : Int): (Int, Int) = {
- require(year >= base && days > 0)
- if (days > 366 && isLeapYear(year))
- daysToYears1(year + 1, days - 366)
- else if (days > 365 && !isLeapYear(year))
- daysToYears1(year + 1, days - 365)
- else (year, days)
- } ensuring { res =>
- res._2 <= 366 &&
- res._2 > 0 &&
- res._1 >= base &&
- (((year,days), res) passes {
- case (1980, 366 ) => (1980, 366)
- case (1980, 1000) => (1982, 269)
- })
- }
-
- def main(args : Array[String]) = {
- println(daysToYears1(base, 10593 ))
- println(daysToYears1(base, 366 ))
- println(daysToYears1(base, 1000 ))
- }
-}
-
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort2.scala b/testcases/synthesis/repair/HeapSort/HeapSort2.scala
index b6fe66f21..df7e82458 100644
--- a/testcases/synthesis/repair/HeapSort/HeapSort2.scala
+++ b/testcases/synthesis/repair/HeapSort/HeapSort2.scala
@@ -63,7 +63,7 @@ object HeapSort {
if(v1 >= v2)
Node(v1, l1, merge(r1, h2)) // FIXME forgot to use makeN
else
- Node(v2, l2, merge(h1, r2)) // The same
+ makeN(v2, l2, merge(h1, r2)) // The same
}
} ensuring { res =>
hasLeftistProperty(res) && hasHeapProperty(res) &&
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort4.scala b/testcases/synthesis/repair/HeapSort/HeapSort4.scala
index e931de5d3..a19ff6c20 100644
--- a/testcases/synthesis/repair/HeapSort/HeapSort4.scala
+++ b/testcases/synthesis/repair/HeapSort/HeapSort4.scala
@@ -58,9 +58,9 @@ object HeapSort {
)
(h1,h2) match {
case (Leaf(), _) => h2
- case (_, Leaf()) => h1
+ case (_, Leaf()) => h2 // FIXME h2 instead of h1
case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
- if(v1 < v2) // FIXME : condition should be >=
+ if(v1 >= v2)
makeN(v1, l1, merge(r1, h2))
else
makeN(v2, l2, merge(h1, r2))
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort6.scala b/testcases/synthesis/repair/HeapSort/HeapSort6.scala
deleted file mode 100644
index a19ff6c20..000000000
--- a/testcases/synthesis/repair/HeapSort/HeapSort6.scala
+++ /dev/null
@@ -1,113 +0,0 @@
-/* Copyright 2009-2013 EPFL, Lausanne
- *
- * Author: Ravi
- * Date: 20.11.2013
- **/
-
-import leon.collection._
-import leon._
-
-object HeapSort {
-
- sealed abstract class Heap {
- val rank : Int = this match {
- case Leaf() => 0
- case Node(_, l, r) =>
- 1 + max(l.rank, r.rank)
- }
- def content : Set[Int] = this match {
- case Leaf() => Set[Int]()
- case Node(v,l,r) => l.content ++ Set(v) ++ r.content
- }
- }
- case class Leaf() extends Heap
- case class Node(value:Int, left: Heap, right: Heap) extends Heap
-
- def max(i1 : Int, i2 : Int) = if (i1 >= i2) i1 else i2
-
- def hasHeapProperty(h : Heap) : Boolean = h match {
- case Leaf() => true
- case Node(v, l, r) =>
- ( l match {
- case Leaf() => true
- case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
- }) &&
- ( r match {
- case Leaf() => true
- case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
- })
- }
-
- def hasLeftistProperty(h: Heap) : Boolean = h match {
- case Leaf() => true
- case Node(_,l,r) =>
- hasLeftistProperty(l) &&
- hasLeftistProperty(r) &&
- l.rank >= r.rank
- }
-
- def heapSize(t: Heap): Int = { t match {
- case Leaf() => 0
- case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
- }} ensuring(_ >= 0)
-
- private def merge(h1: Heap, h2: Heap) : Heap = {
- require(
- hasLeftistProperty(h1) && hasLeftistProperty(h2) &&
- hasHeapProperty(h1) && hasHeapProperty(h2)
- )
- (h1,h2) match {
- case (Leaf(), _) => h2
- case (_, Leaf()) => h2 // FIXME h2 instead of h1
- case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
- if(v1 >= v2)
- makeN(v1, l1, merge(r1, h2))
- else
- makeN(v2, l2, merge(h1, r2))
- }
- } ensuring { res =>
- hasLeftistProperty(res) && hasHeapProperty(res) &&
- heapSize(h1) + heapSize(h2) == heapSize(res) &&
- h1.content ++ h2.content == res.content
- }
-
- private def makeN(value: Int, left: Heap, right: Heap) : Heap = {
- require(
- hasLeftistProperty(left) && hasLeftistProperty(right)
- )
- if(left.rank >= right.rank)
- Node(value, left, right)
- else
- Node(value, right, left)
- } ensuring { res =>
- hasLeftistProperty(res) }
-
- def insert(element: Int, heap: Heap) : Heap = {
- require(hasLeftistProperty(heap) && hasHeapProperty(heap))
-
- merge(Node(element, Leaf(), Leaf()), heap)
-
- } ensuring { res =>
- hasLeftistProperty(res) && hasHeapProperty(res) &&
- heapSize(res) == heapSize(heap) + 1 &&
- res.content == heap.content ++ Set(element)
- }
-
- def findMax(h: Heap) : Option[Int] = {
- h match {
- case Node(m,_,_) => Some(m)
- case Leaf() => None()
- }
- }
-
- def removeMax(h: Heap) : Heap = {
- require(hasLeftistProperty(h) && hasHeapProperty(h))
- h match {
- case Node(_,l,r) => merge(l, r)
- case l => l
- }
- } ensuring { res =>
- hasLeftistProperty(res) && hasHeapProperty(res)
- }
-
-}
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort7.scala b/testcases/synthesis/repair/HeapSort/HeapSort7.scala
deleted file mode 100644
index d2dfa6476..000000000
--- a/testcases/synthesis/repair/HeapSort/HeapSort7.scala
+++ /dev/null
@@ -1,113 +0,0 @@
-/* Copyright 2009-2013 EPFL, Lausanne
- *
- * Author: Ravi
- * Date: 20.11.2013
- **/
-
-import leon.collection._
-import leon._
-
-object HeapSort {
-
- sealed abstract class Heap {
- val rank : Int = this match {
- case Leaf() => 0
- case Node(_, l, r) =>
- 1 + max(l.rank, r.rank)
- }
- def content : Set[Int] = this match {
- case Leaf() => Set[Int]()
- case Node(v,l,r) => l.content ++ Set(v) ++ r.content
- }
- }
- case class Leaf() extends Heap
- case class Node(value:Int, left: Heap, right: Heap) extends Heap
-
- def max(i1 : Int, i2 : Int) = if (i1 >= i2) i1 else i2
-
- def hasHeapProperty(h : Heap) : Boolean = h match {
- case Leaf() => true
- case Node(v, l, r) =>
- ( l match {
- case Leaf() => true
- case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
- }) &&
- ( r match {
- case Leaf() => true
- case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
- })
- }
-
- def hasLeftistProperty(h: Heap) : Boolean = h match {
- case Leaf() => true
- case Node(_,l,r) =>
- hasLeftistProperty(l) &&
- hasLeftistProperty(r) &&
- l.rank >= r.rank
- }
-
- def heapSize(t: Heap): Int = { t match {
- case Leaf() => 0
- case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
- }} ensuring(_ >= 0)
-
- private def merge(h1: Heap, h2: Heap) : Heap = {
- require(
- hasLeftistProperty(h1) && hasLeftistProperty(h2) &&
- hasHeapProperty(h1) && hasHeapProperty(h2)
- )
- (h1,h2) match {
- case (Leaf(), _) => h2
- //case (_, Leaf()) => h1 FIXME : forgot a match case
- case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
- if(v1 >= v2)
- makeN(v1, l1, merge(r1, h2))
- else
- makeN(v2, l2, merge(h1, r2))
- }
- } ensuring { res =>
- hasLeftistProperty(res) && hasHeapProperty(res) &&
- heapSize(h1) + heapSize(h2) == heapSize(res) &&
- h1.content ++ h2.content == res.content
- }
-
- private def makeN(value: Int, left: Heap, right: Heap) : Heap = {
- require(
- hasLeftistProperty(left) && hasLeftistProperty(right)
- )
- if(left.rank >= right.rank)
- Node(value, left, right)
- else
- Node(value, right, left)
- } ensuring { res =>
- hasLeftistProperty(res) }
-
- def insert(element: Int, heap: Heap) : Heap = {
- require(hasLeftistProperty(heap) && hasHeapProperty(heap))
-
- merge(Node(element, Leaf(), Leaf()), heap)
-
- } ensuring { res =>
- hasLeftistProperty(res) && hasHeapProperty(res) &&
- heapSize(res) == heapSize(heap) + 1 &&
- res.content == heap.content ++ Set(element)
- }
-
- def findMax(h: Heap) : Option[Int] = {
- h match {
- case Node(m,_,_) => Some(m)
- case Leaf() => None()
- }
- }
-
- def removeMax(h: Heap) : Heap = {
- require(hasLeftistProperty(h) && hasHeapProperty(h))
- h match {
- case Node(_,l,r) => merge(l, r)
- case l => l
- }
- } ensuring { res =>
- hasLeftistProperty(res) && hasHeapProperty(res)
- }
-
-}
diff --git a/testcases/synthesis/repair/SortedList/SortedList1.scala b/testcases/synthesis/repair/SortedList/SortedList1.scala
index 601912906..6d27fa839 100644
--- a/testcases/synthesis/repair/SortedList/SortedList1.scala
+++ b/testcases/synthesis/repair/SortedList/SortedList1.scala
@@ -41,7 +41,7 @@ object SortedList {
case Nil() => l
case Cons(_, Nil()) => l
case _ =>
- merge(split(l)._1, split(l)._2) // FIXME: Forgot to mergeSort l1 and l2
+ merge(mergeSort(split(l)._1), split(l)._2) // FIXME: Forgot to mergeSort l1 and l2
}} ensuring { res =>
res.content == l.content &&
isSorted(res)
--
GitLab