Class representing the different kinds of partial interpolants that are
used to annotate arithmetic literals. A partial interpolant carries a
"denominator", which represents a factor that the annotated arithmetic
literal has to be multiplied with to make the partial interpolant valid. E.g.
x = 0 [y = 0, 2] can be interpreted as equivalent to
2*x = 0 [y = 0, 1].
Class representing the different kinds of partial interpolants that are used to annotate arithmetic literals. A partial interpolant carries a "denominator", which represents a factor that the annotated arithmetic literal has to be multiplied with to make the partial interpolant valid. E.g.
x = 0 [y = 0, 2]
can be interpreted as equivalent to2*x = 0 [y = 0, 1]
.