diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index cc8003c5ab9e9baafce014471dd47bd98d772cde..ea08be2f4f3fcd523679e4fe11d396cbe0cd3c13 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 741b7c2b65cbd5084d028dc1480658dd935aa1ad..f6ec38673dd707f0f3a3840065ed61561fe6dadc 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 9a6352a2a59460f021cb085d93d99df5dbb8aee4..278b4bc50ff46629ab0f8bb4062f182ee11a0421 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 06c98ed31e9bff826aa4f36906c6f34b1e9fe14c..2d6ad5b412451f60e8de81552c8e743457329101 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 58d1da4a538ffdcf932377969840ddcae7a4d4e0..1e980370b31e4a3808ce7a9110cbadd1112629b8 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 299d5b338c7ea976df17da2527cac72fa11db795..e230c870170d9dcf6986c629d598295ecad73565 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 8e50fcecbf530dd4c58585d0fe5c5a82476a2098..11b411b0a88aaeff961ca7ff40611543fd877742 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 e6a6c9721683d4b7636f931752e1b7974dbcd4ab..9f3985b2c74d771e15cb88e253b6c1b6f9bb2586 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 4f2786528b45daa95f8be11dda4c3fd60942746a..24527eb92aea5713b26602343a4ebf949a06be7e 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 412c486604fd848ab2328a809c6b86bd799fe1ff..c85f2408564a0ca513f2b3b4361e48c80cc975fd 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 4904c9fc57b2357a32bafe672f977c5732c24e48..17b6be8645527074b5f95b0d0012d5b10c4691c7 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 568e09bb1215d7a5db11c3c87870e1867834fcd6..68fad00ff27e5db7529c861a59f662af6e43a62f 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 868cb45561e95552e10b8310c1a17f321515f89b..4e236ae1f7ffac822c932a46168ee31a752b7831 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 bcb7bafc8648364441b380f06933ecf602b1d6f4..fd56989f4a4597e2b9e39fb19acdabd0d2cd6d93 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 fffb8bca90176257ab730d6a8329eafc73d625e4..ea86b67694431ef9efa7eadb30b0a08cac30b4ea 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 0ccc6c8645741f6adfb369dfc2658e29afc6fa93..977da326df20af53b965adb61512c66c25754cce 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