diff --git a/mytest/Bubble.scala b/mytest/Bubble.scala
index 33ad5c1039ad7955a3504005683a0b562eb9f8a7..4e274e2707b0cff262e712ab4b78b53eee0db990 100644
--- a/mytest/Bubble.scala
+++ b/mytest/Bubble.scala
@@ -5,7 +5,7 @@ import leon.Utils._
object Bubble {
def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = ({
- require(size <= 5 && isArray(a, size))
+ require(size < 5 && isArray(a, size))
var i = size - 1
var j = 0
var sortedArray = a
@@ -24,12 +24,12 @@ object Bubble {
i < size &&
isArray(sortedArray, size) &&
partitioned(sortedArray, size, 0, i, i+1, size-1) &&
- partitioned(sortedArray, size, 0, j-1, j, j) &&
- sorted(sortedArray, size, i, size-1)
+ sorted(sortedArray, size, i, size-1) &&
+ partitioned(sortedArray, size, 0, j-1, j, j)
)
i = i - 1
}) invariant(
- i >= -1 &&
+ i >= 0 &&
i < size &&
isArray(sortedArray, size) &&
partitioned(sortedArray, size, 0, i, i+1, size-1) &&
@@ -49,29 +49,81 @@ object Bubble {
}) invariant(k <= u && k >= l)
isSorted
}
+ /*
+ // --------------------- sorted --------------------
+ def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
+ val t = sortedWhile(true, l, l, u, a, size)
+ t._1
+ }
+
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
+ } else (isSorted, k)
+ }
+ */
+ /*
+ // ------------- partitioned ------------------
+ def partitioned(a: Map[Int,Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && u1 < l2 && u2 < size)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, u1, a)
+ t._2
+ }
+ }
+ def partitionedWhile(j: Int, isPartitionned: Boolean, i: Int, l1: Int, size: Int, u2: Int, l2: Int, u1: Int, a: Map[Int,Int]) : (Int, Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && i >= l1)
+
+ if(i <= u1) {
+ val t = partitionedNestedWhile(isPartitionned, l2, i, l1, u1, size, u2, a, l2)
+ partitionedWhile(t._2, t._1, i + 1, l1, size, u2, l2, u1, a)
+ } else (j, isPartitionned, i)
+ }
+ def partitionedNestedWhile(isPartitionned: Boolean, j: Int, i: Int, l1: Int, u1: Int, size: Int, u2: Int, a: Map[Int,Int], l2: Int): (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && j >= l2 && i >= l1 && i <= u1)
+
+ if (j <= u2) {
+ partitionedNestedWhile(
+ (if (a(i) > a(j))
+ false
+ else
+ isPartitionned),
+ j + 1, i, l1, u1, size, u2, a, l2)
+ } else (isPartitionned, j)
+ }
+ */
+
def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
- require(l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && isArray(a, size) && size < 5)
- var i = l1
- var j = l2
- var isPartitionned = true
- (while(i <= u1) {
- j = l2
- (while(j <= u2) {
- if(a(i) > a(j))
- isPartitionned = false
- j = j + 1
- }) invariant(j >= l2 && i <= u1)
- i = i + 1
- }) invariant(i >= l1)
- isPartitionned
+ require(l1 >= 0 && u1 < l2 && u2 < size && isArray(a, size) && size < 5)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ (while(i <= u1) {
+ j = l2
+ (while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j + 1
+ }) invariant(j >= l2 && i <= u1)
+ i = i + 1
+ }) invariant(i >= l1)
+ isPartitionned
+ }
}
def isArray(a: Map[Int, Int], size: Int): Boolean = {
def rec(i: Int): Boolean = if(i >= size) true else {
if(a.isDefinedAt(i)) rec(i+1) else false
}
- if(size < 0)
+ if(size <= 0)
false
else
rec(0)
diff --git a/mytest/BubbleFun.scala b/mytest/BubbleFun.scala
index e4d551a7c9c894707e3ed281c425e0ef26008863..5962eea28e93cbd3d496ae9c7dd92af3a1297d15 100644
--- a/mytest/BubbleFun.scala
+++ b/mytest/BubbleFun.scala
@@ -8,7 +8,7 @@ object BubbleFun {
val i = size - 1
val t = sortWhile(0, a, i, size)
t._2
- }) ensuring(res => isArray(res, size) && sorted(res, size, 0, size-1) && content(res, size) == content(a, size))
+ }) ensuring(res => isArray(res, size) && sorted(res, size, 0, size-1) /*&& content(res, size) == content(a, size)*/)
def sortWhile(j: Int, sortedArray: Map[Int,Int], i: Int, size: Int) : (Int, Map[Int,Int], Int) = ({
require(i >= 0 && i < size && isArray(sortedArray, size) && size < 5 &&
@@ -22,7 +22,7 @@ object BubbleFun {
}) ensuring(res => isArray(res._2, size) &&
sorted(res._2, size, res._3, size - 1) &&
partitioned(res._2, size, 0, res._3, res._3+1, size-1) &&
- res._3 >= 0 && res._3 <= 0 && content(res._2, size) == content(sortedArray, size)
+ res._3 >= 0 && res._3 <= 0 /*&& content(res._2, size) == content(sortedArray, size)*/
)
@@ -43,7 +43,7 @@ object BubbleFun {
sorted(res._1, size, i, size - 1) &&
partitioned(res._1, size, 0, i, i+1, size-1) &&
partitioned(res._1, size, 0, res._2-1, res._2, res._2) &&
- res._2 >= i && res._2 >= 0 && res._2 <= i && content(res._1, size) == content(sortedArray, size))
+ res._2 >= i && res._2 >= 0 && res._2 <= i /*&& content(res._1, size) == content(sortedArray, size)*/)
//some intermediate results
diff --git a/mytest/BubbleWeakInvariant.scala b/mytest/BubbleWeakInvariant.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d335cb81ffce8831f0dc1c203ab47c227d761e7f
--- /dev/null
+++ b/mytest/BubbleWeakInvariant.scala
@@ -0,0 +1,132 @@
+import leon.Utils._
+
+/* The calculus of Computation textbook */
+
+object Bubble {
+
+ def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = ({
+ require(size < 5 && isArray(a, size))
+ var i = size - 1
+ var j = 0
+ var sortedArray = a
+ (while(i > 0) {
+ j = 0
+ (while(j < i) {
+ if(sortedArray(j) > sortedArray(j+1)) {
+ val tmp = sortedArray(j)
+ sortedArray = sortedArray.updated(j, sortedArray(j+1))
+ sortedArray = sortedArray.updated(j+1, tmp)
+ }
+ j = j + 1
+ }) invariant(
+ j >= 0 &&
+ j <= i &&
+ i < size &&
+ isArray(sortedArray, size) &&
+ partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+ //partitioned(sortedArray, size, 0, j-1, j, j) &&
+ sorted(sortedArray, size, i, size-1)
+ )
+ i = i - 1
+ }) invariant(
+ i >= 0 &&
+ i < size &&
+ isArray(sortedArray, size) &&
+ partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+ sorted(sortedArray, size, i, size-1)
+ )
+ sortedArray
+ }) ensuring(res => sorted(res, size, 0, size-1))
+
+ def sorted(a: Map[Int, Int], size: Int, l: Int, u: Int): Boolean = {
+ require(isArray(a, size) && size < 5 && l >= 0 && u < size && 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
+ }
+ /*
+ // --------------------- sorted --------------------
+ def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
+ val t = sortedWhile(true, l, l, u, a, size)
+ t._1
+ }
+
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
+ } else (isSorted, k)
+ }
+ */
+
+ /*
+ // ------------- partitioned ------------------
+ def partitioned(a: Map[Int,Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && u1 < l2 && u2 < size)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, u1, a)
+ t._2
+ }
+ }
+ def partitionedWhile(j: Int, isPartitionned: Boolean, i: Int, l1: Int, size: Int, u2: Int, l2: Int, u1: Int, a: Map[Int,Int]) : (Int, Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && i >= l1)
+
+ if(i <= u1) {
+ val t = partitionedNestedWhile(isPartitionned, l2, i, l1, u1, size, u2, a, l2)
+ partitionedWhile(t._2, t._1, i + 1, l1, size, u2, l2, u1, a)
+ } else (j, isPartitionned, i)
+ }
+ def partitionedNestedWhile(isPartitionned: Boolean, j: Int, i: Int, l1: Int, u1: Int, size: Int, u2: Int, a: Map[Int,Int], l2: Int): (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && j >= l2 && i >= l1 && i <= u1)
+
+ if (j <= u2) {
+ partitionedNestedWhile(
+ (if (a(i) > a(j))
+ false
+ else
+ isPartitionned),
+ j + 1, i, l1, u1, size, u2, a, l2)
+ } else (isPartitionned, j)
+ }
+ */
+
+ def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(l1 >= 0 && u1 < l2 && u2 < size && isArray(a, size) && size < 5)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ (while(i <= u1) {
+ j = l2
+ (while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j + 1
+ }) invariant(j >= l2 && i <= u1)
+ i = i + 1
+ }) invariant(i >= l1)
+ isPartitionned
+ }
+ }
+
+ def isArray(a: Map[Int, Int], size: Int): Boolean = {
+ def rec(i: Int): Boolean = if(i >= size) true else {
+ if(a.isDefinedAt(i)) rec(i+1) else false
+ }
+ if(size <= 0)
+ false
+ else
+ rec(0)
+ }
+
+}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 6593e418c28a4f49f5b8a798b527b468e9f3040c..797a209e57d08d863f24dcd5f97008d4fc875bf7 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -23,4 +23,5 @@ object Settings {
var useParallel : Boolean = false
// When this is None, use real integers
var bitvectorBitwidth : Option[Int] = None
+ var verbose : Boolean = false
}
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index b059ad59dbf218ea9042eb6923484778c3ae5c46..5de24fa44bbf489350371d2bce9775231ebf3e1d 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -39,7 +39,8 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
" --cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
" --quickcheck Use QuickCheck-like random search" + "\n" +
" --parallel Run all solvers in parallel" + "\n" +
- " --noLuckyTests Do not perform additional tests to potentially find models early"
+ " --noLuckyTests Do not perform additional tests to potentially find models early" + "\n" +
+ " --verbose Print debugging informations"
)
/** Processes the command-line options. */
@@ -62,6 +63,7 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
case "quickcheck" => leon.Settings.useQuickCheck = true
case "parallel" => leon.Settings.useParallel = true
case "noLuckyTests" => leon.Settings.luckyTest = false
+ case "verbose" => leon.Settings.verbose = true
case s if s.startsWith("unrolling=") => leon.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("functions=") => leon.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
case s if s.startsWith("extensions=") => leon.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))