vc explanations: add support for guarded fraction normal form

[Philipp15b]

To better be able to see patterns in the generated pres, especially from the @unroll proof rule (#19), a normalization of the pre could help. A normal form in the style of [b1] * quant1 * poly(vars)/poly(vars) + ... [bn] * quantn * poly(vars)/poly(vars) where poly(vars) are multivariate polynomials in terms of program variables.

For this normal form, expressions that cannot be simplified (such as a function call exp(2, x)) would be treated as another variable in the polynomial, and we would get e.g. [true] * 1 * exp(2, x).