diff --git a/src/main/scala/leon/purescala/Quantification.scala b/src/main/scala/leon/purescala/Quantification.scala
index 297ee1fc95105dc55509aaf74439b3640c0c4ca9..21608b0facdb2d2318320a0e58974d23f56dc491 100644
--- a/src/main/scala/leon/purescala/Quantification.scala
+++ b/src/main/scala/leon/purescala/Quantification.scala
@@ -87,7 +87,7 @@ object Quantification {
object QuantificationMatcher {
private def flatApplication(expr: Expr): Option[(Expr, Seq[Expr])] = expr match {
- case Application(fi: FunctionInvocation, args) => Some((fi, args))
+ case Application(fi: FunctionInvocation, args) => None
case Application(caller: Application, args) => flatApplication(caller) match {
case Some((c, prevArgs)) => Some((c, prevArgs ++ args))
case None => None
diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index 362629388e533bcca567cd826fea9ea84e007b7c..a63fdd7a6e06d7ea9cc0b9d8b7ac1f0b89219bab 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -99,7 +99,7 @@ trait KeyedTemplate[T, E <: Expr] {
case _ => Seq.empty
}
- structure -> rec(structure).distinct.map(dependencies)
+ structure -> rec(structure).map(dependencies)
}
}
@@ -210,7 +210,7 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends DatatypeManager(enco
override protected def incrementals: List[IncrementalState] =
super.incrementals ++ List(byID, byType, applications, knownFree, maybeFree, freeBlockers, instantiated)
- def registerFunction(b: T, tpe: FunctionType, f: T): Seq[T] = {
+ def registerFunction(b: T, tpe: FunctionType, f: T): Instantiation[T] = {
val ft = bestRealType(tpe).asInstanceOf[FunctionType]
val bs = fixpoint((bs: Set[T]) => bs ++ bs.flatMap(blockerParents))(Set(b))
@@ -231,7 +231,13 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends DatatypeManager(enco
encoder.mkEquals(oldB, extension)
}
- neqClauses ++ extClauses
+ val instantiation = Instantiation.empty[T] withClauses (neqClauses ++ extClauses)
+
+ applications(tpe).foldLeft(instantiation) {
+ case (instantiation, (app @ (_, App(caller, _, args, _)))) =>
+ val equals = encoder.mkAnd(b, encoder.mkEquals(f, caller))
+ instantiation withApp (app -> TemplateAppInfo(f, equals, args))
+ }
}
def assumptions: Seq[T] = freeBlockers.toSeq.flatMap(_._2.map(p => encoder.mkNot(p._1)))
@@ -282,24 +288,24 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends DatatypeManager(enco
val idT = encoder.encodeId(template.ids._1)
val newTemplate = template.withId(idT)
- var clauses : Clauses[T] = equalityClauses(newTemplate)
- var appBlockers : AppBlockers[T] = Map.empty.withDefaultValue(Set.empty)
-
// make sure the new lambda isn't equal to any free lambda var
- clauses ++= knownFree(newTemplate.tpe).map(f => encoder.mkNot(encoder.mkEquals(idT, f)))
- clauses ++= maybeFree(newTemplate.tpe).map { p =>
- encoder.mkImplies(p._1, encoder.mkNot(encoder.mkEquals(idT, p._2)))
- }
+ val instantiation = Instantiation.empty[T] withClauses (
+ equalityClauses(newTemplate) ++
+ knownFree(newTemplate.tpe).map(f => encoder.mkNot(encoder.mkEquals(idT, f))).toSeq ++
+ maybeFree(newTemplate.tpe).map { p =>
+ encoder.mkImplies(p._1, encoder.mkNot(encoder.mkEquals(idT, p._2)))
+ })
byID += idT -> newTemplate
byType += newTemplate.tpe -> (byType(newTemplate.tpe) + (newTemplate.key -> newTemplate))
- for (blockedApp @ (_, App(caller, tpe, args, _)) <- applications(newTemplate.tpe)) {
- val equals = encoder.mkEquals(idT, caller)
- appBlockers += (blockedApp -> (appBlockers(blockedApp) + TemplateAppInfo(newTemplate, equals, args)))
+ val inst = applications(newTemplate.tpe).foldLeft(instantiation) {
+ case (instantiation, app @ (_, App(caller, _, args, _))) =>
+ val equals = encoder.mkEquals(idT, caller)
+ instantiation withApp (app -> TemplateAppInfo(newTemplate, equals, args))
}
- (idT, (clauses, Map.empty, appBlockers))
+ (idT, inst)
}
}
@@ -312,29 +318,30 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends DatatypeManager(enco
typeUnroller(blocker, app)
}
- if (knownFree(tpe) contains caller) instantiation else {
- val key = blocker -> app
-
- if (instantiated(key)) instantiation else {
- instantiated += key
+ val key = blocker -> app
+ if (instantiated(key)) {
+ instantiation
+ } else {
+ instantiated += key
- if (byID contains caller) {
- empty withApp (key -> TemplateAppInfo(byID(caller), trueT, args))
- } else {
+ if (knownFree(tpe) contains caller) {
+ instantiation withApp (key -> TemplateAppInfo(caller, trueT, args))
+ } else if (byID contains caller) {
+ instantiation withApp (key -> TemplateAppInfo(byID(caller), trueT, args))
+ } else {
- // make sure that even if byType(tpe) is empty, app is recorded in blockers
- // so that UnrollingBank will generate the initial block!
- val init = instantiation withApps Map(key -> Set.empty)
- val inst = byType(tpe).values.foldLeft(init) {
- case (instantiation, template) =>
- val equals = encoder.mkEquals(template.ids._2, caller)
- instantiation withApp (key -> TemplateAppInfo(template, equals, args))
- }
+ // make sure that even if byType(tpe) is empty, app is recorded in blockers
+ // so that UnrollingBank will generate the initial block!
+ val init = instantiation withApps Map(key -> Set.empty)
+ val inst = byType(tpe).values.foldLeft(init) {
+ case (instantiation, template) =>
+ val equals = encoder.mkEquals(template.ids._2, caller)
+ instantiation withApp (key -> TemplateAppInfo(template, equals, args))
+ }
- applications += tpe -> (applications(tpe) + key)
+ applications += tpe -> (applications(tpe) + key)
- inst
- }
+ inst
}
}
}
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index 3b7d97a4ff28f5468a02566cbc196cfea54b7404..85a2add2721a8b03cb3399bdbc73d796d74853e4 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -236,7 +236,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
def +(p: (Set[T], Matcher[T])): Context = if (apply(p)) this else {
- val prev = ctx.getOrElse(p._2, Seq.empty)
+ val prev = ctx.getOrElse(p._2, Set.empty)
val newSet = prev.filterNot(set => p._1.subsetOf(set)).toSet + p._1
new Context(ctx + (p._2 -> newSet))
}
@@ -569,7 +569,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
case Seq(b) if isBlocker(b) => (b, None)
case _ =>
val last = enablersToBlocker.get(enablers).orElse {
- val initialEnablers = enablers.flatMap(blockerToEnablers.get).flatten
+ val initialEnablers = enablers.flatMap(e => blockerToEnablers.getOrElse(e, Set(e)))
enablersToBlocker.get(initialEnablers)
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 16dc1c19895da49d2d88518a2f56ae0a47cd9b83..4556f7dd6507f9a8c8a745b0323dbbdb9cf0032b 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -98,6 +98,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val substMap : Map[Identifier, T] = arguments.toMap + pathVar
+
val (bodyConds, bodyExprs, bodyTree, bodyGuarded, bodyLambdas, bodyQuantifications) = if (isRealFunDef) {
invocationEqualsBody.foldLeft(emptyClauses)((clsSet, cls) => clsSet ++ mkClauses(start, cls, substMap))
} else {
diff --git a/src/main/scala/leon/solvers/templates/TemplateInfo.scala b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
index 27df9b25d13412c106f2bf30d6c75b1266b19d93..dfdd664cbdf1f110690d05e959bc1a14cc615327 100644
--- a/src/main/scala/leon/solvers/templates/TemplateInfo.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
@@ -16,11 +16,24 @@ case class TemplateCallInfo[T](tfd: TypedFunDef, args: Seq[Arg[T]]) {
}
}
-case class TemplateAppInfo[T](template: LambdaTemplate[T], equals: T, args: Seq[Arg[T]]) {
+case class TemplateAppInfo[T](template: Either[LambdaTemplate[T], T], equals: T, args: Seq[Arg[T]]) {
override def toString = {
- template.ids._2 + "|" + equals + args.map {
+ val caller = template match {
+ case Left(tmpl) => tmpl.ids._2
+ case Right(c) => c
+ }
+
+ caller + "|" + equals + args.map {
case Right(m) => m.toString
case Left(v) => v.toString
}.mkString("(", ",", ")")
}
}
+
+object TemplateAppInfo {
+ def apply[T](template: LambdaTemplate[T], equals: T, args: Seq[Arg[T]]): TemplateAppInfo[T] =
+ TemplateAppInfo(Left(template), equals, args)
+
+ def apply[T](caller: T, equals: T, args: Seq[Arg[T]]): TemplateAppInfo[T] =
+ TemplateAppInfo(Right(caller), equals, args)
+}
diff --git a/src/main/scala/leon/solvers/templates/TemplateManager.scala b/src/main/scala/leon/solvers/templates/TemplateManager.scala
index 56c8e6211e033ce0c002f695b535999a724ab223..c81abc384934aea21fb1d5d183925e7c6d013fb7 100644
--- a/src/main/scala/leon/solvers/templates/TemplateManager.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateManager.scala
@@ -34,7 +34,7 @@ object Instantiation {
implicit class MapSeqWrapper[A,B](map: Map[A,Seq[B]]) {
def merge(that: Map[A,Seq[B]]): Map[A,Seq[B]] = (map.keys ++ that.keys).map { k =>
- k -> (map.getOrElse(k, Seq.empty) ++ that.getOrElse(k, Seq.empty))
+ k -> (map.getOrElse(k, Seq.empty) ++ that.getOrElse(k, Seq.empty)).distinct
}.toMap
}
@@ -158,23 +158,25 @@ object Template {
var functions: Set[(T, FunctionType, T)] = Set.empty
var clauses: Seq[T] = Seq.empty
- val cleanGuarded = guardedExprs.map { case (b, es) => b -> es.map { e =>
- def clean(expr: Expr): Expr = postMap {
- case FreshFunction(f) => Some(BooleanLiteral(true))
- case _ => None
- } (expr)
-
- val withPaths = CollectorWithPaths { case FreshFunction(f) => f }.traverse(e)
- functions ++= withPaths.map { case (f, TopLevelAnds(paths)) =>
- val tpe = bestRealType(f.getType).asInstanceOf[FunctionType]
- val path = andJoin(paths.map(clean))
- (encodeExpr(and(Variable(b), path)), tpe, encodeExpr(f))
- }
+ val cleanGuarded = guardedExprs.map {
+ case (b, es) => b -> es.map { e =>
+ def clean(expr: Expr): Expr = postMap {
+ case FreshFunction(f) => Some(BooleanLiteral(true))
+ case _ => None
+ } (expr)
+
+ val withPaths = CollectorWithPaths { case FreshFunction(f) => f }.traverse(e)
+ functions ++= withPaths.map { case (f, TopLevelAnds(paths)) =>
+ val tpe = bestRealType(f.getType).asInstanceOf[FunctionType]
+ val path = andJoin(paths.map(clean))
+ (encodeExpr(and(Variable(b), path)), tpe, encodeExpr(f))
+ }
- val cleanExpr = clean(e)
- clauses :+= encodeExpr(Implies(Variable(b), cleanExpr))
- cleanExpr
- }}
+ val cleanExpr = clean(e)
+ clauses :+= encodeExpr(Implies(Variable(b), cleanExpr))
+ cleanExpr
+ }
+ }
(clauses, cleanGuarded, functions)
}
@@ -190,9 +192,9 @@ object Template {
.map(tfd => invocationMatcher(encodeExpr)(tfd, arguments.map(_._1.toVariable)))
val (blockers, applications, matchers) = {
- var blockers : Map[Identifier, Set[TemplateCallInfo[T]]] = Map.empty
- var applications : Map[Identifier, Set[App[T]]] = Map.empty
- var matchers : Map[Identifier, Set[Matcher[T]]] = Map.empty
+ var blockers : Map[Identifier, Set[TemplateCallInfo[T]]] = Map.empty
+ var applications : Map[Identifier, Set[App[T]]] = Map.empty
+ var matchers : Map[Identifier, Set[Matcher[T]]] = Map.empty
for ((b,es) <- cleanGuarded) {
var funInfos : Set[TemplateCallInfo[T]] = Set.empty
@@ -231,15 +233,15 @@ object Template {
matchInfos ++= exprToMatcher.values
}
- val calls = funInfos -- optIdCall
+ val calls = funInfos.filter(i => Some(i) != optIdCall)
if (calls.nonEmpty) blockers += b -> calls
- val apps = appInfos -- optIdApp
+ val apps = appInfos.filter(i => Some(i) != optIdApp)
if (apps.nonEmpty) applications += b -> apps
- val matchs = matchInfos.filter { case m @ Matcher(_, _, _, menc) =>
+ val matchs = (matchInfos.filter { case m @ Matcher(_, _, _, menc) =>
!optIdApp.exists { case App(_, _, _, aenc) => menc == aenc }
- } ++ (if (funInfos.exists(info => Some(info) == optIdCall)) invocMatcher else None)
+ } ++ (if (funInfos.exists(info => Some(info) == optIdCall)) invocMatcher else None))
if (matchs.nonEmpty) matchers += b -> matchs
}
@@ -298,8 +300,8 @@ object Template {
manager match {
case lmanager: LambdaManager[T] =>
val funSubstituter = encoder.substitute(subst.mapValues(_.encoded))
- for ((b,tpe,f) <- functions) instantiation = instantiation withClauses {
- lmanager.registerFunction(funSubstituter(b), tpe, funSubstituter(f))
+ for ((b,tpe,f) <- functions) {
+ instantiation ++= lmanager.registerFunction(funSubstituter(b), tpe, funSubstituter(f))
}
// /!\ CAREFUL /!\
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index ba6ed43828b11cfb97b8c87825d2b94a84984cd7..cb7fe90d280160d03a5b9fbc190a7851b3cd3c1b 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -28,7 +28,6 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
private val appInfos = new IncrementalMap[(T, App[T]), (Int, Int, T, T, Set[TemplateAppInfo[T]])]()
private val appBlockers = new IncrementalMap[(T, App[T]), T]()
private val blockerToApps = new IncrementalMap[T, (T, App[T])]()
- private val functionVars = new IncrementalMap[TypeTree, Set[T]]()
def push() {
callInfos.push()
@@ -37,7 +36,6 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
appInfos.push()
appBlockers.push()
blockerToApps.push()
- functionVars.push()
}
def pop() {
@@ -47,7 +45,6 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
appInfos.pop()
appBlockers.pop()
blockerToApps.pop()
- functionVars.pop()
}
def clear() {
@@ -57,7 +54,6 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
appInfos.clear()
appBlockers.clear()
blockerToApps.clear()
- functionVars.clear()
}
def reset() {
@@ -67,7 +63,6 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
appInfos.reset()
appBlockers.reset()
blockerToApps.clear()
- functionVars.reset()
}
def dumpBlockers() = {
@@ -142,14 +137,13 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
}
private def freshAppBlocks(apps: Traversable[(T, App[T])]) : Seq[T] = {
- apps.filter(!appBlockers.isDefinedAt(_)).toSeq.map { case app @ (blocker, App(caller, tpe, _, _)) =>
+ apps.filter(!appBlockers.isDefinedAt(_)).toSeq.map {
+ case app @ (blocker, App(caller, tpe, _, _)) =>
+ val firstB = encoder.encodeId(FreshIdentifier("b_lambda", BooleanType, true))
+ val clause = encoder.mkImplies(encoder.mkNot(firstB), encoder.mkNot(blocker))
- val firstB = encoder.encodeId(FreshIdentifier("b_lambda", BooleanType, true))
- val freeEq = functionVars.getOrElse(tpe, Set()).toSeq.map(t => encoder.mkEquals(t, caller))
- val clause = encoder.mkImplies(encoder.mkNot(encoder.mkOr((freeEq :+ firstB) : _*)), encoder.mkNot(blocker))
-
- appBlockers += app -> firstB
- clause
+ appBlockers += app -> firstB
+ clause
}
}
@@ -174,10 +168,6 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
val trArgs = template.tfd.params.map(vd => Left(bindings(Variable(vd.id))))
- for (vd <- template.tfd.params if vd.getType.isInstanceOf[FunctionType]) {
- functionVars += vd.getType -> (functionVars.getOrElse(vd.getType, Set()) + bindings(vd.toVariable))
- }
-
// ...now this template defines clauses that are all guarded
// by that activating boolean. If that activating boolean is
// undefined (or false) these clauses have no effect...
@@ -280,7 +270,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
newClauses :+= extension
}
- var fastAppInfos : Map[(T, App[T]), (Int, Set[TemplateAppInfo[T]])] = Map.empty
+ var fastAppInfos : Seq[((T, App[T]), (Int, Set[TemplateAppInfo[T]]))] = Seq.empty
for ((id, (gen, _, _, infos)) <- newCallInfos; info @ TemplateCallInfo(tfd, args) <- infos) {
var newCls = Seq[T]()
@@ -338,7 +328,9 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
newClauses ++= newCls
}
- for ((app @ (b, _), (gen, infos)) <- thisAppInfos ++ fastAppInfos; info @ TemplateAppInfo(template, equals, args) <- infos) {
+ for ((app @ (b, _), (gen, infos)) <- thisAppInfos ++ fastAppInfos;
+ info @ TemplateAppInfo(tmpl, equals, args) <- infos;
+ template <- tmpl.left) {
var newCls = Seq.empty[T]
val lambdaBlocker = lambdaBlockers.get(info) match {
diff --git a/src/test/resources/regression/verification/purescala/invalid/InductiveQuantification.scala b/src/test/resources/regression/verification/purescala/invalid/InductiveQuantification.scala
deleted file mode 100644
index 970b3b53bddb295db19308e3443309f478ee15cc..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/verification/purescala/invalid/InductiveQuantification.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-import leon.lang._
-
-object SizeInc {
-
- abstract class List[A]
- case class Cons[A](head: A, tail: List[A]) extends List[A]
- case class Nil[A]() extends List[A]
-
- def failling_1[A](x: List[A]): Int => Int = {
- (i: Int) => x match {
- case Cons(head, tail) => 1 + failling_1(tail)(i)
- case Nil() => i
- }
- } ensuring { res => forall((a: Int) => res(a) > 0) }
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/valid/InductiveQuantification.scala b/src/test/resources/regression/verification/purescala/valid/InductiveQuantification.scala
deleted file mode 100644
index 4883043040fdb90df294aac09b076d16c7628cf4..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/verification/purescala/valid/InductiveQuantification.scala
+++ /dev/null
@@ -1,26 +0,0 @@
-import leon.lang._
-
-object SizeInc {
-
- abstract class List[A]
- case class Cons[A](head: A, tail: List[A]) extends List[A]
- case class Nil[A]() extends List[A]
-
- def sizeInc[A](x: List[A]): BigInt => BigInt = {
- (i: BigInt) => x match {
- case Cons(head, tail) => 1 + sizeInc(tail)(i)
- case Nil() => i
- }
- } ensuring { res => forall((a: BigInt) => a > 0 ==> res(a) > 0) }
-
- def sizeInc2[A](x: BigInt): List[A] => BigInt = {
- require(x > 0)
-
- (list: List[A]) => list match {
- case Cons(head, tail) => 1 + sizeInc2(x)(tail)
- case Nil() => x
- }
- } ensuring { res => forall((a: List[A]) => res(a) > 0) }
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala
index 6c2df0820a2b0f0c19ee393c12e1d70b36bbf233..215c72272673c5c6e9bbd5173b2b334ed3fc753c 100644
--- a/src/test/scala/leon/regression/termination/TerminationSuite.scala
+++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala
@@ -34,8 +34,7 @@ class TerminationSuite extends LeonRegressionSuite {
val ignored = List(
"verification/purescala/valid/MergeSort.scala",
- "verification/purescala/valid/Nested14.scala",
- "verification/purescala/valid/InductiveQuantification.scala"
+ "verification/purescala/valid/Nested14.scala"
)
val t = if (ignored.exists(displayName.replaceAll("\\\\","/").endsWith)) {
diff --git a/testcases/verification/quantification/invalid/SizeInc.scala b/testcases/verification/quantification/invalid/SizeInc.scala
deleted file mode 100644
index 970b3b53bddb295db19308e3443309f478ee15cc..0000000000000000000000000000000000000000
--- a/testcases/verification/quantification/invalid/SizeInc.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-import leon.lang._
-
-object SizeInc {
-
- abstract class List[A]
- case class Cons[A](head: A, tail: List[A]) extends List[A]
- case class Nil[A]() extends List[A]
-
- def failling_1[A](x: List[A]): Int => Int = {
- (i: Int) => x match {
- case Cons(head, tail) => 1 + failling_1(tail)(i)
- case Nil() => i
- }
- } ensuring { res => forall((a: Int) => res(a) > 0) }
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/quantification/valid/SizeInc.scala b/testcases/verification/quantification/valid/SizeInc.scala
deleted file mode 100644
index 9fe7ea96eb44bba951ff620507bad750c1560056..0000000000000000000000000000000000000000
--- a/testcases/verification/quantification/valid/SizeInc.scala
+++ /dev/null
@@ -1,26 +0,0 @@
-import leon.lang._
-
-object SizeInc {
-
- abstract class List[A]
- case class Cons[A](head: A, tail: List[A]) extends List[A]
- case class Nil[A]() extends List[A]
-
- def sizeInc[A](x: List[A]): BigInt => BigInt = {
- (i: BigInt) => x match {
- case Cons(head, tail) => 1 + sizeInc(tail)(i)
- case Nil() => i
- }
- } ensuring { res => forall((a: BigInt) => a > 0 ==> res(a) > 0) }
-
- def sizeInc2[A](x: BigInt): List[A] => BigInt = {
- require(x > 0)
-
- (list: List[A]) => list match {
- case Cons(head, tail) => 1 + sizeInc2(x)(tail)
- case Nil() => x
- }
- } ensuring { res => forall((a: List[A]) => res(a) > 0) }
-}
-
-// vim: set ts=4 sw=4 et: