From c6e7ae284ea12b219412777a34019e955f1525e2 Mon Sep 17 00:00:00 2001
From: ravi <ravi.kandhadai@epfl.ch>
Date: Tue, 29 Sep 2015 16:16:23 +0200
Subject: [PATCH] Removing compositional and automatic testcases
---
build.sbt | 2 +-
leon-change-notes | 155 ---------
.../automatic/AmortizedQueue.scala | 74 ----
.../orb-testcases/automatic/BinaryTrie.scala | 63 ----
.../automatic/BinomialHeap.scala | 325 ------------------
.../orb-testcases/automatic/HeapSort.scala | 109 ------
.../automatic/InsertionSort.scala | 25 --
.../orb-testcases/automatic/LeftistHeap.scala | 61 ----
.../automatic/ListOperations.scala | 57 ---
.../automatic/TreeOperations.scala | 91 -----
.../orb-testcases/composition/AVLSort.scala | 189 ----------
.../composition/ConstantPropagation.scala | 291 ----------------
.../orb-testcases/composition/HeapSort.scala | 147 --------
.../orb-testcases/composition/HeapSort2.scala | 132 -------
.../composition/InsertionSort.scala | 30 --
.../composition/LeftistHeap.scala | 113 ------
.../orb-testcases/composition/MergeSort.scala | 150 --------
.../orb-testcases/composition/QuickSort.scala | 44 ---
.../composition/Z3-exception-output.txt | 68 ----
19 files changed, 1 insertion(+), 2125 deletions(-)
delete mode 100644 leon-change-notes
delete mode 100644 testcases/orb-testcases/automatic/AmortizedQueue.scala
delete mode 100755 testcases/orb-testcases/automatic/BinaryTrie.scala
delete mode 100644 testcases/orb-testcases/automatic/BinomialHeap.scala
delete mode 100644 testcases/orb-testcases/automatic/HeapSort.scala
delete mode 100644 testcases/orb-testcases/automatic/InsertionSort.scala
delete mode 100644 testcases/orb-testcases/automatic/LeftistHeap.scala
delete mode 100644 testcases/orb-testcases/automatic/ListOperations.scala
delete mode 100755 testcases/orb-testcases/automatic/TreeOperations.scala
delete mode 100644 testcases/orb-testcases/composition/AVLSort.scala
delete mode 100644 testcases/orb-testcases/composition/ConstantPropagation.scala
delete mode 100644 testcases/orb-testcases/composition/HeapSort.scala
delete mode 100644 testcases/orb-testcases/composition/HeapSort2.scala
delete mode 100644 testcases/orb-testcases/composition/InsertionSort.scala
delete mode 100644 testcases/orb-testcases/composition/LeftistHeap.scala
delete mode 100644 testcases/orb-testcases/composition/MergeSort.scala
delete mode 100644 testcases/orb-testcases/composition/QuickSort.scala
delete mode 100644 testcases/orb-testcases/composition/Z3-exception-output.txt
diff --git a/build.sbt b/build.sbt
index 49df8715f..c6449492b 100644
--- a/build.sbt
+++ b/build.sbt
@@ -1,4 +1,4 @@
-name := "Orb2015"
+name := "Leon"
version := "3.0"
diff --git a/leon-change-notes b/leon-change-notes
deleted file mode 100644
index 4e0a3d4d7..000000000
--- a/leon-change-notes
+++ /dev/null
@@ -1,155 +0,0 @@
-In file ExprOps.scala, in function simplestValue:
-
-SimplestValue(tpe: TypeTree) : Expr = tpe match {
- case Int32Type => IntLiteral(0)
- case IntegerType => InfiniteIntegerLiteral(0)
- case CharType => CharLiteral('a')
- case BooleanType => BooleanLiteral(false)
- case UnitType => UnitLiteral()
- case SetType(baseType) => EmptySet(tpe)
- case MapType(fromType, toType) => EmptyMap(fromType, toType)
- case TupleType(tpes) => Tuple(tpes.map(simplestValue))
- case ArrayType(tpe) => EmptyArray(tpe)
- case RationalType => RationalLiteral(0, 1)
-
-In file Expressions.scala after UntilLiteral definition
-
- case class RationalLiteral(numerator: BigInt, denominator: BigInt) extends Literal[(BigInt,BigInt)] {
- val value = (numerator,denominator)
- val getType = RationalType
-
- override def toString = {
- if(denominator == 1) numerator.toString
- else numerator + "/" + denominator
- }
- }
-In file Expressions.scala, first five arithmetic types
-
-/* Arithmetic */
- case class Plus(lhs: Expr, rhs: Expr) extends Expr {
- val getType = superNumericType(lhs.getType, rhs.getType)
- }
-
- case class Minus(lhs: Expr, rhs: Expr) extends Expr {
- val getType = superNumericType(lhs.getType, rhs.getType)
- }
-
- case class UMinus(expr: Expr) extends Expr {
- require(isNumericType(expr.getType))
- val getType = expr.getType
- }
-
- case class Times(lhs: Expr, rhs: Expr) extends Expr {
- val getType = superNumericType(lhs.getType, rhs.getType)
- }
-
- case class Division(lhs: Expr, rhs: Expr) extends Expr {
- val getType = superNumericType(lhs.getType, rhs.getType)
- }
-
-
-In file PrettyPrinter.scala, in function pp
-
-case Let(b,d,e) =>
- optB { d match {
- case _:LetDef | _ : Let | LetPattern(_,_,_) =>
- p"""|val $b = {
- | $d
- |}
- |$e"""
- case _ =>
- p"""|val $b = $d;
- |$e"""
- }}
-
-'b' is replaced by 'd'
-
-In file PrettyPrinter.scala, In function requireBraces (before the case that returns true)
-
- case (_, Some(_: IfExpr)) => false
-
-In file Types.scala,
-
-import PrinterHelpers._
-
-After the definition of "IntegerType"
-
- case object RationalType extends TypeTree with PrettyPrintable {
- def printWith(implicit pctx: PrinterContext) {
- p"Real"
- }
- }
-
- def isNumericType(t: TypeTree) = t match {
- case IntegerType | RationalType => true
- case _ => false
- }
-
- def superNumericType(t1: TypeTree, t2: TypeTree) = {
- require(isNumericType(t1) && isNumericType(t2))
- if (t1 == RationalType || t2 == RationalType) RationalType
- else IntegerType
- }
-
-In AbstractZ3Solver, in function preparesorts
-
-Add the following after sorts += IntegerType -> ...
-sorts += RationalType -> z3.mkRealSort
-
-In function typeToSort
-add the first "case Int32Type | BooleanType | UnitType | IntegerType | CharType | RationalType"
-
-In function "toZ3Formula"
-
-After infiniteIntegerLiteral add
- case RationalLiteral(num, denom) => z3.mkNumeral(s"${num.toString} / ${denom.toString}", typeToSort(RationalType))
-In Lessthan, lessequals ...
-case LessThan(l, r) => l.getType match {
- case RationalType => z3.mkLT(rec(l), rec(r))
- case IntegerType => z3.mkLT(rec(l), rec(r))
- case Int32Type => z3.mkBVSlt(rec(l), rec(r))
- }
- case LessEquals(l, r) => l.getType match {
- case RationalType => z3.mkLE(rec(l), rec(r))
- case IntegerType => z3.mkLE(rec(l), rec(r))
- case Int32Type => z3.mkBVSle(rec(l), rec(r))
- }
- case GreaterThan(l, r) => l.getType match {
- case RationalType => z3.mkGT(rec(l), rec(r))
- case IntegerType => z3.mkGT(rec(l), rec(r))
- case Int32Type => z3.mkBVSgt(rec(l), rec(r))
- }
- case GreaterEquals(l, r) => l.getType match {
- case RationalType => z3.mkGE(rec(l), rec(r))
- case IntegerType => z3.mkGE(rec(l), rec(r))
- case Int32Type => z3.mkBVSge(rec(l), rec(r))
- }
-
-In function "fromZ3Formula"
-in kind match , add after Z3NumeralIntAST
-
-case Z3NumeralRealAST(num: BigInt, dem: BigInt) => {
- val rl = RationalLiteral(num, dem)
- rl
- }
-
-In file Main.scala, add in list 'allPhases'
-transformations.InstrumentationDriver,
- invariant.engine.InferInvariantsPhase)
-ad the end
-
-add after optEval
-val optInstrument = LeonFlagOptionDef("instrument", "Instrument the code for inferring time/depth/stack bounds", false)
- val optInferInv = LeonFlagOptionDef("inferInv", "Infer invariants from (instrumented) the code", false)
-
-after import MainComponent._
-import invariant.engine.InferInvariantsPhase
- import transformations.InstrumentationDriver
-
-Add after evalF
-val inferInvF = ctx.findOptionOrDefault(optInferInv)
- val instrumentF = ctx.findOptionOrDefault(optInstrument)
-
-In pipe process add after else if(evalF) ...
- else if (inferInvF) InstrumentationDriver andThen InferInvariantsPhase
- else if (instrumentF) InstrumentationDriver
diff --git a/testcases/orb-testcases/automatic/AmortizedQueue.scala b/testcases/orb-testcases/automatic/AmortizedQueue.scala
deleted file mode 100644
index 4aa3e785e..000000000
--- a/testcases/orb-testcases/automatic/AmortizedQueue.scala
+++ /dev/null
@@ -1,74 +0,0 @@
-import leon.lang.invariantLang._
-
-object AmortizedQueue {
- sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
- case class Nil() extends List
-
- case class Queue(front : List, rear : List)
-
- def size(list : List) : Int = (list match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- })
-
-
- def qsize(q : Queue) : Int = size(q.front) + size(q.rear)
-
- def asList(q : Queue) : List = concat(q.front, reverse(q.rear))
-
- def concat(l1 : List, l2 : List) : List = (l1 match {
- case Nil() => l2
- case Cons(x,xs) => Cons(x, concat(xs, l2))
-
- }) //ensuring (res => size(res) == size(l1) + size(l2))
-
- def isAmortized(q : Queue) : Boolean = size(q.front) >= size(q.rear)
-
- def isEmpty(queue : Queue) : Boolean = queue match {
- case Queue(Nil(), Nil()) => true
- case _ => false
- }
-
- def reverseRec(l1: List, l2: List): List = (l1 match {
- case Nil() => l2
- case Cons(x, xs) => reverseRec(xs, Cons(x, l2))
-
- }) //ensuring (res => size(l1) + size(l2) == size(res))
-
- def reverse(l: List): List = {
- reverseRec(l, Nil())
- } //ensuring (res => size(l) == size(res))
-
- def amortizedQueue(front : List, rear : List) : Queue = {
- if (size(rear) <= size(front))
- Queue(front, rear)
- else
- Queue(concat(front, reverse(rear)), Nil())
- }
-
- def enqueue(q : Queue, elem : Int) : Queue = ({
-
- amortizedQueue(q.front, Cons(elem, q.rear))
-
- }) ensuring(res => qsize(res) == qsize(q) + 1)
-
-
- def removeLast(l : List) : List = {
- require(l != Nil())
- l match {
- case Cons(x,Nil()) => Nil()
- case Cons(x,xs) => Cons(x, removeLast(xs))
- case _ => Nil()
- }
- }
-
- def pop(q : Queue) : Queue = {
- require(isAmortized(q) && !isEmpty(q))
- q match {
- case Queue(front, Cons(r,rs)) => Queue(front, rs)
- case Queue(front, rear) => Queue(removeLast(front), rear)
- case _ => Queue(Nil(),Nil())
- }
- } ensuring(res => qsize(res) == qsize(q) - 1)
-}
diff --git a/testcases/orb-testcases/automatic/BinaryTrie.scala b/testcases/orb-testcases/automatic/BinaryTrie.scala
deleted file mode 100755
index e4247d9f7..000000000
--- a/testcases/orb-testcases/automatic/BinaryTrie.scala
+++ /dev/null
@@ -1,63 +0,0 @@
-import leon.lang.invariantLang._
-
-
-object BinaryTrie {
- sealed abstract class Tree
- case class Leaf() extends Tree
- case class Node(nvalue: Int, left : Tree, right: Tree) extends Tree
-
- sealed abstract class IList
- case class Cons(head: Int, tail: IList) extends IList
- case class Nil() extends IList
-
- def listSize(l: IList): Int = (l match {
- case Nil() => 0
- case Cons(x, xs) => 1 + listSize(xs)
- })
-
- def height(t: Tree): Int = {
- t match{
- case Leaf() => 0
- case Node(x,l,r) => {
- val hl = height(l)
- val hr = height(r)
- if(hl > hr) hl + 1 else hr + 1
- }
- }
- }
-
- def insert(inp: IList, t: Tree): Tree = {
- t match {
- case Leaf() => {
- inp match {
- case Nil() => t
- case Cons(x ,xs) => {
- val newch = insert(xs, Leaf())
- newch match {
- case Leaf() => Node(x, Leaf(), Leaf())
- case Node(y, _, _) => if(y > 0) Node(x, newch, Leaf()) else Node(y, Leaf(), newch)
- }
- }
- }
- }
- case Node(v, l, r) => {
- inp match {
- case Nil() => t
- case Cons(x, Nil()) => t
- case Cons(x ,xs@Cons(y, _)) => {
- val ch = if(y > 0) l else r
- if(y > 0)
- Node(v, insert(xs, ch), r)
- else
- Node(v, l, insert(xs, ch))
- }
- case _ => t
- }
- }
- }
-}
-
- def create(inp: IList) : Tree = {
- insert(inp, Leaf())
- }ensuring(res => height(res) >= listSize(inp))
-}
diff --git a/testcases/orb-testcases/automatic/BinomialHeap.scala b/testcases/orb-testcases/automatic/BinomialHeap.scala
deleted file mode 100644
index f9b44e066..000000000
--- a/testcases/orb-testcases/automatic/BinomialHeap.scala
+++ /dev/null
@@ -1,325 +0,0 @@
-/**
- * Okasaki3_2
- *
- * Based on the chapter 3.2 of Okasaki's paper Purely Functional Data Structure
- * Implements the "Binomial Heap" data structure described in the chapter.
- *
- * @author Florian Briant
- **/
-
-import leon.Utils._
-import leon.Annotations._
-
-object BinomialHeap {
- sealed abstract class BinomialTree
- case class Node(rank: Int, elem: Element, children: BinomialHeap) extends BinomialTree
-
- sealed abstract class ElementAbs
- case class Element(n: Int) extends ElementAbs
-
- sealed abstract class BinomialHeap
- case class ConsHeap(head: BinomialTree, tail: BinomialHeap) extends BinomialHeap
- case class NilHeap extends BinomialHeap
-
- sealed abstract class List
- case class NodeL(head: BinomialHeap, tail: List) extends List
- case class NilL() extends List
-
- sealed abstract class OptionalTree
- case class Some(t : BinomialTree) extends OptionalTree
- case class None extends OptionalTree
-
- /* Lower or Equal than for Element structure */
- private def leq(a: Element, b: Element) : Boolean = {
- a match {
- case Element(a1) => {
- b match {
- case Element(a2) => {
- if(a1 <= a2) true
- else false
- }
- }
- }
- }
- }
-
- /* isEmpty function of the Binomial Heap */
- def isEmpty(t: BinomialHeap) = t match {
- case ConsHeap(_,_) => false
- case NilHeap() => true
- }
-
- /* Helper function to determine rank of a BinomialTree */
- def rank(t: BinomialTree) : Int = t match {
- case Node(r, _, _) => r
- }
-
- /* Helper function to get the root element of a BinomialTree */
- def root(t: BinomialTree) : Element = t match {
- case Node(_, e, _) => e
- }
-
- /* Helper function which tell if a binomial tree is valid */
- // private def isBinomialChildrenValid(pare: Element, ch: BinomialHeap) : Boolean = ch match {
- // case ConsHeap(t1@Node(r, e, _), tail@ConsHeap(t2,_)) => rank(t2) == r - 1 && leq(pare,e) && isBinomialTreeValid(t1) && isBinomialChildrenValid(pare, tail)
- // case ConsHeap(t1@Node(r, e, _), NilHeap()) => leq(pare,e) && isBinomialTreeValid(t1)
- // case NilHeap() => true
- // }
- // private def isBinomialTreeValid(l: BinomialTree) : Boolean = l match {
- // case Node(r, e, ch@ConsHeap(t, _)) => rank(t) == r - 1 && isBinomialChildrenValid(e, ch)
- // case Node(_, _, NilHeap()) => true
- // }
- //
- // // Helper function which tell if a binomial heap is valid
- // private def isBinomialHeapValid(h: BinomialHeap) : Boolean = h match {
- // case ConsHeap(e, tail@ConsHeap(e2, _)) => rank(e) < rank(e2) && isBinomialTreeValid(e) && isBinomialHeapValid(tail)
- // case ConsHeap(e, NilHeap()) => isBinomialTreeValid(e)
- // case NilHeap() => true
- // }
-
- def checkChildren(index: Int, origRank: Int, origElem: Element, children: BinomialHeap): Boolean = children match {
- case ConsHeap(h, t) => h match {
- case Node(r1, e1, _) => leq(origElem, e1) && r1 == origRank - index - 1 && isBinomialTreeValid(h) && checkChildren(index + 1, origRank, origElem, t)
- }
- case NilHeap() => index == origRank
- }
- private def isBinomialTreeValid(l: BinomialTree) : Boolean = l match {
- case Node(r, e, c) => {
- checkChildren(0, r, e, c)
- }
- }
- def isBinomialHeapValidStep(h1: BinomialHeap, oldR: Int) : Boolean = h1 match {
- case ConsHeap(e, tail) => oldR < rank(e) && isBinomialHeapValidStep(tail, rank(e)) && isBinomialTreeValid(e)
- case NilHeap() => true
- }
- // Helper function which tell if a binomial heap is valid
- private def isBinomialHeapValid(h: BinomialHeap) : Boolean ={
- isBinomialHeapValidStep(h, -1)
- }
-
- /*private def rankIncrease(h: BinomialHeap) : Boolean = {
- h match {
- case ConsHeap(tr, tail) => {
- tail match{
- case ConsHeap(tr2, tail2) => tr < tr2 && rankIncrease(tail)
- case NilHeap => true
- }
- rank(tr) < heapRank(tail) && rankIncrease(tail)
- }
- case NilHeap() => true
- }
- }*/
-
- /* Linking trees of equal ranks depending on the root element */
- def link(t1: BinomialTree, t2: BinomialTree) : BinomialTree = {
- require(isBinomialTreeValid(t1) && isBinomialTreeValid(t2) && rank(t1) == rank(t2))
- t1 match {
- case Node(r, x1, c1) => {
- t2 match {
- case Node(_, x2, c2) => {
- if (leq(x1,x2)) {
- Node(r+1, x1, ConsHeap(t2, c1))
- } else {
- Node(r+1, x2, ConsHeap(t1, c2))
- }
- }
- }
- }
- }
- } ensuring(res => isBinomialTreeValid(res))
-
- /* Insert a tree into a binomial heap. The tree should be correct in relation to the heap */
- def insTree(t: BinomialTree, h: BinomialHeap) : BinomialHeap = {
- require(isBinomialTreeValid(t) && isBinomialHeapValid(h))// && isTreeValidForInsert(t,h))
- h match {
- case ConsHeap(head, tail) => {
- if (rank(t) < rank(head)) {
- ConsHeap(t, h)
- }else if (rank(t) > rank(head)) {
- ConsHeap(head, insTree(t,tail))
- } else {
- insTree(link(t,head), tail)
- }
- }
- case NilHeap() => ConsHeap(t, NilHeap())
- }
- } ensuring(res => isBinomialHeapValid(res))
-
- /*def mult(x : Int, y : Int) : Int = {
- if(x == 0 || y == 0) 0
- else
- mult(x-1,y-1) + x + y -1
- }*/
-
- /* Merge two heaps together */
- /*def merge(h1: BinomialHeap, h2: BinomialHeap) : BinomialHeap = {
- //require(isBinomialHeapValid(h1) && isBinomialHeapValid(h2))
- require(rankIncrease(h1) && rankIncrease(h2))
- h1 match {
- case ConsHeap(head1, tail1) => {
- h2 match {
- case ConsHeap(head2, tail2) => {
- if (rank(head1) < rank(head2)) {
- ConsHeap(head1, merge(tail1, h2))
- } else if (rank(head2) < rank(head1)) {
- ConsHeap(head2, merge(h1, tail2))
- } else {
- insTree(link(head1, head2), merge(tail1, tail2))
- }
- }
- case NilHeap() => h1
- }
- }
- case NilHeap() => h2
- }
- } ensuring(res => (treeNum(res)<=treeNum(h1)+treeNum(h2) && rankIncrease(res) && heapRank(res)>=min(heapRank(h1),heapRank(h2)))
- template((b,c,d) => time <= b*treeNum(h1) + c*treeNum(h2) + d))*/
- //ensuring(res => treeNum(res)<=treeNum(h1)+treeNum(h2) template((a,b,c,d) => time <= a*mult(treeNum(h1),treeNum(h2)) + b*treeNum(h1) + c*treeNum(h2) + d))
- //((((((2 * res4._2) + (-2 * treeNum2(h2))) + (-1 * treeNum2(h1))) + (-74 * mult2(treeNum2(h1), treeNum2(h2)))) + -6) <= 0)
- //ensuring(res => isBinomialHeapValid(res))
-
- /* Merge two heaps together */
- def merge(h1: BinomialHeap, h2: BinomialHeap): BinomialHeap = {
- require(isBinomialHeapValid(h1) && isBinomialHeapValid(h2))
- h1 match {
- case ConsHeap(head1, tail1) => {
- h2 match {
- case ConsHeap(head2, tail2) => {
- if (rank(head1) < rank(head2)) {
- ConsHeap(head1, merge(tail1, h2))
- } else if (rank(head2) < rank(head1)) {
- ConsHeap(head2, merge(h1, tail2))
- } else {
- mergeWithCarry(link(head1, head2), tail1, tail2)
- }
- }
- case NilHeap() => h1
- }
- }
- case NilHeap() => h2
- }
- } ensuring(res => isBinomialHeapValid(res))
-
- /* Helper function to validate the input tree of insTree */
- private def isValidCarry(t: BinomialTree, h: BinomialHeap) = h match {
- case ConsHeap(head, tail) => rank(t) <= rank(head)
- case NilHeap() => true
- }
-
- def mergeWithCarry(t: BinomialTree, h1: BinomialHeap, h2: BinomialHeap): BinomialHeap = {
- require(isBinomialTreeValid(t) && isBinomialHeapValid(h1) && isBinomialHeapValid(h2) && isValidCarry(t,h1) && isValidCarry(t,h2))
- t match {
- case Node(r, _, _) => {
- h1 match {
- case ConsHeap(head1, tail1) => {
- h2 match {
- case ConsHeap(head2, tail2) => {
- if (rank(head1) < rank(head2)) {
-
- if (rank(t) < rank(head1))
- ConsHeap(t, ConsHeap(head1, merge(tail1, h2)))
- else
- mergeWithCarry(link(t, head1), tail1, h2)
- } else if (rank(head2) < rank(head1)) {
-
- if (rank(t) < rank(head2))
- ConsHeap(t, ConsHeap(head2, merge(h1, tail2)))
- else
- mergeWithCarry(link(t, head2), h1, tail2)
-
- } else {
- ConsHeap(t, mergeWithCarry(link(head1, head2), tail1, tail2))
- }
- }
- case NilHeap() => {
- insTree(t, h1)
- }
- }
- }
- case NilHeap() => insTree(t, h2)
- }
- }
- }
- } ensuring (res => isBinomialHeapValid(res))
-
- /* Helper function to define ensuring clause in removeMinTree */
- private def isRemovedMinTreeValid(x : (OptionalTree, BinomialHeap)) : Boolean = {
- val (opt,h) = x
- opt match {
- case Some(t) => isBinomialTreeValid(t) && isBinomialHeapValid(h)
- case _ => isBinomialHeapValid(h)
- }
- }
-
- //Auxiliary helper function to simplefy findMin and deleteMin
- def removeMinTree(h: BinomialHeap): (OptionalTree, BinomialHeap) = {
- require(!isEmpty(h) && isBinomialHeapValid(h))
- h match {
- case ConsHeap(head, NilHeap()) => (Some(head), NilHeap())
- case ConsHeap(head1, tail1) => {
- val (opthead2, tail2) = removeMinTree(tail1)
- opthead2 match {
- case None() => (Some(head1), tail1)
- case Some(head2) =>
- if (leq(root(head1), root(head2))) {
- (Some(head1), tail1)
- } else {
- (Some(head2), ConsHeap(head1, tail2))
- }
- }
- }
- case _ => (None(), NilHeap())
- }
- } ensuring(res => isRemovedMinTreeValid(res))
-
-// def revRec(l1: BinomialHeap, l2: BinomialHeap): BinomialHeap = (l1 match {
-// case NilHeap() => l2
-// case ConsHeap(x, xs) => revRec(xs, ConsHeap(x, l2))
-//
-// })
-//
-// def rev(l: BinomialHeap): BinomialHeap = {
-// revRec(l, NilHeap())
-// }
-
- // Discard the minimum element of the extracted min tree and put its children back into the heap
- def deleteMin(h: BinomialHeap) : BinomialHeap = {
- require(!isEmpty(h) && isBinomialHeapValid(h))
- val (min, ts2) = removeMinTree(h)
- min match {
- case Some(Node(_,_,ts1)) => merge(ts1, ts2)
- case _ => h
- }
- } ensuring(res => isBinomialHeapValid(h))
-
- /* TEST AREA */
-
- /*def BTtest1() : Boolean = isBinomialTreeValid(Node(1, Element(2), ConsHeap(Node(0, Element(3), NilHeap()),NilHeap())))*/
- /*def BTtest2() : Boolean = isBinomialTreeValid(Node(0, Element(3), NilHeap()))*/
- /*def BTtest3() : Boolean = isBinomialTreeValid(Node(1, Element(975), ConsHeap(Node(0, Element(976), NilHeap()), NilHeap())))*/
- /*def BHtest1() : Boolean = isBinomialHeapValid(ConsHeap(Node(0, Element(0), Nil()),ConsHeap(Node(1, Element(0), ConsHeap(Node(0, Element(1), NilHeap()),NilHeap())),NilHeap())))*/
- /*def testInsTree1() : BinomialHeap = insTree(Node(0, Element(2), NilHeap()), ConsHeap(Node(1, Element(3), ConsHeap(Node(0, Element(4), NilHeap()),NilHeap())),NilHeap()))*/
- /*def testInsTree2() : BinomialHeap = insTree(Node(0, Element(2), NilHeap()), ConsHeap(Node(0, Element(1), NilHeap()), NilHeap()))*/
-
- /*def testMerge1() : BinomialHeap = merge(ConsHeap(Node(0, Element(1), NilHeap()), NilHeap()), ConsHeap(Node(1, Element(3), ConsHeap(Node(0, Element(4), NilHeap()),NilHeap())),NilHeap()))*/
- /*def testMerge2() : BinomialHeap = merge(ConsHeap(Node(1, Element(2), ConsHeap(Node(0, Element(4), NilHeap()),NilHeap())),NilHeap()), ConsHeap(Node(0, Element(3), NilHeap()), NilHeap()))*/
- /*def testMerge3() : BinomialHeap = merge(ConsHeap(Node(0, Element(4), NilHeap()), NilHeap()), ConsHeap(Node(0, Element(1), NilHeap()), NilHeap()))*/
-
- /*def testRemoveMinTree1() : (BinomialTree, BinomialHeap) = removeMinTree(ConsHeap(Node(0, Element(1), NilHeap()), NilHeap()))
- def testRemoveMinTree2() : (BinomialTree, BinomialHeap) = removeMinTree(testMerge1())
- def testRemoveMinTree3() : (BinomialTree, BinomialHeap) = removeMinTree(testMerge2())*/
-
- /*def testFindMin1() : Element = findMin(testMerge1())
-
- def testConcat : List = concat(ConsHeap(Node(0, Element(0), NilHeap()), NilHeap()), ConsHeap(Node(0, Element(0), NilHeap()), ConsHeap(Node(0, Element(0), NilHeap()), NilHeap())))
-
- def testRev: List = rev(ConsHeap(Node(0, Element(0), NilHeap()), ConsHeap(Node(1, Element(1), NilHeap()),ConsHeap(Node(2, Element(2), NilHeap()),NilHeap()))))*/
-
- /*def testDeleteMin1() = deleteMin(testMerge1())*/
-
- /*def sortTest() = bubbleSort(NodeL(testMerge1(), NodeL(testMerge2(), NilL())), true)
- def sortTest2() = bubbleSort(NodeL(testMerge1(), NodeL(testMerge2(), NilL())), false)*/
-
-
-
-}
diff --git a/testcases/orb-testcases/automatic/HeapSort.scala b/testcases/orb-testcases/automatic/HeapSort.scala
deleted file mode 100644
index 4354d8db5..000000000
--- a/testcases/orb-testcases/automatic/HeapSort.scala
+++ /dev/null
@@ -1,109 +0,0 @@
-import scala.collection.immutable.Set
-// import leon.Utils._
-
-object HeapSort {
- sealed abstract class List
- case class Cons(head:Int,tail:List) extends List
- case class Nil() extends List
-
- sealed abstract class Heap
- case class Leaf() extends Heap
- case class Node(rk : Int, value: Int, left: Heap, right: Heap) extends Heap
-
- private def rightHeight(h: Heap) : Int = {h match {
- case Leaf() => 0
- case Node(_,_,_,r) => rightHeight(r) + 1
- }} ensuring(_ >= 0)
-
- private def rank(h: Heap) : Int = h match {
- case Leaf() => 0
- case Node(rk,_,_,_) => rk
- }
-
- private def hasLeftistProperty(h: Heap) : Boolean = (h match {
- case Leaf() => true
- case Node(_,_,l,r) => hasLeftistProperty(l) && hasLeftistProperty(r) && rightHeight(l) >= rightHeight(r) && (rank(h) == rightHeight(h))
- })
-
- def heapSize(t: Heap): Int = {
- require(hasLeftistProperty(t))
- (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))
- h1 match {
- case Leaf() => h2
- case Node(_, v1, l1, r1) => h2 match {
- case Leaf() => h1
- case Node(_, v2, l2, r2) =>
- if(v1 > v2)
- makeT(v1, l1, merge(r1, h2))
- else
- makeT(v2, l2, merge(h1, r2))
- }
- }
- } ensuring(res => hasLeftistProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res))
-
-
- private def makeT(value: Int, left: Heap, right: Heap) : Heap = {
- if(rank(left) >= rank(right))
- Node(rank(right) + 1, value, left, right)
- else
- Node(rank(left) + 1, value, right, left)
- }
-
- def insert(element: Int, heap: Heap) : Heap = {
- require(hasLeftistProperty(heap))
-
- merge(Node(1, element, Leaf(), Leaf()), heap)
-
- } ensuring(res => heapSize(res) == heapSize(heap) + 1)
-
- def findMax(h: Heap) : Int = {
- require(hasLeftistProperty(h))
- h match {
- case Node(_,m,_,_) => m
- case Leaf() => -1000
- }
- }
-
- def removeMax(h: Heap) : Heap = {
- require(hasLeftistProperty(h))
- h match {
- case Node(_,_,l,r) => merge(l, r)
- case l @ Leaf() => l
- }
- }
-
- def listSize(l : List) : Int = (l match {
- case Nil() => 0
- case Cons(_, xs) => 1 + listSize(xs)
- }) ensuring(_ >= 0)
-
- def removeElements(h : Heap, l : List) : List = {
- require(hasLeftistProperty(h))
- h match {
- case Leaf() => l
- case _ => removeElements(removeMax(h),Cons(findMax(h),l))
-
- }} ensuring(res => heapSize(h) + listSize(l) == listSize(res))
-
- def buildHeap(l : List, h: Heap) : Heap = {
- require(hasLeftistProperty(h))
- l match {
- case Nil() => h
- case Cons(x,xs) => buildHeap(xs, insert(x, h))
-
- }} ensuring(res => hasLeftistProperty(res) && heapSize(h) + listSize(l) == heapSize(res))
-
- def sort(l: List): List = ({
-
- val heap = buildHeap(l,Leaf())
- removeElements(heap, Nil())
-
- }) ensuring(res => listSize(res) == listSize(l))
-}
diff --git a/testcases/orb-testcases/automatic/InsertionSort.scala b/testcases/orb-testcases/automatic/InsertionSort.scala
deleted file mode 100644
index ea036f298..000000000
--- a/testcases/orb-testcases/automatic/InsertionSort.scala
+++ /dev/null
@@ -1,25 +0,0 @@
-import leon.lang.invariantLang._
-
-object InsertionSort {
- sealed abstract class List
- case class Cons(head:Int,tail:List) extends List
- case class Nil() extends List
-
- def size(l : List) : Int = (l match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- })
-
- def sortedIns(e: Int, l: List): List = {
- l match {
- case Nil() => Cons(e,Nil())
- case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }
- } //ensuring(res => size(res) = size(l) + 1)
-
- def sort(l: List): List = (l match {
- case Nil() => Nil()
- case Cons(x,xs) => sortedIns(x, sort(xs))
-
- }) ensuring(res => size(res) == size(l))
-}
diff --git a/testcases/orb-testcases/automatic/LeftistHeap.scala b/testcases/orb-testcases/automatic/LeftistHeap.scala
deleted file mode 100644
index 6507f69ec..000000000
--- a/testcases/orb-testcases/automatic/LeftistHeap.scala
+++ /dev/null
@@ -1,61 +0,0 @@
-import leon.lang.invariantLang._
-
-object LeftistHeap {
- sealed abstract class Heap
- case class Leaf() extends Heap
- case class Node(rk : Int, value: Int, left: Heap, right: Heap) extends Heap
-
- private def rightHeight(h: Heap) : Int = h match {
- case Leaf() => 0
- case Node(_,_,_,r) => rightHeight(r) + 1
- }
-
- private def hasLeftistProperty(h: Heap) : Boolean = (h match {
- case Leaf() => true
- case Node(_,_,l,r) => hasLeftistProperty(l) && hasLeftistProperty(r) && rightHeight(l) >= rightHeight(r)
- })
-
- def size(t: Heap): Int = {
- (t match {
- case Leaf() => 0
- case Node(_,v, l, r) => size(l) + 1 + size(r)
- })
- }
-
- def removeMax(h: Heap) : Heap = {
- require(hasLeftistProperty(h))
- h match {
- case Node(_,_,l,r) => merge(l, r)
- case l @ Leaf() => l
- }
- } ensuring(res => size(res) >= size(h) - 1)
-
- private def merge(h1: Heap, h2: Heap) : Heap = {
- require(hasLeftistProperty(h1) && hasLeftistProperty(h2))
- h1 match {
- case Leaf() => h2
- case Node(_, v1, l1, r1) => h2 match {
- case Leaf() => h1
- case Node(_, v2, l2, r2) =>
- if(v1 > v2)
- makeT(v1, l1, merge(r1, h2))
- else
- makeT(v2, l2, merge(h1, r2))
- }
- }
- } //ensuring(res => size(res) == size(h1) + size(h2))
-
- private def makeT(value: Int, left: Heap, right: Heap) : Heap = {
- if(rightHeight(left) >= rightHeight(right))
- Node(rightHeight(right) + 1, value, left, right)
- else
- Node(rightHeight(left) + 1, value, right, left)
- }
-
- def insert(element: Int, heap: Heap) : Heap = {
- require(hasLeftistProperty(heap))
-
- merge(Node(1, element, Leaf(), Leaf()), heap)
-
- }ensuring(res => size(res) == size(heap) + 1)
-}
diff --git a/testcases/orb-testcases/automatic/ListOperations.scala b/testcases/orb-testcases/automatic/ListOperations.scala
deleted file mode 100644
index a7483304d..000000000
--- a/testcases/orb-testcases/automatic/ListOperations.scala
+++ /dev/null
@@ -1,57 +0,0 @@
-import leon.lang.invariantLang._
-
-object ListOperations {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
- def size(l: List): Int = (l match {
- case Nil() => 0
- case Cons(_, t) => 1 + size(t)
- })
-
- def append(l1: List, l2: List): List = (l1 match {
- case Nil() => l2
- case Cons(x, xs) => Cons(x, append(xs, l2))
-
- }) //ensuring (res => size(l1) + size(l2) == size(res))
-
- def reverseRec(l1: List, l2: List): List = (l1 match {
- case Nil() => l2
- case Cons(x, xs) => reverseRec(xs, Cons(x, l2))
-
- }) //ensuring (res => size(l1) + size(l2) == size(res))
-
- def reverse(l: List): List = {
- reverseRec(l, Nil())
- } ensuring (res => size(l) == size(res))
-
- def reverse2(l: List): List = {
- l match {
- case Nil() => l
- case Cons(hd, tl) => append(reverse2(tl), Cons(hd, Nil()))
- }
- } ensuring (res => size(res) == size(l))
-
-// def remove(elem: Int, l: List): List = {
-// l match {
-// case Nil() => Nil()
-// case Cons(hd, tl) => if (hd == elem) remove(elem, tl) else Cons(hd, remove(elem, tl))
-// }
-// }
-//
-// def contains(list: List, elem: Int): Boolean = (list match {
-// case Nil() => false
-// case Cons(x, xs) => x == elem || contains(xs, elem)
-// }) ensuring (res => true)
-//
-// def distinct(l: List): List = (
-// l match {
-// case Nil() => Nil()
-// case Cons(x, xs) => {
-// val newl = distinct(l)
-// if (contains(newl, x)) newl
-// else Cons(x, newl)
-// }
-// })
-}
diff --git a/testcases/orb-testcases/automatic/TreeOperations.scala b/testcases/orb-testcases/automatic/TreeOperations.scala
deleted file mode 100755
index 74e84f0f4..000000000
--- a/testcases/orb-testcases/automatic/TreeOperations.scala
+++ /dev/null
@@ -1,91 +0,0 @@
-import leon.lang.invariantLang._
-
-object TreeOperations {
-
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class Tree
- case class Node(left: Tree, value: Int, right: Tree) extends Tree
- case class Leaf() extends Tree
-
- def listSize(l: List): Int = (l match {
- case Nil() => 0
- case Cons(_, t) => 1 + listSize(t)
- })
-
- def size(t: Tree): Int = {
- t match {
- case Leaf() => 0
- case Node(l, x, r) => {
- size(l) + size(r) + 1
- }
- }
- }
-
- /* def height(t: Tree): Int = {
- t match {
- case Leaf() => 0
- case Node(l, x, r) => {
- val hl = height(l)
- val hr = height(r)
- if (hl > hr) hl + 1 else hr + 1
- }
- }
- } */
- //ensuring(res => res != size(t) + 1 template((a,b,c)=> a*size(t) + b*res +c <= 0))
-
- def insert(elem: Int, t: Tree): Tree = {
- t match {
- case Leaf() => Node(Leaf(), elem, Leaf())
- case Node(l, x, r) => if (x <= elem) Node(l, x, insert(elem, r))
- else Node(insert(elem, l), x, r)
- }
- }
- //ensuring (res => true template ((a, b, c) => a * size(t) + b * size(res) + c == 0))
-
- def addAll(l: List, t: Tree): Tree = {
- l match {
- case Nil() => t
- case Cons(x, xs) => addAll(xs, insert(x, t))
- }
- } ensuring (res => size(res) >= size(t))
-
- def remove(elem: Int, t: Tree): Tree = {
- t match {
- case Leaf() => Leaf()
- case Node(l, x, r) => {
-
- if (x < elem) Node(l, x, remove(elem, r))
- else if (x > elem) Node(remove(elem, l), x, r)
- else {
- t match {
- case Node(Leaf(), x, Leaf()) => Leaf()
- case Node(Leaf(), x, Node(_, rx, _)) => Node(Leaf(), rx, remove(rx, r))
- case Node(Node(_, lx, _), x, r) => Node(remove(lx, l), lx, r)
- case _ => Leaf()
- }
- }
- }
- }
- }
- //ensuring (res => true template ((a, b, c) => a * size(res) + b * size(t) + c <= 0))
-
- def removeAll(l: List, t: Tree): Tree = {
- l match {
- case Nil() => t
- case Cons(x, xs) => removeAll(xs, remove(x, t))
- }
- } ensuring (res => size(res) <= size(t))
-
-/* def contains(elem : Int, t : Tree) : Boolean = {
- t match {
- case Leaf() => false
- case Node(l, x, r) =>
- if(x == elem) true
- else if (x < elem) contains(elem, r)
- else contains(elem, l)
- }
- }*/
-}
\ No newline at end of file
diff --git a/testcases/orb-testcases/composition/AVLSort.scala b/testcases/orb-testcases/composition/AVLSort.scala
deleted file mode 100644
index 411e4719f..000000000
--- a/testcases/orb-testcases/composition/AVLSort.scala
+++ /dev/null
@@ -1,189 +0,0 @@
-import leon.invariant._
-import leon.instrumentation._
-import leon.math._
-
-/**
- * created by manos and modified by ravi.
- * BST property cannot be verified
- */
-object AVLTree {
- sealed abstract class List
- case class Cons(head: BigInt, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class Tree
- case class Leaf() extends Tree
- case class Node(left : Tree, value : BigInt, right: Tree, rank : BigInt) extends Tree
-
- sealed abstract class OptionInt
- case class None() extends OptionInt
- case class Some(i: BigInt) extends OptionInt
-
- // def min(i1:BigInt, i2:BigInt) : BigInt = if (i1<=i2) i1 else i2
- // def max(i1:BigInt, i2:BigInt) : BigInt = if (i1>=i2) i1 else i2
-
- def rank(t: Tree) : BigInt = {
- t match {
- case Leaf() => 0
- case Node(_,_,_,rk) => rk
- }
- }
-
- def listSize(l: List): BigInt = (l match {
- case Nil() => 0
- case Cons(_, t) => 1 + listSize(t)
- })
-
- def height(t: Tree): BigInt = {
- t match {
- case Leaf() => 0
- case Node(l, x, r, _) => {
- val hl = height(l)
- val hr = height(r)
- max(hl,hr) + 1
- }
- }
- }
-
- def size(t: Tree): BigInt = {
- (t match {
- case Leaf() => 0
- case Node(l, _, r,_) => size(l) + 1 + size(r)
- })
- }
-
- def rankHeight(t: Tree) : Boolean = t match {
- case Leaf() => true
- case Node(l,_,r,rk) => rankHeight(l) && rankHeight(r) && rk == height(t)
- }
-
- def balanceFactor(t : Tree) : BigInt = {
- t match{
- case Leaf() => 0
- case Node(l, _, r, _) => rank(l) - rank(r)
- }
- }
-
- def unbalancedInsert(t: Tree, e : BigInt) : Tree = {
- t match {
- case Leaf() => Node(Leaf(), e, Leaf(), 1)
- case Node(l,v,r,h) =>
- if (e == v) t
- else if (e < v){
- val newl = avlInsert(l,e)
- Node(newl, v, r, max(rank(newl), rank(r)) + 1)
- }
- else {
- val newr = avlInsert(r,e)
- Node(l, v, newr, max(rank(l), rank(newr)) + 1)
- }
- }
- }
-
- def avlInsert(t: Tree, e : BigInt) : Tree = {
- balance(unbalancedInsert(t,e))
- } ensuring(res => tmpl((a,b) => time <= a*height(t) + b))
-
- def deletemax(t: Tree): (Tree, OptionInt) = {
- t match {
- case Node(Leaf(), v, Leaf(), _) => (Leaf(), Some(v))
- case Node(l, v, Leaf(), _) => {
- val (newl, opt) = deletemax(l)
- opt match {
- case None() => (t, None())
- case Some(lmax) => {
- val newt = balance(Node(newl, lmax, Leaf(), rank(newl) + 1))
- (newt, Some(v))
- }
- }
- }
- case Node(_, _, r, _) => deletemax(r)
- case _ => (t, None())
- }
- } ensuring(res => tmpl((a,b) => time <= a*height(t) + b))
-
- def unbalancedDelete(t: Tree, e: BigInt): Tree = {
- t match {
- case Leaf() => Leaf() //not found case
- case Node(l, v, r, h) =>
- if (e == v) {
- if (l == Leaf()) r
- else if(r == Leaf()) l
- else {
- val (newl, opt) = deletemax(l)
- opt match {
- case None() => t
- case Some(newe) => {
- Node(newl, newe, r, max(rank(newl), rank(r)) + 1)
- }
- }
- }
- } else if (e < v) {
- val newl = avlDelete(l, e)
- Node(newl, v, r, max(rank(newl), rank(r)) + 1)
- } else {
- val newr = avlDelete(r, e)
- Node(l, v, newr, max(rank(l), rank(newr)) + 1)
- }
- }
- }
-
- def avlDelete(t: Tree, e: BigInt): Tree = {
- balance(unbalancedDelete(t, e))
- } ensuring(res => tmpl((a,b) => time <= a*height(t) + b))
-
- def balance(t:Tree) : Tree = {
- t match {
- case Leaf() => Leaf() // impossible...
- case Node(l, v, r, h) =>
- val bfactor = balanceFactor(t)
- // at this point, the tree is unbalanced
- if(bfactor > 1 ) { // left-heavy
- val newL =
- if (balanceFactor(l) < 0) { // l is right heavy
- rotateLeft(l)
- }
- else l
- rotateRight(Node(newL,v,r, max(rank(newL), rank(r)) + 1))
- }
- else if(bfactor < -1) {
- val newR =
- if (balanceFactor(r) > 0) { // r is left heavy
- rotateRight(r)
- }
- else r
- rotateLeft(Node(l,v,newR, max(rank(newR), rank(l)) + 1))
- } else t
- }
- }
-
- def rotateRight(t:Tree) = {
- t match {
- case Node(Node(ll, vl, rl, _),v,r, _) =>
-
- val hr = max(rank(rl),rank(r)) + 1
- Node(ll, vl, Node(rl,v,r,hr), max(rank(ll),hr) + 1)
-
- case _ => t // this should not happen
- } }
-
- def rotateLeft(t:Tree) = {
- t match {
- case Node(l, v, Node(lr,vr,rr,_), _) =>
-
- val hl = max(rank(l),rank(lr)) + 1
- Node(Node(l,v,lr,hl), vr, rr, max(hl, rank(rr)) + 1)
- case _ => t // this should not happen
- } }
-
- def addAll(l: List, t: Tree): Tree = {
- l match {
- case Nil() => t
- case Cons(x, xs) =>{
- val newt = avlInsert(t, x)
- addAll(xs, newt)
- }
- }
- } ensuring(res => tmpl((a,b,c) => time <= a*(listSize(l) * (height(t) + listSize(l))) + b*listSize(l) + c))
-}
-
diff --git a/testcases/orb-testcases/composition/ConstantPropagation.scala b/testcases/orb-testcases/composition/ConstantPropagation.scala
deleted file mode 100644
index 24caa45dc..000000000
--- a/testcases/orb-testcases/composition/ConstantPropagation.scala
+++ /dev/null
@@ -1,291 +0,0 @@
-import leon.lang._
-import leon.annotation._
-import leon.collection._
-import leon._
-import leon.invariant._
-import leon.instrumentation._
-
-object IntLattice {
- abstract class Element
- case class Bot() extends Element
- case class Top() extends Element
- case class BigIntVal(x: BigInt) extends Element
-
- def height: BigInt = {
- /**
- * A number that depends on the lattice definition.
- * In simplest case it has height 3 (_|_ (bot) <= BigInts <= T (top))
- */
- 3
- } ensuring(res => time <= ?)
-
- def join(oldVal: Element, newVal: Element) = (oldVal, newVal) match {
- case (Bot(), any) => any // bot is the identity for join
- case (any, Bot()) => any
- case (Top(), _) => Top() // top joined with anything is top
- case (_, Top()) => Top()
- case (BigIntVal(x), BigIntVal(y)) if (x == y) => BigIntVal(y)
- case _ =>
- //here old and new vals are different BigIntegers
- Top()
- }
-}
-
-object LatticeOps {
- import IntLattice._
-
- def add(a: Element, b: Element): Element = {
- (a, b) match {
- case (Bot(), _) => Bot()
- case (_, Bot()) => Bot()
- case (Top(), _) => Top()
- case (_, Top()) => Top()
- case (BigIntVal(x), BigIntVal(y)) => BigIntVal(x + y)
- }
- }
-
- def multiply(a: Element, b: Element): Element = {
- (a, b) match {
- case (_, BigIntVal(x)) if x == 0 => BigIntVal(0)
- case (BigIntVal(x), _) if x == 0 => BigIntVal(0)
- case (Bot(), _) => Bot()
- case (_, Bot()) => Bot()
- case (Top(), _) => Top()
- case (_, Top()) => Top()
- case (BigIntVal(x), BigIntVal(y)) => BigIntVal(x * y)
- }
- }
-}
-
-object ConstantPropagation {
- import IntLattice._
- import LatticeOps._
-
- abstract class Expr
- case class Times(lhs: Expr, rhs: Expr) extends Expr
- case class Plus(lhs: Expr, rhs: Expr) extends Expr
- case class BigIntLiteral(v: BigInt) extends Expr
- case class FunctionCall(calleeName: Identifier, args: List[Expr]) extends Expr
- case class IfThenElse(cond: Expr, thenExpr: Expr, elseExpr: Expr) extends Expr
- case class Identifier(id: BigInt) extends Expr
-
- /**
- * Definition of a function AST
- */
- case class Function(name: Identifier, params: List[Expr], body: Expr)
-
- /**
- * Assuming that the functions are ordered from callee to
- * caller and there is no mutual recursion
- */
- case class Program(funcs: List[Function])
-
- def size(l: List[Function]): BigInt = {
- l match {
- case Cons(_, t) => 1 + size(t)
- case Nil() => 0
- }
- } ensuring(_ >= 0)
-
- def sizeExprList(exprs: List[Expr]): BigInt = {
- exprs match {
- case Nil() => 0
- case Cons(currExpr, otherExprs) => sizeExpr(currExpr) + sizeExprList(otherExprs)
- }
- } ensuring(_ >= 0)
-
- def sizeExpr(e: Expr): BigInt = {
- e match {
- case Plus(l, r) => 1 + sizeExpr(l) + sizeExpr(r)
- case Times(l, r) => 1 + sizeExpr(l) + sizeExpr(r)
- case FunctionCall(c, args) => {
- 1 + sizeExprList(args)
- }
- case IfThenElse(c, th, el) =>
- 1 + sizeExpr(c) + sizeExpr(th) + sizeExpr(el)
- case _ => 1
- }
- } ensuring(_ >= 0)
-
- def sizeFuncList(funcs: List[Function]): BigInt = {
- funcs match {
- case Nil() => 0
- case Cons(currFunc, otherFuncs) =>
- 1 + sizeExpr(currFunc.body) + sizeFuncList(otherFuncs)
- }
- } ensuring(_ >= 0)
-
- def initToBot(l: List[Function]): List[(BigInt /*function id*/ , Element)] = {
- l match {
- case Nil() => Nil[(BigInt /*function id*/ , Element)]()
- case Cons(fun, tail) => Cons((fun.name.id, Bot()), initToBot(tail))
- }
- } ensuring (res => tmpl ((a, b) => time <= a * size(l) + b))
-
- def foldConstants(p: Program): Program = {
- val initVals = initToBot(p.funcs)
- val fvals = computeSummaries(p, initVals, height)
- val newfuns = transformFuns(p.funcs, fvals)
- Program(newfuns)
- } ensuring(res => tmpl((a, b, c, d, e) => time <= a*(height*sizeFuncList(p.funcs)) + b*height + c*sizeFuncList(p.funcs) + d*size(p.funcs) + e))
-
- /**
- * The initVals is the initial values for the
- * values of the functions
- */
- @compose
- def computeSummaries(p: Program, initVals: List[(BigInt /*function id*/ , Element)], noIters: BigInt): List[(BigInt /*function id*/ , Element)] = {
- require(noIters >= 0)
- if (noIters <= 0) {
- initVals
- } else
- computeSummaries(p, analyzeFuns(p.funcs, initVals, initVals), noIters - 1)
- } ensuring(res =>
- time <= ? * (noIters * sizeFuncList(p.funcs)) + ? * sizeFuncList(p.funcs) + ? * noIters + ? &&
- rec <= noIters + ? &&
- tpr <= ? * sizeFuncList(p.funcs) + ? &&
- true)
-
- /**
- * Initial fvals and oldVals are the same
- * but as the function progresses, fvals will only have the olds values
- * of the functions that are yet to be processed, whereas oldVals will remain the same.
- */
- def analyzeFuns(funcs: List[Function], fvals: List[(BigInt, Element)], oldVals: List[(BigInt, Element)]): List[(BigInt, Element)] = {
- (funcs, fvals) match {
- case (Cons(f, otherFuns), Cons((fid, fval), otherVals)) =>
- val newval = analyzeFunction(f, oldVals)
- val approxVal = join(fval, newval) //creates an approximation of newVal to ensure convergence
- Cons((fid, approxVal), analyzeFuns (otherFuns, otherVals, oldVals))
- case _ =>
- Nil[(BigInt, Element)]() //this also handles precondition violations e.g. lists aren't of same size etc.
- }
- } ensuring (res => tmpl ((a, b) => time <= a * sizeFuncList(funcs) + b))
-
- @library
- def getFunctionVal(funcId: BigInt, funcVals: List[(BigInt, Element)]): Element = {
- funcVals match {
- case Nil() => Bot()
- case Cons((currFuncId, currFuncVal), otherFuncVals) if (currFuncId == funcId) => currFuncVal
- case Cons(_, otherFuncVals) =>
- getFunctionVal(funcId, otherFuncVals)
- }
- } ensuring (res => time <= 1)
-
- def analyzeExprList(l: List[Expr], funcVals: List[(BigInt, Element)]): List[Element] = {
- l match {
- case Nil() => Nil[Element]()
- case Cons(expr, otherExprs) => Cons(analyzeExpr(expr, funcVals), analyzeExprList(otherExprs, funcVals))
- }
- } ensuring (res => tmpl ((a, b) => time <= a * sizeExprList(l) + b))
-
- /**
- * Returns the value of the expression when "abstractly BigInterpreted"
- * using the lattice.
- */
- def analyzeExpr(e: Expr, funcVals: List[(BigInt, Element)]): Element = {
- e match {
- case Times(lhs: Expr, rhs: Expr) => {
- val lval = analyzeExpr(lhs, funcVals)
- val rval = analyzeExpr(rhs, funcVals)
- multiply(lval, rval)
- }
- case Plus(lhs: Expr, rhs: Expr) => {
- val lval = analyzeExpr(lhs, funcVals)
- val rval = analyzeExpr(rhs, funcVals)
- add(lval, rval)
- }
- case FunctionCall(calleeName, args: List[Expr]) => {
- getFunctionVal(calleeName.id, funcVals)
- }
- case IfThenElse(c, th, el) => {
- //analyze then and else branches and join their values
- //TODO: this can be made more precise e.g. if 'c' is
- //a non-zero value it can only execute the then branch.
- val v1 = analyzeExpr(th, funcVals)
- val v2 = analyzeExpr(el, funcVals)
- join(v1, v2)
- }
- case lit @ BigIntLiteral(v) =>
- BigIntVal(v)
-
- case Identifier(_) => Bot()
- }
- } ensuring (res => tmpl ((a, b) => time <= a * sizeExpr(e) + b))
-
- def analyzeFunction(f: Function, oldVals: List[(BigInt, Element)]): Element = {
- // traverse the body of the function and simplify constants
- // for function calls assume the value given by oldVals
- // also for if-then-else statments, take a join of the values along if and else branches
- // assume that bot op any = bot and top op any = top (but this can be made more precise).
- analyzeExpr(f.body, oldVals)
- } ensuring (res => tmpl ((a, b) => time <= a * sizeExpr(f.body) + b))
-
- def transformExprList(l: List[Expr], funcVals: List[(BigInt, Element)]): List[Expr] = {
- l match {
- case Nil() => Nil[Expr]()
- case Cons(expr, otherExprs) => Cons(transformExpr(expr, funcVals),
- transformExprList(otherExprs, funcVals))
- }
- } ensuring (res => tmpl ((a, b) => time <= a * sizeExprList(l) + b))
-
- /**
- * Returns the folded expression
- */
- def transformExpr(e: Expr, funcVals: List[(BigInt, Element)]): Expr = {
- e match {
- case Times(lhs: Expr, rhs: Expr) => {
- val foldedLHS = transformExpr(lhs, funcVals)
- val foldedRHS = transformExpr(rhs, funcVals)
- (foldedLHS, foldedRHS) match {
- case (BigIntLiteral(x), BigIntLiteral(y)) =>
- BigIntLiteral(x * y)
- case _ =>
- Times(foldedLHS, foldedRHS)
- }
- }
- case Plus(lhs: Expr, rhs: Expr) => {
- val foldedLHS = transformExpr(lhs, funcVals)
- val foldedRHS = transformExpr(rhs, funcVals)
- (foldedLHS, foldedRHS) match {
- case (BigIntLiteral(x), BigIntLiteral(y)) =>
- BigIntLiteral(x + y)
- case _ =>
- Plus(foldedLHS, foldedRHS)
- }
- }
- case FunctionCall(calleeName, args: List[Expr]) => {
- getFunctionVal(calleeName.id, funcVals) match {
- case BigIntVal(x) =>
- BigIntLiteral(x)
- case _ =>
- val foldedArgs = transformExprList(args, funcVals)
- FunctionCall(calleeName, foldedArgs)
- }
- }
- case IfThenElse(c, th, el) => {
- val foldedCond = transformExpr(c, funcVals)
- val foldedTh = transformExpr(th, funcVals)
- val foldedEl = transformExpr(el, funcVals)
- foldedCond match {
- case BigIntLiteral(x) => {
- if (x != 0) foldedTh
- else foldedEl
- }
- case _ => IfThenElse(foldedCond, foldedTh, foldedEl)
- }
- }
- case _ => e
- }
- } ensuring (res => tmpl ((a, b) => time <= a * sizeExpr(e) + b))
-
- def transformFuns(funcs: List[Function], fvals: List[(BigInt, Element)]): List[Function] = {
- funcs match {
- case Cons(f, otherFuns) =>
- val newfun = Function(f.name, f.params, transformExpr(f.body, fvals))
- Cons(newfun, transformFuns(otherFuns, fvals))
- case _ =>
- Nil[Function]()
- }
- } ensuring (res => tmpl ((a, b) => time <= a * sizeFuncList(funcs) + b))
-}
diff --git a/testcases/orb-testcases/composition/HeapSort.scala b/testcases/orb-testcases/composition/HeapSort.scala
deleted file mode 100644
index a95e6e114..000000000
--- a/testcases/orb-testcases/composition/HeapSort.scala
+++ /dev/null
@@ -1,147 +0,0 @@
-import scala.collection.immutable.Set
-import leon.invariant._
-import leon.instrumentation._
-import leon.annotation._
-import leon.lang._
-
-object HeapSort {
- sealed abstract class List
- case class Cons(head: BigInt, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class Heap
- case class Leaf() extends Heap
- case class Node(rk: BigInt, value: BigInt, left: Heap, right: Heap) extends Heap
-
- @monotonic
- def log(x: BigInt): BigInt = {
- require(x >= 0)
- if (x <= 1) 0
- else {
- 1 + log(x / 2)
- }
- } ensuring (_ >= 0)
-
- // @library
- // def logMonotone(x: BigInt, y: BigInt) = {
- // require(x >= 0 && y >=0 )
- // if(x <= y) log(x) <= log(y)
- // else log(x) >= log(y)
- // } holds
-
- @library
- def heapSize(t: Heap): BigInt = {
- require(hasLeftistProperty(t))
- t match {
- case Leaf() => 0
- case Node(_, v, l, r) => heapSize(l) + 1 + heapSize(r)
- }
- } ensuring (res => res >= 0 && rightHeight(t) <= log(res) + 1)
-
- private def rightHeight(h: Heap): BigInt = {
- h match {
- case Leaf() => 0
- case Node(_, _, _, r) => rightHeight(r) + 1
- }
- } ensuring (res => res >= 0)
-
- private def rank(h: Heap): BigInt = h match {
- case Leaf() => 0
- case Node(rk, _, _, _) => rk
- }
-
- private def hasLeftistProperty(h: Heap): Boolean = (h match {
- case Leaf() => true
- case Node(_, _, l, r) => hasLeftistProperty(l) && hasLeftistProperty(r) && rightHeight(l) >= rightHeight(r) && (rank(h) == rightHeight(h))
- })
-
- def leftRightHeight(h: Heap): BigInt = {
- h match {
- case Leaf() => 0
- case Node(_, _, l, r) => rightHeight(l)
- }
- }
-
- // @library
- private def merge(h1: Heap, h2: Heap): Heap = {
- require(hasLeftistProperty(h1) && hasLeftistProperty(h2))
- h1 match {
- case Leaf() => h2
- case Node(_, v1, l1, r1) => h2 match {
- case Leaf() => h1
- case Node(_, v2, l2, r2) =>
- if (v1 > v2)
- makeT(v1, l1, merge(r1, h2))
- else
- makeT(v2, l2, merge(h1, r2))
- }
- }
- } ensuring (res => hasLeftistProperty(res) && heapSize(res) == heapSize(h1) + heapSize(h2) &&
- //time <= ? * rightHeight(h1) + ? * rightHeight(h2) + ? )
- time <= 35*rightHeight(h1) + 35*rightHeight(h2) + 2)
-
- private def makeT(value: BigInt, left: Heap, right: Heap): Heap = {
- require(hasLeftistProperty(left) && hasLeftistProperty(right))
- if (rank(left) >= rank(right))
- Node(rank(right) + 1, value, left, right)
- else
- Node(rank(left) + 1, value, right, left)
- }
-
- // @library
- def insert(element: BigInt, heap: Heap): Heap = {
- require(hasLeftistProperty(heap))
-
- merge(Node(1, element, Leaf(), Leaf()), heap)
-
- } ensuring(res => heapSize(res) == heapSize(heap) + 1 &&
- time <= 35*rightHeight(heap) + 41)
-
- // def findMax(h: Heap) : BigInt = {
- // require(hasLeftistProperty(h))
- // h match {
- // case Node(_,m,_,_) => m
- // case Leaf() => -1000
- // }
- // }
-
- // def removeMax(h: Heap) : Heap = {
- // require(hasLeftistProperty(h))
- // h match {
- // case Node(_,_,l,r) => merge(l, r)
- // case l @ Leaf() => l
- // }
- // } ensuring(res => true && tmpl((a,b) => time <= a*leftRightHeight(h) + b))
-
- // def listSize(l: List): BigInt = (l match {
- // case Nil() => 0
- // case Cons(_, xs) => 1 + listSize(xs)
- // }) ensuring (_ >= 0)
-
- // def removeElements(h : Heap, l : List) : List = {
- // require(hasLeftistProperty(h))
- // h match {
- // case Leaf() => l
- // case _ => removeElements(removeMax(h),Cons(findMax(h),l))
- // }
- // } ensuring(res => heapSize(h) + listSize(l) == listSize(res))
-
- // @compose
- // def buildHeap(l: List, h: Heap): Heap = {
- // require(hasLeftistProperty(h))
- // l match {
- // case Nil() => h
- // case Cons(x, xs) => buildHeap(xs, insert(x, h))
- // }
- // } ensuring (res => hasLeftistProperty(res) &&
- // heapSize(res) >= heapSize(h) &&
- // logMonotone(heapSize(h), heapSize(res)) &&
- // tpr <= ? * log(heapSize(res)) + ? &&
- // rec <= ? * listSize(l) + ? &&
- // time <= ? *(listSize(l)*log(heapSize(res))) + ? *log(heapSize(res)) + ?)
-
- // def sort(l: List): List = ({
- // val heap = buildHeap(l,Leaf())
- // removeElements(heap, Nil())
- // }) ensuring(res => listSize(res) == listSize(l))
-}
\ No newline at end of file
diff --git a/testcases/orb-testcases/composition/HeapSort2.scala b/testcases/orb-testcases/composition/HeapSort2.scala
deleted file mode 100644
index b6edc137b..000000000
--- a/testcases/orb-testcases/composition/HeapSort2.scala
+++ /dev/null
@@ -1,132 +0,0 @@
-import scala.collection.immutable.Set
-import leon.invariant._
-import leon.instrumentation._
-import leon.annotation._
-import leon.lang._
-
-object LeftistHeap {
- sealed abstract class List
- case class Cons(head: BigInt, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class Heap
- case class Leaf() extends Heap
- case class Node(rk : BigInt, value: BigInt, left: Heap, right: Heap) extends Heap
-
- private def rightHeight(h: Heap) : BigInt = {
- h match {
- case Leaf() => 0
- case Node(_,_,_,r) => rightHeight(r) + 1
- }
- } ensuring (res => res >= 0)
-
- private def rank(h: Heap) : BigInt = h match {
- case Leaf() => 0
- case Node(rk,_,_,_) => rk
- }
-
- private def hasLeftistProperty(h: Heap) : Boolean = (h match {
- case Leaf() => true
- case Node(_,_,l,r) => hasLeftistProperty(l) && hasLeftistProperty(r) && rightHeight(l) >= rightHeight(r) && (rank(h) == rightHeight(h))
- })
-
- @monotonic
- def log(x: BigInt): BigInt = {
- require(x >= 0)
- if (x <= 1) 0
- else {
- 1 + log(x / 2)
- }
- } ensuring (_ >= 0)
-
- def heapSize(t: Heap): BigInt = {
- require(hasLeftistProperty(t))
- (t match {
- case Leaf() => 0
- case Node(_,v, l, r) => heapSize(l) + 1 + heapSize(r)
- })
- } ensuring (res => res >= 0 && rightHeight(t) <= log(res) + 1)
-
- def listSize(l: List): BigInt = (l match {
- case Nil() => 0
- case Cons(_, xs) => 1 + listSize(xs)
- }) ensuring (_ >= 0)
-
- def leftRightHeight(h: Heap) : BigInt = {h match {
- case Leaf() => 0
- case Node(_,_,l,r) => rightHeight(l)
- }}
-
- @library
- private def merge(h1: Heap, h2: Heap) : Heap = {
- require(hasLeftistProperty(h1) && hasLeftistProperty(h2))
- h1 match {
- case Leaf() => h2
- case Node(_, v1, l1, r1) => h2 match {
- case Leaf() => h1
- case Node(_, v2, l2, r2) =>
- if(v1 > v2)
- makeT(v1, l1, merge(r1, h2))
- else
- makeT(v2, l2, merge(h1, r2))
- }
- }
- } ensuring(res => hasLeftistProperty(res) && heapSize(res) == heapSize(h1) + heapSize(h2) && time <= 35 * rightHeight(h1) + 35 * rightHeight(h2) + 2)
-
- private def makeT(value: BigInt, left: Heap, right: Heap) : Heap = {
- if(rank(left) >= rank(right))
- Node(rank(right) + 1, value, left, right)
- else
- Node(rank(left) + 1, value, right, left)
- }
-
- @library
- def insert(element: BigInt, heap: Heap) : Heap = {
- require(hasLeftistProperty(heap))
-
- merge(Node(1, element, Leaf(), Leaf()), heap)
- } ensuring(res => hasLeftistProperty(res) && heapSize(res) == heapSize(heap) + 1 && time <= 35 * rightHeight(heap) + 41)
-
- // // @compose
- // @library
- // def buildHeap(l: List, h: Heap): Heap = {
- // require(hasLeftistProperty(h))
- // l match {
- // case Nil() => h
- // case Cons(x, xs) => buildHeap(xs, insert(x, h))
- // }
- // } ensuring (res => hasLeftistProperty(res) && heapSize(res) >= heapSize(h) &&
- // // rec <= 1 * listSize(l) + 1 &&
- // // tpr <= ? * log(heapSize(res)) + ? &&
- // // time <= ? * (listSize(l) * log(heapSize(res))) + ? * log(heapSize(res)) + ? * listSize(l) + ?)
- // (((-20 * listSize(l) + -260 * log(heapSize(res86._1))) + time) + -130 * (listSize(l) * log(heapSize(res86._1)))) + -40 <= 0)
-
- def findMax(h: Heap) : BigInt = {
- require(hasLeftistProperty(h) && h != Leaf())
- h match {
- case Node(_,m,_,_) => m
- case Leaf() => -1000
- }
- }
-
- @library
- def removeMax(h: Heap) : Heap = {
- require(hasLeftistProperty(h) && h != Leaf())
- h match {
- case Node(_,_,l,r) => merge(l, r)
- case l @ Leaf() => l
- }
- } ensuring(res => hasLeftistProperty(res) && heapSize(h) - 1 == heapSize(res) && time <= 70 * leftRightHeight(h) + 7)
-
- // @compose
- def removeElements(h : Heap, l : List) : List = {
- require(hasLeftistProperty(h))
- h match {
- case Leaf() => l
- case _ => removeElements(removeMax(h),Cons(findMax(h),l))
- }
- } ensuring(res => heapSize(h) + listSize(l) == listSize(res) &&
- /*rec <= ? * heapSize(h) + ? &&*/
- tpr <= ? * log(heapSize(h)) + ? /*&&
- time <= ? * (heapSize(h) * log(heapSize(h))) + ? * heapSize(h) + ? * log(heapSize(h)) + ?*/)
-}
diff --git a/testcases/orb-testcases/composition/InsertionSort.scala b/testcases/orb-testcases/composition/InsertionSort.scala
deleted file mode 100644
index 483d30cbe..000000000
--- a/testcases/orb-testcases/composition/InsertionSort.scala
+++ /dev/null
@@ -1,30 +0,0 @@
-import leon.invariant._
-import leon.instrumentation._
-import leon.annotation._
-
-object InsertionSort {
- sealed abstract class List
- case class Cons(head: BigInt, tail:List) extends List
- case class Nil() extends List
-
- def size(l : List) : BigInt = (l match {
- case Cons(_, xs) => 1 + size(xs)
- case _ => 0
- })
-
- def sortedIns(e: BigInt, l: List): List = {
- l match {
- case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- case _ => Cons(e,Nil())
- }
- } ensuring(res => size(res) == size(l) + 1 && time <= ? * size(l) + ?)
-
- @compose
- def sort(l: List): List = (l match {
- case Cons(x,xs) => sortedIns(x, sort(xs))
- case _ => Nil()
- }) ensuring(res => size(res) == size(l) &&
- time <= ? * (size(l) * size(l)) + ? &&
- rec <= ? * size(l) + ? &&
- tpr <= ? * size(l) + ?)
-}
diff --git a/testcases/orb-testcases/composition/LeftistHeap.scala b/testcases/orb-testcases/composition/LeftistHeap.scala
deleted file mode 100644
index 5c2f2555a..000000000
--- a/testcases/orb-testcases/composition/LeftistHeap.scala
+++ /dev/null
@@ -1,113 +0,0 @@
-import leon.invariant._
-import leon.instrumentation._
-import leon.annotation._
-
-object LeftistHeap {
- sealed abstract class List
- case class Cons(head:BigInt,tail:List) extends List
- case class Nil() extends List
-
- sealed abstract class Heap
- case class Leaf() extends Heap
- case class Node(rk : BigInt, value: BigInt, left: Heap, right: Heap) extends Heap
-
- private def rightHeight(h: Heap) : BigInt = h match {
- case Leaf() => 0
- case Node(_,_,_,r) => rightHeight(r) + 1
- }
-
- private def rank(h: Heap) : BigInt = h match {
- case Leaf() => 0
- case Node(rk,_,_,_) => rk
- }
-
- private def hasLeftistProperty(h: Heap) : Boolean = (h match {
- case Leaf() => true
- case Node(_,_,l,r) => hasLeftistProperty(l) && hasLeftistProperty(r) && rightHeight(l) >= rightHeight(r) && (rank(h) == rightHeight(h))
- })
-
- @monotonic
- def twopower(x: BigInt) : BigInt = {
- require(x >= 0)
- if(x < 1) 1
- else
- 2* twopower(x - 1)
- }
-
- def heapSize(t: Heap): BigInt = {
- require(hasLeftistProperty(t))
- (t match {
- case Leaf() => 0
- case Node(_,v, l, r) => heapSize(l) + 1 + heapSize(r)
- })
- } ensuring (res => tmpl((a,b) => twopower(rightHeight(t)) <= a*res + b)/* _ >= 0*/)
-
- def leftRightHeight(h: Heap) : BigInt = {h match {
- case Leaf() => 0
- case Node(_,_,l,r) => rightHeight(l)
- }}
-
- def listSize(l : List) : BigInt = (l match {
- case Nil() => 0
- case Cons(_, xs) => 1 + listSize(xs)
- }) ensuring(_ >= 0)
-
- def removeMax(h: Heap) : Heap = {
- require(hasLeftistProperty(h))
- h match {
- case Node(_,_,l,r) => merge(l, r)
- case l @ Leaf() => l
- }
- } ensuring(res => /*hasLeftistProperty(res)*/ /*&& (if (h != Leaf()) heapSize(res) == heapSize(h) - 1 else true) &&*/ tmpl((a,b) => time <= a*leftRightHeight(h) + b))
-
- private def merge(h1: Heap, h2: Heap) : Heap = {
- require(hasLeftistProperty(h1) && hasLeftistProperty(h2))
- h1 match {
- case Leaf() => h2
- case Node(_, v1, l1, r1) => h2 match {
- case Leaf() => h1
- case Node(_, v2, l2, r2) =>
- if(v1 > v2)
- makeT(v1, l1, merge(r1, h2))
- else
- makeT(v2, l2, merge(h1, r2))
- }
- }
- } ensuring(res => hasLeftistProperty(res) && tmpl((a,b,c) => time <= a*rightHeight(h1) + b*rightHeight(h2) + c))
-
- private def makeT(value: BigInt, left: Heap, right: Heap) : Heap = {
- if(rank(left) >= rank(right))
- Node(rank(right) + 1, value, left, right)
- else
- Node(rank(left) + 1, value, right, left)
- }
-
- def insert(element: BigInt, heap: Heap) : Heap = {
- require(hasLeftistProperty(heap))
- merge(Node(1, element, Leaf(), Leaf()), heap)
- } ensuring(res => hasLeftistProperty(res) && tmpl((a,b,c) => time <= a*rightHeight(heap) + c))
-
- /*def buildHeap(l : List, h: Heap) : Heap = {
- require(hasLeftistProperty(h))
- l match {
- case Nil() => h
- case Cons(x,xs) => buildHeap(xs, insert(x, h))
- }
- } ensuring(res => hasLeftistProperty(res) && heapSize(h) + listSize(l) == heapSize(res) tmpl((a, b, c) => nonRecTime <= a*rightHeight(h) + b && rec <= listSize(l) + c))
-
- def findMax(h: Heap) : BigInt = {
- require(hasLeftistProperty(h))
- h match {
- case Node(_,m,_,_) => m
- case Leaf() => -1000
- }
- }
-
- def removeElements(h : Heap, l : List) : List = {
- require(hasLeftistProperty(h))
- h match {
- case Leaf() => l
- case _ => removeElements(removeMax(h),Cons(findMax(h),l))
- }
- }*/ //ensuring(res => /*heapSize(h) + listSize(l) == listSize(res)*/ tmpl((a, b, c) => nonRecTime <= a*leftRightHeight(h) + b /*&& rec <= heapSize(h) + c*/))
-}
diff --git a/testcases/orb-testcases/composition/MergeSort.scala b/testcases/orb-testcases/composition/MergeSort.scala
deleted file mode 100644
index 971237608..000000000
--- a/testcases/orb-testcases/composition/MergeSort.scala
+++ /dev/null
@@ -1,150 +0,0 @@
-import leon.invariant._
-import leon.instrumentation._
-<<<<<<< HEAD
-
-=======
->>>>>>> b03689012b84b65708b49a01c70e68ceb6f413bf
-import leon.annotation._
-
-object MergeSort {
- sealed abstract class List
- case class Cons(head:BigInt,tail:List) extends List
- case class Nil() extends List
-<<<<<<< HEAD
-
- @monotonic
- def log(x: BigInt) : BigInt = {
- require(x >= 0)
- if(x <= 1) -1
- else {
- // val k = x/2
- // 1 + log(x - k)
- 1 + log(x / 2)
- }
- } ensuring(res => true && res >= -1)
-
- def size(list:List): BigInt = {list match {
- case Nil() => 0
- case Cons(x,xs) => 1 + size(xs)
- }} ensuring(res => true && res >= 0)
-=======
-
- def size(list:List): BigInt = {list match {
- case Nil() => 0
- case Cons(x,xs) => 1 + size(xs)
- }} ensuring(res => res >= 0)
->>>>>>> b03689012b84b65708b49a01c70e68ceb6f413bf
-
- def length(l:List): BigInt = {
- l match {
- case Nil() => 0
- case Cons(x,xs) => 1 + length(xs)
- }
-<<<<<<< HEAD
- } ensuring(res => res == size(l) /*&& tmpl((a,b) => time <= a*size(l) + b)*/)
-=======
- } ensuring(res => res == size(l) && time <= ? *size(l) + ?)
->>>>>>> b03689012b84b65708b49a01c70e68ceb6f413bf
-
- def split(l:List,n:BigInt): (List,List) = {
- require(n >= 0 && n <= size(l))
- if (n <= 0) (Nil(),l)
- else
-<<<<<<< HEAD
- l match {
- case Nil() => (Nil(),l)
- case Cons(x,xs) => {
- if(n == 1) (Cons(x,Nil()), xs)
- else {
- val (fst,snd) = split(xs, n-1)
- (Cons(x,fst), snd)
- }
- }
- }
- } ensuring(res => size(res._2) == size(l) - n && size(res._1) == n && size(res._2) + size(res._1) == size(l) /*&& tmpl((a,b) => time <= a*n +b)*/)
-=======
- l match {
- case Nil() => (Nil(),l)
- case Cons(x,xs) => {
- if(n == 1) (Cons(x,Nil()), xs)
- else {
- val (fst,snd) = split(xs, n-1)
- (Cons(x,fst), snd)
- }
- }
- }
- } ensuring(res => size(res._2) + size(res._1) == size(l) && time <= ? *n + ?)
->>>>>>> b03689012b84b65708b49a01c70e68ceb6f413bf
-
- def merge(aList:List, bList:List):List = (bList match {
- case Nil() => aList
- case Cons(x,xs) =>
-<<<<<<< HEAD
- aList match {
- case Nil() => bList
- case Cons(y,ys) =>
- if (y < x)
- Cons(y,merge(ys, bList))
- else
- Cons(x,merge(aList, xs))
- }
- }) ensuring(res => size(aList) + size(bList) == size(res) /*&& tmpl((a,b,c) => time <= a*size(aList) + b*size(bList) + c)*/)
-
- // @compose
-=======
- aList match {
- case Nil() => bList
- case Cons(y,ys) =>
- if (y < x)
- Cons(y,merge(ys, bList))
- else
- Cons(x,merge(aList, xs))
- }
- }) ensuring(res => size(aList)+size(bList) == size(res) && time <= ? *size(aList) + ? *size(bList) + ?)
-
- @compose
->>>>>>> b03689012b84b65708b49a01c70e68ceb6f413bf
- def mergeSort(list:List):List = {
- list match {
- case Cons(x,Nil()) => list
- case Cons(_,Cons(_,_)) =>
-<<<<<<< HEAD
- val lby2 = length(list)/2
- val (fst,snd) = split(list,lby2)
- merge(mergeSort(fst),mergeSort(snd))
-
- case _ => list
- }} ensuring(res => size(res) == size(list) &&
- //time <= ? * (size(list) * size(list)) + ? &&
- (if (size(list) >= 10) rec <= 1 * size(list) + 2 * log(size(list)) + 2 else true) &&
- //tpr <= ? * size(list) + ?
- true)
-
-
- // def mergeSort(list : List): (List, BigInt) = {
- // val bd =
- // list match {
- // case Cons(x,Nil()) => (list, BigInt(0))
- // case Cons(_,Cons(_,_)) => {
- // val e23 = split(list, length(list) / BigInt(2));
- // val e32 = mergeSort(e23._1);
- // val e30 = mergeSort(e23._2);
- // (merge(e32._1, e30._1), ((BigInt(2) + e32._2) + e30._2))
- // }
- // case _ => (list, BigInt(0))
- // };
- // (bd._1, bd._2)
- // } ensuring(res => size(res._1) == size(list) &&
- // //time <= ? * (size(list) * size(list)) + ? &&
- // (if (size(list) >= 10) res._2 <= 1 * size(list) + 2 * log(size(list)) + 2 else true) &&
- // //tpr <= ? * size(list) + ?
- // true)
-=======
- val lby2 = length(list)/2
- val (fst,snd) = split(list,lby2)
- merge(mergeSort(fst),mergeSort(snd))
-
- case _ => list
- }} ensuring(res => time <= ? *(size(list)*size(list)) + b && tpr <= ? *size(list) + ? && rec <= ? *size(list))
->>>>>>> b03689012b84b65708b49a01c70e68ceb6f413bf
-}
diff --git a/testcases/orb-testcases/composition/QuickSort.scala b/testcases/orb-testcases/composition/QuickSort.scala
deleted file mode 100644
index cff28d0a1..000000000
--- a/testcases/orb-testcases/composition/QuickSort.scala
+++ /dev/null
@@ -1,44 +0,0 @@
-import leon.invariant._
-import leon.instrumentation._
-import leon.annotation._
-
-object QuickSort {
- sealed abstract class List
- case class Cons(head:BigInt,tail:List) extends List
- case class Nil() extends List
-
- def size(l:List): BigInt = {l match {
- case Nil() => 0
- case Cons(x,xs) => 1 + size(xs)
- }}
-
- case class Triple(fst:List,snd:List, trd: List)
-
- def append(aList:List,bList:List): List = {aList match {
- case Nil() => bList
- case Cons(x, xs) => Cons(x,append(xs,bList))
- }} ensuring(res => size(res) == size(aList) + size(bList) && time <= ? *size(aList) + ?)
-
- def partition(n:BigInt,l:List) : Triple = (l match {
- case Nil() => Triple(Nil(), Nil(), Nil())
- case Cons(x,xs) => {
- val t = partition(n,xs)
- if (n < x) Triple(t.fst, t.snd, Cons(x,t.trd))
- else if(n == x) Triple(t.fst, Cons(x,t.snd), t.trd)
- else Triple(Cons(x,t.fst), t.snd, t.trd)
- }
- }) ensuring(res => (size(l) == size(res.fst) + size(res.snd) + size(res.trd)) && time <= ? *size(l) + ?)
-
- @compose
- def quickSort(l:List): List = (l match {
- case Nil() => Nil()
- case Cons(x,Nil()) => l
- case Cons(x,xs) => {
- val t = partition(x, xs)
- append(append(quickSort(t.fst), Cons(x, t.snd)), quickSort(t.trd))
- }
- case _ => l
- })ensuring(res => size(res) == size(l) && time <= ? *(size(l)*size(l)) + ? *size(l) + ? &&
- tpr <= ? *size(l) + ? && rec <= ? *size(l))
-}
-
diff --git a/testcases/orb-testcases/composition/Z3-exception-output.txt b/testcases/orb-testcases/composition/Z3-exception-output.txt
deleted file mode 100644
index e1dab02bb..000000000
--- a/testcases/orb-testcases/composition/Z3-exception-output.txt
+++ /dev/null
@@ -1,68 +0,0 @@
- Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
-[Warning ] Second case - Z3 AST: 281474976710656 tpe: BigInt
-[Warning ] Unexpected target type for BV value: BigInt
--
GitLab