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.
Even more extended version of the InputAbsy simplifier that also rewrites certain array expression.
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