From ab6fc65dfc2038908396d263692c342847ca5863 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 24 Sep 2013 21:10:42 +0200
Subject: [PATCH] Updated project and added solver memory freeing
---
.../scala/leon/purescala/Definitions.scala | 2 +-
.../scala/leon/termination/ChainBuilder.scala | 10 +-
.../leon/termination/ChainComparator.scala | 128 ++++++++----------
.../leon/termination/ChainProcessor.scala | 6 +-
.../leon/termination/ComponentProcessor.scala | 4 +-
.../scala/leon/termination/Processor.scala | 84 +++++++-----
.../leon/termination/RelationBuilder.scala | 14 +-
.../leon/termination/RelationComparator.scala | 10 +-
.../leon/termination/RelationProcessor.scala | 2 +-
.../leon/termination/StructuralSize.scala | 26 ++--
.../looping/Termination_failling1.scala | 2 +-
.../termination/valid/ComplexChains.scala | 2 +-
.../termination/valid/ListWithSize.scala | 10 +-
.../termination/valid/SimpInterpret.scala | 4 +-
.../valid/Termination_passing1.scala | 2 +-
.../termination/TerminationRegression.scala | 15 +-
16 files changed, 151 insertions(+), 170 deletions(-)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index cc8003c5a..ea08be2f4 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -112,7 +112,7 @@ object Definitions {
val resSet: CallGraph = (for(funDef <- definedFunctions) yield {
funDef.precondition.map(treeCatamorphism[CallGraph](convert, combine, compute(funDef)_, _)).getOrElse(Set.empty) ++
funDef.body.map(treeCatamorphism[CallGraph](convert, combine, compute(funDef)_, _)).getOrElse(Set.empty) ++
- funDef.postcondition.map( pc => treeCatamorphism[CallGraph](convert, combine, compute(funDef)_, pc._2)).getOrElse(Set.empty)
+ funDef.postcondition.map(pc => treeCatamorphism[CallGraph](convert, combine, compute(funDef)_, pc._2)).getOrElse(Set.empty)
}).foldLeft(Set[(FunDef, FunDef)]())(_ ++ _)
var callers: Map[FunDef,Set[FunDef]] =
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index 741b7c2b6..f6ec38673 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -21,7 +21,7 @@ final case class Chain(chain: List[Relation]) {
override def hashCode(): Int = id
def funDef : FunDef = chain.head.funDef
- def funDefs : Set[FunDef] = chain.map(_.funDef) toSet
+ def funDefs : Set[FunDef] = chain.map(_.funDef).toSet
lazy val size: Int = chain.size
@@ -38,7 +38,7 @@ final case class Chain(chain: List[Relation]) {
case Relation(_, path, FunctionInvocation(fd, args)) :: xs =>
val formalArgs = fd.args.map(_.id)
val freshFormalArgVars = formalArgs.map(_.freshen.toVariable)
- val formalArgsMap: Map[Identifier, Expr] = formalArgs zip freshFormalArgVars toMap
+ val formalArgsMap: Map[Identifier, Expr] = (formalArgs zip freshFormalArgVars).toMap
val (newPath, newArgs) = (path.map(replaceFromIDs(subst, _)), args.map(replaceFromIDs(subst, _)))
val constraints = newPath ++ (freshFormalArgVars zip newArgs).map(p => Equals(p._1, p._2))
constraints ++ rec(xs, formalArgsMap)
@@ -68,14 +68,14 @@ final case class Chain(chain: List[Relation]) {
val mappedArgs = args.map(replaceFromIDs(mapping, _))
val newMapping = fd.args.map(_.id).zip(mappedArgs).toMap
// We assume we have a body at this point. It would be weird to have gotten here without one...
- val expr = hoistIte(expandLets(matchToIfThenElse(fd.getBody)))
+ val expr = hoistIte(expandLets(matchToIfThenElse(fd.body.get)))
val inlinedExpr = replaceFromIDs(newMapping, expr)
inlinedExpr:: rec(xs, newMapping)
case Nil => Nil
}
- val body = hoistIte(expandLets(matchToIfThenElse(funDef.getBody)))
- body :: rec(chain, funDef.args.map(arg => arg.id -> arg.toVariable) toMap)
+ val body = hoistIte(expandLets(matchToIfThenElse(funDef.body.get)))
+ body :: rec(chain, funDef.args.map(arg => arg.id -> arg.toVariable).toMap)
}
}
diff --git a/src/main/scala/leon/termination/ChainComparator.scala b/src/main/scala/leon/termination/ChainComparator.scala
index 9a6352a2a..278b4bc50 100644
--- a/src/main/scala/leon/termination/ChainComparator.scala
+++ b/src/main/scala/leon/termination/ChainComparator.scala
@@ -12,13 +12,6 @@ object ChainComparator {
def init : Unit = StructuralSize.init
- def sizeDecreasing(e1: TypedExpr, e2s: Seq[(Seq[Expr], Expr)]) = _sizeDecreasing(e1, e2s map {
- case (path, e2) => (path, exprToTypedExpr(e2))
- })
- def sizeDecreasing(e1: Expr, e2s: Seq[(Seq[Expr], Expr)]) = _sizeDecreasing(e1, e2s map {
- case (path, e2) => (path, exprToTypedExpr(e2))
- })
-
private object ContainerType {
def unapply(c: ClassType): Option[(CaseClassDef, Seq[(Identifier, TypeTree)])] = c match {
case CaseClassType(classDef) =>
@@ -29,32 +22,32 @@ object ChainComparator {
}
}
- private def _sizeDecreasing(te1: TypedExpr, te2s: Seq[(Seq[Expr], TypedExpr)]) : Expr = te1 match {
- case TypedExpr(e1, ContainerType(def1, types1)) => Or(types1.zipWithIndex map { case ((id1, type1), index) =>
- val newTe1 = TypedExpr(CaseClassSelector(def1, e1, id1), type1)
- val newTe2s = te2s.map({
- case (path, TypedExpr(e2, ContainerType(def2, types2))) =>
- val (id2, type2) = types2(index)
- (path, TypedExpr(CaseClassSelector(def2, e2, id2), type2))
- case (_, te2) => scala.sys.error("Unexpected input combinations: " + te1 + " " + te2)
+ def sizeDecreasing(e1: Expr, e2s: Seq[(Seq[Expr], Expr)]) : Expr = e1.getType match {
+ case ContainerType(def1, fields1) => Or(fields1.zipWithIndex map { case ((id1, type1), index) =>
+ sizeDecreasing(CaseClassSelector(def1, e1, id1), e2s.map { case (path, e2) =>
+ e2.getType match {
+ case ContainerType(def2, fields2) => (path, CaseClassSelector(def2, e2, fields2(index)._1))
+ case _ => scala.sys.error("Unexpected input combinations: " + e1 + " " + e2)
+ }
})
- _sizeDecreasing(newTe1, newTe2s)
})
- case TypedExpr(e1, TupleType(types1)) => Or(types1.zipWithIndex map { case (type1, index) =>
- val newTe1 = TypedExpr(TupleSelect(e1, index + 1), type1)
- val newTe2s = te2s.map({
- case (path, TypedExpr(e2, TupleType(types2))) => (path, TypedExpr(TupleSelect(e2, index + 1), types2(index)))
- case (_, te2) => scala.sys.error("Unexpected input combinations: " + te1 + " " + te2)
+ case TupleType(types1) => Or((0 until types1.length) map { case index =>
+ sizeDecreasing(TupleSelect(e1, index + 1), e2s.map { case (path, e2) =>
+ e2.getType match {
+ case TupleType(_) => (path, TupleSelect(e2, index + 1))
+ case _ => scala.sys.error("Unexpected input combination: " + e1 + " " + e2)
+ }
})
- _sizeDecreasing(newTe1, newTe2s)
})
- case TypedExpr(_, _: ClassType) => And(te2s map {
- case (path, te2 @ TypedExpr(_, _: ClassType)) => Implies(And(path), GreaterThan(size(te1), size(te2)))
- case (_, te2) => scala.sys.error("Unexpected input combinations: " + te1 + " " + te2)
+ case c: ClassType => And(e2s map { case (path, e2) =>
+ e2.getType match {
+ case c2: ClassType => Implies(And(path), GreaterThan(size(e1), size(e2)))
+ case _ => scala.sys.error("Unexpected input combination: " + e1 + " " + e2)
+ }
})
- case TypedExpr(_, BooleanType) => BooleanLiteral(false)
- case TypedExpr(_, Int32Type) => BooleanLiteral(false)
- case _ => scala.sys.error("Unexpected type " + te1.tpe)
+ case BooleanType => BooleanLiteral(false)
+ case Int32Type => BooleanLiteral(false)
+ case tpe => scala.sys.error("Unexpected type " + tpe)
}
private sealed abstract class NumericEndpoint {
@@ -133,13 +126,13 @@ object ChainComparator {
}
def endpoint(expr: Expr) : NumericEndpoint = expr match {
- case IfExpr(cond, then, elze) => matches(cond) match {
+ case IfExpr(cond, thenn, elze) => matches(cond) match {
case NoEndpoint =>
- endpoint(then) min endpoint(elze)
+ endpoint(thenn) min endpoint(elze)
case ep =>
- val terminatingThen = functionCallsOf(then).forall(fi => checker.terminates(fi.funDef).isGuaranteed)
+ val terminatingThen = functionCallsOf(thenn).forall(fi => checker.terminates(fi.funDef).isGuaranteed)
val terminatingElze = functionCallsOf(elze).forall(fi => checker.terminates(fi.funDef).isGuaranteed)
- val thenEndpoint = if (terminatingThen) ep max endpoint(then) else endpoint(then)
+ val thenEndpoint = if (terminatingThen) ep max endpoint(thenn) else endpoint(thenn)
val elzeEndpoint = if (terminatingElze) ep.inverse max endpoint(elze) else endpoint(elze)
thenEndpoint max elzeEndpoint
}
@@ -151,54 +144,45 @@ object ChainComparator {
})
}
- def numericConverging(e1: TypedExpr, e2s: Seq[(Seq[Expr], Expr)], cluster: Set[Chain], checker: TerminationChecker) = _numericConverging(e1, e2s map {
- case (path, e2) => (path, exprToTypedExpr(e2))
- }, cluster, checker)
- def numericConverging(e1: Expr, e2s: Seq[(Seq[Expr], Expr)], cluster: Set[Chain], checker: TerminationChecker) = _numericConverging(e1, e2s map {
- case (path, e2) => (path, exprToTypedExpr(e2))
- }, cluster, checker)
-
- private def _numericConverging(te1: TypedExpr, te2s: Seq[(Seq[Expr], TypedExpr)], cluster: Set[Chain], checker: TerminationChecker) : Expr = te1 match {
- case TypedExpr(e1, ContainerType(def1, types1)) => Or(types1.zipWithIndex map { case ((id1, type1), index) =>
- val newTe1 = TypedExpr(CaseClassSelector(def1, e1, id1), type1)
- val newTe2s = te2s.map({
- case (path, TypedExpr(e2, ContainerType(def2, types2))) =>
- val (id2, type2) = types2(index)
- (path, TypedExpr(CaseClassSelector(def2, e2, id2), type2))
- case (_, te2) => scala.sys.error("Unexpected input combinations: " + te1 + " " + te2)
- })
- _numericConverging(newTe1, newTe2s, cluster, checker)
+ def numericConverging(e1: Expr, e2s: Seq[(Seq[Expr], Expr)], cluster: Set[Chain], checker: TerminationChecker) : Expr = e1.getType match {
+ case ContainerType(def1, fields1) => Or(fields1.zipWithIndex map { case ((id1, type1), index) =>
+ numericConverging(CaseClassSelector(def1, e1, id1), e2s.map { case (path, e2) =>
+ e2.getType match {
+ case ContainerType(def2, fields2) => (path, CaseClassSelector(def2, e2, fields2(index)._1))
+ case _ => scala.sys.error("Unexpected input combination: " + e1 + " " + e2)
+ }
+ }, cluster, checker)
})
- case TypedExpr(e1, TupleType(types1)) => Or(types1.zipWithIndex map { case (type1, index) =>
- val newTe1 = TypedExpr(TupleSelect(e1, index + 1), type1)
- val newTe2s = te2s.map({
- case (path, TypedExpr(e2, TupleType(types2))) => (path, TypedExpr(TupleSelect(e2, index + 1), types2(index)))
- case (_, te2) => scala.sys.error("Unexpected input combinations: " + te1 + " " + te2)
- })
- _numericConverging(newTe1, newTe2s, cluster, checker)
+ case TupleType(types) => Or((0 until types.length) map { case index =>
+ numericConverging(TupleSelect(e1, index + 1), e2s.map { case (path, e2) =>
+ e2.getType match {
+ case TupleType(_) => (path, TupleSelect(e2, index + 1))
+ case _ => scala.sys.error("Unexpected input combination: " + e1 + " " + e2)
+ }
+ }, cluster, checker)
})
- case TypedExpr(e1, Int32Type) => numericEndpoint(e1, cluster, checker) match {
- case UpperBoundEndpoint => And(te2s map {
- case (path, TypedExpr(e2, Int32Type)) => Implies(And(path), GreaterThan(e1, e2))
- case (_, te2) => scala.sys.error("Unexpected input combinations: " + te1 + " " + te2)
+ case Int32Type => numericEndpoint(e1, cluster, checker) match {
+ case UpperBoundEndpoint => And(e2s map {
+ case (path, e2) if e2.getType == Int32Type => Implies(And(path), GreaterThan(e1, e2))
+ case (_, e2) => scala.sys.error("Unexpected input combinations: " + e1 + " " + e2)
})
- case LowerBoundEndpoint => And(te2s map {
- case (path, TypedExpr(e2, Int32Type)) => Implies(And(path), LessThan(e1, e2))
- case (_, te2) => scala.sys.error("Unexpected input combinations: " + te1 + " " + te2)
+ case LowerBoundEndpoint => And(e2s map {
+ case (path, e2) if e2.getType == Int32Type => Implies(And(path), LessThan(e1, e2))
+ case (_, e2) => scala.sys.error("Unexpected input combinations: " + e1 + " " + e2)
})
- case AnyEndpoint => Or(And(te2s map {
- case (path, TypedExpr(e2, Int32Type)) => Implies(And(path), GreaterThan(e1, e2))
- case (_, te2) => scala.sys.error("Unexpected input combinations: " + te1 + " " + te2)
- }), And(te2s map {
- case (path, TypedExpr(e2, Int32Type)) => Implies(And(path), LessThan(e1, e2))
- case (_, te2) => scala.sys.error("Unexpected input combinations: " + te1 + " " + te2)
+ case AnyEndpoint => Or(And(e2s map {
+ case (path, e2) if e2.getType == Int32Type => Implies(And(path), GreaterThan(e1, e2))
+ case (_, e2) => scala.sys.error("Unexpected input combinations: " + e1 + " " + e2)
+ }), And(e2s map {
+ case (path, e2) if e2.getType == Int32Type => Implies(And(path), LessThan(e1, e2))
+ case (_, e2) => scala.sys.error("Unexpected input combinations: " + e1 + " " + e2)
}))
case InnerEndpoint => BooleanLiteral(false)
case NoEndpoint => BooleanLiteral(false)
}
- case TypedExpr(_, _: ClassType) => BooleanLiteral(false)
- case TypedExpr(_, BooleanType) => BooleanLiteral(false)
- case _ => scala.sys.error("Unexpected type " + te1.tpe)
+ case _: ClassType => BooleanLiteral(false)
+ case BooleanType => BooleanLiteral(false)
+ case tpe => scala.sys.error("Unexpected type " + tpe)
}
}
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index 06c98ed31..2d6ad5b41 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -56,7 +56,7 @@ class ChainProcessor(checker: TerminationChecker) extends Processor(checker) wit
all.map(cluster => cluster.toSeq.sortBy(_.size).foldLeft(Set[Chain]())({ case (acc, chain) =>
val chainElements : Set[Relation] = chain.chain.toSet
val seenElements : Set[Relation] = acc.map(_.chain).flatten.toSet
- if (chainElements -- seenElements nonEmpty) acc + chain else acc
+ if ((chainElements -- seenElements).nonEmpty) acc + chain else acc
})).filter(_.nonEmpty)
}
@@ -119,10 +119,10 @@ class ChainProcessor(checker: TerminationChecker) extends Processor(checker) wit
val (okPairs, nokPairs) = numericCleared.partition(_._2.isEmpty)
val nok = nokPairs.map(_._1).toSet
val (ok, transitiveNok) = okPairs.map(_._1).partition({ fd =>
- checker.program.transitiveCallees(fd) intersect nok isEmpty
+ (checker.program.transitiveCallees(fd) intersect nok).isEmpty
})
val allNok = nok ++ transitiveNok
- val newProblems = if (allNok nonEmpty) List(Problem(allNok)) else Nil
+ val newProblems = if (allNok.nonEmpty) List(Problem(allNok)) else Nil
(ok.map(Cleared(_)), newProblems)
}
}
diff --git a/src/main/scala/leon/termination/ComponentProcessor.scala b/src/main/scala/leon/termination/ComponentProcessor.scala
index 58d1da4a5..1e980370b 100644
--- a/src/main/scala/leon/termination/ComponentProcessor.scala
+++ b/src/main/scala/leon/termination/ComponentProcessor.scala
@@ -26,8 +26,8 @@ class ComponentProcessor(checker: TerminationChecker) extends Processor(checker)
})
val terminating = problem.funDefs.filter(terminates(_))
- assert(components.forall(scc => (scc subsetOf terminating) || (scc intersect terminating isEmpty)))
- val newProblems = components.filter(scc => scc intersect terminating isEmpty).map(Problem(_))
+ assert(components.forall(scc => (scc subsetOf terminating) || (scc intersect terminating).isEmpty))
+ val newProblems = components.filter(scc => (scc intersect terminating).isEmpty).map(Problem(_))
(terminating.map(Cleared(_)), newProblems)
}
}
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index 299d5b338..e230c8701 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -23,31 +23,36 @@ abstract class Processor(val checker: TerminationChecker) {
val reporter = checker.context.reporter
- def run(problem: Problem): (TraversableOnce[Result], TraversableOnce[Problem])
+ protected def run(problem: Problem): (TraversableOnce[Result], TraversableOnce[Problem])
+
+ def process(problem: Problem): (TraversableOnce[Result], TraversableOnce[Problem]) = run(problem)
}
object Solvable {
import scala.collection.mutable.{Set => MutableSet}
private val strengthened : MutableSet[FunDef] = MutableSet()
- private def strengthenPostcondition(funDef: FunDef, cmp: (Expr, TypedExpr) => Expr)
+ private def strengthenPostcondition(funDef: FunDef, cmp: (Expr, Expr) => Expr)
(implicit solver: Processor with Solvable) : Boolean = if (!funDef.hasBody) false else {
assert(solver.checker.terminates(funDef).isGuaranteed)
- val postcondition = funDef.postcondition
- val args = funDef.args.map(_.toVariable)
- val typedResult = TypedExpr(ResultVariable(), funDef.returnType)
- val sizePost = cmp(Tuple(args), typedResult)
- funDef.postcondition = Some(And(postcondition.toSeq :+ sizePost))
+ val old = funDef.postcondition
+ val (res, postcondition) = {
+ val (res, post) = old.getOrElse(FreshIdentifier("res").setType(funDef.returnType) -> BooleanLiteral(true))
+ val args = funDef.args.map(_.toVariable)
+ val sizePost = cmp(Tuple(funDef.args.map(_.toVariable)), res.toVariable)
+ (res, And(post, sizePost))
+ }
+
+ funDef.postcondition = Some(res -> postcondition)
val prec = matchToIfThenElse(funDef.precondition.getOrElse(BooleanLiteral(true)))
- val post = matchToIfThenElse(funDef.postcondition.get)
val body = matchToIfThenElse(funDef.body.get)
- val resFresh = FreshIdentifier("result", true).setType(body.getType)
- val formula = Implies(prec, Let(resFresh, body, replace(Map(ResultVariable() -> Variable(resFresh)), post)))
+ val post = matchToIfThenElse(postcondition)
+ val formula = Implies(prec, Let(res, body, post))
if (!solver.isAlwaysSAT(formula)) {
- funDef.postcondition = postcondition
+ funDef.postcondition = old
strengthened.add(funDef)
false
} else {
@@ -74,19 +79,36 @@ object Solvable {
trait Solvable { self: Processor =>
- private var solvers: List[Solver] = null
+ override def process(problem: Problem): (TraversableOnce[Result], TraversableOnce[Problem]) = {
+ try {
+ self.run(problem)
+ } finally {
+ destroySolvers
+ }
+ }
+
+ private var solvers: List[SolverFactory[Solver]] = null
+ private var lastDefs: Set[FunDef] = Set()
def strengthenPostconditions(funDefs: Set[FunDef]) = Solvable.strengthenPostconditions(funDefs)(this)
private def initSolvers {
- val program : Program = self.checker.program
- val allDefs : Seq[Definition] = program.mainObject.defs ++ StructuralSize.defs
- val newProgram : Program = program.copy(mainObject = program.mainObject.copy(defs = allDefs))
- val context : LeonContext = self.checker.context.copy(reporter = new QuietReporter())
-
- val solvers0 = new TrivialSolver(context) :: new FairZ3Solver(context) :: Nil
- solvers = solvers0.map(new TimeoutSolver(_, 500))
- solvers.foreach(_.setProgram(newProgram))
+ val structDefs = StructuralSize.defs
+ if (structDefs != lastDefs || solvers == null) {
+ destroySolvers
+
+ val program : Program = self.checker.program
+ val allDefs : Seq[Definition] = program.mainObject.defs ++ structDefs
+ val newProgram : Program = program.copy(mainObject = program.mainObject.copy(defs = allDefs))
+ val context : LeonContext = self.checker.context
+
+ val solvers0 = new FairZ3SolverFactory(context, newProgram) :: Nil
+ solvers = solvers0.map(_.withTimeout(500))
+ }
+ }
+
+ protected def destroySolvers {
+ if (solvers != null) solvers.foreach(_.free())
}
type Solution = (Option[Boolean], Map[Identifier, Expr])
@@ -104,19 +126,11 @@ trait Solvable { self: Processor =>
val expr = searchAndReplace(dangerousCallsMap.get, recursive=false)(problem)
object Solved {
- var superseeded : Set[String] = Set.empty[String]
- def unapply(se: Solver): Option[Solution] = {
- if(superseeded(se.name) || superseeded(se.description)) {
- None
- } else {
- superseeded = superseeded ++ Set(se.superseeds: _*)
-
- se.init()
- val (satResult, model) = se.solveSAT(expr)
-
- if (!satResult.isDefined) None
- else Some(satResult, model)
- }
+ def unapply(se: SolverFactory[Solver]): Option[Solution] = {
+ val (satResult, model) = SimpleSolverAPI(se).solveSAT(expr)
+
+ if (!satResult.isDefined) None
+ else Some(satResult -> model)
}
}
@@ -176,7 +190,7 @@ class ProcessingPipeline(program: Program, context: LeonContext, _processors: Pr
def clear(fd: FunDef) : Boolean = {
lazy val unsolvedDefs = unsolved.map(_.funDefs).flatten.toSet
lazy val problemDefs = problems.map({ case (problem, _) => problem.funDefs }).flatten.toSet
- def issue(defs: Set[FunDef]) : Boolean = defs(fd) || (defs intersect program.transitiveCallees(fd) nonEmpty)
+ def issue(defs: Set[FunDef]) : Boolean = defs(fd) || (defs intersect program.transitiveCallees(fd)).nonEmpty
! (issue(unsolvedDefs) || issue(problemDefs))
}
@@ -192,7 +206,7 @@ class ProcessingPipeline(program: Program, context: LeonContext, _processors: Pr
printQueue
val (problem, index) = problems.head
val processor : Processor = processors(index)
- val (_results, nextProblems) = processor.run(problem)
+ val (_results, nextProblems) = processor.process(problem)
val results = _results.toList
printResult(results)
diff --git a/src/main/scala/leon/termination/RelationBuilder.scala b/src/main/scala/leon/termination/RelationBuilder.scala
index 8e50fcecb..11b411b0a 100644
--- a/src/main/scala/leon/termination/RelationBuilder.scala
+++ b/src/main/scala/leon/termination/RelationBuilder.scala
@@ -33,9 +33,9 @@ object RelationBuilder {
val vb = visit(b, Equals(Variable(i), e) :: path)
ve ++ vb
- case IfExpr(cond, then, elze) =>
+ case IfExpr(cond, thenn, elze) =>
val vc = visit(cond, path)
- val vt = visit(then, cond :: path)
+ val vt = visit(thenn, cond :: path)
val ve = visit(elze, Not(cond) :: path)
vc ++ vt ++ ve
@@ -44,14 +44,14 @@ object RelationBuilder {
case x :: xs => visit(x, p ++ path) ++ resolveAnds(xs, x :: p)
case Nil => Set()
}
- resolveAnds(es toList, Nil)
+ resolveAnds(es.toList, Nil)
case Or(es) =>
def resolveOrs(ors: List[Expr], p: List[Expr]): Set[Relation] = ors match {
case x :: xs => visit(x, p ++ path) ++ resolveOrs(xs, Not(x) :: p)
case Nil => Set()
}
- resolveOrs(es toList, Nil)
+ resolveOrs(es.toList, Nil)
case UnaryOperator(e, _) => visit(e, path)
@@ -65,9 +65,9 @@ object RelationBuilder {
}
val precondition = funDef.precondition getOrElse BooleanLiteral(true)
- val precRelations = funDef.precondition.map(e => visit(simplifyLets(matchToIfThenElse(e)), Nil)).flatten.toSet
- val bodyRelations = funDef.body.map(e => visit(simplifyLets(matchToIfThenElse(e)), List(precondition))).flatten.toSet
- val postRelations = funDef.postcondition.map(e => visit(simplifyLets(matchToIfThenElse(e)), Nil)).flatten.toSet
+ val precRelations = funDef.precondition.map(e => visit(simplifyLets(matchToIfThenElse(e)), Nil)) getOrElse Set()
+ val bodyRelations = funDef.body.map(e => visit(simplifyLets(matchToIfThenElse(e)), List(precondition))) getOrElse Set()
+ val postRelations = funDef.postcondition.map(e => visit(simplifyLets(matchToIfThenElse(e._2)), Nil)) getOrElse Set()
val relations = precRelations ++ bodyRelations ++ postRelations
relationCache(funDef) = relations
relations
diff --git a/src/main/scala/leon/termination/RelationComparator.scala b/src/main/scala/leon/termination/RelationComparator.scala
index e6a6c9721..9f3985b2c 100644
--- a/src/main/scala/leon/termination/RelationComparator.scala
+++ b/src/main/scala/leon/termination/RelationComparator.scala
@@ -12,15 +12,9 @@ object RelationComparator {
def init : Unit = StructuralSize.init
- def sizeDecreasing(e1: TypedExpr, e2: TypedExpr) = GreaterThan(size(e1), size(e2))
- def sizeDecreasing(e1: Expr, e2: TypedExpr) = GreaterThan(size(e1), size(e2))
- def sizeDecreasing(e1: TypedExpr, e2: Expr) = GreaterThan(size(e1), size(e2))
- def sizeDecreasing(e1: Expr, e2: Expr) = GreaterThan(size(e1), size(e2))
+ def sizeDecreasing(e1: Expr, e2: Expr) = GreaterThan(size(e1), size(e2))
- def softDecreasing(e1: TypedExpr, e2: TypedExpr) = GreaterEquals(size(e1), size(e2))
- def softDecreasing(e1: Expr, e2: TypedExpr) = GreaterEquals(size(e1), size(e2))
- def softDecreasing(e1: TypedExpr, e2: Expr) = GreaterEquals(size(e1), size(e2))
- def softDecreasing(e1: Expr, e2: Expr) = GreaterEquals(size(e1), size(e2))
+ def softDecreasing(e1: Expr, e2: Expr) = GreaterEquals(size(e1), size(e2))
}
// vim: set ts=4 sw=4 et:
diff --git a/src/main/scala/leon/termination/RelationProcessor.scala b/src/main/scala/leon/termination/RelationProcessor.scala
index 4f2786528..24527eb92 100644
--- a/src/main/scala/leon/termination/RelationProcessor.scala
+++ b/src/main/scala/leon/termination/RelationProcessor.scala
@@ -70,7 +70,7 @@ class RelationProcessor(checker: TerminationChecker) extends Processor(checker)
assert(terminating ++ nonTerminating == problem.funDefs)
val results = terminating.map(Cleared(_)).toList
- val newProblems = if (problem.funDefs intersect nonTerminating nonEmpty) List(Problem(nonTerminating)) else Nil
+ val newProblems = if ((problem.funDefs intersect nonTerminating).nonEmpty) List(Problem(nonTerminating)) else Nil
(results, newProblems)
}
}
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 412c48660..c85f24085 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -7,18 +7,11 @@ import purescala.TypeTrees._
import purescala.Definitions._
import purescala.Common._
-case class TypedExpr(expr: Expr, tpe: TypeTree)
-
object StructuralSize {
import scala.collection.mutable.{Map => MutableMap}
- implicit def exprToTypedExpr(expr: Expr): TypedExpr = {
- assert(expr.getType != Untyped)
- TypedExpr(expr, expr.getType)
- }
-
private val sizeFunctionCache : MutableMap[TypeTree, FunDef] = MutableMap()
- def size(typedExpr: TypedExpr) : Expr = {
+ def size(expr: Expr) : Expr = {
def funDef(tpe: TypeTree, cases: => Seq[MatchCase]) = {
// we want to reuse generic size functions for sub-types
val argumentType = tpe match {
@@ -34,12 +27,13 @@ object StructuralSize {
sizeFunctionCache(argumentType) = fd
val body = simplifyLets(matchToIfThenElse(MatchExpr(argument.toVariable, cases)))
+ val postId = FreshIdentifier("res", false).setType(Int32Type)
val postSubcalls = functionCallsOf(body).map(GreaterThan(_, IntLiteral(0))).toSeq
- val postRecursive = GreaterThan(ResultVariable(), IntLiteral(0))
+ val postRecursive = GreaterThan(Variable(postId), IntLiteral(0))
val postcondition = And(postSubcalls :+ postRecursive)
fd.body = Some(body)
- fd.postcondition = Some(postcondition)
+ fd.postcondition = Some(postId, postcondition)
fd
}
}
@@ -48,20 +42,20 @@ object StructuralSize {
val c = _c.asInstanceOf[CaseClassDef] // 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(TypedExpr(Variable(p._2), p._1.tpe)))
+ val sizes = arguments.map(p => size(Variable(p._2)))
val result = sizes.foldLeft[Expr](IntLiteral(1))(Plus(_,_))
SimpleCase(CaseClassPattern(None, c, argumentPatterns), result)
}
- typedExpr match {
- case TypedExpr(expr, a: AbstractClassType) =>
+ expr.getType match {
+ case a: AbstractClassType =>
val sizeFd = funDef(a, a.classDef.knownChildren map caseClassType2MatchCase)
FunctionInvocation(sizeFd, Seq(expr))
- case TypedExpr(expr, c: CaseClassType) =>
+ case c: CaseClassType =>
val sizeFd = funDef(c, Seq(caseClassType2MatchCase(c.classDef)))
FunctionInvocation(sizeFd, Seq(expr))
- case TypedExpr(expr, TupleType(argTypes)) => argTypes.zipWithIndex.map({
- case (tpe, index) => size(TypedExpr(TupleSelect(expr, index + 1), tpe))
+ case TupleType(argTypes) => argTypes.zipWithIndex.map({
+ case (_, index) => size(TupleSelect(expr, index + 1))
}).foldLeft[Expr](IntLiteral(0))(Plus(_,_))
case _ => IntLiteral(0)
}
diff --git a/src/test/resources/regression/termination/looping/Termination_failling1.scala b/src/test/resources/regression/termination/looping/Termination_failling1.scala
index 4904c9fc5..17b6be864 100644
--- a/src/test/resources/regression/termination/looping/Termination_failling1.scala
+++ b/src/test/resources/regression/termination/looping/Termination_failling1.scala
@@ -3,7 +3,7 @@ import leon.Utils._
object Termination {
abstract class List
case class Cons(head: Int, tail: List) extends List
- case class Nil extends List
+ case class Nil() extends List
def looping1(list: List) : Int = looping2(list)
diff --git a/src/test/resources/regression/termination/valid/ComplexChains.scala b/src/test/resources/regression/termination/valid/ComplexChains.scala
index 568e09bb1..68fad00ff 100644
--- a/src/test/resources/regression/termination/valid/ComplexChains.scala
+++ b/src/test/resources/regression/termination/valid/ComplexChains.scala
@@ -4,7 +4,7 @@ object ComplexChains {
abstract class List
case class Cons(head: Int, tail: List) extends List
- case class Nil extends List
+ case class Nil() extends List
def f1(list: List): List = list match {
case Cons(head, tail) if head > 0 => f2(Cons(1, list))
diff --git a/src/test/resources/regression/termination/valid/ListWithSize.scala b/src/test/resources/regression/termination/valid/ListWithSize.scala
index 868cb4556..4e236ae1f 100644
--- a/src/test/resources/regression/termination/valid/ListWithSize.scala
+++ b/src/test/resources/regression/termination/valid/ListWithSize.scala
@@ -49,7 +49,7 @@ object ListWithSize {
def sizesAreEquiv(l: List) : Boolean = {
size(l) == sizeTailRec(l)
- } holds
+ }.holds
def content(l: List) : Set[Int] = l match {
case Nil() => Set.empty[Int]
@@ -58,7 +58,7 @@ object ListWithSize {
def sizeAndContent(l: List) : Boolean = {
size(l) == 0 || content(l) != Set.empty[Int]
- } holds
+ }.holds
def drunk(l : List) : List = (l match {
case Nil() => Nil()
@@ -84,7 +84,7 @@ object ListWithSize {
}) ensuring(content(_) == content(l1) ++ content(l2))
@induct
- def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
+ def nilAppend(l : List) : Boolean = (append(l, Nil()) == l).holds
// unclear if we needed this--it was meant to force folding
//def appendFold(x : Int, xs : List, ys : List) : Boolean = {
@@ -93,7 +93,7 @@ object ListWithSize {
@induct
def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
- (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
+ (append(append(xs, ys), zs) == append(xs, append(ys, zs))).holds
def revAuxBroken(l1 : List, e : Int, l2 : List) : Boolean = {
(append(reverse(l1), Cons(e,l2)) == reverse0(l1, l2))
@@ -106,7 +106,7 @@ object ListWithSize {
@induct
def sizeAppend(l1 : List, l2 : List) : Boolean =
- (size(append(l1, l2)) == size(l1) + size(l2)) holds
+ (size(append(l1, l2)) == size(l1) + size(l2)).holds
// proved with unrolling=4
@induct
diff --git a/src/test/resources/regression/termination/valid/SimpInterpret.scala b/src/test/resources/regression/termination/valid/SimpInterpret.scala
index bcb7bafc8..fd56989f4 100644
--- a/src/test/resources/regression/termination/valid/SimpInterpret.scala
+++ b/src/test/resources/regression/termination/valid/SimpInterpret.scala
@@ -55,11 +55,11 @@ object Interpret {
def treeBad(t : IntTree) : Boolean = {
!(repOk(t) && computesPositive(t) && identityForPositive(t))
- } holds
+ }.holds
def thereIsGoodTree() : Boolean = {
!treeBad(If(Less(Const(0),Var()), Var(), Minus(Const(0),Var())))
- } holds
+ }.holds
def main(args : Array[String]) {
thereIsGoodTree()
diff --git a/src/test/resources/regression/termination/valid/Termination_passing1.scala b/src/test/resources/regression/termination/valid/Termination_passing1.scala
index fffb8bca9..ea86b6769 100644
--- a/src/test/resources/regression/termination/valid/Termination_passing1.scala
+++ b/src/test/resources/regression/termination/valid/Termination_passing1.scala
@@ -3,7 +3,7 @@ import leon.Utils._
object Termination {
abstract class List
case class Cons(head: Int, tail: List) extends List
- case class Nil extends List
+ case class Nil() extends List
def f1(list: List) : Int = f2(list)
diff --git a/src/test/scala/leon/test/termination/TerminationRegression.scala b/src/test/scala/leon/test/termination/TerminationRegression.scala
index 0ccc6c864..977da326d 100644
--- a/src/test/scala/leon/test/termination/TerminationRegression.scala
+++ b/src/test/scala/leon/test/termination/TerminationRegression.scala
@@ -6,13 +6,9 @@ package termination
import leon.termination._
-import org.scalatest.FunSuite
-
import java.io.File
-import TestUtils._
-
-class TerminationRegression extends FunSuite {
+class TerminationRegression extends LeonTestSuite {
private var counter : Int = 0
private def nextInt() : Int = {
counter += 1
@@ -21,7 +17,7 @@ class TerminationRegression extends FunSuite {
private case class Output(report : TerminationReport, reporter : Reporter)
private def mkPipeline : Pipeline[List[String],TerminationReport] =
- leon.plugin.ExtractionPhase andThen leon.SubtypingPhase andThen leon.termination.TerminationPhase
+ leon.plugin.ExtractionPhase andThen leon.utils.SubtypingPhase andThen leon.termination.TerminationPhase
private def mkTest(file : File, leonOptions: Seq[LeonOption], forError: Boolean)(block: Output=>Unit) = {
val fullName = file.getPath()
@@ -37,16 +33,15 @@ class TerminationRegression extends FunSuite {
assert(file.exists && file.isFile && file.canRead,
"Benchmark %s is not a readable file".format(displayName))
- val ctx = LeonContext(
+ val ctx = testContext.copy(
settings = Settings(
synthesis = false,
xlang = false,
verify = false,
termination = true
),
- options = leonOptions,
- files = List(file),
- reporter = new SilentReporter
+ options = leonOptions.toList,
+ files = List(file)
)
val pipeline = mkPipeline
--
GitLab