Even more extended version of the InputAbsy simplifier that also rewrites certain array expression.
Class to simplify bit-vector expressions using information about the range of operands.
Extended version of the InputAbsy simplifier that also rewrites certain array expressions: \exists int a; x = store(a, b, c) is replaced with select(x, b) = c
Class representing the different kinds of partial interpolants that are used to annotate arithmetic literals.
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]
.
Abstract class providing some functionality commonly needed for interpolation-based software verification, e.g., axioms and prover for bitvector arithmetic, arrays, etc.
Class to store information about the value range of constants; this information is later used to simplify expressions
Module for simplifying a proof (certificate) by eliminating as many rounding steps as possible; this is currently done in a rather naive way
Class to simplify bit-vector expressions using information about the range of operands. In particular, bit-vector operations are replaced with simple Presburger operations if it is guaranteed that no overflows can occur