Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
93
Fig. 5. Runtime of boxing versus naive: scatter plot and ratio plot
Fig. 6. Size of interpolants in boxing versus naive and its impact on performance
5 Related work
The problem of reasoning about machine arithmetic and wrapping arises not only
in model checking, but abstract interpretation too, where solvers are augmented
with support for relaxing abstractions by join rather than interpolation.
Despite the long-standing work [3, 7, 27] in deciding BV theories, there has
been scant work on BV interpolation. Although not focussing on BV interpolation, an early work on deriving work-level interpolants [23] uses bit-vectors to
interpolate equality logic. This logic supports equations of the form x = y and
x = c where x and y are variables and c is drawn from a finite set of symbols C.
Bit-vectors with width log 2 (|C|) are used to bit-blast equations [29] so that
formulae are encoded entirely propositionally. Then a propositional resolution
proof of the inconsistence of two formulae is lifted to the work-level.
Seminal work by Griggio [16] advocated encoding BV formulae in theories of
increasing complexity. The pair of BV formulae are encoded in a theory whose
interpolation engine is used to find an interpolant in that theory. The interpolant
is then reinterpreted as a BV formula and tested to see if it is still an interpolant
the pair of BV formulae. The approach resorts to bit-blasting if no simpler theory can find an interpolant, at the cost of losing world-level information. By way
93
Fig. 5. Runtime of boxing versus naive: scatter plot and ratio plot
Fig. 6. Size of interpolants in boxing versus naive and its impact on performance
5 Related work
The problem of reasoning about machine arithmetic and wrapping arises not only
in model checking, but abstract interpretation too, where solvers are augmented
with support for relaxing abstractions by join rather than interpolation.
Despite the long-standing work [3, 7, 27] in deciding BV theories, there has
been scant work on BV interpolation. Although not focussing on BV interpolation, an early work on deriving work-level interpolants [23] uses bit-vectors to
interpolate equality logic. This logic supports equations of the form x = y and
x = c where x and y are variables and c is drawn from a finite set of symbols C.
Bit-vectors with width log 2 (|C|) are used to bit-blast equations [29] so that
formulae are encoded entirely propositionally. Then a propositional resolution
proof of the inconsistence of two formulae is lifted to the work-level.
Seminal work by Griggio [16] advocated encoding BV formulae in theories of
increasing complexity. The pair of BV formulae are encoded in a theory whose
interpolation engine is used to find an interpolant in that theory. The interpolant
is then reinterpreted as a BV formula and tested to see if it is still an interpolant
the pair of BV formulae. The approach resorts to bit-blasting if no simpler theory can find an interpolant, at the cost of losing world-level information. By way