Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
83
Boxing Observe from Figure 1(a) that the extra solutions of
x + y ≤ 3
BV
over
x + y ≤ 3
LIA
stem from overflow. Overflow can be avoided by constraining BV
solutions with x ≤ 3 and y ≤ 3 which amounts to placing a box (in general a
hyper-rectangle) around the LIA solutions, as illustrated in Figure 1(b). This
tactic, henceforth called boxing, leads to the following formula:
f 3 = (x + y ≤ 3 ∧ x ≤ 3 ∧ y ≤ 3)
which requires 2 binary conjuncts.
Gapping Figure 1(c) illustrates that in general boxing cannot be applied in
isolation because a box around the LIA solutions would not eliminate any extraneous BV solutions. Boxing is successful for Figure 1(b) because of the absence
of solutions (a gap) between the LIA solutions inside the box and the BV solutions outside the box. No such gap exists for the box of Figure 1(c). Yet
boxing can still be applied by decomposing the inequality x + y ≤ 7 into two
inequalities both of which are amenable to boxing. The construction is based on
x + y ≤ 7
LIA
=
x + y ≤ 3
LIA
∪
4 ≤ x + y ∧ x + y ≤ 7
LIA
=
x + y ≤ 3
LIA
∪
0 ≤ x + y − 4 ∧ x + y − 4 ≤ 3
LIA
. Recall that boxing alone allows the LIA solutions of x + y ≤ 3 to be expressed as a BV formula of 2 binary connectives.
Thus consider the compound formula
= (0 ≤ x + y − 4 ∧ x + y − 4 ≤ 3) whose
LIA solutions are illustrated in Figure 1(d). Observe that the BV solutions of
can be covered with two rectangles without including the extraneous 6 BV
solutions in top right. Then
LIA
=
x + y − 4 ≤ 3 ∧ (x ≤ 3 ∨ y ≤ 3)
BV
which
leads to the complete formula
f 3 = (x + y ≤ 3 ∧ x ≤ 3 ∧ y ≤ 3) ∨ (x + y − 4 ≤ 3 ∧ (x ≤ 3 ∨ y ≤ 3))
such that
f 3
BV
=
x + y ≤ 7
LIA
. This tactic of artificially introducing a gap,
henceforth called gapping, is equally applicable for larger grids too. For instance,
working over a modulo of 32
x + y ≤ 31
LIA
=
f 4
BV
where
f 4 = (x + y ≤ 15 ∧ x ≤ 15 ∧ y ≤ 15) ∨ (x + y − 16 ≤ 15 ∧ (x ≤ 15 ∨ y ≤ 15))
3 Formal correctness of boxing and gapping
In what follows we consider LIA and BV formulae over an ordered set of variables
{x 1 , . . . , x d } for some d > 1. We consider bit-vectors of fixed width w > 1
and interpret LIA and BV formulae over the product space M
d where M =
{0, 1, 2, . . . , m − 1} and m = 2
w as follows:
Definition 1. Let c, c
∈ Z
d and b, b
∈ Z. If ≡ (
d
i=1 c i x i )+b ≤ (
d
i=1 c
i x i )+
b
then
LIA
=
x ∈ M
d
d
i=1 c i x i + b ≤
d
i=1 c
i x i + b
BV
=
x ∈ M
d
(
d
i=1 c i x i + b) mod m ≤ (
d
i=1 c
i x i + b
) mod m
83
Boxing Observe from Figure 1(a) that the extra solutions of
x + y ≤ 3
BV
over
x + y ≤ 3
LIA
stem from overflow. Overflow can be avoided by constraining BV
solutions with x ≤ 3 and y ≤ 3 which amounts to placing a box (in general a
hyper-rectangle) around the LIA solutions, as illustrated in Figure 1(b). This
tactic, henceforth called boxing, leads to the following formula:
f 3 = (x + y ≤ 3 ∧ x ≤ 3 ∧ y ≤ 3)
which requires 2 binary conjuncts.
Gapping Figure 1(c) illustrates that in general boxing cannot be applied in
isolation because a box around the LIA solutions would not eliminate any extraneous BV solutions. Boxing is successful for Figure 1(b) because of the absence
of solutions (a gap) between the LIA solutions inside the box and the BV solutions outside the box. No such gap exists for the box of Figure 1(c). Yet
boxing can still be applied by decomposing the inequality x + y ≤ 7 into two
inequalities both of which are amenable to boxing. The construction is based on
x + y ≤ 7
LIA
=
x + y ≤ 3
LIA
∪
4 ≤ x + y ∧ x + y ≤ 7
LIA
=
x + y ≤ 3
LIA
∪
0 ≤ x + y − 4 ∧ x + y − 4 ≤ 3
LIA
. Recall that boxing alone allows the LIA solutions of x + y ≤ 3 to be expressed as a BV formula of 2 binary connectives.
Thus consider the compound formula
= (0 ≤ x + y − 4 ∧ x + y − 4 ≤ 3) whose
LIA solutions are illustrated in Figure 1(d). Observe that the BV solutions of
can be covered with two rectangles without including the extraneous 6 BV
solutions in top right. Then
LIA
=
x + y − 4 ≤ 3 ∧ (x ≤ 3 ∨ y ≤ 3)
BV
which
leads to the complete formula
f 3 = (x + y ≤ 3 ∧ x ≤ 3 ∧ y ≤ 3) ∨ (x + y − 4 ≤ 3 ∧ (x ≤ 3 ∨ y ≤ 3))
such that
f 3
BV
=
x + y ≤ 7
LIA
. This tactic of artificially introducing a gap,
henceforth called gapping, is equally applicable for larger grids too. For instance,
working over a modulo of 32
x + y ≤ 31
LIA
=
f 4
BV
where
f 4 = (x + y ≤ 15 ∧ x ≤ 15 ∧ y ≤ 15) ∨ (x + y − 16 ≤ 15 ∧ (x ≤ 15 ∨ y ≤ 15))
3 Formal correctness of boxing and gapping
In what follows we consider LIA and BV formulae over an ordered set of variables
{x 1 , . . . , x d } for some d > 1. We consider bit-vectors of fixed width w > 1
and interpret LIA and BV formulae over the product space M
d where M =
{0, 1, 2, . . . , m − 1} and m = 2
w as follows:
Definition 1. Let c, c
∈ Z
d and b, b
∈ Z. If ≡ (
d
i=1 c i x i )+b ≤ (
d
i=1 c
i x i )+
b
then
LIA
=
x ∈ M
d
d
i=1 c i x i + b ≤
d
i=1 c
i x i + b
BV
=
x ∈ M
d
(
d
i=1 c i x i + b) mod m ≤ (
d
i=1 c
i x i + b
) mod m