diff --git a/demo/Arith.scala b/demo/Arith.scala
deleted file mode 100644
index d4b02f51b5e532a15b9fb3571534316e0cc962ce..0000000000000000000000000000000000000000
--- a/demo/Arith.scala
+++ /dev/null
@@ -1,41 +0,0 @@
-import leon.Utils._
-
-object Arith {
-
- def mult(x : Int, y : Int): Int = ({
- var r = 0
- if(y < 0) {
- var n = y
- (while(n != 0) {
- r = r - x
- n = n + 1
- }) invariant(r == x * (y - n) && 0 <= -n)
- } else {
- var n = y
- (while(n != 0) {
- r = r + x
- n = n - 1
- }) invariant(r == x * (y - n) && 0 <= n)
- }
- r
- }) ensuring(_ == x*y)
-
- def add(x : Int, y : Int): Int = ({
- var r = x
- if(y < 0) {
- var n = y
- (while(n != 0) {
- r = r - 1
- n = n + 1
- }) invariant(r == x + y - n && 0 <= -n)
- } else {
- var n = y
- (while(n != 0) {
- r = r + 1
- n = n - 1
- }) invariant(r == x + y - n && 0 <= n)
- }
- r
- }) ensuring(_ == x+y)
-
-}
diff --git a/demo/BubbleSortBug.scala b/demo/BubbleSortBug.scala
deleted file mode 100644
index a25554f0305d57c53774cdc0b4d514393217b4f2..0000000000000000000000000000000000000000
--- a/demo/BubbleSortBug.scala
+++ /dev/null
@@ -1,39 +0,0 @@
-import leon.Utils._
-
-/* The calculus of Computation textbook */
-
-object BubbleSortBug {
-
- def sort(a: Array[Int]): Array[Int] = ({
- require(a.length >= 1)
- var i = a.length - 1
- var j = 0
- val sa = a.clone
- (while(i > 0) {
- j = 0
- (while(j < i) {
- if(sa(j) < sa(j+1)) {
- val tmp = sa(j)
- sa(j) = sa(j+1)
- sa(j+1) = tmp
- }
- j = j + 1
- }) invariant(j >= 0 && j <= i && i < sa.length)
- i = i - 1
- }) invariant(i >= 0 && i < sa.length)
- sa
- }) ensuring(res => sorted(res, 0, a.length-1))
-
- def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
- require(a.length >= 0 && l >= 0 && u < a.length && l <= u)
- var k = l
- var isSorted = true
- (while(k < u) {
- if(a(k) > a(k+1))
- isSorted = false
- k = k + 1
- }) invariant(k <= u && k >= l)
- isSorted
- }
-
-}
diff --git a/demo/List.scala b/demo/List.scala
deleted file mode 100644
index 302e86774c7d1e68e08d48ce957c87ec483b3d56..0000000000000000000000000000000000000000
--- a/demo/List.scala
+++ /dev/null
@@ -1,20 +0,0 @@
-import leon.Utils._
-
-object List {
-
- abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
- def size(l: List): Int = waypoint(1, (l match {
- case Cons(_, tail) => sizeTail(tail, 1)
- case Nil() => 0
- })) ensuring(_ >= 0)
-
-
- def sizeTail(l2: List, acc: Int): Int = l2 match {
- case Cons(_, tail) => sizeTail(tail, acc+1)
- case Nil() => acc
- }
-
-}
diff --git a/demo/ListOperations.scala b/demo/ListOperations.scala
deleted file mode 100644
index a4fc4f8dc44a90f59a772b52b1a05053316e94d2..0000000000000000000000000000000000000000
--- a/demo/ListOperations.scala
+++ /dev/null
@@ -1,107 +0,0 @@
-import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
-
-object ListOperations {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class IntPairList
- case class IPCons(head: IntPair, tail: IntPairList) extends IntPairList
- case class IPNil() extends IntPairList
-
- sealed abstract class IntPair
- case class IP(fst: Int, snd: Int) extends IntPair
-
- def size(l: List) : Int = (l match {
- case Nil() => 0
- case Cons(_, t) => 1 + size(t)
- }) ensuring(res => res >= 0)
-
- def iplSize(l: IntPairList) : Int = (l match {
- case IPNil() => 0
- case IPCons(_, xs) => 1 + iplSize(xs)
- }) ensuring(_ >= 0)
-
- def zip(l1: List, l2: List) : IntPairList = {
- // try to comment this and see how pattern-matching becomes
- // non-exhaustive and post-condition fails
- require(size(l1) == size(l2))
-
- l1 match {
- case Nil() => IPNil()
- case Cons(x, xs) => l2 match {
- case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys))
- }
- }
- } ensuring(iplSize(_) == size(l1))
-
- def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0)
- def sizeTailRecAcc(l: List, acc: Int) : Int = {
- require(acc >= 0)
- l match {
- case Nil() => acc
- case Cons(_, xs) => sizeTailRecAcc(xs, acc+1)
- }
- } ensuring(res => res == size(l) + acc)
-
- def sizesAreEquiv(l: List) : Boolean = {
- size(l) == sizeTailRec(l)
- } holds
-
- def content(l: List) : Set[Int] = l match {
- case Nil() => Set.empty[Int]
- case Cons(x, xs) => Set(x) ++ content(xs)
- }
-
- 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)))
- }) ensuring (size(_) == 2 * size(l))
-
- def reverse(l: List) : List = reverse0(l, Nil()) ensuring(content(_) == content(l))
- def reverse0(l1: List, l2: List) : List = (l1 match {
- case Nil() => l2
- case Cons(x, xs) => reverse0(xs, Cons(x, l2))
- }) ensuring(content(_) == content(l1) ++ content(l2))
-
- def append(l1 : List, l2 : List) : List = (l1 match {
- case Nil() => l2
- case Cons(x,xs) => Cons(x, append(xs, l2))
- }) ensuring(content(_) == content(l1) ++ content(l2))
-
- @induct
- def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
-
- @induct
- def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
- (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
-
- def revAuxBroken(l1 : List, e : Int, l2 : List) : Boolean = {
- (append(reverse(l1), Cons(e,l2)) == reverse0(l1, l2))
- } holds
-
- @induct
- def sizeAppend(l1 : List, l2 : List) : Boolean =
- (size(append(l1, l2)) == size(l1) + size(l2)) holds
-
- @induct
- def concat(l1: List, l2: List) : List =
- concat0(l1, l2, Nil()) ensuring(content(_) == content(l1) ++ content(l2))
-
- @induct
- def concat0(l1: List, l2: List, l3: List) : List = (l1 match {
- case Nil() => l2 match {
- case Nil() => reverse(l3)
- case Cons(y, ys) => {
- concat0(Nil(), ys, Cons(y, l3))
- }
- }
- case Cons(x, xs) => concat0(xs, l2, Cons(x, l3))
- }) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3))
-}
diff --git a/demo/MaxSum.scala b/demo/MaxSum.scala
deleted file mode 100644
index ba724d255c23b782e1b4de716ccc8d50043e2059..0000000000000000000000000000000000000000
--- a/demo/MaxSum.scala
+++ /dev/null
@@ -1,38 +0,0 @@
-import leon.Utils._
-
-/* VSTTE 2010 challenge 1 */
-
-object MaxSum {
-
- def maxSum(a: Array[Int]): (Int, Int) = ({
- require(a.length >= 0 && isPositive(a))
- var sum = 0
- var max = 0
- var i = 0
- (while(i < a.length) {
- if(max < a(i))
- max = a(i)
- sum = sum + a(i)
- i = i + 1
- }) invariant (sum <= i * max && i >= 0 && i <= a.length)
- (sum, max)
- }) ensuring(res => res._1 <= a.length * res._2)
-
-
- def isPositive(a: Array[Int]): Boolean = {
- require(a.length >= 0)
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= a.length)
- true
- else {
- if(a(i) < 0)
- false
- else
- rec(i+1)
- }
- }
- rec(0)
- }
-
-}
diff --git a/demo/RedBlackTree.scala b/demo/RedBlackTree.scala
deleted file mode 100644
index bc2de6ba96ee699736d4558932b752eea9ebba9f..0000000000000000000000000000000000000000
--- a/demo/RedBlackTree.scala
+++ /dev/null
@@ -1,117 +0,0 @@
-import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
-
-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
-
- sealed abstract class OptionInt
- case class Some(v : Int) extends OptionInt
- case class None() extends OptionInt
-
- def content(t: Tree) : Set[Int] = t match {
- case Empty() => Set.empty
- case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
- }
-
- def size(t: Tree) : Int = (t match {
- case Empty() => 0
- case Node(_, l, v, r) => size(l) + 1 + size(r)
- }) ensuring(_ >= 0)
-
- /* We consider leaves to be black by definition */
- def isBlack(t: Tree) : Boolean = t match {
- case Empty() => true
- case Node(Black(),_,_,_) => true
- case _ => false
- }
-
- def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
- case Empty() => true
- case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
- case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
- }
-
- def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
- case Empty() => true
- case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
- }
-
- def blackBalanced(t : Tree) : Boolean = t match {
- case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
- case Empty() => true
- }
-
- def blackHeight(t : Tree) : Int = t match {
- case Empty() => 1
- case Node(Black(), l, _, _) => blackHeight(l) + 1
- case Node(Red(), l, _, _) => blackHeight(l)
- }
-
- // <<insert element x into the tree t>>
- def ins(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t))
- t match {
- case Empty() => Node(Red(),Empty(),x,Empty())
- case Node(c,a,y,b) =>
- if (x < y) balance(c, ins(x, a), y, b)
- else if (x == y) Node(c,a,y,b)
- else balance(c,a,y,ins(x, b))
- }
- } ensuring (res => content(res) == content(t) ++ Set(x)
- && size(t) <= size(res) && size(res) <= size(t) + 1
- && redDescHaveBlackChildren(res)
- && blackBalanced(res))
-
- def makeBlack(n: Tree): Tree = {
- require(redDescHaveBlackChildren(n) && blackBalanced(n))
- n match {
- case Node(Red(),l,v,r) => Node(Black(),l,v,r)
- case _ => n
- }
- } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res))
-
- def add(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t))
- makeBlack(ins(x, t))
- } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res))
-
- def buggyAdd(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t))
- ins(x, t)
- } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
-
- 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) =>
- 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) =>
- 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)) =>
- 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))) =>
- 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)))// && redDescHaveBlackChildren(res))
-
- def buggyBalance(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) =>
- 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) =>
- 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)) =>
- 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))) =>
- 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)))// && redDescHaveBlackChildren(res))
-}
diff --git a/project/Build.scala b/project/Build.scala
index e01392ba68cad6ca95e8b4cbc06f609a5f32797d..cdce363a1872dbd4a597ffc9be6e5f2be44868f5 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -17,65 +17,68 @@ object Leon extends Build {
}
val scriptTask = TaskKey[Unit]("script", "Generate the " + scriptName + " Bash script") <<= (streams, dependencyClasspath in Compile, classDirectory in Compile) map { (s, deps, out) =>
- if(!scriptFile.exists) {
+ if(scriptFile.exists) {
+ s.log.info("Re-generating script ("+(if(is64) "64b" else "32b")+")...")
+ scriptFile.delete
+ } else {
s.log.info("Generating script ("+(if(is64) "64b" else "32b")+")...")
- try {
- val depsPaths = deps.map(_.data.absolutePath)
-
- val depsPaths64 = depsPaths.filterNot(_.endsWith("unmanaged/z3.jar"))
- val depsPaths32 = depsPaths.filterNot(_.endsWith("unmanaged/z3-64.jar"))
-
- // One ugly hack... Likely to fail for Windows, but it's a Bash script anyway.
- val scalaHomeDir = depsPaths.find(_.endsWith("lib/scala-library.jar")) match {
- case None => throw new Exception("Couldn't guess SCALA_HOME.")
- case Some(p) => p.substring(0, p.length - 21)
- }
- s.log.info("Will use " + scalaHomeDir + " as SCALA_HOME.")
-
- val nl = System.getProperty("line.separator")
- val fw = new java.io.FileWriter(scriptFile)
- fw.write("#!/bin/bash --posix" + nl)
- if (is64) {
+ }
+ try {
+ val depsPaths = deps.map(_.data.absolutePath)
+
+ val depsPaths64 = depsPaths.filterNot(_.endsWith("unmanaged/z3.jar"))
+ val depsPaths32 = depsPaths.filterNot(_.endsWith("unmanaged/z3-64.jar"))
+
+ // One ugly hack... Likely to fail for Windows, but it's a Bash script anyway.
+ val scalaHomeDir = depsPaths.find(_.endsWith("lib/scala-library.jar")) match {
+ case None => throw new Exception("Couldn't guess SCALA_HOME.")
+ case Some(p) => p.substring(0, p.length - 21)
+ }
+ s.log.info("Will use " + scalaHomeDir + " as SCALA_HOME.")
+
+ val nl = System.getProperty("line.separator")
+ val fw = new java.io.FileWriter(scriptFile)
+ fw.write("#!/bin/bash --posix" + nl)
+ if (is64) {
+ fw.write("SCALACLASSPATH=\"")
+ fw.write((out.absolutePath +: depsPaths64).mkString(":"))
+ fw.write("\"" + nl + nl)
+
+ // Setting the dynamic lib path
+ fw.write("LIBRARY_PATH=\"" + ldLibraryDir64.absolutePath + "\"" + nl)
+ } else {
+ fw.write("if [ `uname -m` == \"x86_64\" ]; then "+nl)
+
fw.write("SCALACLASSPATH=\"")
fw.write((out.absolutePath +: depsPaths64).mkString(":"))
fw.write("\"" + nl + nl)
// Setting the dynamic lib path
fw.write("LIBRARY_PATH=\"" + ldLibraryDir64.absolutePath + "\"" + nl)
- } else {
- fw.write("if [ `uname -m` == \"x86_64\" ]; then "+nl)
-
- fw.write("SCALACLASSPATH=\"")
- fw.write((out.absolutePath +: depsPaths64).mkString(":"))
- fw.write("\"" + nl + nl)
-
- // Setting the dynamic lib path
- fw.write("LIBRARY_PATH=\"" + ldLibraryDir64.absolutePath + "\"" + nl)
-
- fw.write("else" + nl)
-
- fw.write("SCALACLASSPATH=\"")
- fw.write((out.absolutePath +: depsPaths32).mkString(":"))
- fw.write("\"" + nl + nl)
-
- // Setting the dynamic lib path
- fw.write("LIBRARY_PATH=\"" + ldLibraryDir32.absolutePath + "\"" + nl)
- fw.write("fi" + nl)
-
- }
-
- // the Java command that uses sbt's local Scala to run the whole contraption.
- fw.write("LD_LIBRARY_PATH=\"$LIBRARY_PATH\" \\"+nl)
- fw.write("java -Xmx2G -Xms512M -classpath ${SCALACLASSPATH} -Dscala.home=\"")
- fw.write(scalaHomeDir)
- fw.write("\" -Dscala.usejavacp=true ")
- fw.write("scala.tools.nsc.MainGenericRunner -classpath ${SCALACLASSPATH} ")
- fw.write("leon.Main $@" + nl)
- fw.close
- scriptFile.setExecutable(true)
- } catch {
- case e => s.log.error("There was an error while generating the script file: " + e.getLocalizedMessage)
+
+ fw.write("else" + nl)
+
+ fw.write("SCALACLASSPATH=\"")
+ fw.write((out.absolutePath +: depsPaths32).mkString(":"))
+ fw.write("\"" + nl + nl)
+
+ // Setting the dynamic lib path
+ fw.write("LIBRARY_PATH=\"" + ldLibraryDir32.absolutePath + "\"" + nl)
+ fw.write("fi" + nl)
+
}
+
+ // the Java command that uses sbt's local Scala to run the whole contraption.
+ fw.write("LD_LIBRARY_PATH=\"$LIBRARY_PATH\" \\"+nl)
+ fw.write("java -Xmx2G -Xms512M -classpath ${SCALACLASSPATH} -Dscala.home=\"")
+ fw.write(scalaHomeDir)
+ fw.write("\" -Dscala.usejavacp=true ")
+ fw.write("scala.tools.nsc.MainGenericRunner -classpath ${SCALACLASSPATH} ")
+ fw.write("leon.Main $@" + nl)
+ fw.close
+ scriptFile.setExecutable(true)
+ } catch {
+ case e => s.log.error("There was an error while generating the script file: " + e.getLocalizedMessage)
}
}