From f76dd21de31ef78cda37d6d518808152a2d5d69e Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sat, 24 Jan 2015 14:09:23 +0100
Subject: [PATCH] Extended termination to HO functions
---
src/main/scala/leon/purescala/TypeTrees.scala | 3 ++
.../solvers/z3/Z3ModelReconstruction.scala | 2 +-
.../scala/leon/termination/ChainBuilder.scala | 12 +++---
.../leon/termination/ChainComparator.scala | 8 ++--
.../leon/termination/ChainProcessor.scala | 6 +--
.../leon/termination/LoopProcessor.scala | 6 +--
.../leon/termination/RelationBuilder.scala | 14 +++----
.../leon/termination/RelationProcessor.scala | 4 +-
.../scala/leon/termination/Strengthener.scala | 26 ++++++-------
.../leon/termination/StructuralSize.scala | 8 ++--
.../termination/looping/Looping1.scala.BAK | 33 ----------------
.../termination/looping/Looping2.scala.BAK | 32 ---------------
.../termination/looping/Looping3.scala.BAK | 32 ---------------
.../termination/valid/HOTermination.scala | 39 +++++++++++++++++++
.../termination/valid/HardChains.scala.BAK | 37 ------------------
.../verification/purescala/valid/Lists2.scala | 19 +++++++++
16 files changed, 103 insertions(+), 178 deletions(-)
delete mode 100644 src/test/resources/regression/termination/looping/Looping1.scala.BAK
delete mode 100644 src/test/resources/regression/termination/looping/Looping2.scala.BAK
delete mode 100644 src/test/resources/regression/termination/looping/Looping3.scala.BAK
create mode 100644 src/test/resources/regression/termination/valid/HOTermination.scala
delete mode 100644 src/test/resources/regression/termination/valid/HardChains.scala.BAK
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 16274e086..6b283b8ef 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -99,6 +99,9 @@ object TypeTrees {
if (tmap.isEmpty) {
classDef.fields
} else {
+ // !! WARNING !!
+ // vd.id.getType will NOT match vd.tpe, but we kind of need this for selectorID2Index...
+ // See with Etienne about changing this!
classDef.fields.map(vd => ValDef(vd.id, instantiateType(vd.tpe, tmap)))
}
}
diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index 21f829502..5953fc422 100644
--- a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
@@ -37,7 +37,7 @@ trait Z3ModelReconstruction {
def completeID(id : Identifier) : Unit = {
asMap = asMap + ((id -> simplestValue(id.getType)))
- reporter.info("Completing variable '" + id + "' to simplest value")
+ reporter.debug("Completing variable '" + id + "' to simplest value")
}
for(id <- ids) {
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index 26c557608..5bbfc7cc9 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -31,20 +31,20 @@ final case class Chain(relations: List[Relation]) {
lazy val size: Int = relations.size
private lazy val inlining : Seq[(Seq[ValDef], Expr)] = {
- def rec(list: List[Relation], funDef: TypedFunDef, subst: Map[Identifier, Expr]): Seq[(Seq[ValDef], Expr)] = list match {
- case Relation(_, _, fi @ FunctionInvocation(fitfd, args), _) :: xs =>
+ def rec(list: List[Relation], funDef: TypedFunDef, args: Seq[Expr]): Seq[(Seq[ValDef], Expr)] = list match {
+ case Relation(_, _, fi @ FunctionInvocation(fitfd, nextArgs), _) :: xs =>
val tfd = TypedFunDef(fitfd.fd, fitfd.tps.map(funDef.translated(_)))
+ val subst = (tfd.params.map(_.id) zip args).toMap
val expr = replaceFromIDs(subst, hoistIte(expandLets(matchToIfThenElse(tfd.body.get))))
+ val mappedArgs = nextArgs.map(e => replaceFromIDs(subst, tfd.translated(e)))
- val mappedArgs = args.map(e => replaceFromIDs(subst, tfd.translated(e)))
- val newSubst = (tfd.params.map(_.id) zip mappedArgs).toMap
- (tfd.params, expr) +: rec(xs, tfd, newSubst)
+ (tfd.params, expr) +: rec(xs, tfd, mappedArgs)
case Nil => Seq.empty
}
val body = hoistIte(expandLets(matchToIfThenElse(funDef.body.get)))
val tfd = funDef.typed(funDef.tparams.map(_.tp))
- (tfd.params, body) +: rec(relations, tfd, funDef.params.map(arg => arg.id -> arg.toVariable).toMap)
+ (tfd.params, body) +: rec(relations, tfd, tfd.params.map(_.toVariable))
}
lazy val finalParams : Seq[ValDef] = inlining.last._1
diff --git a/src/main/scala/leon/termination/ChainComparator.scala b/src/main/scala/leon/termination/ChainComparator.scala
index 743db6335..91958f60d 100644
--- a/src/main/scala/leon/termination/ChainComparator.scala
+++ b/src/main/scala/leon/termination/ChainComparator.scala
@@ -184,9 +184,11 @@ trait ChainComparator { self : StructuralSize with TerminationChecker =>
case _ => NoEndpoint
}
- cluster.foldLeft[NumericEndpoint](AnyEndpoint)((acc, chain) => {
- acc min chain.inlined.foldLeft[NumericEndpoint](NoEndpoint)((acc, expr) => acc max endpoint(expr))
- })
+ cluster.foldLeft[NumericEndpoint](AnyEndpoint) { (acc, chain) =>
+ acc min chain.inlined.foldLeft[NumericEndpoint](NoEndpoint) { (acc, expr) =>
+ acc max endpoint(expr)
+ }
+ }
}
def numericConverging(e1: Expr, e2s: Seq[(Seq[Expr], Expr)], cluster: Set[Chain]) : Seq[Expr] = flatType(e1.getType).toSeq.flatMap {
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index 0c4e1608a..d0e51f24b 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -20,8 +20,8 @@ class ChainProcessor(val checker: TerminationChecker with ChainBuilder with Chai
reporter.debug("- Strengthening postconditions")
checker.strengthenPostconditions(problem.funDefs)(this)
-// reporter.debug("- Strengthening applications")
-// checker.strengthenApplications(problem.funDefs)(this)
+ reporter.debug("- Strengthening applications")
+ checker.strengthenApplications(problem.funDefs)(this)
reporter.debug("- Running ChainBuilder")
val chainsMap : Map[FunDef, (Set[FunDef], Set[Chain])] = problem.funDefs.map { funDef =>
@@ -37,8 +37,6 @@ class ChainProcessor(val checker: TerminationChecker with ChainBuilder with Chai
def exprs(fd: FunDef): (Expr, Seq[(Seq[Expr], Expr)], Set[Chain]) = {
val fdChains = chainsMap(fd)._2
- val nfdChains = chainsMap.filter(_._1 != fd).values.foldLeft(Set.empty[Chain])((set, p) => set ++ p._2)
- assert(nfdChains.subsetOf(fdChains))
val e1 = Tuple(fd.params.map(_.toVariable))
val e2s = fdChains.toSeq.map { chain =>
diff --git a/src/main/scala/leon/termination/LoopProcessor.scala b/src/main/scala/leon/termination/LoopProcessor.scala
index 7ff9039af..1f28c405c 100644
--- a/src/main/scala/leon/termination/LoopProcessor.scala
+++ b/src/main/scala/leon/termination/LoopProcessor.scala
@@ -15,8 +15,8 @@ class LoopProcessor(val checker: TerminationChecker with ChainBuilder with Stren
val name: String = "Loop Processor"
def run(problem: Problem) = {
-// reporter.debug("- Strengthening applications")
-// checker.strengthenApplications(problem.funDefs)(this)
+ reporter.debug("- Strengthening applications")
+ checker.strengthenApplications(problem.funDefs)(this)
reporter.debug("- Running ChainBuilder")
val chains : Set[Chain] = problem.funDefs.flatMap(fd => checker.getChains(fd)(this)._2)
@@ -38,7 +38,7 @@ class LoopProcessor(val checker: TerminationChecker with ChainBuilder with Stren
definitiveSATwithModel(And(path :+ Equals(srcTuple, resTuple))) match {
case Some(map) =>
val args = chain.funDef.params.map(arg => map(arg.id))
- val res = if (chain.relations.exists(_.inAnon)) MaybeBroken(chain.funDef, args) else Broken(chain.funDef, args)
+ val res = if (chain.relations.exists(_.inLambda)) MaybeBroken(chain.funDef, args) else Broken(chain.funDef, args)
nonTerminating(chain.funDef) = res
case None =>
}
diff --git a/src/main/scala/leon/termination/RelationBuilder.scala b/src/main/scala/leon/termination/RelationBuilder.scala
index a597ebde8..c9acd8ccf 100644
--- a/src/main/scala/leon/termination/RelationBuilder.scala
+++ b/src/main/scala/leon/termination/RelationBuilder.scala
@@ -11,8 +11,8 @@ import purescala.Definitions._
import scala.collection.mutable.{Map => MutableMap}
-final case class Relation(funDef: FunDef, path: Seq[Expr], call: FunctionInvocation, inAnon: Boolean) {
- override def toString : String = "Relation(" + funDef.id + "," + path + ", " + call.tfd.id + call.args.mkString("(",",",")") + "," + inAnon + ")"
+final case class Relation(funDef: FunDef, path: Seq[Expr], call: FunctionInvocation, inLambda: Boolean) {
+ override def toString : String = "Relation(" + funDef.id + "," + path + ", " + call.tfd.id + call.args.mkString("(",",",")") + "," + inLambda + ")"
}
trait RelationBuilder { self: TerminationChecker with Strengthener =>
@@ -30,13 +30,13 @@ trait RelationBuilder { self: TerminationChecker with Strengthener =>
case Some((relations, signature)) if signature == funDefRelationSignature(funDef) => relations
case _ => {
val collector = new CollectorWithPaths[Relation] {
- var inAnon: Boolean = false
+ var inLambda: Boolean = false
def collect(e: Expr, path: Seq[Expr]): Option[Relation] = e match {
case fi @ FunctionInvocation(f, args) if self.functions(f.fd) =>
- Some(Relation(funDef, path, fi, inAnon))
-// case af @ AnonymousFunction(args, body) =>
-// inAnon = true
-// None
+ Some(Relation(funDef, path, fi, inLambda))
+ case l @ Lambda(args, body) =>
+ inLambda = true
+ None
case _ => None
}
diff --git a/src/main/scala/leon/termination/RelationProcessor.scala b/src/main/scala/leon/termination/RelationProcessor.scala
index 4982968e2..4908ec1d4 100644
--- a/src/main/scala/leon/termination/RelationProcessor.scala
+++ b/src/main/scala/leon/termination/RelationProcessor.scala
@@ -20,8 +20,8 @@ class RelationProcessor(
reporter.debug("- Strengthening postconditions")
checker.strengthenPostconditions(problem.funDefs)(this)
-// reporter.debug("- Strengthening applications")
-// checker.strengthenApplications(problem.funDefs)(this)
+ reporter.debug("- Strengthening applications")
+ checker.strengthenApplications(problem.funDefs)(this)
val formulas = problem.funDefs.map({ funDef =>
funDef -> checker.getRelations(funDef).collect({
diff --git a/src/main/scala/leon/termination/Strengthener.scala b/src/main/scala/leon/termination/Strengthener.scala
index 31f076498..a827162ca 100644
--- a/src/main/scala/leon/termination/Strengthener.scala
+++ b/src/main/scala/leon/termination/Strengthener.scala
@@ -60,7 +60,6 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
case object WeakDecreasing extends SizeConstraint
case object NoConstraint extends SizeConstraint
- /*
private val strengthenedApp : MutableSet[FunDef] = MutableSet.empty
protected def strengthened(fd: FunDef): Boolean = strengthenedApp(fd)
@@ -68,7 +67,7 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
private val appConstraint : MutableMap[(FunDef, Identifier), SizeConstraint] = MutableMap.empty
def applicationConstraint(fd: FunDef, id: Identifier, arg: Expr, args: Seq[Expr]): Expr = arg match {
- case AnonymousFunction(fargs, body) => appConstraint.get(fd -> id) match {
+ case Lambda(fargs, body) => appConstraint.get(fd -> id) match {
case Some(StrongDecreasing) => self.sizeDecreasing(Tuple(args), Tuple(fargs.map(_.toVariable)))
case Some(WeakDecreasing) => self.softDecreasing(Tuple(args), Tuple(fargs.map(_.toVariable)))
case _ => BooleanLiteral(true)
@@ -84,14 +83,14 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
val appCollector = new CollectorWithPaths[(Identifier,Expr,Expr)] {
def collect(e: Expr, path: Seq[Expr]): Option[(Identifier, Expr, Expr)] = e match {
- case FunctionApplication(Variable(id), args) => Some((id, And(path), Tuple(args)))
+ case Application(Variable(id), args) => Some((id, And(path), Tuple(args)))
case _ => None
}
}
val applications = appCollector.traverse(funDef).distinct
- val funDefArgTuple = Tuple(funDef.args.map(_.toVariable))
+ val funDefArgTuple = Tuple(funDef.params.map(_.toVariable))
val allFormulas = for ((id, path, appArgs) <- applications) yield {
val soft = Implies(path, self.softDecreasing(funDefArgTuple, appArgs))
@@ -102,8 +101,8 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
val formulaMap = allFormulas.groupBy(_._1).mapValues(_.map(_._2).unzip)
val constraints = for ((id, (weakFormulas, strongFormulas)) <- formulaMap) yield id -> {
- if (solver.definitiveALL(And(weakFormulas.toSeq), funDef.precondition)) {
- if (solver.definitiveALL(And(strongFormulas.toSeq), funDef.precondition)) {
+ if (solver.definitiveALL(And(weakFormulas.toSeq))) {
+ if (solver.definitiveALL(And(strongFormulas.toSeq))) {
StrongDecreasing
} else {
WeakDecreasing
@@ -113,13 +112,13 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
}
}
- val funDefHOArgs = funDef.args.map(_.id).filter(_.getType.isInstanceOf[FunctionType]).toSet
+ val funDefHOArgs = funDef.params.map(_.id).filter(_.getType.isInstanceOf[FunctionType]).toSet
val fiCollector = new CollectorWithPaths[(Expr, Expr, Seq[(Identifier,(FunDef, Identifier))])] {
def collect(e: Expr, path: Seq[Expr]): Option[(Expr, Expr, Seq[(Identifier,(FunDef, Identifier))])] = e match {
case FunctionInvocation(fd, args) if (funDefHOArgs intersect args.collect({ case Variable(id) => id }).toSet).nonEmpty =>
- Some((And(path), Tuple(args), (args zip fd.args).collect {
- case (Variable(id), vd) if funDefHOArgs(id) => id -> ((fd, vd.id))
+ Some((And(path), Tuple(args), (args zip fd.params).collect {
+ case (Variable(id), vd) if funDefHOArgs(id) => id -> ((fd.fd, vd.id))
}))
case _ => None
}
@@ -145,14 +144,14 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
case (_, None) => NoConstraint
case (NoConstraint, _) => NoConstraint
case (StrongDecreasing | WeakDecreasing, Some(StrongDecreasing)) =>
- if (solver.definitiveALL(weakFormula, funDef.precondition)) StrongDecreasing
+ if (solver.definitiveALL(weakFormula)) StrongDecreasing
else NoConstraint
case (StrongDecreasing, Some(WeakDecreasing)) =>
- if (solver.definitiveALL(strongFormula, funDef.precondition)) StrongDecreasing
- else if (solver.definitiveALL(weakFormula, funDef.precondition)) WeakDecreasing
+ if (solver.definitiveALL(strongFormula)) StrongDecreasing
+ else if (solver.definitiveALL(weakFormula)) WeakDecreasing
else NoConstraint
case (WeakDecreasing, Some(WeakDecreasing)) =>
- if (solver.definitiveALL(weakFormula, funDef.precondition)) WeakDecreasing
+ if (solver.definitiveALL(weakFormula)) WeakDecreasing
else NoConstraint
}
}
@@ -167,7 +166,6 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
strengthenedApp += funDef
}
}
- */
}
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index e9753151b..fe966ed49 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -31,7 +31,7 @@ trait StructuralSize {
sizeCache.get(argumentType) match {
case Some(fd) => fd
case None =>
- val argument = ValDef(FreshIdentifier("x").setType(argumentType), argumentType)
+ val argument = ValDef(FreshIdentifier("x", true).setType(argumentType), argumentType)
val formalTParams = typeParams.map(TypeParameterDef(_))
val fd = new FunDef(FreshIdentifier("size", true), formalTParams, Int32Type, Seq(argument), DefType.MethodDef)
sizeCache(argumentType) = fd
@@ -48,9 +48,9 @@ trait StructuralSize {
def caseClassType2MatchCase(_c: ClassType): MatchCase = {
val c = _c.asInstanceOf[CaseClassType] // required by leon framework
- val arguments = c.fields.map(f => f -> f.id.freshen)
- val argumentPatterns = arguments.map(p => WildcardPattern(Some(p._2)))
- val sizes = arguments.map(p => size(Variable(p._2)))
+ val arguments = c.fields.map(vd => FreshIdentifier(vd.id.name).setType(vd.tpe))
+ val argumentPatterns = arguments.map(id => WildcardPattern(Some(id)))
+ val sizes = arguments.map(id => size(Variable(id)))
val result = sizes.foldLeft[Expr](IntLiteral(1))(Plus(_,_))
SimpleCase(CaseClassPattern(None, c, argumentPatterns), result)
}
diff --git a/src/test/resources/regression/termination/looping/Looping1.scala.BAK b/src/test/resources/regression/termination/looping/Looping1.scala.BAK
deleted file mode 100644
index 04affc481..000000000
--- a/src/test/resources/regression/termination/looping/Looping1.scala.BAK
+++ /dev/null
@@ -1,33 +0,0 @@
-import leon.lang._
-
-object ComplexChains {
-
- abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil extends List
-
- def looping1(list: List): List = list match {
- case Cons(head, tail) if head > 0 => looping2(tail)
- case Cons(head, tail) if head < 0 => looping3(tail)
- case _ => looping4(Cons(1, list))
- }
-
- def looping2(list: List): List = list match {
- case Cons(head, tail) if head > 0 => looping1(tail)
- case _ => looping4(list)
- }
-
- def looping3(list: List): List = list match {
- case Cons(head, tail) if head < 0 => looping1(tail)
- case _ => looping2(Cons(1, list))
- }
-
- def looping4(list: List): List = list match {
- case Cons(head, tail) if head == 0 => looping4(tail)
- case Cons(_, Cons(_, tail)) => looping1(Cons(1, list))
- case Cons(_, tail) => looping3(Nil())
- case Nil() => Nil()
- }
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/looping/Looping2.scala.BAK b/src/test/resources/regression/termination/looping/Looping2.scala.BAK
deleted file mode 100644
index ac3cf66ae..000000000
--- a/src/test/resources/regression/termination/looping/Looping2.scala.BAK
+++ /dev/null
@@ -1,32 +0,0 @@
-import leon.lang._
-
-object ComplexChains {
-
- abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil extends List
-
- def looping1(list: List): List = list match {
- case Cons(head, tail) if head > 0 => calling2(list)
- case Cons(head, tail) if head < 0 => calling3(list)
- case _ => looping4(Cons(1, list))
- }
-
- def calling2(list: List): List = list match {
- case Cons(head, tail) if head > 0 => looping1(tail)
- case _ => looping4(list)
- }
-
- def calling3(list: List): List = list match {
- case Cons(head, tail) if head < 0 => looping1(tail)
- case _ => looping4(list)
- }
-
- def looping4(list: List): List = list match {
- case Cons(_, Cons(_, tail)) => looping1(tail)
- case Cons(_, tail) => looping1(tail)
- case Nil() => calling2(Cons(1, Nil()))
- }
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/looping/Looping3.scala.BAK b/src/test/resources/regression/termination/looping/Looping3.scala.BAK
deleted file mode 100644
index 29b3c9f82..000000000
--- a/src/test/resources/regression/termination/looping/Looping3.scala.BAK
+++ /dev/null
@@ -1,32 +0,0 @@
-import leon.lang._
-
-object ComplexChains {
-
- abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil extends List
-
- def looping1(list: List): List = list match {
- case Cons(head, tail) if head > 0 => looping2(list)
- case Cons(head, tail) if head < 0 => looping3(list)
- case _ => looping4(Cons(1, list))
- }
-
- def looping2(list: List): List = list match {
- case Cons(head, tail) if head > 0 => looping1(tail)
- case _ => looping3(list)
- }
-
- def looping3(list: List): List = list match {
- case Cons(head, tail) if head < 0 => looping1(tail)
- case _ => looping2(list)
- }
-
- def looping4(list: List): List = list match {
- case Cons(_, Cons(_, tail)) => looping1(tail)
- case Cons(_, tail) => looping1(tail)
- case Nil() => looping2(Cons(1, Nil()))
- }
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/valid/HOTermination.scala b/src/test/resources/regression/termination/valid/HOTermination.scala
new file mode 100644
index 000000000..f7e1b5694
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/HOTermination.scala
@@ -0,0 +1,39 @@
+
+import leon.lang._
+
+object HOTermination {
+ abstract class List[T]
+ case class Cons[T](head: T, tail: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+ abstract class Option[T]
+ case class Some[T](value: T) extends Option[T]
+ case class None[T]() extends Option[T]
+
+ def map[A,B](list: List[A], f: A => B): List[B] = list match {
+ case Cons(head, tail) => Cons(f(head), map(tail, f))
+ case Nil() => Nil()
+ }
+
+ abstract class Expr
+ case class Invocation(e: Expr, args: List[Expr]) extends Expr
+ case class Addition(e1: Expr, e2: Expr) extends Expr
+ case class Variable(i: Int) extends Expr
+
+ def transform(e: Expr, f: Expr => Option[Expr]): Expr = {
+ f(e) match {
+ case Some(newExpr) => newExpr
+ case None() => e match {
+ case Invocation(c, args) =>
+ val newC = transform(c, f)
+ val newArgs = map(args, (x: Expr) => transform(x, f))
+ Invocation(newC, newArgs)
+ case Addition(e1, e2) =>
+ Addition(transform(e1, f), transform(e2, f))
+ case Variable(i) => e
+ }
+ }
+ }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/termination/valid/HardChains.scala.BAK b/src/test/resources/regression/termination/valid/HardChains.scala.BAK
deleted file mode 100644
index 9efb8304e..000000000
--- a/src/test/resources/regression/termination/valid/HardChains.scala.BAK
+++ /dev/null
@@ -1,37 +0,0 @@
-import leon.lang._
-
-object HardChains {
-
- abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil extends List
-
- def f1(list: List): List = list match {
- case Cons(head, tail) if head > 0 => f2(list)
- case Cons(head, tail) if head < 0 => f3(list)
- case Nil() => Nil()
- case _ => f4(list)
- }
-
- def f2(list: List): List = list match {
- case Cons(head, tail) if head > 0 => f4(Cons(0, list))
- case _ => f1(list)
- }
-
- def f3(list: List): List = list match {
- case Cons(head, tail) if head < 0 => f4(Cons(0, list))
- case Cons(head, tail) if head == 0 => f2(tail)
- case _ => f4(list)
- }
-
- def f4(list: List): List = list match {
- case Cons(head, tail) if head == 0 => f3(tail)
- case Cons(head, Cons(head2, Cons(head3, tail))) => tail
- case Cons(head, Cons(head2, tail)) => tail
- case Cons(head, tail) if head > 0 => f4(Cons(0, tail))
- case Cons(head, tail) => f4(tail)
- case _ => f1(list)
- }
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists2.scala b/src/test/resources/regression/verification/purescala/valid/Lists2.scala
index da096d1d3..654046ba0 100644
--- a/src/test/resources/regression/verification/purescala/valid/Lists2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Lists2.scala
@@ -25,6 +25,25 @@ object Lists2 {
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:
--
GitLab