Add debug option to dump blocker graph

[gsps]

Adds a debug section blocker-graph that dumps the (non-strict) implication graph among all blocking literals. The current graph is dumped at the end of checkAssumptions and saved in blocker-graphs/*file*-*n*.dot.

Nodes that correspond to defBlockers also contain the corresponding function name and the call site's position. The positional information is unreliable, since we only store the call site position when the callee's FunctionTemplate is first cached (the cache key being the TypedFunDef).

As an example, the following program requires multiple unfolding steps to prove the assertion in testUnfoldMe:

object MustUnfoldThriceExample {
  def unfoldMe(xs: List[BigInt]): BigInt = {
    require(xs.forall(_ >= 0))
    xs match {
      case Nil() => BigInt(0)
      case Cons(x, xs0) => x + unfoldMe(xs0)
    }
  } ensuring (_ >= 0)

  def testUnfoldMe(xs: List[BigInt]): Unit = {
    require(xs.size >= 3 && xs.forall(_ >= 0))
    val sum = unfoldMe(xs)
    assert(sum >= xs(0) + xs(1) + xs(2))
  }
}

Running with --debug=blocker-graph yields multiple .dot files, one of which corresponds to the assertion's VC:
must-unfold-thrice.pdf

@samarion Any preference on where to move the dot-graph-dumping code that new lives in checkAssumptions?

[samarion]

Maybe you could add an UnrollingDebugger trait similarly to the SMTLIBDebugger and have it override checkAssumptions?

[samarion]

Is the goal here to ensure that all calls in the dumped blocker graph have positions? If so, I don't think you need to set a position on this call because it should never be part of the blocker graph.

(If possible, I'd like to avoid making positions part of the FunctionTemplate API)