Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
89
(a)
φ
LIA
(b)
F y (φ 0 ) = 7x − 3y + 13 ≤ 3
∧ F y (box BV (c; 11))
(c)
F y (φ 1 ) = 7x − 3y − 9 ≤ 3
∧ F y (box BV (c; 15))
(d)
F y (φ 2 ) = 7x − 3y + 5 ≤ 1
∧ F y (box BV (c; 17))
Fig. 4. Flipping φ = 7x − 3y ≤ −4 where m = 8, x = x, y, x
+ = x and x
− = y
The overall strategy involves applying boxing and gapping to an inequality derived by the flipping function F x − . The validity of this strategy is based on the
following proposition:
Proposition 2. If |x
−
| = e then
–
F x − (f )
LIA
= F e (
f
LIA
)
–
F x − (f )
BV
= F e (
f
BV
)
A complete strategy for handling inequalities with negative coefficients is justified by the following corollary. The strategy entails flipping an LIA inequality,
deriving a BV formula by boxing and gapping, and then flipping the BV formula.
Corollary 3. Suppose c
+ > 0, c
− < 0 and
c
+
· x
+
− c
−
· x
−
≤ b + (1 − m)(c
−
· 1)
LIA
=
φ 0 ∨ φ 1 ∨ φ 2
BV
Then
c
+
· x
+ + c
−
· x
−
≤ b
LIA
=
F x − (φ 0 ) ∨ F x − (φ 1 ) ∨ F x − (φ 2 )
BV
Example 8. Consider φ = 7x − 3y ≤ −4 which is illustrated in Fig. 4(a). Then
x
+ = x, x
− = y and F x − (φ) = F y (φ) = 7x + 3y − 21 ≤ −4. Fig. 3(a)