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?