Add debug option to dump blocker graph

src/main/scala/inox/Main.scala

@@ -12,6 +12,7 @@ trait MainHelpers {
     utils.DebugSectionTimers,
     solvers.DebugSectionSolver,
     solvers.smtlib.DebugSectionSMT,
+    solvers.unrolling.DebugSectionBlockerGraph,
     tip.DebugSectionTip
   )
 

src/main/scala/inox/ast/SymbolOps.scala

@@ -63,7 +63,7 @@ trait SymbolOps { self: TypeOps =>
 
 
   /** Override point for transformer with PC creation
-    * 
+    *
     * Note that we don't actually need the `PathProvider[P]` here but it will
     * become useful in the Stainless overrides. */
   protected def transformerWithPC[P <: PathLike[P]](
@@ -247,7 +247,7 @@ trait SymbolOps { self: TypeOps =>
     }
 
     def evalChildren(e: Expr)(implicit opts: PurityOptions): Expr = e match {
-      case Operator(es, recons) => recons(es.map(rec))
+      case Operator(es, recons) => recons(es.map(rec)).copiedFrom(e)
     }
 
     // TODO: Should we run this within a fixpoint with simplifyByConstructor?
@@ -398,7 +398,7 @@ trait SymbolOps { self: TypeOps =>
       class Liftable(path: Path) {
         def unapply(e: Expr): Option[Seq[Expr]] = {
           // The set of minimal conditions that must be met for an expression to be liftable
-          val minimal = 
+          val minimal =
             (isSimple(e) || !onlySimple)           && // check whether we want only simple expression
             !containsChoose(e)                     && // expressions containing chooses can't be lifted
             (!inFunction || !containsRecursive(e))    // recursive functions can't be lifted from lambdas
@@ -438,7 +438,7 @@ trait SymbolOps { self: TypeOps =>
               preserveApps
             ) =>
               val Operator(es, recons) = e
-              recons(es.map(op(_, env)))
+              recons(es.map(op(_, env))).copiedFrom(e)
 
             case Let(vd, e @ liftable(conditions), b) =>
               subst(vd.toVariable) = (e, conditions)
@@ -501,7 +501,7 @@ trait SymbolOps { self: TypeOps =>
               val lambda = Lambda(params, recons(esWithParams.map {
                 case (_, Some(vd)) => vd.toVariable
                 case (e, _) => e
-              }))
+              }).copiedFrom(e))
 
               Application(
                 getVariable(lambda, lambda.getType, conditions = conditions),
@@ -511,7 +511,7 @@ trait SymbolOps { self: TypeOps =>
             case _ =>
               val (ids, vs, es, tps, flags, recons) = deconstructor.deconstruct(e)
               val newVs = vs map transformVar
-              op.sup(recons(ids, newVs, es, tps, flags), env)
+              op.sup(recons(ids, newVs, es, tps, flags).copiedFrom(e), env)
           }
         },
         (tpe, env, op) => transformType(vars, tpe, inFunction, env)
@@ -695,7 +695,7 @@ trait SymbolOps { self: TypeOps =>
       case Forall(args, body) =>
         Forall(args, rec(body, lambdas, true))
       case Operator(es, recons) =>
-        recons(es.map(rec(_, lambdas, inForall)))
+        recons(es.map(rec(_, lambdas, inForall))).copiedFrom(e)
     }
 
     rec(e, Map.empty, false)

src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala

@@ -33,12 +33,13 @@ trait FunctionTemplates { self: Templates =>
   object FunctionTemplate {
     private val cache: MutableMap[TypedFunDef, FunctionTemplate] = MutableMap.empty
 
-    def apply(tfd: TypedFunDef): FunctionTemplate = cache.getOrElse(tfd, {
+    def apply(tfd: TypedFunDef, pos: utils.Position): FunctionTemplate = cache.getOrElse(tfd, {
       val body: Expr = timers.solvers.simplify.run { simplifyFormula(tfd.fullBody) }
 
       val tpVars = tfd.tps.flatMap(variableSeq).distinct
       val fdArgs: Seq[Variable] = tfd.params.map(_.toVariable)
-      val call: Expr = tfd.applied(fdArgs)
+      // Note: This position is best-effort, since function templates are cached.
+      val call: Expr = tfd.applied(fdArgs).setPos(pos)
 
       val start = Variable.fresh("start", BooleanType(), true)
       val pathVar = start -> encodeSymbol(start)
@@ -237,7 +238,7 @@ trait FunctionTemplates { self: Templates =>
                 val templateClauses = Template.instantiate(clauses, calls, apps, matchers, equalities, substMap)
                 substClauses ++ templateClauses
               } getOrElse {
-                FunctionTemplate(tfd).instantiate(defBlocker, args ++ tpSubst)
+                FunctionTemplate(tfd, call.getPos).instantiate(defBlocker, args ++ tpSubst)
               }
             }
 

src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala

@@ -141,7 +141,7 @@ trait TemplateGenerator { self: Templates =>
         newArg
       }
 
-      val newCall = thenCall.tfd.applied(newArgs)
+      val newCall = thenCall.tfd.applied(newArgs).copiedFrom(thenCall)
       builder.storeGuarded(newBlocker, Equals(newExpr, newCall))
     }
 
@@ -514,7 +514,7 @@ trait TemplateGenerator { self: Templates =>
         storeEquality(pathVar, re1, re2)
         Application(v, Seq(re1, re2))
 
-      case Operator(as, r) => r(as.map(a => rec(pathVar, a, None)))
+      case Operator(as, recons) => recons(as.map(a => rec(pathVar, a, None))).copiedFrom(expr)
     }
 
     val p = rec(pathVar, expr, polarity)
@@ -578,7 +578,7 @@ trait TemplateGenerator { self: Templates =>
         and(
           sort.invariant
             .filter(_ => generator == FreeGenerator)
-            .map(_.applied(Seq(expr)))
+            .map(tfd => tfd.applied(Seq(expr)).copiedFrom(tfd))
             .getOrElse(BooleanLiteral(true)),
           if (sort.definition.isInductive && !state.recurseAdt) {
             storeType(pathVar, tpe, expr)

src/main/scala/inox/solvers/unrolling/Templates.scala

@@ -177,6 +177,18 @@ trait Templates
     if (equal.nonEmpty) equal else (condImplied(b) + b)
   })(bs).filter(_ != trueT)
 
+  def blockerGraph(strict: Boolean = true): Graphs.DiGraph[Encoded, Graphs.SimpleEdge[Encoded]] = {
+    var implies = condImplies.toSeq.toMap
+    if (!strict)
+      implies = implies merge potImplies.toSeq.toMap
+    val nodes = implies.keySet ++ implies.values.flatten
+    val edges = implies.iterator
+      .flatMap(imp => imp._2.map(imp._1 -> _))
+      .map(e => Graphs.SimpleEdge(e._1, e._2))
+      .toSet
+    Graphs.DiGraph(nodes, edges)
+  }
+
   def promoteBlocker(b: Encoded, force: Boolean = false): Boolean = {
     var seen: Set[Encoded] = Set.empty
     var promoted: Boolean = false
@@ -226,7 +238,7 @@ trait Templates
   }
 
   /** Represents a named function call in the unfolding procedure */
-  case class Call(tfd: TypedFunDef, args: Seq[Arg], tpSubst: Seq[Arg]) {
+  case class Call(tfd: TypedFunDef, args: Seq[Arg], tpSubst: Seq[Arg]) extends utils.Positioned {
     override def toString: String = {
       def pArgs(args: Seq[Arg]): String = args.map {
         case Right(m) => m.toString
@@ -246,7 +258,7 @@ trait Templates
     def substitute(substituter: Encoded => Encoded, msubst: Map[Encoded, Matcher]): Call = copy(
       args = args.map(_.substitute(substituter, msubst)),
       tpSubst = tpSubst.map(_.substitute(substituter, msubst))
-    )
+    ).setPos(this.getPos)
   }
 
   /** Represents an application of a first-class function in the unfolding procedure */
@@ -594,9 +606,10 @@ trait Templates
       val calls = exprOps.collect[FunctionInvocation] {
         case fi: FunctionInvocation => Set(fi)
         case _ => Set.empty
-      } (expr).map { case FunctionInvocation(id, tps, args) =>
+      } (expr).map { case fi @ FunctionInvocation(id, tps, args) =>
         val tpVars = tps.flatMap(variableSeq).distinct
         Call(getFunction(id, tps), args.map(encodeArg), tpVars.map(encodeArg))
+          .setPos(fi.getPos)
       }.filter { case Call(tfd, args, _) =>
         !optCall.exists(p => p._1 == tfd && p._2 == args)
       }

src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala

@@ -23,6 +23,10 @@ object optModelFinding      extends IntOptionDef("model-finding", 0, "<PosInt> |
   })
 }
 
+object DebugSectionBlockerGraph extends inox.DebugSection("blocker-graph")
+
+private[unrolling] object DebugBlockerGraphFileNumbers extends UniqueCounter[String]
+
 trait AbstractUnrollingSolver extends Solver { self =>
 
   import context._
@@ -826,6 +830,29 @@ trait AbstractUnrollingSolver extends Solver { self =>
       }
     }
 
+    reporter.whenDebug(DebugSectionBlockerGraph) { debug =>
+      val file = options.findOptionOrDefault(Main.optFiles).headOption.map(_.getName).getOrElse("NA")
+      val n = DebugBlockerGraphFileNumbers.next(file)
+      val fileName = s"blocker-graphs/$file-$n.dot"
+
+      val javaFile = new java.io.File(fileName)
+      javaFile.getParentFile.mkdirs()
+
+      debug(s"Outputting blocker graph into $fileName")
+
+      val calls = templates.getCalls
+      val callsMap = calls.toMap
+      assert(calls.size == callsMap.size)
+
+      type Graph = Graphs.DiGraph[Encoded, Graphs.SimpleEdge[Encoded]]
+      val printer = new GraphPrinters.DotPrinter[Encoded, Graphs.SimpleEdge[Encoded], Graph]()
+      printer.setNodeLabel { n =>
+        val callStr = callsMap.get(n).map(call => s"\n(${call.tfd.id} @ ${call.getPos})").getOrElse("")
+        s"$n$callStr"
+      }
+      printer.asFile(templates.blockerGraph(strict = false), fileName)
+    }
+
     val CheckResult(res) = currentState
     res
   }).recover {