80
T. Okudono and A. King
Context As solvers for richer theories have evolved so have interpolation engines
for these theories, with a notable flurry of activity around one decade ago [10, 11,
19, 20, 23, 24, 30]. However, progress on the important theory of bit-vectors (BV)
has been surprisingly slow, the two key works [2, 16] taking opposing approaches.
One takes advantage of existing interpolation engines [16] and the another develops a bespoke interpolation engine around lazy reduction [2], which supports
bit-vector operations by expanding them, on demand, to Presburger arithmetic
[2]. This paper develops the former approach, aiming to use an LIA solver as is.
The central problem in bit-vector interpolation is to construct an interpolant
which is compact (one might even say beautiful [1]). Although a pair of inconsistent BV formulae can always be bit-blasted (unfolded) into a pair of inconsistent
propositional formulae, it is not always obvious how the resulting propositional
interpolant can be folded back into a compact bit-vector (BV) formula to derive
a BV interpolant. Interpolation engines over linear integer arithmetic (LIA) have
thus been repurposed for BV interpolation [16]. First, operations on bit-vectors
are reformulated as LIA formulae. An interpolant over LIA is then reinterpreted
as a candidate interpolant for a pair of BV formulae. Because of wrap-around,
LIA does not necessarily align with BV arithmetic, hence the LIA interpolant
is adopted as a BV interpolant only if it passes a (unsatisfiability) check over
bit-vectors. This checks that the interpolant relaxes the first BV formula of the
pair and yet is still inconsistent with the second. If the candidate fails the check,
then the two BV formulae are bit-blasted to recover a propositional interpolant,
albeit one which looses the high-level structure of bit-vectors, and therefore is
not compact. This approach is promising: it exploits robust off-the-shelf LIA
interpolation [17] yet is compromised by the quality of the interpolants which
follow from bit-blasting.
Contribution This paper plugs this gap, addressing the issue of interpolant quality by developing a new, principled encoding LIA formulae into BV formulae
which does not enlarge the bit-width of the BV formulae. This ensures that
the interpolant is still drawn from the language used to define BV formulae.
We show that a na¨ ıve encoding of an LIA inequality as a BV inequality can
give a formula which has a completely different meaning from LIA inequality:
the BV inequality can have solutions not admitted by the LIA inequality and
vice versa. Moreover, we illustrate how a straightforward encoding of a single
LIA inequality can require many BV inequalities, which compromises the quality
of a BV interpolant. We therefore propose a technique, which we call gapping,
which adds range constraints to LIA inequality which reduces the LIA inequality
into two or three LIA systems the solutions of which are amenable to compact
BV representation. The term gapping reflects a geometric interpretation of this
transformation which introduces a gap
4 between the solutions of the two LIA
systems. We demonstrate the value of this approach with a BV interpolation
engine which side-steps bit-blasting (and the complexity of providing bit-level
4 The title of the paper alludes to both this geometric technique, the conceptual gap
in previous work, and collaboration which entailed traveling through London.
T. Okudono and A. King
Context As solvers for richer theories have evolved so have interpolation engines
for these theories, with a notable flurry of activity around one decade ago [10, 11,
19, 20, 23, 24, 30]. However, progress on the important theory of bit-vectors (BV)
has been surprisingly slow, the two key works [2, 16] taking opposing approaches.
One takes advantage of existing interpolation engines [16] and the another develops a bespoke interpolation engine around lazy reduction [2], which supports
bit-vector operations by expanding them, on demand, to Presburger arithmetic
[2]. This paper develops the former approach, aiming to use an LIA solver as is.
The central problem in bit-vector interpolation is to construct an interpolant
which is compact (one might even say beautiful [1]). Although a pair of inconsistent BV formulae can always be bit-blasted (unfolded) into a pair of inconsistent
propositional formulae, it is not always obvious how the resulting propositional
interpolant can be folded back into a compact bit-vector (BV) formula to derive
a BV interpolant. Interpolation engines over linear integer arithmetic (LIA) have
thus been repurposed for BV interpolation [16]. First, operations on bit-vectors
are reformulated as LIA formulae. An interpolant over LIA is then reinterpreted
as a candidate interpolant for a pair of BV formulae. Because of wrap-around,
LIA does not necessarily align with BV arithmetic, hence the LIA interpolant
is adopted as a BV interpolant only if it passes a (unsatisfiability) check over
bit-vectors. This checks that the interpolant relaxes the first BV formula of the
pair and yet is still inconsistent with the second. If the candidate fails the check,
then the two BV formulae are bit-blasted to recover a propositional interpolant,
albeit one which looses the high-level structure of bit-vectors, and therefore is
not compact. This approach is promising: it exploits robust off-the-shelf LIA
interpolation [17] yet is compromised by the quality of the interpolants which
follow from bit-blasting.
Contribution This paper plugs this gap, addressing the issue of interpolant quality by developing a new, principled encoding LIA formulae into BV formulae
which does not enlarge the bit-width of the BV formulae. This ensures that
the interpolant is still drawn from the language used to define BV formulae.
We show that a na¨ ıve encoding of an LIA inequality as a BV inequality can
give a formula which has a completely different meaning from LIA inequality:
the BV inequality can have solutions not admitted by the LIA inequality and
vice versa. Moreover, we illustrate how a straightforward encoding of a single
LIA inequality can require many BV inequalities, which compromises the quality
of a BV interpolant. We therefore propose a technique, which we call gapping,
which adds range constraints to LIA inequality which reduces the LIA inequality
into two or three LIA systems the solutions of which are amenable to compact
BV representation. The term gapping reflects a geometric interpretation of this
transformation which introduces a gap
4 between the solutions of the two LIA
systems. We demonstrate the value of this approach with a BV interpolation
engine which side-steps bit-blasting (and the complexity of providing bit-level
4 The title of the paper alludes to both this geometric technique, the conceptual gap
in previous work, and collaboration which entailed traveling through London.