Refactor some benchmarks

testcases/synthesis/repair/DaysToYears/DaysToYears3.scala

-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 ))
-  }
-}
-

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) &&

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))

testcases/synthesis/repair/HeapSort/HeapSort6.scala

-/* 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)
-  }
-
-} 

testcases/synthesis/repair/HeapSort/HeapSort7.scala

-/* 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)
-  }
-
-} 

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)