From 82f37c6b07c327eefdec180a002ee3e1a038c668 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Wed, 20 Nov 2013 16:16:57 +0100
Subject: [PATCH] Consolidate and re-organize testcases
---
testcases/Account.scala | 13 --
testcases/AddressBook.scala | 16 ---
testcases/Interpret.scala | 2 -
testcases/MutuallyRecursive.scala | 40 +++---
testcases/Naturals.scala | 8 +-
testcases/PropositionalLogic.scala | 59 +++++++++
testcases/README | 2 -
testcases/SimpInterpret.scala | 6 +-
.../AmortizedQueue.scala} | 27 ++---
.../BinarySearchTree.scala} | 3 -
testcases/datastructures/BinaryTrie.scala | 68 +++++++++++
testcases/datastructures/HeapSort.scala | 114 ++++++++++++++++++
.../{ => datastructures}/InsertionSort.scala | 27 +----
testcases/datastructures/LeftistHeap.scala | 67 ++++++++++
.../{ => datastructures}/ListWithSize.scala | 4 +-
.../{ => datastructures}/MergeSort.scala | 37 +++---
.../{ => datastructures}/QuickSort.scala | 2 +-
.../{ => datastructures}/RedBlackTree.scala | 14 +--
.../{ => datastructures}/SortedList.scala | 4 +-
.../TreeListSetNoDup.scala | 12 +-
.../{ => graveyard}/BinarySearchTree.scala | 8 +-
testcases/{ => graveyard}/Choose.scala | 0
testcases/{ => graveyard}/ConnectedTest.scala | 0
testcases/{ => graveyard}/Expr2Comp.scala | 0
testcases/{ => graveyard}/ExprComp.scala | 0
.../{ => graveyard}/PaperDemoExample.scala | 0
testcases/{ => graveyard}/Sat.scala | 0
testcases/{ => graveyard}/SetOperations.scala | 0
testcases/{ => graveyard}/SortedTree.scala | 0
testcases/{ => graveyard}/Test.scala | 0
.../{ => graveyard}/UnificationTest.scala | 32 ++---
.../UseContradictoryLemma.scala | 0
testcases/{ => graveyard}/VerySimple.scala | 0
testcases/{ => graveyard}/Viktor.scala | 0
.../{ => graveyard}/malkis/Hardest.scala | 0
.../{ => graveyard/multisets}/MultiBug.scala | 0
.../multisets}/MultiExample.scala | 0
.../multisets}/MultisetOperations.scala | 0
testcases/runtime/CachedList.scala | 42 +++++++
testcases/runtime/SquareRoot.scala | 28 +++++
testcases/{ => xlang}/AbsArray.scala | 0
testcases/{ => xlang}/AbsFun.scala | 0
testcases/{ => xlang}/Add.scala | 0
.../ArrayBinarySearch.scala} | 0
.../ArrayBinarySearchProcedural.scala} | 0
testcases/{ => xlang}/BinaryTreeImp.scala | 8 +-
testcases/{ => xlang}/BubbleFun.scala | 0
testcases/{ => xlang}/BubbleSort.scala | 0
.../{ => xlang}/BubbleWeakInvariant.scala | 0
testcases/{ => xlang}/InsertionSortImp.scala | 0
testcases/{ => xlang}/IntOperations.scala | 0
testcases/{ => xlang}/LinearSearch.scala | 0
testcases/{ => xlang}/ListImp.scala | 0
testcases/{ => xlang}/MaxSum.scala | 0
testcases/{ => xlang}/Mult.scala | 0
.../{ => xlang}/NonDeterministicList.scala | 0
testcases/{ => xlang}/QuickSortImp.scala | 0
testcases/{ => xlang}/buggyEpsilon.scala | 0
.../master-thesis-regis/Arithmetic.scala | 0
.../master-thesis-regis/ArrayBubbleSort.scala | 0
.../master-thesis-regis/ArrayOperations.scala | 0
.../master-thesis-regis/Constraints.scala | 0
.../master-thesis-regis/ListOperations.scala | 0
testcases/{ => xlang}/xplusone.scala | 0
64 files changed, 480 insertions(+), 163 deletions(-)
delete mode 100644 testcases/Account.scala
delete mode 100644 testcases/AddressBook.scala
create mode 100644 testcases/PropositionalLogic.scala
delete mode 100644 testcases/README
rename testcases/{AmortizedQueueStrongSpec.scala => datastructures/AmortizedQueue.scala} (91%)
rename testcases/{BSTSimpler.scala => datastructures/BinarySearchTree.scala} (97%)
create mode 100644 testcases/datastructures/BinaryTrie.scala
create mode 100644 testcases/datastructures/HeapSort.scala
rename testcases/{ => datastructures}/InsertionSort.scala (74%)
create mode 100644 testcases/datastructures/LeftistHeap.scala
rename testcases/{ => datastructures}/ListWithSize.scala (98%)
rename testcases/{ => datastructures}/MergeSort.scala (68%)
rename testcases/{ => datastructures}/QuickSort.scala (99%)
rename testcases/{ => datastructures}/RedBlackTree.scala (97%)
rename testcases/{ => datastructures}/SortedList.scala (99%)
rename testcases/{ => datastructures}/TreeListSetNoDup.scala (90%)
rename testcases/{ => graveyard}/BinarySearchTree.scala (95%)
rename testcases/{ => graveyard}/Choose.scala (100%)
rename testcases/{ => graveyard}/ConnectedTest.scala (100%)
rename testcases/{ => graveyard}/Expr2Comp.scala (100%)
rename testcases/{ => graveyard}/ExprComp.scala (100%)
rename testcases/{ => graveyard}/PaperDemoExample.scala (100%)
rename testcases/{ => graveyard}/Sat.scala (100%)
rename testcases/{ => graveyard}/SetOperations.scala (100%)
rename testcases/{ => graveyard}/SortedTree.scala (100%)
rename testcases/{ => graveyard}/Test.scala (100%)
rename testcases/{ => graveyard}/UnificationTest.scala (88%)
rename testcases/{ => graveyard}/UseContradictoryLemma.scala (100%)
rename testcases/{ => graveyard}/VerySimple.scala (100%)
rename testcases/{ => graveyard}/Viktor.scala (100%)
rename testcases/{ => graveyard}/malkis/Hardest.scala (100%)
rename testcases/{ => graveyard/multisets}/MultiBug.scala (100%)
rename testcases/{ => graveyard/multisets}/MultiExample.scala (100%)
rename testcases/{ => graveyard/multisets}/MultisetOperations.scala (100%)
create mode 100644 testcases/runtime/CachedList.scala
create mode 100644 testcases/runtime/SquareRoot.scala
rename testcases/{ => xlang}/AbsArray.scala (100%)
rename testcases/{ => xlang}/AbsFun.scala (100%)
rename testcases/{ => xlang}/Add.scala (100%)
rename testcases/{BinarySearchFun.scala => xlang/ArrayBinarySearch.scala} (100%)
rename testcases/{BinarySearch.scala => xlang/ArrayBinarySearchProcedural.scala} (100%)
rename testcases/{ => xlang}/BinaryTreeImp.scala (98%)
rename testcases/{ => xlang}/BubbleFun.scala (100%)
rename testcases/{ => xlang}/BubbleSort.scala (100%)
rename testcases/{ => xlang}/BubbleWeakInvariant.scala (100%)
rename testcases/{ => xlang}/InsertionSortImp.scala (100%)
rename testcases/{ => xlang}/IntOperations.scala (100%)
rename testcases/{ => xlang}/LinearSearch.scala (100%)
rename testcases/{ => xlang}/ListImp.scala (100%)
rename testcases/{ => xlang}/MaxSum.scala (100%)
rename testcases/{ => xlang}/Mult.scala (100%)
rename testcases/{ => xlang}/NonDeterministicList.scala (100%)
rename testcases/{ => xlang}/QuickSortImp.scala (100%)
rename testcases/{ => xlang}/buggyEpsilon.scala (100%)
rename testcases/{ => xlang}/master-thesis-regis/Arithmetic.scala (100%)
rename testcases/{ => xlang}/master-thesis-regis/ArrayBubbleSort.scala (100%)
rename testcases/{ => xlang}/master-thesis-regis/ArrayOperations.scala (100%)
rename testcases/{ => xlang}/master-thesis-regis/Constraints.scala (100%)
rename testcases/{ => xlang}/master-thesis-regis/ListOperations.scala (100%)
rename testcases/{ => xlang}/xplusone.scala (100%)
diff --git a/testcases/Account.scala b/testcases/Account.scala
deleted file mode 100644
index 66c5e352a..000000000
--- a/testcases/Account.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-object Account {
- sealed abstract class AccLike
- case class Acc(checking : Int, savings : Int) extends AccLike
-
- def sameTotal(a1 : Acc, a2 : Acc) : Boolean = {
- a1.checking + a1.savings == a2.checking + a2.savings
- }
-
- def toSavings(x : Int, a : Acc) : Acc = {
- require (x >= 0 && a.checking >= x)
- Acc(a.checking - x, a.savings + x)
- } ensuring (res => (res.checking >= 0 && sameTotal(a, res)))
-}
diff --git a/testcases/AddressBook.scala b/testcases/AddressBook.scala
deleted file mode 100644
index aaad0040a..000000000
--- a/testcases/AddressBook.scala
+++ /dev/null
@@ -1,16 +0,0 @@
-import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
-
-// Ongoing work: take Chapter 2 of Daniel Jackson's book,
-// adapt the addressbook example from there.
-object AddressBook {
- sealed abstract class U1
- case class Name(v : Int) extends U1
-
- sealed abstract class U2
- case class Addr(v : Int) extends U2
-
- sealed abstract class U3
- case class Book(addr : Map[Name, Addr]) extends U3
-}
diff --git a/testcases/Interpret.scala b/testcases/Interpret.scala
index 531e7ffbe..795eb4ae3 100644
--- a/testcases/Interpret.scala
+++ b/testcases/Interpret.scala
@@ -1,5 +1,3 @@
-//import scala.collection.immutable.Set
-//import leon.Annotations._
import leon.Utils._
object Interpret {
diff --git a/testcases/MutuallyRecursive.scala b/testcases/MutuallyRecursive.scala
index bd5a6bfe4..186afcffe 100644
--- a/testcases/MutuallyRecursive.scala
+++ b/testcases/MutuallyRecursive.scala
@@ -3,26 +3,26 @@ import leon.Utils._
import leon.Annotations._
object MutuallyRecursive {
- def f(n : Int) : Int = {
- if(n <= 0){
- 1
- }
- else{
- f(n-1) + g(n-1)
- }
- }
+ def f(n : Int) : Int = {
+ if(n <= 0){
+ 1
+ }
+ else{
+ f(n-1) + g(n-1)
+ }
+ }
- def g(n : Int) : Int = {
- if(n <= 0)
- 1
- else
- f(n-1)
- }ensuring(_ == fib(n + 1))
+ def g(n : Int) : Int = {
+ if(n <= 0)
+ 1
+ else
+ f(n-1)
+ }ensuring(_ == fib(n + 1))
- def fib(n : Int ) : Int = {
- if(n <= 2)
- 1
- else
- fib(n-1) + fib (n-2)
- }
+ def fib(n : Int ) : Int = {
+ if(n <= 2)
+ 1
+ else
+ fib(n-1) + fib (n-2)
+ }
}
diff --git a/testcases/Naturals.scala b/testcases/Naturals.scala
index 9b621b0a0..be821c963 100644
--- a/testcases/Naturals.scala
+++ b/testcases/Naturals.scala
@@ -9,8 +9,8 @@ object Naturals {
def plus(x : Nat, y : Nat) : Nat = {
x match {
- case Zero() => y
- case Succ(x1) => Succ(plus(x1, y))
+ case Zero() => y
+ case Succ(x1) => Succ(plus(x1, y))
}
}
@@ -48,8 +48,8 @@ object Naturals {
} holds
- //we need simplification !
- //(x.isInstanceOf[Zero] ==> (plus(x, y) == plus(y, x))) this base case does not work even if it is above!!
+ //we need simplification !
+ //(x.isInstanceOf[Zero] ==> (plus(x, y) == plus(y, x))) this base case does not work even if it is above!!
// we do not know why this inductive proof fails
@induct
def commut(x : Nat, y : Nat) : Boolean = {
diff --git a/testcases/PropositionalLogic.scala b/testcases/PropositionalLogic.scala
new file mode 100644
index 000000000..6d2daeb2e
--- /dev/null
+++ b/testcases/PropositionalLogic.scala
@@ -0,0 +1,59 @@
+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+object PropositionalLogic {
+
+ sealed abstract class Formula
+ case class And(lhs: Formula, rhs: Formula) extends Formula
+ 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
+
+ def size(f : Formula) : Int = (f match {
+ case And(lhs, rhs) => size(lhs) + size(rhs) + 1
+ case Or(lhs, rhs) => size(lhs) + size(rhs) + 1
+ case Implies(lhs, rhs) => size(lhs) + size(rhs) + 1
+ case Not(f) => size(f) + 1
+ case _ => 1
+ })
+
+ 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 _ => f
+
+ })
+
+
+ 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
+ case _ => formula
+ }) ensuring((res) => size(res) <= 2*size(formula) - 1)
+
+ def nnfSimplify(f: Formula): Formula = {
+ simplify(nnf(f))
+ } //ensuring((res) => size(res) <= 2*size(f) - 1)
+
+// 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)
+// }
+// }
+}
diff --git a/testcases/README b/testcases/README
deleted file mode 100644
index 896a958ee..000000000
--- a/testcases/README
+++ /dev/null
@@ -1,2 +0,0 @@
-Anything that's in this directory needs to be parsable by Leon, otherwise
-it will make me angry.
diff --git a/testcases/SimpInterpret.scala b/testcases/SimpInterpret.scala
index bcb7bafc8..a3ef9ee38 100644
--- a/testcases/SimpInterpret.scala
+++ b/testcases/SimpInterpret.scala
@@ -3,12 +3,12 @@
import leon.Utils._
object Interpret {
- abstract class BoolTree
+ abstract class BoolTree
case class Eq(t1 : IntTree, t2 : IntTree) extends BoolTree
case class And(t1 : BoolTree, t2 : BoolTree) extends BoolTree
case class Not(t : BoolTree) extends BoolTree
- abstract class IntTree
+ abstract class IntTree
case class Const(c:Int) extends IntTree
case class Var() extends IntTree
case class Plus(t1 : IntTree, t2 : IntTree) extends IntTree
@@ -21,7 +21,7 @@ object Interpret {
}
def beval(t:BoolTree, x0 : Int) : Boolean = {
- t match {
+ t match {
case Less(t1, t2) => ieval(t1,x0) < ieval(t2,x0)
case Eq(t1, t2) => ieval(t1,x0) == ieval(t2,x0)
case And(t1, t2) => beval(t1,x0) && beval(t2,x0)
diff --git a/testcases/AmortizedQueueStrongSpec.scala b/testcases/datastructures/AmortizedQueue.scala
similarity index 91%
rename from testcases/AmortizedQueueStrongSpec.scala
rename to testcases/datastructures/AmortizedQueue.scala
index 410be2255..6a2518499 100644
--- a/testcases/AmortizedQueueStrongSpec.scala
+++ b/testcases/datastructures/AmortizedQueue.scala
@@ -1,4 +1,3 @@
-import scala.collection.immutable.Set
import leon.Utils._
import leon.Annotations._
@@ -19,7 +18,7 @@ object AmortizedQueue {
case Nil() => Set.empty[Int]
case Cons(x, xs) => Set(x) ++ content(xs)
}
-
+
def q2l(queue : AbsQueue) : List = queue match {
case Queue(front, rear) => concat(front, reverse(rear))
}
@@ -27,8 +26,8 @@ object AmortizedQueue {
def nth(l:List, n:Int) : Int = {
require(0 <= n && n < size(l))
l match {
- case Cons(x,xs) =>
- if (n==0) x else nth(xs, n-1)
+ case Cons(x,xs) =>
+ if (n==0) x else nth(xs, n-1)
}
}
@@ -48,14 +47,14 @@ object AmortizedQueue {
require(0 <= i && i < size(l1) + size(l2))
l1 match {
case Nil() => l2
- case Cons(x,xs) => Cons(x,
- if (i == 0) concat(xs, l2)
- else concatTest(xs, l2, i-1))
+ case Cons(x,xs) => Cons(x,
+ if (i == 0) concat(xs, l2)
+ else concatTest(xs, l2, i-1))
}
- }) ensuring (res => size(res) == size(l1) + size(l2) &&
- content(res) == content(l1) ++ content(l2) &&
- nth(res,i) == (if (i < size(l1)) nth(l1,i) else nth(l2,i-size(l1))) &&
- res == concat(l1,l2))
+ }) ensuring (res => size(res) == size(l1) + size(l2) &&
+ content(res) == content(l1) ++ content(l2) &&
+ nth(res,i) == (if (i < size(l1)) nth(l1,i) else nth(l2,i-size(l1))) &&
+ res == concat(l1,l2))
def nthConcat(l1:List, l2:List, i:Int) : Boolean = {
require(0 <= i && i < size(l1) + size(l2))
@@ -70,7 +69,7 @@ object AmortizedQueue {
case (Nil(),_) => false
case (_,Nil()) => false
case (Cons(x,xs),Cons(y,ys)) => {
- x==y && (if (k==0) true else sameUpto(xs,ys,k-1))
+ x==y && (if (k==0) true else sameUpto(xs,ys,k-1))
}
}
} ensuring(res => !(size(l1)==k && size(l2)==k && res) || l1==l2)
@@ -141,7 +140,7 @@ object AmortizedQueue {
queue match {
case Queue(Cons(f, fs), rear) => amortizedQueue(fs, rear)
}
- }) ensuring(res => isAmortized(res) && (q2l(queue) match {
+ }) ensuring(res => isAmortized(res) && (q2l(queue) match {
case Nil() => false
case Cons(_,xs) => q2l(res)==xs
}))
@@ -151,7 +150,7 @@ object AmortizedQueue {
queue match {
case Queue(Cons(f, _), _) => f
}
- }) ensuring(res => q2l(queue) match {
+ }) ensuring(res => q2l(queue) match {
case Nil() => false
case Cons(x,_) => x==res
})
diff --git a/testcases/BSTSimpler.scala b/testcases/datastructures/BinarySearchTree.scala
similarity index 97%
rename from testcases/BSTSimpler.scala
rename to testcases/datastructures/BinarySearchTree.scala
index f3b2b6893..471813c13 100644
--- a/testcases/BSTSimpler.scala
+++ b/testcases/datastructures/BinarySearchTree.scala
@@ -1,6 +1,3 @@
-import scala.collection.immutable.Set
-//import scala.collection.immutable.Multiset
-
object BSTSimpler {
sealed abstract class Tree
case class Node(left: Tree, value: Int, right: Tree) extends Tree
diff --git a/testcases/datastructures/BinaryTrie.scala b/testcases/datastructures/BinaryTrie.scala
new file mode 100644
index 000000000..83c7bb490
--- /dev/null
+++ b/testcases/datastructures/BinaryTrie.scala
@@ -0,0 +1,68 @@
+/* Copyright 2009-2013 EPFL, Lausanne
+ *
+ * Author: Ravi
+ * Date: 20.11.2013
+ **/
+
+import leon.Utils._
+
+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)
+ }) ensuring(_ >= 0)
+
+ 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
+ }
+ }
+ } ensuring(_ >= 0)
+
+ 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
+ }
+ }
+ }
+ } ensuring(res => height(res) + height(t) >= listSize(inp))
+
+ def create(inp: IList) : Tree = {
+ insert(inp, Leaf())
+ }ensuring(res => height(res) >= listSize(inp))
+}
diff --git a/testcases/datastructures/HeapSort.scala b/testcases/datastructures/HeapSort.scala
new file mode 100644
index 000000000..78a72ed2f
--- /dev/null
+++ b/testcases/datastructures/HeapSort.scala
@@ -0,0 +1,114 @@
+/* Copyright 2009-2013 EPFL, Lausanne
+ *
+ * Author: Ravi
+ * Date: 20.11.2013
+ **/
+
+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/InsertionSort.scala b/testcases/datastructures/InsertionSort.scala
similarity index 74%
rename from testcases/InsertionSort.scala
rename to testcases/datastructures/InsertionSort.scala
index 6b162246f..e3963ade5 100644
--- a/testcases/InsertionSort.scala
+++ b/testcases/datastructures/InsertionSort.scala
@@ -51,37 +51,14 @@ object InsertionSort {
case Nil() => true
case Cons(x, Nil()) => true
case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
- }
-
-// def sortedInsInduct0(e: Int, l: List) : List = {
-// require(l == Nil())
-// 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 => isSorted(res))
-//
-// def sortedInsInduct1(e: Int, l: List) : List = {
-// require(
-// isSorted(l) &&
-// (l match {
-// case Nil() => false
-// case Cons(x,xs) => isSorted(sortedIns(e,xs))
-// })
-// )
-//
-// 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 => isSorted(res))
+ }
def sortedIns(e: Int, l: List): List = {
require(isSorted(l) && size(l) <= 5)
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 => contents(res) == contents(l) ++ Set(e) && isSorted(res))
def sort(l: List): List = (l match {
diff --git a/testcases/datastructures/LeftistHeap.scala b/testcases/datastructures/LeftistHeap.scala
new file mode 100644
index 000000000..df3bf23c9
--- /dev/null
+++ b/testcases/datastructures/LeftistHeap.scala
@@ -0,0 +1,67 @@
+/* Copyright 2009-2013 EPFL, Lausanne
+ *
+ * Author: Ravi
+ * Date: 20.11.2013
+ **/
+
+import leon.Utils._
+
+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
+ }} ensuring(_ >= 0)
+
+ 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/ListWithSize.scala b/testcases/datastructures/ListWithSize.scala
similarity index 98%
rename from testcases/ListWithSize.scala
rename to testcases/datastructures/ListWithSize.scala
index 868cb4556..2df0c0cb7 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/datastructures/ListWithSize.scala
@@ -59,7 +59,7 @@ object ListWithSize {
def sizeAndContent(l: List) : Boolean = {
size(l) == 0 || content(l) != Set.empty[Int]
} holds
-
+
def drunk(l : List) : List = (l match {
case Nil() => Nil()
case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
@@ -110,7 +110,7 @@ object ListWithSize {
// proved with unrolling=4
@induct
- def concat(l1: List, l2: List) : List =
+ def concat(l1: List, l2: List) : List =
concat0(l1, l2, Nil()) ensuring(content(_) == content(l1) ++ content(l2))
@induct
diff --git a/testcases/MergeSort.scala b/testcases/datastructures/MergeSort.scala
similarity index 68%
rename from testcases/MergeSort.scala
rename to testcases/datastructures/MergeSort.scala
index da575c8bb..408830ced 100644
--- a/testcases/MergeSort.scala
+++ b/testcases/datastructures/MergeSort.scala
@@ -18,48 +18,47 @@ object MergeSort {
case Nil() => true
case Cons(y, ys) => x <= y && is_sorted(Cons(y, ys))
}
- }
+ }
def length(list:List): Int = list match {
case Nil() => 0
case Cons(x,xs) => 1 + length(xs)
}
- def splithelper(aList:List,bList:List,n:Int): Pair =
+ def splithelper(aList:List,bList:List,n:Int): Pair =
if (n <= 0) Pair(aList,bList)
else
- bList match {
- case Nil() => Pair(aList,bList)
- case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
- }
+ bList match {
+ case Nil() => Pair(aList,bList)
+ case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+ }
def split(list:List,n:Int): Pair = splithelper(Nil(),list,n)
- def merge(aList:List, bList:List):List = (bList match {
+ def merge(aList:List, bList:List):List = (bList match {
case Nil() => aList
case Cons(x,xs) =>
- aList match {
- case Nil() => bList
- case Cons(y,ys) =>
- if (y < x)
- Cons(y,merge(ys, bList))
- else
- Cons(x,merge(aList, xs))
- }
+ 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 => contents(res) == contents(aList) ++ contents(bList))
def mergeSort(list:List):List = (list match {
case Nil() => list
case Cons(x,Nil()) => list
case _ =>
- val p = split(list,length(list)/2)
- merge(mergeSort(p.fst), mergeSort(p.snd))
+ val p = split(list,length(list)/2)
+ merge(mergeSort(p.fst), mergeSort(p.snd))
}) ensuring(res => contents(res) == contents(list) && is_sorted(res))
-
+
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
-
println(ls)
println(mergeSort(ls))
}
diff --git a/testcases/QuickSort.scala b/testcases/datastructures/QuickSort.scala
similarity index 99%
rename from testcases/QuickSort.scala
rename to testcases/datastructures/QuickSort.scala
index 83dd2c364..a5f03f214 100644
--- a/testcases/QuickSort.scala
+++ b/testcases/datastructures/QuickSort.scala
@@ -27,7 +27,7 @@ object QuickSort {
case Nil() => bList
case _ => rev_append(reverse(aList),bList)
}
-
+
def greater(n:Int,list:List) : List = list match {
case Nil() => Nil()
case Cons(x,xs) => if (n < x) Cons(x,greater(n,xs)) else greater(n,xs)
diff --git a/testcases/RedBlackTree.scala b/testcases/datastructures/RedBlackTree.scala
similarity index 97%
rename from testcases/RedBlackTree.scala
rename to testcases/datastructures/RedBlackTree.scala
index 0952a11fe..98a70c191 100644
--- a/testcases/RedBlackTree.scala
+++ b/testcases/datastructures/RedBlackTree.scala
@@ -1,11 +1,11 @@
import scala.collection.immutable.Set
//import scala.collection.immutable.Multiset
-object RedBlackTree {
+object RedBlackTree {
sealed abstract class Color
case class Red() extends Color
case class Black() extends Color
-
+
sealed abstract class Tree
case class Empty() extends Tree
case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
@@ -34,15 +34,15 @@ object RedBlackTree {
def add(x: Int, t: Tree): Tree = {
makeBlack(ins(x, t))
} ensuring (content(_) == content(t) ++ Set(x))
-
+
def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = (Node(c,a,x,b) match {
- case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
case Node(c,a,xV,b) => Node(c,a,xV,b)
}) ensuring (res => content(res) == content(Node(c,a,x,b)))
diff --git a/testcases/SortedList.scala b/testcases/datastructures/SortedList.scala
similarity index 99%
rename from testcases/SortedList.scala
rename to testcases/datastructures/SortedList.scala
index 882dbe2a7..6e530b688 100644
--- a/testcases/SortedList.scala
+++ b/testcases/datastructures/SortedList.scala
@@ -112,12 +112,12 @@ object SortedList {
}) ensuring(res => !res || !contains(l, x))
def discard(value : Boolean) = true
-
+
@induct
def ltaLemma(x : Int, y : Int, l : List) : Boolean = {
require(lessThanAll(y, l) && x < y)
lessThanAll(x, Cons(y, l))
- } holds
+ } holds
def isSorted(l: List): Boolean = l match {
case Nil() => true
diff --git a/testcases/TreeListSetNoDup.scala b/testcases/datastructures/TreeListSetNoDup.scala
similarity index 90%
rename from testcases/TreeListSetNoDup.scala
rename to testcases/datastructures/TreeListSetNoDup.scala
index b45794109..b6649c5ca 100644
--- a/testcases/TreeListSetNoDup.scala
+++ b/testcases/datastructures/TreeListSetNoDup.scala
@@ -24,7 +24,7 @@ object BinaryTree {
def noDup(l:List): Boolean = noDupWith(l,Set.empty[Int])
// removing duplicates from l1 gives l2
- def removeDupGives(l1:List,l2:List) : Boolean =
+ def removeDupGives(l1:List,l2:List) : Boolean =
l2s(l1)==l2s(l2) && noDup(l2)
def removeDupAnd(l:List,s0:Set[Int]) : List = (l match {
@@ -44,8 +44,8 @@ object BinaryTree {
l match {
case Nil() => l0
case Cons(h,l1) => {
- if (s0.contains(h)) revRemoveDupAnd(l1,s0,l0)
- else revRemoveDupAnd(l1,Set(h)++s0,Cons(h,l0))
+ if (s0.contains(h)) revRemoveDupAnd(l1,s0,l0)
+ else revRemoveDupAnd(l1,Set(h)++s0,Cons(h,l0))
}
}
}) ensuring (res => noDupWith(res,s0) && l2s(l) ++l2s(l0) ++ s0 == l2s(res) ++ s0)
@@ -82,9 +82,9 @@ object BinaryTree {
t match {
case Leaf() => (l0,s0)
case Node(l, v, r) => {
- val (rl,rs) = seqNoDup(r,l0,s0)
- val (l1,s1) = if (rs.contains(v)) (rl,rs) else (Cons(v,rl),Set(v)++rs)
- seqNoDup(l,l1,s1)
+ val (rl,rs) = seqNoDup(r,l0,s0)
+ val (l1,s1) = if (rs.contains(v)) (rl,rs) else (Cons(v,rl),Set(v)++rs)
+ seqNoDup(l,l1,s1)
}
}
}) ensuring (res => {
diff --git a/testcases/BinarySearchTree.scala b/testcases/graveyard/BinarySearchTree.scala
similarity index 95%
rename from testcases/BinarySearchTree.scala
rename to testcases/graveyard/BinarySearchTree.scala
index 5ef9b95d5..452e21a26 100644
--- a/testcases/BinarySearchTree.scala
+++ b/testcases/graveyard/BinarySearchTree.scala
@@ -55,10 +55,10 @@ object BinarySearchTree {
}
}
}) ensuring (res => res match { case SortedTriple(min,max,sort) => min match {
- case None() => res == SortedTriple(None(),None(),sort)
- case Some(minv) => max match {
- case None() => false
- case Some(maxv) => sort && minv <= maxv}}})
+ case None() => res == SortedTriple(None(),None(),sort)
+ case Some(minv) => max match {
+ case None() => false
+ case Some(maxv) => sort && minv <= maxv}}})
def treeMin(tree: Node): Int = {
require(isSorted(tree).sorted)
diff --git a/testcases/Choose.scala b/testcases/graveyard/Choose.scala
similarity index 100%
rename from testcases/Choose.scala
rename to testcases/graveyard/Choose.scala
diff --git a/testcases/ConnectedTest.scala b/testcases/graveyard/ConnectedTest.scala
similarity index 100%
rename from testcases/ConnectedTest.scala
rename to testcases/graveyard/ConnectedTest.scala
diff --git a/testcases/Expr2Comp.scala b/testcases/graveyard/Expr2Comp.scala
similarity index 100%
rename from testcases/Expr2Comp.scala
rename to testcases/graveyard/Expr2Comp.scala
diff --git a/testcases/ExprComp.scala b/testcases/graveyard/ExprComp.scala
similarity index 100%
rename from testcases/ExprComp.scala
rename to testcases/graveyard/ExprComp.scala
diff --git a/testcases/PaperDemoExample.scala b/testcases/graveyard/PaperDemoExample.scala
similarity index 100%
rename from testcases/PaperDemoExample.scala
rename to testcases/graveyard/PaperDemoExample.scala
diff --git a/testcases/Sat.scala b/testcases/graveyard/Sat.scala
similarity index 100%
rename from testcases/Sat.scala
rename to testcases/graveyard/Sat.scala
diff --git a/testcases/SetOperations.scala b/testcases/graveyard/SetOperations.scala
similarity index 100%
rename from testcases/SetOperations.scala
rename to testcases/graveyard/SetOperations.scala
diff --git a/testcases/SortedTree.scala b/testcases/graveyard/SortedTree.scala
similarity index 100%
rename from testcases/SortedTree.scala
rename to testcases/graveyard/SortedTree.scala
diff --git a/testcases/Test.scala b/testcases/graveyard/Test.scala
similarity index 100%
rename from testcases/Test.scala
rename to testcases/graveyard/Test.scala
diff --git a/testcases/UnificationTest.scala b/testcases/graveyard/UnificationTest.scala
similarity index 88%
rename from testcases/UnificationTest.scala
rename to testcases/graveyard/UnificationTest.scala
index 2202a573d..f44714923 100644
--- a/testcases/UnificationTest.scala
+++ b/testcases/graveyard/UnificationTest.scala
@@ -5,35 +5,35 @@ object UnificationTest {
sealed abstract class Tree
case class Leaf() extends Tree
- case class Node(left: Tree, value: Int, right: Tree) extends Tree
+ case class Node(left: Tree, value: Int, right: Tree) extends Tree
// Proved by unifier
def mkTree(a: Int, b: Int, c: Int) = {
Node(Node(Leaf(), a, Leaf()), b, Node(Leaf(), c, Leaf()))
//Node(Leaf(), b, Node(Leaf(), c, Leaf()))
- } ensuring ( res => {
+ } ensuring ( res => {
res.left != Leaf() &&
- res.value == b &&
- res.right == Node(Leaf(), c, Leaf())
+ res.value == b &&
+ res.right == Node(Leaf(), c, Leaf())
})
-
-
-
+
+
+
sealed abstract class Term
case class F(t1: Term, t2: Term, t3: Term, t4: Term) extends Term
case class G(s1: Term, s2: Term) extends Term
case class H(r1: Term, r2: Term) extends Term
case class A extends Term
case class B extends Term
-
+
def examplePage268(x1: Term, x2: Term, x3: Term, x4: Term, x5: Term) = {
F(G(H(A(), x5), x2), x1, H(A(), x4), x4)
} //ensuring ( _ == F(x1, G(x2, x3), x2, B()) )
-
-
-
+
+
+
case class Tuple3(_1: Term, _2: Term, _3: Term)
-
+
def examplePage269(x1: Term, x2: Term, x3: Term, x4: Term) = {
Tuple3(H(x1, x1), H(x2, x2), H(x3, x3))
} /*ensuring ( res => {
@@ -41,8 +41,8 @@ object UnificationTest {
x3 == res._2 &&
x4 == res._3
})*/
-
-
+
+
// Cannot be solved yet, due to the presence of an if expression
def insert(tree: Tree, value: Int) : Node = (tree match {
case Leaf() => Node(Leaf(), value, Leaf())
@@ -54,5 +54,5 @@ object UnificationTest {
n
}
}) ensuring(_ != Leaf())
-
-}
\ No newline at end of file
+
+}
diff --git a/testcases/UseContradictoryLemma.scala b/testcases/graveyard/UseContradictoryLemma.scala
similarity index 100%
rename from testcases/UseContradictoryLemma.scala
rename to testcases/graveyard/UseContradictoryLemma.scala
diff --git a/testcases/VerySimple.scala b/testcases/graveyard/VerySimple.scala
similarity index 100%
rename from testcases/VerySimple.scala
rename to testcases/graveyard/VerySimple.scala
diff --git a/testcases/Viktor.scala b/testcases/graveyard/Viktor.scala
similarity index 100%
rename from testcases/Viktor.scala
rename to testcases/graveyard/Viktor.scala
diff --git a/testcases/malkis/Hardest.scala b/testcases/graveyard/malkis/Hardest.scala
similarity index 100%
rename from testcases/malkis/Hardest.scala
rename to testcases/graveyard/malkis/Hardest.scala
diff --git a/testcases/MultiBug.scala b/testcases/graveyard/multisets/MultiBug.scala
similarity index 100%
rename from testcases/MultiBug.scala
rename to testcases/graveyard/multisets/MultiBug.scala
diff --git a/testcases/MultiExample.scala b/testcases/graveyard/multisets/MultiExample.scala
similarity index 100%
rename from testcases/MultiExample.scala
rename to testcases/graveyard/multisets/MultiExample.scala
diff --git a/testcases/MultisetOperations.scala b/testcases/graveyard/multisets/MultisetOperations.scala
similarity index 100%
rename from testcases/MultisetOperations.scala
rename to testcases/graveyard/multisets/MultisetOperations.scala
diff --git a/testcases/runtime/CachedList.scala b/testcases/runtime/CachedList.scala
new file mode 100644
index 000000000..ac34d980a
--- /dev/null
+++ b/testcases/runtime/CachedList.scala
@@ -0,0 +1,42 @@
+import leon.Utils._
+
+object SortedList {
+ abstract class List
+ case class Cons(h: Int, t: List) extends List
+ case object Nil extends List
+
+ def size(l: List): Int = l match {
+ case Cons(h, t) => 1 + size(t)
+ case Nil => 0
+ }
+
+ def content(l: List): Set[Int] = l match {
+ case Cons(h, t) => Set(h) ++ content(t)
+ case Nil => Set()
+ }
+
+ case class CachedList(cache: Int, data: List)
+
+ def inv(cl: CachedList) = {
+ (content(cl.data) contains cl.cache) || (cl.data == Nil)
+ }
+
+ def withCache(l: List): CachedList = choose {
+ (x: CachedList) => inv(x) && content(x.data) == content(l)
+ }
+
+ def insert(l: CachedList, i: Int): CachedList = {
+ require(inv(l))
+ choose{ (x: CachedList) => content(x.data) == content(l.data) ++ Set(i) && inv(x) }
+ }
+
+ def delete(l: CachedList, i: Int): CachedList = {
+ require(inv(l))
+ choose{ (x: CachedList) => content(x.data) == content(l.data) -- Set(i) && inv(x) }
+ }
+
+ def contains(l: CachedList, i: Int): Boolean = {
+ require(inv(l))
+ choose{ (x: Boolean) => x == (content(l.data) contains i) }
+ }
+}
diff --git a/testcases/runtime/SquareRoot.scala b/testcases/runtime/SquareRoot.scala
new file mode 100644
index 000000000..dd4eee922
--- /dev/null
+++ b/testcases/runtime/SquareRoot.scala
@@ -0,0 +1,28 @@
+import leon.Utils._
+
+object SquareRoot {
+
+ def isqrt(x : Int) : Int = {
+ choose { (y : Int) =>
+ y * y <= x && (y + 1) * (y + 1) >= x
+ }
+ }
+
+ def isqrt2(x: Int): Int = {
+ if ((x == 0)) {
+ 0
+ } else {
+ if ((x < 0)) {
+ leon.Utils.error[(Int)]("(((y * y) ≤ x) ∧ (((y + 1) * (y + 1)) ≥ x)) is UNSAT!")
+ } else {
+ (choose { (y: Int) =>
+ (((y * y) <= x) && (((y + 1) * (y + 1)) >= x))
+ })
+ }
+ }
+ }
+
+ def main(a: Array[String]) {
+ isqrt2(42)
+ }
+}
diff --git a/testcases/AbsArray.scala b/testcases/xlang/AbsArray.scala
similarity index 100%
rename from testcases/AbsArray.scala
rename to testcases/xlang/AbsArray.scala
diff --git a/testcases/AbsFun.scala b/testcases/xlang/AbsFun.scala
similarity index 100%
rename from testcases/AbsFun.scala
rename to testcases/xlang/AbsFun.scala
diff --git a/testcases/Add.scala b/testcases/xlang/Add.scala
similarity index 100%
rename from testcases/Add.scala
rename to testcases/xlang/Add.scala
diff --git a/testcases/BinarySearchFun.scala b/testcases/xlang/ArrayBinarySearch.scala
similarity index 100%
rename from testcases/BinarySearchFun.scala
rename to testcases/xlang/ArrayBinarySearch.scala
diff --git a/testcases/BinarySearch.scala b/testcases/xlang/ArrayBinarySearchProcedural.scala
similarity index 100%
rename from testcases/BinarySearch.scala
rename to testcases/xlang/ArrayBinarySearchProcedural.scala
diff --git a/testcases/BinaryTreeImp.scala b/testcases/xlang/BinaryTreeImp.scala
similarity index 98%
rename from testcases/BinaryTreeImp.scala
rename to testcases/xlang/BinaryTreeImp.scala
index 3005d1991..6db0d5ec0 100644
--- a/testcases/BinaryTreeImp.scala
+++ b/testcases/xlang/BinaryTreeImp.scala
@@ -2,8 +2,8 @@ import scala.collection.immutable.Set
import leon.Annotations._
import leon.Utils._
-object BinaryTree {
-
+object BinaryTree {
+
sealed abstract class Tree
case class Leaf() extends Tree
case class Node(left: Tree, value: Int, right: Tree) extends Tree
@@ -81,7 +81,7 @@ object BinaryTree {
else search(left, x)
}
} ensuring(res => res == content(t).contains(x))
-
+
def searchImp(t: Tree, x: Int): Boolean = {
require(binaryTreeProp(t))
var res = false
@@ -90,7 +90,7 @@ object BinaryTree {
val Node(left, value, right) = t2
if(value == x)
res = true
- else if(value < x)
+ else if(value < x)
t2 = right
else
t2 = left
diff --git a/testcases/BubbleFun.scala b/testcases/xlang/BubbleFun.scala
similarity index 100%
rename from testcases/BubbleFun.scala
rename to testcases/xlang/BubbleFun.scala
diff --git a/testcases/BubbleSort.scala b/testcases/xlang/BubbleSort.scala
similarity index 100%
rename from testcases/BubbleSort.scala
rename to testcases/xlang/BubbleSort.scala
diff --git a/testcases/BubbleWeakInvariant.scala b/testcases/xlang/BubbleWeakInvariant.scala
similarity index 100%
rename from testcases/BubbleWeakInvariant.scala
rename to testcases/xlang/BubbleWeakInvariant.scala
diff --git a/testcases/InsertionSortImp.scala b/testcases/xlang/InsertionSortImp.scala
similarity index 100%
rename from testcases/InsertionSortImp.scala
rename to testcases/xlang/InsertionSortImp.scala
diff --git a/testcases/IntOperations.scala b/testcases/xlang/IntOperations.scala
similarity index 100%
rename from testcases/IntOperations.scala
rename to testcases/xlang/IntOperations.scala
diff --git a/testcases/LinearSearch.scala b/testcases/xlang/LinearSearch.scala
similarity index 100%
rename from testcases/LinearSearch.scala
rename to testcases/xlang/LinearSearch.scala
diff --git a/testcases/ListImp.scala b/testcases/xlang/ListImp.scala
similarity index 100%
rename from testcases/ListImp.scala
rename to testcases/xlang/ListImp.scala
diff --git a/testcases/MaxSum.scala b/testcases/xlang/MaxSum.scala
similarity index 100%
rename from testcases/MaxSum.scala
rename to testcases/xlang/MaxSum.scala
diff --git a/testcases/Mult.scala b/testcases/xlang/Mult.scala
similarity index 100%
rename from testcases/Mult.scala
rename to testcases/xlang/Mult.scala
diff --git a/testcases/NonDeterministicList.scala b/testcases/xlang/NonDeterministicList.scala
similarity index 100%
rename from testcases/NonDeterministicList.scala
rename to testcases/xlang/NonDeterministicList.scala
diff --git a/testcases/QuickSortImp.scala b/testcases/xlang/QuickSortImp.scala
similarity index 100%
rename from testcases/QuickSortImp.scala
rename to testcases/xlang/QuickSortImp.scala
diff --git a/testcases/buggyEpsilon.scala b/testcases/xlang/buggyEpsilon.scala
similarity index 100%
rename from testcases/buggyEpsilon.scala
rename to testcases/xlang/buggyEpsilon.scala
diff --git a/testcases/master-thesis-regis/Arithmetic.scala b/testcases/xlang/master-thesis-regis/Arithmetic.scala
similarity index 100%
rename from testcases/master-thesis-regis/Arithmetic.scala
rename to testcases/xlang/master-thesis-regis/Arithmetic.scala
diff --git a/testcases/master-thesis-regis/ArrayBubbleSort.scala b/testcases/xlang/master-thesis-regis/ArrayBubbleSort.scala
similarity index 100%
rename from testcases/master-thesis-regis/ArrayBubbleSort.scala
rename to testcases/xlang/master-thesis-regis/ArrayBubbleSort.scala
diff --git a/testcases/master-thesis-regis/ArrayOperations.scala b/testcases/xlang/master-thesis-regis/ArrayOperations.scala
similarity index 100%
rename from testcases/master-thesis-regis/ArrayOperations.scala
rename to testcases/xlang/master-thesis-regis/ArrayOperations.scala
diff --git a/testcases/master-thesis-regis/Constraints.scala b/testcases/xlang/master-thesis-regis/Constraints.scala
similarity index 100%
rename from testcases/master-thesis-regis/Constraints.scala
rename to testcases/xlang/master-thesis-regis/Constraints.scala
diff --git a/testcases/master-thesis-regis/ListOperations.scala b/testcases/xlang/master-thesis-regis/ListOperations.scala
similarity index 100%
rename from testcases/master-thesis-regis/ListOperations.scala
rename to testcases/xlang/master-thesis-regis/ListOperations.scala
diff --git a/testcases/xplusone.scala b/testcases/xlang/xplusone.scala
similarity index 100%
rename from testcases/xplusone.scala
rename to testcases/xlang/xplusone.scala
--
GitLab