Extend termination ChainProcessor to single-inlinings

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 {

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
+      }
     }
   }
 }

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 = {

src/test/resources/regression/termination/valid/NNF.scala

+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
+}