diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index 0c6106127ce7187ff4dded02b18863fcd332677b..f2410fd82cac6a518740a575230172a246d14e21 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -156,7 +156,7 @@ trait ChainBuilder extends RelationBuilder { self: Strengthener with RelationCom
if (!checker.program.callGraph.transitivelyCalls(fd, funDef)) {
Set.empty[FunDef] -> Set.empty[Chain]
} else if (fd == funDef) {
- Set.empty[FunDef] -> Set(Chain(chain.reverse))
+ Set(fd) -> Set(Chain(chain.reverse))
} else if (seen(fd)) {
Set(fd) -> Set.empty[Chain]
} else {
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index c5a8ccb69c870b16f91e1c1dcfa5cb933bc8138b..af50911bd46dfc0c3519ab885acd94416df57267 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -6,7 +6,7 @@ package termination
import purescala.Expressions._
import purescala.Common._
import purescala.Definitions._
-import purescala.Constructors.tupleWrap
+import purescala.Constructors._
class ChainProcessor(
val checker: TerminationChecker,
@@ -33,40 +33,37 @@ class ChainProcessor(
reporter.debug("-+> Multiple looping points, can't build chain proof")
None
} else {
+ val funDef = loopPoints.head
+ val chains = chainsMap(funDef)._2
- def exprs(fd: FunDef): (Expr, Seq[(Seq[Expr], Expr)], Set[Chain]) = {
- val fdChains = chainsMap(fd)._2
-
- val e1 = tupleWrap(fd.params.map(_.toVariable))
- val e2s = fdChains.toSeq.map { chain =>
- val freshParams = chain.finalParams.map(arg => FreshIdentifier(arg.id.name, arg.id.getType, true))
- (chain.loop(finalArgs = freshParams), tupleWrap(freshParams.map(_.toVariable)))
- }
-
- (e1, e2s, fdChains)
+ val e1 = tupleWrap(funDef.params.map(_.toVariable))
+ val e2s = chains.toSeq.map { chain =>
+ val freshParams = chain.finalParams.map(arg => FreshIdentifier(arg.id.name, arg.id.getType, true))
+ (chain.loop(finalArgs = freshParams), tupleWrap(freshParams.map(_.toVariable)))
}
- val funDefs = if (loopPoints.size == 1) Set(loopPoints.head) else problem.funSet
-
reporter.debug("-+> Searching for structural size decrease")
- val (se1, se2s, _) = exprs(funDefs.head)
- val structuralFormulas = modules.structuralDecreasing(se1, se2s)
+ val structuralFormulas = modules.structuralDecreasing(e1, e2s)
val structuralDecreasing = structuralFormulas.exists(formula => definitiveALL(formula))
reporter.debug("-+> Searching for numerical converging")
- // worth checking multiple funDefs as the endpoint discovery can be context sensitive
- val numericDecreasing = funDefs.exists { fd =>
- val (ne1, ne2s, fdChains) = exprs(fd)
- val numericFormulas = modules.numericConverging(ne1, ne2s, fdChains)
- numericFormulas.exists(formula => definitiveALL(formula))
- }
+ val numericFormulas = modules.numericConverging(e1, e2s, chains)
+ val numericDecreasing = numericFormulas.exists(formula => definitiveALL(formula))
if (structuralDecreasing || numericDecreasing)
Some(problem.funDefs map Cleared)
- else
- None
+ else {
+ val chainsUnlooping = chains.flatMap(c1 => chains.flatMap(c2 => c1 compose c2)).forall {
+ chain => !definitiveSATwithModel(andJoin(chain.loop())).isDefined
+ }
+
+ if (chainsUnlooping)
+ Some(problem.funDefs map Cleared)
+ else
+ None
+ }
}
}
}
diff --git a/src/main/scala/leon/termination/ProcessingPipeline.scala b/src/main/scala/leon/termination/ProcessingPipeline.scala
index d2bae17b326623178671a2fc7db26954e013057e..92a11c6452c88f49986cd9382cae9ed72f70619a 100644
--- a/src/main/scala/leon/termination/ProcessingPipeline.scala
+++ b/src/main/scala/leon/termination/ProcessingPipeline.scala
@@ -165,8 +165,8 @@ abstract class ProcessingPipeline(context: LeonContext, initProgram: Program) ex
val components = SCC.scc(callGraph)
for (fd <- funDefs -- components.toSet.flatten) clearedMap(fd) = "Non-recursive"
-
- components.map(fds => Problem(fds.toSeq))
+ val newProblems = components.filter(fds => fds.forall { fd => !terminationMap.isDefinedAt(fd) })
+ newProblems.map(fds => Problem(fds.toSeq))
}
def verifyTermination(funDef: FunDef): Unit = {
diff --git a/src/test/resources/regression/termination/valid/NNF.scala b/src/test/resources/regression/termination/valid/NNF.scala
new file mode 100644
index 0000000000000000000000000000000000000000..455cef7ec5201fd17edee71059dc38c9d7afa3d8
--- /dev/null
+++ b/src/test/resources/regression/termination/valid/NNF.scala
@@ -0,0 +1,99 @@
+import leon.lang._
+import leon.annotation._
+
+object PropositionalLogic {
+
+ sealed abstract class Formula
+ case class And(lhs: Formula, rhs: Formula) extends Formula
+ case class Or(lhs: Formula, rhs: Formula) extends Formula
+ case class Implies(lhs: Formula, rhs: Formula) extends Formula
+ case class Not(f: Formula) extends Formula
+ case class Literal(id: BigInt) extends Formula
+
+ def simplify(f: Formula): Formula = (f match {
+ case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
+ case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
+ case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
+ case Not(f) => Not(simplify(f))
+ case Literal(_) => f
+ }) ensuring(isSimplified(_))
+
+ def isSimplified(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Implies(_,_) => false
+ case Not(f) => isSimplified(f)
+ case Literal(_) => true
+ }
+
+ def nnf(formula: Formula): Formula = (formula match {
+ case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ case Implies(lhs, rhs) => nnf(Or(Not(lhs), rhs))
+ case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
+ case Not(Not(f)) => nnf(f)
+ case Not(Literal(_)) => formula
+ case Literal(_) => formula
+ }) ensuring(isNNF(_))
+
+ def isNNF(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Implies(lhs, rhs) => false
+ case Not(Literal(_)) => true
+ case Not(_) => false
+ case Literal(_) => true
+ }
+
+ def evalLit(id : BigInt) : Boolean = (id == 42) // could be any function
+ def eval(f: Formula) : Boolean = f match {
+ case And(lhs, rhs) => eval(lhs) && eval(rhs)
+ case Or(lhs, rhs) => eval(lhs) || eval(rhs)
+ case Implies(lhs, rhs) => !eval(lhs) || eval(rhs)
+ case Not(f) => !eval(f)
+ case Literal(id) => evalLit(id)
+ }
+
+ @induct
+ def simplifySemantics(f: Formula) : Boolean = {
+ eval(f) == eval(simplify(f))
+ } holds
+
+ // Note that matching is exhaustive due to precondition.
+ def vars(f: Formula): Set[BigInt] = {
+ require(isNNF(f))
+ f match {
+ case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Not(Literal(i)) => Set[BigInt](i)
+ case Literal(i) => Set[BigInt](i)
+ }
+ }
+
+ def fv(f : Formula) = { vars(nnf(f)) }
+
+ @induct
+ def wrongCommutative(f: Formula) : Boolean = {
+ nnf(simplify(f)) == simplify(nnf(f))
+ } holds
+
+ @induct
+ def simplifyPreservesNNF(f: Formula) : Boolean = {
+ require(isNNF(f))
+ isNNF(simplify(f))
+ } holds
+
+ @induct
+ def nnfIsStable(f: Formula) : Boolean = {
+ require(isNNF(f))
+ nnf(f) == f
+ } holds
+
+ @induct
+ def simplifyIsStable(f: Formula) : Boolean = {
+ require(isSimplified(f))
+ simplify(f) == f
+ } holds
+}