diff --git a/src/test/resources/regression/verification/newsolvers/invalid/Acc.scala b/src/test/resources/regression/verification/newsolvers/invalid/Acc.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2edd23ab78401f64fe7e6623cf3ace59d35007a7
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/Acc.scala
@@ -0,0 +1,24 @@
+import leon.annotation._
+import leon.lang._
+
+object Acc {
+
+ case class Acc(checking : Int, savings : Int)
+
+ def putAside(x: Int, a: Acc): Acc = {
+ require (x > 0 && notRed(a) && a.checking >= x)
+ Acc(a.checking - x, a.savings + x)
+ } ensuring {
+ r => notRed(r) && sameTotal(a, r)
+ }
+
+
+ def sameTotal(a1: Acc, a2: Acc): Boolean = {
+ a1.checking + a1.savings == a2.checking + a2.savings
+ }
+
+ def notRed(a: Acc) : Boolean = {
+ a.checking >= 0 && a.savings >= 0
+ }
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Acc.scala b/src/test/resources/regression/verification/newsolvers/valid/Acc.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6dce9c294de8c788db4ffa7f205c1ac47905d5a5
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Acc.scala
@@ -0,0 +1,24 @@
+import leon.annotation._
+import leon.lang._
+
+object Acc {
+
+ case class Acc(checking : BigInt, savings : BigInt)
+
+ def putAside(x: BigInt, a: Acc): Acc = {
+ require (x > 0 && notRed(a) && a.checking >= x)
+ Acc(a.checking - x, a.savings + x)
+ } ensuring {
+ r => notRed(r) && sameTotal(a, r)
+ }
+
+
+ def sameTotal(a1: Acc, a2: Acc): Boolean = {
+ a1.checking + a1.savings == a2.checking + a2.savings
+ }
+
+ def notRed(a: Acc) : Boolean = {
+ a.checking >= 0 && a.savings >= 0
+ }
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/AddingPositiveNumbers.scala b/src/test/resources/regression/verification/newsolvers/valid/AddingPositiveNumbers.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ad5efa8794a974e620fe5c0ea936380a36dd562b
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/AddingPositiveNumbers.scala
@@ -0,0 +1,11 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object AddingPositiveNumbers {
+
+ //this should not overflow
+ def additionSound(x: BigInt, y: BigInt): BigInt = {
+ require(x >= 0 && y >= 0)
+ x + y
+ } ensuring(_ >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala b/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1f74ed4b12933352dedeb22dadff0f1d1121f19d
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala
@@ -0,0 +1,126 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import scala.collection.immutable.Set
+import leon.lang._
+import leon.annotation._
+
+object AmortizedQueue {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class AbsQueue
+ case class Queue(front : List, rear : List) extends AbsQueue
+
+ def size(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def asList(queue : AbsQueue) : List = queue match {
+ case Queue(front, rear) => concat(front, reverse(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) && content(res) == content(l1) ++ content(l2))
+
+ def isAmortized(queue : AbsQueue) : Boolean = queue match {
+ case Queue(front, rear) => size(front) >= size(rear)
+ }
+
+ def isEmpty(queue : AbsQueue) : Boolean = queue match {
+ case Queue(Nil(), Nil()) => true
+ case _ => false
+ }
+
+ def reverse(l : List) : List = (l match {
+ case Nil() => Nil()
+ case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil()))
+ }) ensuring (content(_) == content(l))
+
+ def amortizedQueue(front : List, rear : List) : AbsQueue = {
+ if (size(rear) <= size(front))
+ Queue(front, rear)
+ else
+ Queue(concat(front, reverse(rear)), Nil())
+ } ensuring(isAmortized(_))
+
+ def enqueue(queue : AbsQueue, elem : Int) : AbsQueue = (queue match {
+ case Queue(front, rear) => amortizedQueue(front, Cons(elem, rear))
+ }) ensuring(isAmortized(_))
+
+ def tail(queue : AbsQueue) : AbsQueue = {
+ require(isAmortized(queue) && !isEmpty(queue))
+ queue match {
+ case Queue(Cons(f, fs), rear) => amortizedQueue(fs, rear)
+ }
+ } ensuring (isAmortized(_))
+
+ def front(queue : AbsQueue) : Int = {
+ require(isAmortized(queue) && !isEmpty(queue))
+ queue match {
+ case Queue(Cons(f, _), _) => f
+ }
+ }
+
+ // @induct
+ // def propEnqueue(rear : List, front : List, list : List, elem : Int) : Boolean = {
+ // require(isAmortized(Queue(front, rear)))
+ // val queue = Queue(front, rear)
+ // if (asList(queue) == list) {
+ // asList(enqueue(queue, elem)) == concat(list, Cons(elem, Nil()))
+ // } else
+ // true
+ // }.holds
+
+ @induct
+ def propFront(queue : AbsQueue, list : List, elem : Int) : Boolean = {
+ require(!isEmpty(queue) && isAmortized(queue))
+ if (asList(queue) == list) {
+ list match {
+ case Cons(x, _) => front(queue) == x
+ }
+ } else
+ true
+ }.holds
+
+ @induct
+ def propTail(rear : List, front : List, list : List, elem : Int) : Boolean = {
+ require(!isEmpty(Queue(front, rear)) && isAmortized(Queue(front, rear)))
+ if (asList(Queue(front, rear)) == list) {
+ list match {
+ case Cons(_, xs) => asList(tail(Queue(front, rear))) == xs
+ }
+ } else
+ true
+ } //.holds
+
+ def enqueueAndFront(queue : AbsQueue, elem : Int) : Boolean = {
+ if (isEmpty(queue))
+ front(enqueue(queue, elem)) == elem
+ else
+ true
+ }.holds
+
+ def enqueueDequeueThrice(queue : AbsQueue, e1 : Int, e2 : Int, e3 : Int) : Boolean = {
+ if (isEmpty(queue)) {
+ val q1 = enqueue(queue, e1)
+ val q2 = enqueue(q1, e2)
+ val q3 = enqueue(q2, e3)
+ val e1prime = front(q3)
+ val q4 = tail(q3)
+ val e2prime = front(q4)
+ val q5 = tail(q4)
+ val e3prime = front(q5)
+ e1 == e1prime && e2 == e2prime && e3 == e3prime
+ } else
+ true
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Anonymous.scala b/src/test/resources/regression/verification/newsolvers/valid/Anonymous.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d69b1f8423c3ae681527e2a49fb75d6c54672b4f
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Anonymous.scala
@@ -0,0 +1,9 @@
+import leon.lang._
+
+object Anonymous {
+ def test(x: BigInt) = {
+ require(x > 0)
+ val i = (a: BigInt) => a + 1
+ i(x) + i(2)
+ } ensuring { res => res > 0 }
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/ArrayLiterals.scala b/src/test/resources/regression/verification/newsolvers/valid/ArrayLiterals.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d80fcf4f09995c9980ce71cee981d0c0452660c8
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/ArrayLiterals.scala
@@ -0,0 +1,10 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.lang._
+object Numerals {
+ def foo(): Int = {
+ val b : Array[Int] = Array[Int](1,2,3)
+ val a : Array[Int] = Array(1,2,3)
+ a.length
+ } ensuring { _ > 0 }
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/ArrayUpdated.scala b/src/test/resources/regression/verification/newsolvers/valid/ArrayUpdated.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5d336d01dad49d68d1e3d09cc6df719d435261e6
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/ArrayUpdated.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.lang._
+
+object Test {
+
+ def test(a: Array[Int]): Int = {
+ require(a.length > 0)
+ val a2 = a.updated(0, 2)
+ a2(0)
+ } ensuring(res => res == 2)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Asserts1.scala b/src/test/resources/regression/verification/newsolvers/valid/Asserts1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0851ba5adf9eaa3b80a73fe263b904e93fc474da
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Asserts1.scala
@@ -0,0 +1,32 @@
+import leon.lang._
+import leon.annotation._
+import leon._
+
+object Operators {
+
+ def foo(a: BigInt): BigInt = {
+ require(a > 0)
+
+ {
+ val b = a
+ assert(b > 0, "Hey now")
+ b + bar(1)
+ } ensuring { _ > 2 }
+
+ } ensuring {
+ _ > a
+ }
+
+ def bar(a: BigInt): BigInt = {
+ require(a > 0)
+
+ {
+ val b = a
+ assert(b > 0, "Hey now")
+ b + 2
+ } ensuring { _ > 2 }
+
+ } ensuring {
+ _ > a
+ }
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/AssociativeList.scala b/src/test/resources/regression/verification/newsolvers/valid/AssociativeList.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a62a765f5eb3700b90be8fea45df8812413f1b43
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/AssociativeList.scala
@@ -0,0 +1,52 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import scala.collection.immutable.Set
+import leon.lang._
+import leon.annotation._
+
+object AssociativeList {
+ sealed abstract class KeyValuePairAbs
+ case class KeyValuePair(key: Int, value: Int) extends KeyValuePairAbs
+
+ sealed abstract class List
+ case class Cons(head: KeyValuePairAbs, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class OptionInt
+ case class Some(i: Int) extends OptionInt
+ case class None() extends OptionInt
+
+ def domain(l: List): Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(KeyValuePair(k,_), xs) => Set(k) ++ domain(xs)
+ }
+
+ def find(l: List, e: Int): OptionInt = l match {
+ case Nil() => None()
+ case Cons(KeyValuePair(k, v), xs) => if (k == e) Some(v) else find(xs, e)
+ }
+
+ def noDuplicates(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(KeyValuePair(k, v), xs) => find(xs, k) == None() && noDuplicates(xs)
+ }
+
+ def updateAll(l1: List, l2: List): List = (l2 match {
+ case Nil() => l1
+ case Cons(x, xs) => updateAll(updateElem(l1, x), xs)
+ }) ensuring(domain(_) == domain(l1) ++ domain(l2))
+
+ def updateElem(l: List, e: KeyValuePairAbs): List = (l match {
+ case Nil() => Cons(e, Nil())
+ case Cons(KeyValuePair(k, v), xs) => e match {
+ case KeyValuePair(ek, ev) => if (ek == k) Cons(KeyValuePair(ek, ev), xs) else Cons(KeyValuePair(k, v), updateElem(xs, e))
+ }
+ }) ensuring(res => e match {
+ case KeyValuePair(k, v) => domain(res) == domain(l) ++ Set[Int](k)
+ })
+
+ @induct
+ def readOverWrite(l: List, k1: Int, k2: Int, e: Int) : Boolean = {
+ find(updateElem(l, KeyValuePair(k2,e)), k1) == (if (k1 == k2) Some(e) else find(l, k1))
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/BestRealTypes.scala b/src/test/resources/regression/verification/newsolvers/valid/BestRealTypes.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9b1002f7f68f8594f65afd7dfebec9f9920e5f1c
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/BestRealTypes.scala
@@ -0,0 +1,27 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.lang._
+
+/** This benchmarks tests some potential issues with the legacy "bestRealType" function, which was original introduced to work around
+ * Scala's well-too-precise-for-Leon type inference. */
+object BestRealTypes {
+ sealed abstract class Num
+ case class Zero() extends Num
+ case class Succ(pred : Num) extends Num
+
+ case class Wrapper(num : Num)
+
+ def boolToNum(b : Boolean) : Num = if(b) {
+ Zero()
+ } else {
+ Succ(Zero())
+ }
+
+ // This requires computing the "bestRealTypes" of w1 and w2.
+ def zipWrap(w1 : Wrapper, w2 : Wrapper) : (Wrapper,Wrapper) = (w1, w2)
+
+ def somethingToProve(b : Boolean) : Boolean = {
+ val (z1,z2) = zipWrap(Wrapper(boolToNum(b)), Wrapper(boolToNum(!b)))
+ z1.num == Zero() || z2.num == Zero()
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/BitsTricks.scala b/src/test/resources/regression/verification/newsolvers/valid/BitsTricks.scala
new file mode 100644
index 0000000000000000000000000000000000000000..561f38a190cd4edf8fdf1eaee7912e86493c97f7
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/BitsTricks.scala
@@ -0,0 +1,103 @@
+import leon.annotation._
+import leon.lang._
+
+object BitsTricks {
+
+ def bitAt(x: Int, n: Int): Boolean = {
+ require(n >= 0 && n < 32)
+ ((x >> n) & 1) == 1
+ }
+
+ def isEven(x: Int): Boolean = {
+ (x & 1) == 0
+ } ensuring(res => res == (x % 2 == 0))
+
+ def isNegative(x: Int): Boolean = {
+ (x >>> 31) == 1
+ } ensuring(b => b == x < 0)
+
+ def isBitNSet(x: Int, n: Int): Int = {
+ require(n >= 0 && n < 32)
+ (x & (1 << n))
+ }
+
+ def testBitSet1(): Int = {
+ isBitNSet(122, 3)
+ } ensuring(_ != 0)
+ def testBitSet2(): Int = {
+ isBitNSet(-33, 5)
+ } ensuring(_ == 0)
+
+ def setBitN(x: Int, n: Int): Int = {
+ require(n >= 0 && n < 32)
+ x | (1 << n)
+ } ensuring(res => isBitNSet(res, n) != 0)
+
+ def toggleBitN(x: Int, n: Int): Int = {
+ require(n >= 0 && n < 32)
+ x ^ (1 << n)
+ } ensuring(res =>
+ if(isBitNSet(x, n) != 0) isBitNSet(res, n) == 0
+ else isBitNSet(res, n) != 0)
+
+
+ def checkDoubleXor(x: Int, y: Int): Int = {
+ x ^ y ^ x
+ } ensuring(res => res == y)
+
+
+ def turnOffRightmostOneRec(x: Int, index: Int): Int = {
+ require(index >= 0 && index < 32)
+ if(bitAt(x, index)) toggleBitN(x, index)//(x ^ (1 << index))
+ else if(index == 31) x
+ else turnOffRightmostOneRec(x, index + 1)
+ }
+
+ /*
+ * loops forever on the proof
+ */
+ def turnOffRightmostOne(x: Int): Int = {
+ x & (x - 1)
+ } //ensuring(_ == turnOffRightmostOneRec(x, 0))
+
+ // 010100 -> 010111
+ def rightPropagateRightmostOne(x: Int): Int = {
+ x | (x - 1)
+ }
+
+ def property1(x: Int): Boolean = {
+ val y = rightPropagateRightmostOne(x)
+ y == rightPropagateRightmostOne(y)
+ } ensuring(b => b)
+
+ def isRotationLeft(x: Int, y: Int, n: Int, i: Int): Boolean = {
+ require(i >= 0 && i <= 32 && n >= 0 && n < 32)
+ if(i == 32)
+ true
+ else bitAt(x, i) == bitAt(y, (i + n) % 32) && isRotationLeft(x, y, n, i+1)
+ }
+
+ //rotateLeft proves in 1 minute (on very powerful computer)
+ def rotateLeft(x: Int, n: Int): Int = {
+ require(n >= 0 && n < 32)
+ val front = x >>> (32 - n)
+ (x << n) | front
+ } //ensuring(res => isRotationLeft(x, res, n, 0))
+
+ //careful with overflows, case definition, truncated
+ def safeMean(x: Int, y: Int): Int = {
+ if(x >= 0 && y <= 0 || x <= 0 && y >= 0) (x + y)/2
+ else if(x >= 0 && x <= y) x + (y - x)/2
+ else if(x >= 0 && y <= x) y + (x - y)/2
+ else if(x <= 0 && x <= y) y + (x - y)/2
+ else x + (y - x)/2
+ }
+
+ //proves in 45 seconds
+ def magicMean(x: Int, y: Int): Int = {
+ val t = (x&y)+((x^y) >> 1)
+ t + ((t >>> 31) & (x ^ y))
+ } //ensuring(res => res == safeMean(x, y))
+
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/CaseObject1.scala b/src/test/resources/regression/verification/newsolvers/valid/CaseObject1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e46c15305d243b5a07b328813b40eb41964585e7
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/CaseObject1.scala
@@ -0,0 +1,23 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object CaseObject1 {
+
+ abstract sealed class A
+ case class B(size: Int) extends A
+ case object C extends A
+
+ def foo(): A = {
+ C
+ }
+
+ def foo1(a: A): A = a match {
+ case C => a
+ case B(s) => a
+ }
+
+ def foo2(a: A): A = a match {
+ case c @ C => c
+ case B(s) => a
+ }
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Choose1.scala b/src/test/resources/regression/verification/newsolvers/valid/Choose1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..da4b4e7752a7a4a6fcbd21c72533e0312c18cb73
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Choose1.scala
@@ -0,0 +1,42 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang.synthesis._
+import leon.lang._
+
+object Choose1 {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil() => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def listOfSize(i: BigInt): List = {
+ require(i >= 0)
+
+ if (i == BigInt(0)) {
+ Nil()
+ } else {
+ choose { (res: List) => size(res) == i }
+ }
+ } ensuring ( size(_) == i )
+
+
+ def listOfSize2(i: BigInt): List = {
+ require(i >= 0)
+
+ if (i > 0) {
+ Cons(0, listOfSize(i-1))
+ } else {
+ Nil()
+ }
+ } ensuring ( size(_) == i )
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Closures.scala b/src/test/resources/regression/verification/newsolvers/valid/Closures.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5e191cf814e4c66b2df0a3fa16fe19d78a1c343d
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Closures.scala
@@ -0,0 +1,15 @@
+import leon.lang._
+
+object Closures {
+ def addX(x: Int): Int => Int = {
+ (a: Int) => a + x
+ }
+
+ def test(x: Int): Boolean = {
+ val add1 = addX(1)
+ val add2 = addX(2)
+ add1(add2(1)) == 4
+ }.holds
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Closures2.scala b/src/test/resources/regression/verification/newsolvers/valid/Closures2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b791965d1e06edd872d747a68fe084efed52a206
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Closures2.scala
@@ -0,0 +1,35 @@
+import leon.lang._
+
+object Closures2 {
+ def set(i: Int): Int => Boolean = x => x == i
+
+ def union(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) || s2(x)
+
+ def intersection(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && s2(x)
+
+ def diff(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && !s2(x)
+
+ def set123(): Int => Boolean = union(set(1), union(set(2), set(3)))
+
+ def test1(): Boolean = {
+ val s1 = set123()
+ val s2 = union(s1, set(4))
+ s2(1) && s2(2) && s2(3) && s2(4)
+ }.holds
+
+ def test2(): Boolean = {
+ val s1 = set123()
+ val s2 = intersection(s1, union(set(1), set(3)))
+ val s3 = diff(s1, s2)
+ s3(2) && !s3(1) && !s3(3)
+ }.holds
+
+ def test3(): Boolean = {
+ val s1 = set123()
+ val s2 = set123()
+ val s3 = union(s1, s2)
+ s3(1) && s3(2) && s3(3)
+ }.holds
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Field1.scala b/src/test/resources/regression/verification/newsolvers/valid/Field1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7865db5e17b7c7a68acff16c1a4f5dee466f9833
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Field1.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object Field1 {
+
+ abstract sealed class A
+ case class B(size: Int) extends A
+
+ def foo(): Int = {
+ val b = B(3)
+ b.size
+ } ensuring(_ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Field2.scala b/src/test/resources/regression/verification/newsolvers/valid/Field2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..659b64815d6e068b17734670bfb65359205218d4
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Field2.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object Field2 {
+
+ abstract sealed class A
+ case class B(length: Int) extends A
+
+ def foo(): Int = {
+ val b = B(3)
+ b.length
+ } ensuring(_ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/FiniteSort.scala b/src/test/resources/regression/verification/newsolvers/valid/FiniteSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..94d90c3f49d726b17dc0a00cbac91bcb0bdd0f45
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/FiniteSort.scala
@@ -0,0 +1,61 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.lang._
+
+object FiniteSorting {
+
+ // These finite sorting functions essentially implement insertion sort.
+ def sort2(x : Int, y : Int) : (Int,Int) = {
+ if(x < y) (x, y) else (y, x)
+ } ensuring (_ match {
+ case (a, b) => a <= b && Set(a,b) == Set(x,y)
+ })
+
+ def sort3(x1 : Int, x2 : Int, x3 : Int) : (Int, Int, Int) = {
+ val (x1s, x2s) = sort2(x1, x2)
+
+ if(x2s <= x3) {
+ (x1s, x2s, x3)
+ } else if(x1s <= x3) {
+ (x1s, x3, x2s)
+ } else {
+ (x3, x1s, x2s)
+ }
+ } ensuring (_ match {
+ case (a, b, c) => a <= b && b <= c && Set(a,b,c) == Set(x1,x2,x3)
+ })
+
+ def sort4(x1 : Int, x2 : Int, x3 : Int, x4 : Int) : (Int, Int, Int, Int) = {
+ val (x1s, x2s, x3s) = sort3(x1, x2, x3)
+
+ if(x3s <= x4) {
+ (x1s, x2s, x3s, x4)
+ } else if(x2s <= x4) {
+ (x1s, x2s, x4, x3s)
+ } else if(x1s <= x4) {
+ (x1s, x4, x2s, x3s)
+ } else {
+ (x4, x1s, x2s, x3s)
+ }
+ } ensuring (_ match {
+ case (a, b, c, d) => a <= b && b <= c && c <= d && Set(a,b,c,d) == Set(x1,x2,x3,x4)
+ })
+
+ def sort5(x1 : Int, x2 : Int, x3 : Int, x4 : Int, x5 : Int) : (Int, Int, Int, Int, Int) = {
+ val (x1s, x2s, x3s, x4s) = sort4(x1, x2, x3, x4)
+
+ if(x4s <= x5) {
+ (x1s, x2s, x3s, x4s, x5)
+ } else if(x3s <= x5) {
+ (x1s, x2s, x3s, x5, x4s)
+ } else if(x2s <= x5) {
+ (x1s, x2s, x5, x3s, x4s)
+ } else if(x1s <= x5) {
+ (x1s, x5, x2s, x3s, x4s)
+ } else {
+ (x5, x1s, x2s, x3s, x4s)
+ }
+ } ensuring (_ match {
+ case (a, b, c, d, e) => a <= b && b <= c && c <= d && d <= e && Set(a,b,c,d,e) == Set(x1,x2,x3,x4,x5)
+ })
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/FlatMap.scala b/src/test/resources/regression/verification/newsolvers/valid/FlatMap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..56f8c47e86d835055e6c3a9ea44cb7b886e464fb
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/FlatMap.scala
@@ -0,0 +1,48 @@
+import leon.lang._
+import leon.collection._
+
+object FlatMap {
+
+ def append[T](l1: List[T], l2: List[T]): List[T] = l1 match {
+ case Cons(head, tail) => Cons(head, append(tail, l2))
+ case Nil() => l2
+ }
+
+ def associative_append_lemma[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
+ append(append(l1, l2), l3) == append(l1, append(l2, l3))
+ }
+
+ def associative_append_lemma_induct[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
+ l1 match {
+ case Nil() => associative_append_lemma(l1, l2, l3)
+ case Cons(head, tail) => associative_append_lemma(l1, l2, l3) && associative_append_lemma_induct(tail, l2, l3)
+ }
+ }.holds
+
+ def flatMap[T,U](list: List[T], f: T => List[U]): List[U] = list match {
+ case Cons(head, tail) => append(f(head), flatMap(tail, f))
+ case Nil() => Nil()
+ }
+
+ def associative_lemma[T,U,V](list: List[T], f: T => List[U], g: U => List[V]): Boolean = {
+ flatMap(flatMap(list, f), g) == flatMap(list, (x: T) => flatMap(f(x), g))
+ }
+
+ def associative_lemma_induct[T,U,V](list: List[T], flist: List[U], glist: List[V], f: T => List[U], g: U => List[V]): Boolean = {
+ associative_lemma(list, f, g) &&
+ append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) &&
+ (glist match {
+ case Cons(ghead, gtail) =>
+ associative_lemma_induct(list, flist, gtail, f, g)
+ case Nil() => flist match {
+ case Cons(fhead, ftail) =>
+ associative_lemma_induct(list, ftail, g(fhead), f, g)
+ case Nil() => list match {
+ case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
+ case Nil() => true
+ }
+ }
+ })
+ }.holds
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/FoldAssociative.scala b/src/test/resources/regression/verification/newsolvers/valid/FoldAssociative.scala
new file mode 100644
index 0000000000000000000000000000000000000000..261d15c0fcd6419f5a2d024d2155257726ba8394
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/FoldAssociative.scala
@@ -0,0 +1,101 @@
+import leon._
+import leon.lang._
+
+object FoldAssociative {
+
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class Option
+ case class Some(x: Int) extends Option
+ case class None() extends Option
+
+ def foldRight[A](list: List, state: A, f: (Int, A) => A): A = list match {
+ case Cons(head, tail) =>
+ val tailState = foldRight(tail, state, f)
+ f(head, tailState)
+ case Nil() => state
+ }
+
+ def take(list: List, count: Int): List = {
+ require(count >= 0)
+ list match {
+ case Cons(head, tail) if count > 0 => Cons(head, take(tail, count - 1))
+ case _ => Nil()
+ }
+ }
+
+ def drop(list: List, count: Int): List = {
+ require(count >= 0)
+ list match {
+ case Cons(head, tail) if count > 0 => drop(tail, count - 1)
+ case _ => list
+ }
+ }
+
+ def append(l1: List, l2: List): List = {
+ l1 match {
+ case Cons(head, tail) => Cons(head, append(tail, l2))
+ case Nil() => l2
+ }
+ }
+
+ def lemma_split(list: List, x: Int): Boolean = {
+ require(x >= 0)
+ val f = (x: Int, s: Int) => x + s
+ val l1 = take(list, x)
+ val l2 = drop(list, x)
+ foldRight(list, 0, f) == foldRight(l1, foldRight(l2, 0, f), f)
+ }
+
+ def lemma_split_induct(list: List, x: Int): Boolean = {
+ require(x >= 0)
+ val f = (x: Int, s: Int) => x + s
+ val l1 = take(list, x)
+ val l2 = drop(list, x)
+ lemma_split(list, x) && (list match {
+ case Cons(head, tail) if x > 0 =>
+ lemma_split_induct(tail, x - 1)
+ case _ => true
+ })
+ }.holds
+
+ def lemma_reassociative(list: List, x: Int): Boolean = {
+ require(x >= 0)
+ val f = (x: Int, s: Int) => x + s
+ val l1 = take(list, x)
+ val l2 = drop(list, x)
+
+ foldRight(list, 0, f) == foldRight(l1, 0, f) + foldRight(l2, 0, f)
+ }
+
+ def lemma_reassociative_induct(list: List, x: Int): Boolean = {
+ require(x >= 0)
+ val f = (x: Int, s: Int) => x + s
+ val l1 = take(list, x)
+ val l2 = drop(list, x)
+ lemma_reassociative(list, x) && (list match {
+ case Cons(head, tail) if x > 0 =>
+ lemma_reassociative_induct(tail, x - 1)
+ case _ => true
+ })
+ }.holds
+
+ def lemma_reassociative_presplit(l1: List, l2: List): Boolean = {
+ val f = (x: Int, s: Int) => x + s
+ val list = append(l1, l2)
+ foldRight(list, 0, f) == foldRight(l1, 0, f) + foldRight(l2, 0, f)
+ }
+
+ def lemma_reassociative_presplit_induct(l1: List, l2: List): Boolean = {
+ val f = (x: Int, s: Int) => x + s
+ val list = append(l1, l2)
+ lemma_reassociative_presplit(l1, l2) && (l1 match {
+ case Cons(head, tail) =>
+ lemma_reassociative_presplit_induct(tail, l2)
+ case Nil() => true
+ })
+ }.holds
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/FoolProofAdder.scala b/src/test/resources/regression/verification/newsolvers/valid/FoolProofAdder.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4fd46f85fc051b8de8d1025e74a7a6a6275e0611
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/FoolProofAdder.scala
@@ -0,0 +1,11 @@
+import leon.annotation._
+import leon.lang._
+
+object FoolProofAdder {
+
+ def foolProofAdder(x: BigInt): BigInt = {
+ require(x > 0)
+ x + BigInt(999999) + BigInt("999999999999999")
+ } ensuring(_ > 0)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Generics.scala b/src/test/resources/regression/verification/newsolvers/valid/Generics.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f4c5c1b20bf0b6183e94d34d7c51de8eac7aa499
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Generics.scala
@@ -0,0 +1,23 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.lang._
+
+object Generics {
+ abstract class List[T]
+ case class Cons[A](head: A, tail: List[A]) extends List[A]
+ case class Nil[B]() extends List[B]
+
+ def size[T](l: List[T]): BigInt = (l match {
+ case Nil() => BigInt(0)
+ case Cons(h, t) => 1+size(t)
+ })ensuring { _ >= 0 }
+
+ def content[T](l: List[T]): Set[T] = l match {
+ case Nil() => Set()
+ case Cons(h, t) => Set(h) ++ content(t)
+ }
+
+ def insert[T](a: T, l: List[T]): List[T] = {
+ Cons(a, l)
+ } ensuring { res => (size(res) == size(l) + 1) && (content(res) == content(l) ++ Set(a))}
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Generics2.scala b/src/test/resources/regression/verification/newsolvers/valid/Generics2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3ad9b7df9a5090a1abfa268f3bdbcbd7a57f2119
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Generics2.scala
@@ -0,0 +1,27 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.lang._
+
+object Generics1 {
+ abstract class List[T]
+ case class Cons[A](head: A, tail: List[A]) extends List[A]
+ case class Nil[B]() extends List[B]
+
+ def size[T](l: List[T]): BigInt = (l match {
+ case Nil() => BigInt(0)
+ case Cons(h, t) => size(t) + BigInt(1)
+ }) ensuring((res: BigInt) => res >= BigInt(0))
+
+ def content[T](l: List[T]): Set[T] = l match {
+ case Nil() => Set()
+ case Cons(h, t) => Set(h) ++ content(t)
+ }
+
+ def insert[T](a: T, l: List[T]): List[T] = {
+ Cons(a, l)
+ } ensuring { res => (size(res) == size(l) + 1) && (content(res) == content(l) ++ Set(a))}
+
+ def insertInt(a: BigInt, l: List[BigInt]): List[BigInt] = {
+ insert(a,l)
+ } ensuring { res => (size(res) == size(l) + 1) && (content(res) == content(l) ++ Set(a))}
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/HOInvocations.scala b/src/test/resources/regression/verification/newsolvers/valid/HOInvocations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0f2fbda2ff6e892e200b475f06d8e1876bd6ed64
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/HOInvocations.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object HOInvocations {
+ def switch(x: Int, f: (Int) => Int, g: (Int) => Int) = if(x > 0) f else g
+
+ def passing_1(f: (Int) => Int) = {
+ switch(10, (x: Int) => x + 1, f)(2)
+ } ensuring { res => res > 0 }
+
+ def passing_2(x: Int, f: (Int) => Int, g: (Int) => Int) = {
+ require(x > 0)
+ switch(1, switch(x, f, g), g)(1)
+ } ensuring { res => res == f(1) }
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Heap.scala b/src/test/resources/regression/verification/newsolvers/valid/Heap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..260cc858364b8bd702de2d686745f0a6173fe510
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Heap.scala
@@ -0,0 +1,147 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+
+object Heaps {
+ /*~~~~~~~~~~~~~~~~~~~~~~~*/
+ /* Data type definitions */
+ /*~~~~~~~~~~~~~~~~~~~~~~~*/
+ private case class Node(rank : BigInt, elem : Int, nodes : Heap)
+
+ sealed abstract class Heap
+ private case class Nodes(head : Node, tail : Heap) extends Heap
+ private case object Empty extends Heap
+
+ sealed abstract class OptInt
+ case class Some(value : Int) extends OptInt
+ case object None extends OptInt
+
+ /*~~~~~~~~~~~~~~~~~~~~~~~*/
+ /* Abstraction functions */
+ /*~~~~~~~~~~~~~~~~~~~~~~~*/
+ def heapContent(h : Heap) : Set[Int] = h match {
+ case Empty => Set.empty[Int]
+ case Nodes(n, ns) => nodeContent(n) ++ heapContent(ns)
+ }
+
+ def nodeContent(n : Node) : Set[Int] = n match {
+ case Node(_, e, h) => Set(e) ++ heapContent(h)
+ }
+
+ /*~~~~~~~~~~~~~~~~~~~~~~~~*/
+ /* Helper/local functions */
+ /*~~~~~~~~~~~~~~~~~~~~~~~~*/
+ private def reverse(h : Heap) : Heap = reverse0(h, Empty)
+ private def reverse0(h : Heap, acc : Heap) : Heap = (h match {
+ case Empty => acc
+ case Nodes(n, ns) => reverse0(ns, Nodes(n, acc))
+ }) ensuring(res => heapContent(res) == heapContent(h) ++ heapContent(acc))
+
+ private def link(t1 : Node, t2 : Node) = (t1, t2) match {
+ case (Node(r, e1, ns1), Node(_, e2, ns2)) =>
+ if(e1 <= e2) {
+ Node(r + 1, e1, Nodes(t2, ns1))
+ } else {
+ Node(r + 1, e2, Nodes(t1, ns2))
+ }
+ }
+
+ private def insertNode(t : Node, h : Heap) : Heap = (h match {
+ case Empty => Nodes(t, Empty)
+ case Nodes(t2, h2) =>
+ if(t.rank < t2.rank) {
+ Nodes(t, h)
+ } else {
+ insertNode(link(t, t2), h2)
+ }
+ }) ensuring(res => heapContent(res) == nodeContent(t) ++ heapContent(h))
+
+ private def getMin(h : Heap) : (Node, Heap) = {
+ require(h != Empty)
+ h match {
+ case Nodes(t, Empty) => (t, Empty)
+ case Nodes(t, ts) =>
+ val (t0, ts0) = getMin(ts)
+ if(t.elem < t0.elem) {
+ (t, ts)
+ } else {
+ (t0, Nodes(t, ts0))
+ }
+ }
+ } ensuring(_ match {
+ case (n,h2) => nodeContent(n) ++ heapContent(h2) == heapContent(h)
+ })
+
+ /*~~~~~~~~~~~~~~~~*/
+ /* Heap interface */
+ /*~~~~~~~~~~~~~~~~*/
+ def empty() : Heap = {
+ Empty
+ } ensuring(res => heapContent(res) == Set.empty[Int])
+
+ def isEmpty(h : Heap) : Boolean = {
+ (h == Empty)
+ } ensuring(res => res == (heapContent(h) == Set.empty[Int]))
+
+ def insert(e : Int, h : Heap) : Heap = {
+ insertNode(Node(0, e, Empty), h)
+ } ensuring(res => heapContent(res) == heapContent(h) ++ Set(e))
+
+ def merge(h1 : Heap, h2 : Heap) : Heap = ((h1,h2) match {
+ case (_, Empty) => h1
+ case (Empty, _) => h2
+ case (Nodes(t1, ts1), Nodes(t2, ts2)) =>
+ if(t1.rank < t2.rank) {
+ Nodes(t1, merge(ts1, h2))
+ } else if(t2.rank < t1.rank) {
+ Nodes(t2, merge(h1, ts2))
+ } else {
+ insertNode(link(t1, t2), merge(ts1, ts2))
+ }
+ }) ensuring(res => heapContent(res) == heapContent(h1) ++ heapContent(h2))
+
+ def findMin(h : Heap) : OptInt = (h match {
+ case Empty => None
+ case Nodes(Node(_, e, _), ns) =>
+ findMin(ns) match {
+ case None => Some(e)
+ case Some(e2) => Some(if(e < e2) e else e2)
+ }
+ }) ensuring(_ match {
+ case None => isEmpty(h)
+ case Some(v) => heapContent(h).contains(v)
+ })
+
+ def deleteMin(h : Heap) : Heap = (h match {
+ case Empty => Empty
+ case ts : Nodes =>
+ val (Node(_, e, ns1), ns2) = getMin(ts)
+ merge(reverse(ns1), ns2)
+ }) ensuring(res => heapContent(res).subsetOf(heapContent(h)))
+
+ def sanity0() : Boolean = {
+ val h0 : Heap = Empty
+ val h1 = insert(42, h0)
+ val h2 = insert(72, h1)
+ val h3 = insert(0, h2)
+ findMin(h0) == None &&
+ findMin(h1) == Some(42) &&
+ findMin(h2) == Some(42) &&
+ findMin(h3) == Some(0)
+ }.holds
+
+ def sanity1() : Boolean = {
+ val h0 = insert(42, Empty)
+ val h1 = insert(0, Empty)
+ val h2 = merge(h0, h1)
+ findMin(h2) == Some(0)
+ }.holds
+
+ def sanity3() : Boolean = {
+ val h0 = insert(42, insert(0, insert(12, Empty)))
+ val h1 = deleteMin(h0)
+ findMin(h1) == Some(12)
+ }.holds
+}
+
diff --git a/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala b/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a3120a9bc9e728ab5a6f352d649b64e9c67e761c
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
@@ -0,0 +1,69 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import scala.collection.immutable.Set
+import leon.annotation._
+import leon.lang._
+
+object InsertionSort {
+ sealed abstract class List
+ case class Cons(head:Int,tail:List) extends List
+ case class Nil() extends List
+
+ sealed abstract class OptInt
+ case class Some(value: Int) extends OptInt
+ case class None() extends OptInt
+
+ def size(l : List) : BigInt = (l match {
+ case Nil() => BigInt(0)
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def min(l : List) : OptInt = l match {
+ case Nil() => None()
+ case Cons(x, xs) => min(xs) match {
+ case None() => Some(x)
+ case Some(x2) => if(x < x2) Some(x) else Some(x2)
+ }
+ }
+
+ def isSorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x, Nil()) => true
+ case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
+ }
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def sortedIns(e: Int, l: List): List = {
+ require(isSorted(l))
+ 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)
+ && size(res) == size(l) + 1
+ )
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def sort(l: List): List = (l match {
+ case Nil() => Nil()
+ case Cons(x,xs) => sortedIns(x, sort(xs))
+ }) ensuring(res => contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l)
+ )
+
+ 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(sort(ls))
+ }
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/InstanceOf1.scala b/src/test/resources/regression/verification/newsolvers/valid/InstanceOf1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..14dab69bcd3df6e4030542d333e41b6f3ce7c56a
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/InstanceOf1.scala
@@ -0,0 +1,20 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object InstanceOf1 {
+
+ abstract class A
+ case class B(i: Int) extends A
+ case class C(i: Int) extends A
+
+ def foo(): Int = {
+ require(C(3).isInstanceOf[C])
+ val b: A = B(2)
+ if(b.isInstanceOf[B])
+ 0
+ else
+ -1
+ } ensuring(_ == 0)
+
+ def bar(): Int = foo()
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Lambdas.scala b/src/test/resources/regression/verification/newsolvers/valid/Lambdas.scala
new file mode 100644
index 0000000000000000000000000000000000000000..36ae0c7ad7f8a68e36358d9e5adb885e7bb108da
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Lambdas.scala
@@ -0,0 +1,15 @@
+import leon.lang._
+
+object Lambdas {
+ def gen(x: Int): (Int) => Int = {
+ val f = (x: Int) => x + 1
+ val g = (x: Int) => x + 2
+ if (x > 0) g else f
+ }
+
+ def test(x: Int): Boolean = {
+ require(x > 0)
+ val f = gen(x)
+ f(x) == x + 2
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala b/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2986a4342ac0bf5f65b2bb21dad5324fdb5223b8
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala
@@ -0,0 +1,105 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import scala.collection.immutable.Set
+import leon.annotation._
+import leon.lang._
+
+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) : BigInt = (l match {
+ case Nil() => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def iplSize(l: IntPairList) : BigInt = (l match {
+ case IPNil() => BigInt(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) : BigInt = sizeTailRecAcc(l, 0)
+ def sizeTailRecAcc(l: List, acc: BigInt) : BigInt = {
+ 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) == BigInt(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
+
+ @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/src/test/resources/regression/verification/newsolvers/valid/Lists1.scala b/src/test/resources/regression/verification/newsolvers/valid/Lists1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..719c3d236009c96aa62986725df47ea20e3a906a
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Lists1.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.collection._
+import leon.annotation._
+
+object Lists1 {
+
+ def exists[T](list: List[T], f: T => Boolean): Boolean = list match {
+ case Cons(head, tail) => f(head) || exists(tail, f)
+ case Nil() => false
+ }
+
+ def forall[T](list: List[T], f: T => Boolean): Boolean = list match {
+ case Cons(head, tail) => f(head) && forall(tail, f)
+ case Nil() => true
+ }
+
+ def exists_lemma[T](list: List[T], f: T => Boolean): Boolean = {
+ exists(list, f) == !forall(list, (x: T) => !f(x))
+ }
+
+ def exists_lemma_induct[T](list: List[T], f: T => Boolean): Boolean = {
+ list match {
+ case Nil() => exists_lemma(list, f)
+ case Cons(head, tail) => exists_lemma(list, f) && exists_lemma_induct(tail, f)
+ }
+ }.holds
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Lists2.scala b/src/test/resources/regression/verification/newsolvers/valid/Lists2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..654046ba0dbf59fba888ec4975b35135a18c88d7
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Lists2.scala
@@ -0,0 +1,49 @@
+import leon.lang._
+
+object Lists2 {
+ abstract class List[T]
+ case class Cons[T](head: T, tail: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+ def forall[T](list: List[T], f: T => Boolean): Boolean = list match {
+ case Cons(head, tail) => f(head) && forall(tail, f)
+ case Nil() => true
+ }
+
+ def positive(list: List[Int]): Boolean = list match {
+ case Cons(head, tail) => if (head < 0) false else positive(tail)
+ case Nil() => true
+ }
+
+ def positive_lemma(list: List[Int]): Boolean = {
+ positive(list) == forall(list, (x: Int) => x >= 0)
+ }
+
+ def positive_lemma_induct(list: List[Int]): Boolean = {
+ list match {
+ case Nil() => positive_lemma(list)
+ case Cons(head, tail) => positive_lemma(list) && positive_lemma_induct(tail)
+ }
+ }.holds
+
+ def remove[T](list: List[T], e: T) : List[T] = {
+ list match {
+ case Nil() => Nil()
+ case Cons(x, xs) if x == e => remove(xs, e)
+ case Cons(x, xs) => Cons(x, remove(xs, e))
+ }
+ } //ensuring { (res: List[T]) => forall(res, (x : T) => x != e) }
+
+ def remove_lemma[T](list: List[T], e: T): Boolean = {
+ forall(remove(list, e), (x : T) => x != e)
+ }
+
+ def remove_lemma_induct[T](list: List[T], e: T): Boolean = {
+ list match {
+ case Nil() => remove_lemma(list, e)
+ case Cons(head, tail) => remove_lemma(list, e) && remove_lemma_induct(tail, e)
+ }
+ }.holds
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Lists3.scala b/src/test/resources/regression/verification/newsolvers/valid/Lists3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..67060133a65e1661b32757ff98b0857e71897d12
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Lists3.scala
@@ -0,0 +1,34 @@
+import leon.lang._
+
+object Lists3 {
+ abstract class List[T]
+ case class Cons[T](head: T, tail: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+ def forall[T](list: List[T], f: T => Boolean): Boolean = list match {
+ case Cons(head, tail) => f(head) && forall(tail, f)
+ case Nil() => true
+ }
+
+ def positive(list: List[Int]): Boolean = list match {
+ case Cons(head, tail) => if (head < 0) false else positive(tail)
+ case Nil() => true
+ }
+
+ def gt(i: Int): Int => Boolean = x => x > i
+
+ def gte(i: Int): Int => Boolean = x => gt(i)(x) || x == i
+
+ def positive_lemma(list: List[Int]): Boolean = {
+ positive(list) == forall(list, gte(0))
+ }
+
+ def positive_lemma_induct(list: List[Int]): Boolean = {
+ list match {
+ case Nil() => positive_lemma(list)
+ case Cons(head, tail) => positive_lemma(list) && positive_lemma_induct(tail)
+ }
+ }.holds
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Lists4.scala b/src/test/resources/regression/verification/newsolvers/valid/Lists4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..02c24111d2a9936ba14764355f7c51d4cfc9e1fa
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Lists4.scala
@@ -0,0 +1,26 @@
+import leon.lang._
+
+object Lists4 {
+ abstract class List[T]
+ case class Cons[T](head: T, tail: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+ def map[F,T](list: List[F], f: F => T): List[T] = list match {
+ case Cons(head, tail) => Cons(f(head), map(tail, f))
+ case Nil() => Nil()
+ }
+
+ def map_lemma[A,B,C](list: List[A], f: A => B, g: B => C): Boolean = {
+ map(list, (x: A) => g(f(x))) == map(map(list, f), g)
+ }
+
+ def map_lemma_induct[D,E,F](list: List[D], f: D => E, g: E => F): Boolean = {
+ list match {
+ case Nil() => map_lemma(list, f, g)
+ case Cons(head, tail) => map_lemma(list, f, g) && map_lemma_induct(tail, f, g)
+ }
+ }.holds
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Lists5.scala b/src/test/resources/regression/verification/newsolvers/valid/Lists5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..51ff810c6bcae4ebcb8bb7273dca57b6e0fe3fdd
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Lists5.scala
@@ -0,0 +1,32 @@
+import leon.lang._
+import leon.collection._
+
+object Lists5 {
+ abstract class Option[T]
+ case class Some[T](value: T) extends Option[T]
+ case class None[T]() extends Option[T]
+
+ def find[T](f: T => Boolean, list: List[T]): Option[T] = list match {
+ case Cons(head, tail) => if (f(head)) Some(head) else find(f, tail)
+ case Nil() => None()
+ }
+
+ def exists[T](f: T => Boolean, list: List[T]): Boolean = list match {
+ case Cons(head, tail) => f(head) || exists(f, tail)
+ case Nil() => false
+ }
+
+ def equivalence_lemma[T](f: T => Boolean, list: List[T]): Boolean = {
+ find(f, list) match {
+ case Some(e) => exists(f, list)
+ case None() => !exists(f, list)
+ }
+ }
+
+ def equivalence_lemma_induct[T](f: T => Boolean, list: List[T]): Boolean = {
+ list match {
+ case Cons(head, tail) => equivalence_lemma(f, list) && equivalence_lemma_induct(f, tail)
+ case Nil() => equivalence_lemma(f, list)
+ }
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Lists6.scala b/src/test/resources/regression/verification/newsolvers/valid/Lists6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f70d523c7f9139cef806bb6549c06c14c057e6d1
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Lists6.scala
@@ -0,0 +1,22 @@
+import leon.lang._
+import leon.collection._
+
+object Lists6 {
+ def exists[T](list: List[T], f: T => Boolean): Boolean = {
+ list match {
+ case Cons(head, tail) => f(head) || exists(tail, f)
+ case Nil() => false
+ }
+ }
+
+ def associative_lemma[T](list: List[T], f: T => Boolean, g: T => Boolean): Boolean = {
+ exists(list, (x: T) => f(x) || g(x)) == (exists(list, f) || exists(list, g))
+ }
+
+ def associative_lemma_induct[T](list: List[T], f: T => Boolean, g: T => Boolean): Boolean = {
+ associative_lemma(list, f, g) && (list match {
+ case Cons(head, tail) => associative_lemma_induct(tail, f, g)
+ case Nil() => true
+ })
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/LiteralMaps.scala b/src/test/resources/regression/verification/newsolvers/valid/LiteralMaps.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d6c07c261fa9b1df57dc153545f2ea66e3e57585
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/LiteralMaps.scala
@@ -0,0 +1,23 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object LiteralMaps {
+ def test(): Map[Int, Int] = {
+ Map(1 -> 2, 3 -> 4, (5, 6))
+ }
+
+ def test2(): (Int, Int) = {
+ 1 -> 2
+ }
+
+ def test3(): Map[Int, Int] = {
+ Map[Int, Int]()
+ }
+
+ def test4(): Map[Int, Int] = {
+ Map.empty[Int, Int]
+ }
+
+ def test5(): Map[Int, Int] = {
+ Map.empty[Int, Int]
+ }
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MergeSort.scala b/src/test/resources/regression/verification/newsolvers/valid/MergeSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..de8b0c32b21cca1d1cbe869fe89dd3fb70d0cece
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/MergeSort.scala
@@ -0,0 +1,122 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+
+object MergeSort {
+ // Data types
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class LList
+ case class LCons(head : List, tail : LList) extends LList
+ case class LNil() extends LList
+
+ def content(list : List) : Set[Int] = list match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def lContent(llist : LList) : Set[Int] = llist match {
+ case LNil() => Set.empty[Int]
+ case LCons(x, xs) => content(x) ++ lContent(xs)
+ }
+
+ def size(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil() => true
+ case Cons(_, Nil()) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def lIsSorted(llist : LList) : Boolean = llist match {
+ case LNil() => true
+ case LCons(x, xs) => isSorted(x) && lIsSorted(xs)
+ }
+
+ def abs(i : BigInt) : BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def mergeSpec(list1 : List, list2 : List, res : List) : Boolean = {
+ isSorted(res) && content(res) == content(list1) ++ content(list2)
+ }
+
+ def mergeFast(list1 : List, list2 : List) : List = {
+ require(isSorted(list1) && isSorted(list2))
+
+ (list1, list2) match {
+ case (_, Nil()) => list1
+ case (Nil(), _) => list2
+ case (Cons(x, xs), Cons(y, ys)) =>
+ if(x <= y) {
+ Cons(x, mergeFast(xs, list2))
+ } else {
+ Cons(y, mergeFast(list1, ys))
+ }
+ }
+ } ensuring(res => mergeSpec(list1, list2, res))
+
+ def splitSpec(list : List, res : (List,List)) : Boolean = {
+ val s1 = size(res._1)
+ val s2 = size(res._2)
+ abs(s1 - s2) <= 1 && s1 + s2 == size(list) &&
+ content(res._1) ++ content(res._2) == content(list)
+ }
+
+ def split(list : List) : (List,List) = (list match {
+ case Nil() => (Nil(), Nil())
+ case Cons(x, Nil()) => (Cons(x, Nil()), Nil())
+ case Cons(x1, Cons(x2, xs)) =>
+ val (s1,s2) = split(xs)
+ (Cons(x1, s1), Cons(x2, s2))
+ }) ensuring(res => splitSpec(list, res))
+
+ def sortSpec(in : List, out : List) : Boolean = {
+ content(out) == content(in) && isSorted(out)
+ }
+
+ // Not really quicksort, neither mergesort.
+ def weirdSort(in : List) : List = (in match {
+ case Nil() => Nil()
+ case Cons(x, Nil()) => Cons(x, Nil())
+ case _ =>
+ val (s1,s2) = split(in)
+ mergeFast(weirdSort(s1), weirdSort(s2))
+ }) ensuring(res => sortSpec(in, res))
+
+ def toLList(list : List) : LList = (list match {
+ case Nil() => LNil()
+ case Cons(x, xs) => LCons(Cons(x, Nil()), toLList(xs))
+ }) ensuring(res => lContent(res) == content(list) && lIsSorted(res))
+
+ def mergeMap(llist : LList) : LList = {
+ require(lIsSorted(llist))
+
+ llist match {
+ case LNil() => LNil()
+ case o @ LCons(x, LNil()) => o
+ case LCons(x, LCons(y, ys)) => LCons(mergeFast(x, y), mergeMap(ys))
+ }
+ } ensuring(res => lContent(res) == lContent(llist) && lIsSorted(res))
+
+ def mergeReduce(llist : LList) : List = {
+ require(lIsSorted(llist))
+
+ llist match {
+ case LNil() => Nil()
+ case LCons(x, LNil()) => x
+ case _ => mergeReduce(mergeMap(llist))
+ }
+ } ensuring(res => content(res) == lContent(llist) && isSorted(res))
+
+ def mergeSort(in : List) : List = {
+ mergeReduce(toLList(in))
+ } ensuring(res => sortSpec(in, res))
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Monads1.scala b/src/test/resources/regression/verification/newsolvers/valid/Monads1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..da9cd6cec6cd3ff2e802beeaabcf8e4b4f20a939
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Monads1.scala
@@ -0,0 +1,24 @@
+import leon.lang._
+
+object Monads1 {
+ abstract class Try[T]
+ case class Success[T](value: T) extends Try[T]
+ case class Failure[T](error: Int) extends Try[T]
+
+ def flatMap[T,U](t: Try[T], f: T => Try[U]): Try[U] = t match {
+ case Success(value) => f(value)
+ case fail @ Failure(error) => Failure(error)
+ }
+
+ def associative_law[T,U,V](t: Try[T], f: T => Try[U], g: U => Try[V]): Boolean = {
+ flatMap(flatMap(t, f), g) == flatMap(t, (x: T) => flatMap(f(x), g))
+ }.holds
+
+ def left_unit_law[T,U](x: T, f: T => Try[U]): Boolean = {
+ flatMap(Success(x), f) == f(x)
+ }.holds
+
+ def right_unit_law[T,U](t: Try[T]): Boolean = {
+ flatMap(t, (x: T) => Success(x)) == t
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Monads2.scala b/src/test/resources/regression/verification/newsolvers/valid/Monads2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f89b2b7f7b71d6b5260bc87b861cd1b3fef9355b
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Monads2.scala
@@ -0,0 +1,47 @@
+import leon.lang._
+
+object Monads2 {
+ abstract class Option[T]
+ case class Some[T](t: T) extends Option[T]
+ case class None[T]() extends Option[T]
+
+ def flatMap[T,U](opt: Option[T], f: T => Option[U]): Option[U] = opt match {
+ case Some(x) => f(x)
+ case None() => None()
+ }
+
+ def add[T](o1: Option[T], o2: Option[T]): Option[T] = o1 match {
+ case Some(x) => o1
+ case None() => o2
+ }
+
+ def associative_law[T,U,V](opt: Option[T], f: T => Option[U], g: U => Option[V]): Boolean = {
+ flatMap(flatMap(opt, f), g) == flatMap(opt, (x: T) => flatMap(f(x), g))
+ }.holds
+
+ def left_unit_law[T,U](x: T, f: T => Option[U]): Boolean = {
+ flatMap(Some(x), f) == f(x)
+ }.holds
+
+ def right_unit_law[T,U](opt: Option[T]): Boolean = {
+ flatMap(opt, (x: T) => Some(x)) == opt
+ }.holds
+
+ def flatMap_zero_law[T,U](none: None[T], f: T => Option[U]): Boolean = {
+ flatMap(none, f) == None[U]()
+ }.holds
+
+ def flatMap_to_zero_law[T,U](opt: Option[T]): Boolean = {
+ flatMap(opt, (x: T) => None[U]()) == None[U]()
+ }.holds
+
+ def add_zero_law[T](opt: Option[T]): Boolean = {
+ add(opt, None[T]()) == opt
+ }.holds
+
+ def zero_add_law[T](opt: Option[T]): Boolean = {
+ add(None[T](), opt) == opt
+ }.holds
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Monads3.scala b/src/test/resources/regression/verification/newsolvers/valid/Monads3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f1c19997078f25545f9c3f05f55186b0db23525b
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Monads3.scala
@@ -0,0 +1,77 @@
+import leon.lang._
+import leon.collection._
+
+object Monads3 {
+
+ def append[T](l1: List[T], l2: List[T]): List[T] = {
+ l1 match {
+ case Cons(head, tail) => Cons(head, append(tail, l2))
+ case Nil() => l2
+ }
+ } ensuring { res => (res == l1) || (l2 != Nil[T]()) }
+
+ def flatMap[T,U](list: List[T], f: T => List[U]): List[U] = list match {
+ case Cons(head, tail) => append(f(head), flatMap(tail, f))
+ case Nil() => Nil()
+ }
+
+ def associative_lemma[T,U,V](list: List[T], f: T => List[U], g: U => List[V]): Boolean = {
+ flatMap(flatMap(list, f), g) == flatMap(list, (x: T) => flatMap(f(x), g))
+ }
+
+ def associative_lemma_induct[T,U,V](list: List[T], flist: List[U], glist: List[V], f: T => List[U], g: U => List[V]): Boolean = {
+ associative_lemma(list, f, g) &&
+ append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) &&
+ (glist match {
+ case Cons(ghead, gtail) =>
+ associative_lemma_induct(list, flist, gtail, f, g)
+ case Nil() => flist match {
+ case Cons(fhead, ftail) =>
+ associative_lemma_induct(list, ftail, g(fhead), f, g)
+ case Nil() => list match {
+ case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
+ case Nil() => true
+ }
+ }
+ })
+ }.holds
+
+ def left_unit_law[T,U](x: T, f: T => List[U]): Boolean = {
+ flatMap(Cons(x, Nil()), f) == f(x)
+ }.holds
+
+ def right_unit_law[T](list: List[T]): Boolean = {
+ flatMap(list, (x: T) => Cons(x, Nil())) == list
+ }
+
+ def right_unit_induct[T,U](list: List[T]): Boolean = {
+ right_unit_law(list) && (list match {
+ case Cons(head, tail) => right_unit_induct(tail)
+ case Nil() => true
+ })
+ }.holds
+
+ def flatMap_zero_law[T,U](f: T => List[U]): Boolean = {
+ flatMap(Nil[T](), f) == Nil[U]()
+ }.holds
+
+ def flatMap_to_zero_law[T](list: List[T]): Boolean = {
+ flatMap(list, (x: T) => Nil[T]()) == Nil[T]()
+ }
+
+ def flatMap_to_zero_induct[T,U](list: List[T]): Boolean = {
+ flatMap_to_zero_law(list) && (list match {
+ case Cons(head, tail) => flatMap_to_zero_induct(tail)
+ case Nil() => true
+ })
+ }.holds
+
+ def add_zero_law[T](list: List[T]): Boolean = {
+ append(list, Nil()) == list
+ }.holds
+
+ def zero_add_law[T](list: List[T]): Boolean = {
+ append(Nil(), list) == list
+ }.holds
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyMap.scala b/src/test/resources/regression/verification/newsolvers/valid/MyMap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..84e9c4967c53609caf9aaeb5584e727a48c788e3
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyMap.scala
@@ -0,0 +1,18 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.lang._
+
+object MyMap {
+
+ def map1(): Int = {
+ val m = Map(1 -> 2, 2 -> 3, 3 -> 4)
+ m(2)
+ } ensuring(_ == 3)
+
+ def map2(): Boolean = {
+ val m1 = Map[Int, Int]()
+ val m2 = Map.empty[Int, Int]
+ m1 == m2
+ }.holds
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MySet.scala b/src/test/resources/regression/verification/newsolvers/valid/MySet.scala
new file mode 100644
index 0000000000000000000000000000000000000000..19b83a93d6e57d33c7dfd9d763b35d51782d2129
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/MySet.scala
@@ -0,0 +1,18 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.lang._
+
+object MySet {
+
+ def set1(): Boolean = {
+ val s = Set(1, 2, 3, 4)
+ s.contains(3)
+ }.holds
+
+ def set2(): Boolean = {
+ val s1 = Set[Int]()
+ val s2 = Set.empty[Int]
+ s1 == s2
+ }.holds
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyTuple1.scala b/src/test/resources/regression/verification/newsolvers/valid/MyTuple1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b7fa2e8c3a0ad1470b568beb399be42995c231f3
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyTuple1.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object MyTuple1 {
+
+ def foo(): Int = {
+ val t = (1, true, 3)
+ val a1 = t._1
+ val a2 = t._2
+ val a3 = t._3
+ a3
+ } ensuring( _ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyTuple2.scala b/src/test/resources/regression/verification/newsolvers/valid/MyTuple2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9117fab370cc56957aba2e3a8587551377f8cb47
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyTuple2.scala
@@ -0,0 +1,16 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object MyTuple2 {
+
+ abstract class A
+ case class B(i: Int) extends A
+ case class C(a: A) extends A
+
+ def foo(): Int = {
+ val t = (B(2), C(B(3)))
+ t match {
+ case (B(x), C(y)) => x
+ }
+ } ensuring(_ == 2)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyTuple3.scala b/src/test/resources/regression/verification/newsolvers/valid/MyTuple3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7bae15f427d498f3ab402536db720682a8f26f06
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyTuple3.scala
@@ -0,0 +1,10 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object MyTuple3 {
+
+ def foo(): Int = {
+ val t = ((2, 3), true)
+ t._1._2
+ } ensuring( _ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyTuple4.scala b/src/test/resources/regression/verification/newsolvers/valid/MyTuple4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..77ba6dc1b141f310eddd1e05d0728b1577950f86
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyTuple4.scala
@@ -0,0 +1,16 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+
+object MyTuple4 {
+
+ abstract class A
+ case class B(i: Int) extends A
+ case class C(a: A) extends A
+
+ def foo(): Int = {
+ val t = (1, (C(B(4)), 2), 3)
+ val (a1, (C(B(x)), a2), a3) = t
+ x
+ } ensuring( _ == 4)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyTuple5.scala b/src/test/resources/regression/verification/newsolvers/valid/MyTuple5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a427c410debc8c87f89377bf404ac3d43d8b1a92
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyTuple5.scala
@@ -0,0 +1,18 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object MyTuple5 {
+
+ abstract class A
+ case class B(t: (Int, Int)) extends A
+ case class C(a: A) extends A
+
+ def foo(): Int = {
+ val t: (Int, (A, Int), Int) = (1, (C(B((4, 5))), 2), 3)
+ t match {
+ case (_, (B((x, y)), _), _) => x
+ case (_, (C(B((_, x))), _), y) => x
+ case (_, _, x) => x
+ }
+ } ensuring( _ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyTuple6.scala b/src/test/resources/regression/verification/newsolvers/valid/MyTuple6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..85287265240ccd8d383912eb2f70d43ad16d4aa7
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyTuple6.scala
@@ -0,0 +1,10 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object MyTuple6 {
+
+ def foo(t: (Int, Int)): (Int, Int) = {
+ require(t._1 > 0 && t._2 > 1)
+ t
+ } ensuring(res => res._1 > 0 && res._2 > 1)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Nat.scala b/src/test/resources/regression/verification/newsolvers/valid/Nat.scala
new file mode 100644
index 0000000000000000000000000000000000000000..eb7fe27c56595bfb442644e8f258305fafbc4bf2
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Nat.scala
@@ -0,0 +1,26 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+
+object Nat {
+ sealed abstract class Nat
+ case class Zero() extends Nat
+ case class Succ(num: Nat) extends Nat
+
+ def plus(a: Nat, b: Nat): Nat = a match {
+ case Zero() => b
+ case Succ(a1) => Succ(plus(a1, b))
+ }
+
+ def nat2Int(n: Nat): Int = n match {
+ case Zero() => 0
+ case Succ(n1) => 1 + nat2Int(n1)
+ }
+
+ def int2Nat(n: Int): Nat = if (n == 0) Zero() else Succ(int2Nat(n-1))
+
+ def sum_lemma(): Boolean = {
+ 3 == nat2Int(plus(int2Nat(1), int2Nat(2)))
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/NotEquals.scala b/src/test/resources/regression/verification/newsolvers/valid/NotEquals.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f33e1bb5dd509a02e68eaf30d2164d5e5920e3c0
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/NotEquals.scala
@@ -0,0 +1,20 @@
+import leon.annotation._
+import leon.lang._
+
+object NotEquals {
+
+ // Represents n/d
+ case class Q(n: BigInt, d: BigInt)
+
+ def op(a: Q, b: Q) = {
+ require(isRational(a) && isRational(b))
+
+ Q(a.n + b.n, a.d)
+ } ensuring {
+ isRational(_)
+ }
+
+ //def isRational(a: Q) = a.d != 0
+ def isRational(a: Q) = a.d != 0
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/ParBalance.scala b/src/test/resources/regression/verification/newsolvers/valid/ParBalance.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6943d3268a97ebadb5e2b49619ce119478d56c65
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/ParBalance.scala
@@ -0,0 +1,206 @@
+import leon._
+import leon.lang._
+
+object ParBalance {
+
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class Option
+ case class Some(x: BigInt) extends Option
+ case class None() extends Option
+
+ val openPar : BigInt = BigInt(1)
+ val closePar : BigInt = BigInt(2)
+
+ def balanced(list: List, counter: BigInt): Boolean = {
+ if (counter < 0) false else list match {
+ case Cons(head, tail) =>
+ val c = if (head == openPar) counter + 1
+ else if (head == closePar) counter - 1
+ else counter
+ balanced(tail, c)
+ case Nil() => counter == 0
+ }
+ }
+
+ def balanced_nonEarly(list: List, counter: BigInt): Boolean = {
+ list match {
+ case Cons(head, tail) =>
+ if (counter < 0) balanced_nonEarly(tail, counter) else {
+ val c = if (head == openPar) counter + 1
+ else if (head == closePar) counter - 1
+ else counter
+ balanced_nonEarly(tail, c)
+ }
+ case Nil() => counter == 0
+ }
+ } ensuring { res => res == balanced(list, counter) }
+
+ def balanced_withFailure(list: List, counter: BigInt, failed: Boolean): Boolean = {
+ require(counter >= 0 || failed)
+ list match {
+ case Cons(head, tail) =>
+ val c = if (head == openPar) counter + 1
+ else if (head == closePar) counter - 1
+ else counter
+ balanced_withFailure(tail, c, failed || c < 0)
+ case Nil() => !failed && counter == 0
+ }
+ } ensuring { res =>
+ if (failed) {
+ res == balanced_nonEarly(list, -1)
+ } else {
+ res == balanced_nonEarly(list, counter)
+ }
+ }
+
+ def balanced_withReduce(list: List, p: (BigInt, BigInt)): Boolean = {
+ require(p._1 >= 0 && p._2 >= 0)
+ list match {
+ case Cons(head, tail) =>
+ val p2 = reduce(p, parPair(head))
+ balanced_withReduce(tail, p2)
+ case Nil() =>
+ p._1 == 0 && p._2 == 0
+ }
+ } ensuring { res => res == balanced_withFailure(list, p._1 - p._2, p._2 > 0) }
+
+ def balanced_foldLeft_equivalence(list: List, p: (BigInt, BigInt)): Boolean = {
+ require(p._1 >= 0 && p._2 >= 0)
+ val f = (s: (BigInt, BigInt), x: BigInt) => reduce(s, parPair(x))
+ (foldLeft(list, p, f) == (BigInt(0), BigInt(0))) == balanced_withReduce(list, p) && (list match {
+ case Cons(head, tail) =>
+ val p2 = f(p, head)
+ balanced_foldLeft_equivalence(tail, p2)
+ case Nil() => true
+ })
+ }.holds
+
+ def foldRight[A](list: List, state: A, f: (BigInt, A) => A): A = list match {
+ case Cons(head, tail) =>
+ val tailState = foldRight(tail, state, f)
+ f(head, tailState)
+ case Nil() => state
+ }
+
+ def foldLeft[A](list: List, state: A, f: (A, BigInt) => A): A = list match {
+ case Cons(head, tail) =>
+ val nextState = f(state, head)
+ foldLeft(tail, nextState, f)
+ case Nil() => state
+ }
+
+ def reduce(p1: (BigInt, BigInt), p2: (BigInt, BigInt)): (BigInt, BigInt) = {
+ if (p1._1 >= p2._2) {
+ (p1._1 - p2._2 + p2._1, p1._2)
+ } else {
+ (p2._1, p2._2 - p1._1 + p1._2)
+ }
+ }
+
+ def reduce_associative(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+ reduce(p1, reduce(p2, p3)) == reduce(reduce(p1, p2), p3)
+ }.holds
+
+ def swap(p: (BigInt, BigInt)): (BigInt, BigInt) = (p._2, p._1)
+
+ def reduce_inverse(p1: (BigInt, BigInt), p2: (BigInt, BigInt)): Boolean = {
+ reduce(p1, p2) == swap(reduce(swap(p2), swap(p1)))
+ }.holds
+
+ def reduce_associative_inverse(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+ reduce(p1, reduce(p2, p3)) == swap(reduce(reduce(swap(p3), swap(p2)), swap(p1)))
+ }.holds
+
+ def reduce_associative_inverse2(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+ reduce(reduce(p1, p2), p3) == swap(reduce(swap(p3), reduce(swap(p2), swap(p1))))
+ }.holds
+
+ def parPair(x: BigInt): (BigInt, BigInt) = {
+ if (x == openPar) (1, 0) else if (x == closePar) (0, 1) else (0, 0)
+ }
+
+ def headOption(list: List): Option = list match {
+ case Cons(head, tail) => Some(head)
+ case Nil() => None()
+ }
+
+ def lastOption(list: List): Option = list match {
+ case Cons(head, Nil()) => Some(head)
+ case Cons(head, tail) => lastOption(tail)
+ case Nil() => None()
+ }
+
+ def init(list: List): List = list match {
+ case Cons(head, Nil()) => Nil()
+ case Cons(head, tail) => Cons(head, init(tail))
+ case Nil() => Nil()
+ }
+
+ def tail(list: List): List = list match {
+ case Cons(head, tail) => tail
+ case Nil() => Nil()
+ }
+
+ def addLast(list: List, x: BigInt): List = {
+ list match {
+ case Cons(head, tail) => Cons(head, addLast(tail, x))
+ case Nil() => Cons(x, Nil())
+ }
+ } ensuring { res => lastOption(res) == Some(x) && init(res) == list }
+
+ def reverse(list: List): List = {
+ list match {
+ case Cons(head, tail) => addLast(reverse(tail), head)
+ case Nil() => Nil()
+ }
+ } ensuring { res =>
+ lastOption(res) == headOption(list) &&
+ lastOption(list) == headOption(res)
+ }
+
+ def reverse_tail_equivalence(list: List): Boolean = {
+ reverse(tail(list)) == init(reverse(list))
+ }.holds
+
+ def reverse_init_equivalence(list: List): Boolean = {
+ reverse(init(list)) == tail(reverse(list)) && (list match {
+ case Cons(head, tail) => reverse_init_equivalence(tail)
+ case Nil() => true
+ })
+ }.holds
+
+ def reverse_equality_equivalence(l1: List, l2: List): Boolean = {
+ (l1 == l2) == (reverse(l1) == reverse(l2)) && ((l1, l2) match {
+ case (Cons(h1, t1), Cons(h2, t2)) => reverse_equality_equivalence(t1, t2)
+ case _ => true
+ })
+ }.holds
+
+ def reverse_reverse_equivalence(list: List): Boolean = {
+ reverse(reverse(list)) == list && ((list, reverse(list)) match {
+ case (Cons(h1, t1), Cons(h2, t2)) =>
+ reverse_reverse_equivalence(t1) && reverse_reverse_equivalence(t2)
+ case _ => true
+ })
+ }.holds
+
+ /*
+ def fold_equivalence(list: List): Boolean = {
+ val s = (0, 0)
+ val fl = (s: (BigInt, BigInt), x: BigInt) => reduce(s, parPair(x))
+ val fr = (x: BigInt, s: (BigInt, BigInt)) => reduce(parPair(x), s)
+
+ foldLeft(list, s, fl) == foldRight(list, s, fr)
+ }.holds
+
+ def lemma(list: List): Boolean = {
+ val f = (x: BigInt, s: (BigInt, BigInt)) => reduce(parPair(x), s)
+ fold_equivalence(list) && balanced_foldLeft_equivalence(list, (0, 0)) &&
+ (foldRight(list, (0, 0), f) == (0, 0)) == balanced(list, 0)
+ }.holds
+ */
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/PositiveMap.scala b/src/test/resources/regression/verification/newsolvers/valid/PositiveMap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0441ec26ca74f98dec17e05e91e487f0756b78ad
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/PositiveMap.scala
@@ -0,0 +1,36 @@
+import leon.lang._
+
+object PositiveMap {
+
+ abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ def positive(list: List): Boolean = list match {
+ case Cons(head, tail) => if (head < 0) false else positive(tail)
+ case Nil() => true
+ }
+
+ def positiveMap_passing_1(f: (BigInt) => BigInt, list: List): List = {
+ list match {
+ case Cons(head, tail) =>
+ val fh = f(head)
+ val nh = if (fh <= 0) -fh else fh
+ Cons(nh, positiveMap_passing_1(f, tail))
+ case Nil() => Nil()
+ }
+ } ensuring { res => positive(res) }
+
+ def positiveMap_passing_2(f: (BigInt) => BigInt, list: List): List = {
+ list match {
+ case Cons(head, tail) =>
+ val fh = f(head)
+ val nh = if (fh < 0) -fh else fh
+ Cons(nh, positiveMap_passing_2(f, tail))
+ case Nil() => Nil()
+ }
+ } ensuring { res => positive(res) }
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/newsolvers/valid/PropositionalLogic.scala b/src/test/resources/regression/verification/newsolvers/valid/PropositionalLogic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a41dab8262f9910662a994b0d6def78bf1bac5c7
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/PropositionalLogic.scala
@@ -0,0 +1,77 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import scala.collection.immutable.Set
+import leon.lang._
+import leon.annotation._
+
+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 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 Literal(_) => f
+ }) ensuring(isSimplified(_))
+
+ def isSimplified(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Implies(_,_) => false
+ case Not(f) => isSimplified(f)
+ case Literal(_) => true
+ }
+
+ 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
+ }) ensuring(isNNF(_))
+
+ def isNNF(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Implies(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Not(Literal(_)) => true
+ case Not(_) => false
+ case Literal(_) => true
+ }
+
+ 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)
+ }
+ }
+
+ def fv(f : Formula) = { vars(nnf(f)) }
+
+ @induct
+ def nnfIsStable(f: Formula) : Boolean = {
+ require(isNNF(f))
+ nnf(f) == f
+ }.holds
+
+ @induct
+ def simplifyIsStable(f: Formula) : Boolean = {
+ require(isSimplified(f))
+ simplify(f) == f
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/README b/src/test/resources/regression/verification/newsolvers/valid/README
new file mode 100644
index 0000000000000000000000000000000000000000..2bb01d5fdbd6b59970c0c84f2c10db1ead6097a2
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/README
@@ -0,0 +1,2 @@
+This particular directory contains PureScala programs that can be entirely
+proved correct by Leon.
diff --git a/src/test/resources/regression/verification/newsolvers/valid/RedBlackTree.scala b/src/test/resources/regression/verification/newsolvers/valid/RedBlackTree.scala
new file mode 100644
index 0000000000000000000000000000000000000000..841befb415c77e3609b9ad7bf28a1e760d3ce39f
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/RedBlackTree.scala
@@ -0,0 +1,100 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import scala.collection.immutable.Set
+import leon.annotation._
+import leon.lang._
+
+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: BigInt, right: Tree) extends Tree
+
+ sealed abstract class OptionInt
+ case class Some(v : BigInt) extends OptionInt
+ case class None() extends OptionInt
+
+ def content(t: Tree) : Set[BigInt] = t match {
+ case Empty() => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : BigInt = (t match {
+ case Empty() => BigInt(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) : BigInt = 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: BigInt, 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: BigInt, 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 balance(c: Color, a: Tree, x: BigInt, 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/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala b/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bd0596fbaab48f4a64309e71d019db53ed72db2a
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala
@@ -0,0 +1,50 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import scala.collection.immutable.Set
+import leon.lang._
+import leon.annotation._
+
+object SearchLinkedList {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ def size(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contains(list : List, elem : Int) : Boolean = (list match {
+ case Nil() => false
+ case Cons(x, xs) => x == elem || contains(xs, elem)
+ })
+
+ def firstZero(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
+ case Cons(x, xs) => if (x == 0) BigInt(0) else firstZero(xs) + 1
+ }) ensuring (res =>
+ res >= 0 && (if (contains(list, 0)) {
+ firstZeroAtPos(list, res)
+ } else {
+ res == size(list)
+ }))
+
+ def firstZeroAtPos(list : List, pos : BigInt) : Boolean = {
+ list match {
+ case Nil() => false
+ case Cons(x, xs) => if (pos == BigInt(0)) x == 0 else x != 0 && firstZeroAtPos(xs, pos - 1)
+ }
+ }
+
+ def goal(list : List, i : BigInt) : Boolean = {
+ if(firstZero(list) == i) {
+ if(contains(list, 0)) {
+ firstZeroAtPos(list, i)
+ } else {
+ i == size(list)
+ }
+ } else {
+ true
+ }
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Sets1.scala b/src/test/resources/regression/verification/newsolvers/valid/Sets1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4cfca4890810e544407f2200aaae8ab4ca5381ec
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Sets1.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object Sets1 {
+ def set(i: Int): Int => Boolean = x => x == i
+
+ def complement(s: Int => Boolean): Int => Boolean = x => !s(x)
+
+ def union(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) || s2(x)
+
+ def intersection(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && s2(x)
+
+ def de_morgan_1(s1: Int => Boolean, s2: Int => Boolean, x: Int): Boolean = {
+ val u1 = union(s1, s2)
+ val u2 = complement(intersection(complement(s1), complement(s2)))
+ u1(x) == u2(x)
+ }.holds
+
+ def de_morgan_2(s1: Int => Boolean, s2: Int => Boolean, x: Int): Boolean = {
+ val u1 = intersection(s1, s2)
+ val u2 = complement(union(complement(s1), complement(s2)))
+ u1(x) == u2(x)
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Sets2.scala b/src/test/resources/regression/verification/newsolvers/valid/Sets2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..244f5bebff8032d4fe685be216ee48a1533faab5
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Sets2.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object Sets2 {
+ def set(i: Int): Int => Boolean = x => x == i
+
+ def complement(s: Int => Boolean): Int => Boolean = x => !s(x)
+
+ def union(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) || s2(x)
+
+ def intersection(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && s2(x)
+
+ def union_associativity(sa1: Int => Boolean, sa2: Int => Boolean, sa3: Int => Boolean, x: Int): Boolean = {
+ val u1 = union(union(sa1, sa2), sa3)
+ val u2 = union(sa1, union(sa2, sa3))
+ u1(x) == u2(x)
+ }.holds
+
+ def intersection_associativity(sa1: Int => Boolean, sa2: Int => Boolean, sa3: Int => Boolean, x: Int): Boolean = {
+ val u1 = intersection(intersection(sa1, sa2), sa3)
+ val u2 = intersection(sa1, intersection(sa2, sa3))
+ u1(x) == u2(x)
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Subtyping1.scala b/src/test/resources/regression/verification/newsolvers/valid/Subtyping1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4352d070fbb5fba8f76348bb2f2bc53452288fe5
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Subtyping1.scala
@@ -0,0 +1,33 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object Subtyping1 {
+
+ sealed abstract class Tree
+ case class Leaf() extends Tree
+ case class Node(left: Tree, value: Int, right: Tree) extends Tree
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Leaf() => Set.empty
+ case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def treeMax(tree: Node): Int = {
+ tree match {
+ case Node(_, v, right) => right match {
+ case Leaf() => v
+ case Node(l, v, r) => treeMax(Node(l, v, r))
+ }
+ }
+ } ensuring(content(tree).contains(_))
+
+ def f2(tree: Node): Int = {
+ require(treeMax(tree) > 0)
+ tree match {
+ case Node(_, v, right) => right match {
+ case Leaf() => v
+ case Node(l, v, r) => treeMax(Node(l, v, r))
+ }
+ }
+ } ensuring(content(tree).contains(_))
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Subtyping2.scala b/src/test/resources/regression/verification/newsolvers/valid/Subtyping2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bc96d0617a8bf2361e16c35316a15c8895eb71a2
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Subtyping2.scala
@@ -0,0 +1,23 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.lang._
+
+object Subtyping2 {
+
+ abstract class List
+ case class Nil() extends List
+ case class Cons(head: Int, tail: List) extends List
+
+ def test(x: List): Nil = {
+ x match {
+ case Cons(_, tail) => test(tail)
+ case Nil() => Nil()
+ }
+ } ensuring((res: Nil) => isEmpty(res))
+
+ def isEmpty(x: List): Boolean = x match {
+ case Nil() => true
+ case _ => false
+ }
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Trees1.scala b/src/test/resources/regression/verification/newsolvers/valid/Trees1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4c01ae06ef89aeed1e13a4c2baf63df776607322
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Trees1.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object Trees1 {
+ abstract class Tree[T]
+ case class Node[T](left: Tree[T], right: Tree[T]) extends Tree[T]
+ case class Leaf[T](value: T) extends Tree[T]
+
+ def map[T,U](tree: Tree[T], f: T => U): Tree[U] = tree match {
+ case Node(left, right) => Node(map(left, f), map(right, f))
+ case Leaf(value) => Leaf(f(value))
+ }
+
+ def associative_lemma[T,U,V](tree: Tree[T], f: T => U, g: U => V): Boolean = {
+ map(map(tree, f), g) == map(tree, (x: T) => g(f(x)))
+ }
+
+ def associative_lemma_induct[T,U,V](tree: Tree[T], f: T => U, g: U => V): Boolean = {
+ tree match {
+ case Node(left, right) => associative_lemma_induct(left, f, g) && associative_lemma_induct(right, f, g) && associative_lemma(tree, f, g)
+ case Leaf(value) => associative_lemma(tree, f, g)
+ }
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Unit1.scala b/src/test/resources/regression/verification/newsolvers/valid/Unit1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e1456aaa651ac72ce9211948880a56c170ac151c
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Unit1.scala
@@ -0,0 +1,9 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object Unit1 {
+
+ def foo(): Unit = ({
+ ()
+ }) ensuring(r => true)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Unit2.scala b/src/test/resources/regression/verification/newsolvers/valid/Unit2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f71ea0ff5e80be50f001d3ff41f9ddfccbd4f147
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/valid/Unit2.scala
@@ -0,0 +1,9 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object Unit2 {
+
+ def foo(u: Unit): Unit = {
+ u
+ } ensuring(res => true)
+
+}
diff --git a/src/test/scala/leon/test/verification/NewSolversRegression.scala b/src/test/scala/leon/test/verification/NewSolversRegression.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e882900023c2d72cef5bbac04c9cba0b6c045cba
--- /dev/null
+++ b/src/test/scala/leon/test/verification/NewSolversRegression.scala
@@ -0,0 +1,46 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.test.verification
+
+import _root_.smtlib.interpreters._
+import leon._
+import leon.verification.AnalysisPhase
+
+// If you add another regression test, make sure it contains one object whose name matches the file name
+// This is because we compile all tests from each folder separately.
+class NewSolversRegression extends VerificationRegression {
+
+ val testDir = "regression/verification/newsolvers/"
+ val pipeFront = xlang.NoXLangFeaturesChecking
+ val pipeBack = AnalysisPhase
+ val optionVariants: List[List[String]] = {
+ val isZ3Available = try {
+ new Z3Interpreter()
+ true
+ } catch {
+ case e: java.io.IOException =>
+ false
+ }
+
+ val isCVC4Available = try {
+ new CVC4Interpreter()
+ true
+ } catch {
+ case e: java.io.IOException =>
+ false
+ }
+
+ (
+ if (isZ3Available)
+ List(List("--solvers=smt-z3-quantified", "--feelinglucky"))
+ else Nil
+ ) ++ (
+ if (isCVC4Available)
+ List(List("--solvers=smt-2.5-cvc4", "--feelinglucky"))
+ else Nil
+ )
+ }
+
+ test()
+
+}
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 2c4d00fefd5cc4cad1d689b233b2ce75d3ec2688..2041322191909b59e49fd4aca0c061de492fdec8 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -37,33 +37,15 @@ class PureScalaVerificationRegression extends VerificationRegression {
List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky")
) ++ (
if (isZ3Available) List(
- List("--solvers=smt-z3", "--feelinglucky"),
- List("--solvers=smt-z3-quantified", "--feelinglucky")
+ List("--solvers=smt-z3", "--feelinglucky")
) else Nil
) ++ (
if (isCVC4Available) List(
- List("--solvers=smt-cvc4", "--feelinglucky"),
- List("--solvers=smt-2.5-cvc4", "--feelinglucky")
+ List("--solvers=smt-cvc4", "--feelinglucky")
) else Nil
)
}
-
- forEachFileIn("valid") { output =>
- val Output(report, reporter) = output
- for ((vc, vr) <- report.vrs) {
- if (!vr.isValid) {
- fail("The following verification condition was invalid: " + vc.toString + " @" + vc.getPos)
- }
- }
- reporter.terminateIfError()
- }
- forEachFileIn("invalid") { output =>
- val Output(report, reporter) = output
- assert(report.totalInvalid > 0,
- "There should be at least one invalid verification condition.")
- assert(report.totalUnknown === 0,
- "There should not be unknown verification conditions.")
- }
+ test()
}
diff --git a/src/test/scala/leon/test/verification/VerificationRegression.scala b/src/test/scala/leon/test/verification/VerificationRegression.scala
index 286fa774d6a178ed414925c4ebe23a1723538d13..2cd355a6601548914e102cfa23fc4cb686820a01 100644
--- a/src/test/scala/leon/test/verification/VerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/VerificationRegression.scala
@@ -63,6 +63,24 @@ trait VerificationRegression extends LeonTestSuite {
mkTest(files)(block)
}
-
-
+
+ def test() = {
+ forEachFileIn("valid") { output =>
+ val Output(report, reporter) = output
+ for ((vc, vr) <- report.vrs) {
+ if (!vr.isValid) {
+ fail("The following verification condition was invalid: " + vc.toString + " @" + vc.getPos)
+ }
+ }
+ reporter.terminateIfError()
+ }
+
+ forEachFileIn("invalid") { output =>
+ val Output(report, reporter) = output
+ assert(report.totalInvalid > 0,
+ "There should be at least one invalid verification condition.")
+ assert(report.totalUnknown === 0,
+ "There should not be unknown verification conditions.")
+ }
+ }
}