From 915ebc6f18754f703a01d18c2e144cf64d6d7fec Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 30 Mar 2015 16:22:23 +0200
Subject: [PATCH] Remove unhandled tests for now
---
.../newsolvers/valid/Anonymous.scala | 9 -
.../newsolvers/valid/Closures.scala | 15 --
.../newsolvers/valid/Closures2.scala | 35 ---
.../newsolvers/valid/FlatMap.scala | 48 ----
.../newsolvers/valid/FoldAssociative.scala | 101 ---------
.../newsolvers/valid/HOInvocations.scala | 17 --
.../newsolvers/valid/Lambdas.scala | 15 --
.../newsolvers/valid/Lists1.scala | 30 ---
.../newsolvers/valid/Lists2.scala | 49 -----
.../newsolvers/valid/Lists3.scala | 34 ---
.../newsolvers/valid/Lists4.scala | 26 ---
.../newsolvers/valid/Lists5.scala | 32 ---
.../newsolvers/valid/Lists6.scala | 22 --
.../newsolvers/valid/Monads1.scala | 24 --
.../newsolvers/valid/Monads2.scala | 47 ----
.../newsolvers/valid/Monads3.scala | 77 -------
.../newsolvers/valid/ParBalance.scala | 206 ------------------
.../verification/newsolvers/valid/Sets1.scala | 23 --
.../verification/newsolvers/valid/Sets2.scala | 23 --
.../newsolvers/valid/Trees1.scala | 23 --
20 files changed, 856 deletions(-)
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Anonymous.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Closures.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Closures2.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/FlatMap.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/FoldAssociative.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/HOInvocations.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Lambdas.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Lists1.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Lists2.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Lists3.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Lists4.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Lists5.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Lists6.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Monads1.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Monads2.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Monads3.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/ParBalance.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Sets1.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Sets2.scala
delete mode 100644 src/test/resources/regression/verification/newsolvers/valid/Trees1.scala
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Anonymous.scala b/src/test/resources/regression/verification/newsolvers/valid/Anonymous.scala
deleted file mode 100644
index d69b1f842..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Anonymous.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-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/Closures.scala b/src/test/resources/regression/verification/newsolvers/valid/Closures.scala
deleted file mode 100644
index 5e191cf81..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Closures.scala
+++ /dev/null
@@ -1,15 +0,0 @@
-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
deleted file mode 100644
index b791965d1..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Closures2.scala
+++ /dev/null
@@ -1,35 +0,0 @@
-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/FlatMap.scala b/src/test/resources/regression/verification/newsolvers/valid/FlatMap.scala
deleted file mode 100644
index 56f8c47e8..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/FlatMap.scala
+++ /dev/null
@@ -1,48 +0,0 @@
-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
deleted file mode 100644
index 261d15c0f..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/FoldAssociative.scala
+++ /dev/null
@@ -1,101 +0,0 @@
-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/HOInvocations.scala b/src/test/resources/regression/verification/newsolvers/valid/HOInvocations.scala
deleted file mode 100644
index 0f2fbda2f..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/HOInvocations.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-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/Lambdas.scala b/src/test/resources/regression/verification/newsolvers/valid/Lambdas.scala
deleted file mode 100644
index 36ae0c7ad..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Lambdas.scala
+++ /dev/null
@@ -1,15 +0,0 @@
-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/Lists1.scala b/src/test/resources/regression/verification/newsolvers/valid/Lists1.scala
deleted file mode 100644
index 719c3d236..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Lists1.scala
+++ /dev/null
@@ -1,30 +0,0 @@
-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
deleted file mode 100644
index 654046ba0..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Lists2.scala
+++ /dev/null
@@ -1,49 +0,0 @@
-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
deleted file mode 100644
index 67060133a..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Lists3.scala
+++ /dev/null
@@ -1,34 +0,0 @@
-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
deleted file mode 100644
index 02c24111d..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Lists4.scala
+++ /dev/null
@@ -1,26 +0,0 @@
-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
deleted file mode 100644
index 51ff810c6..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Lists5.scala
+++ /dev/null
@@ -1,32 +0,0 @@
-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
deleted file mode 100644
index f70d523c7..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Lists6.scala
+++ /dev/null
@@ -1,22 +0,0 @@
-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/Monads1.scala b/src/test/resources/regression/verification/newsolvers/valid/Monads1.scala
deleted file mode 100644
index da9cd6cec..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Monads1.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-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
deleted file mode 100644
index f89b2b7f7..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Monads2.scala
+++ /dev/null
@@ -1,47 +0,0 @@
-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
deleted file mode 100644
index f1c199970..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Monads3.scala
+++ /dev/null
@@ -1,77 +0,0 @@
-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/ParBalance.scala b/src/test/resources/regression/verification/newsolvers/valid/ParBalance.scala
deleted file mode 100644
index 6943d3268..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/ParBalance.scala
+++ /dev/null
@@ -1,206 +0,0 @@
-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/Sets1.scala b/src/test/resources/regression/verification/newsolvers/valid/Sets1.scala
deleted file mode 100644
index 4cfca4890..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Sets1.scala
+++ /dev/null
@@ -1,23 +0,0 @@
-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
deleted file mode 100644
index 244f5bebf..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Sets2.scala
+++ /dev/null
@@ -1,23 +0,0 @@
-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/Trees1.scala b/src/test/resources/regression/verification/newsolvers/valid/Trees1.scala
deleted file mode 100644
index 4c01ae06e..000000000
--- a/src/test/resources/regression/verification/newsolvers/valid/Trees1.scala
+++ /dev/null
@@ -1,23 +0,0 @@
-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
-}
--
GitLab