Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
85
Given m and b ∈ N, it is always possible to find a unique L ∈ N which satisfies
Definition 2 by putting L =
2b
m + 1. Then L − 1 =
2b
m ≤
2b
m <
2b
m + 1 = L
hence (L − 1)(m/2) ≤ b < L(m/2) whence (L − 1)(m/2) ≤ b ≤ L(m/2) − 1
because b and L(m/2) are integral.
One might expect that the cardinality of I d ((d − 1)(L + 1)) becomes large
as d or L grow large. Yet d is the number of variables occurring in the LIA
interpolant, which is typically small. Furthermore, when L is large, the values
of p are also large, so that many terms become equivalent because of the min
operation in equation (2) of Definition 2. Thus the number of terms required to
define box BV (c; b) does not grow excessively large in practice.
The following proposition asserts that the boxing and reduced boxing formulae share the same solution set when interpreted with, respectively, the LIA and
BV semantics.
Proposition 1.
box LIA (c; b)
LIA
=
box BV (c; b)
BV
Example 1. To demonstrate this equivalence, consider again x+y ≤ 3 for m = 8.
Then put L = 6/8 + 1 = 1 and I 2 ((d − 1)(L + 1)) = I 2 (2) = {{1, 1}. Observe
box LIA (1, 1; 3) = box BV (1, 1; 3) since
box LIA (1, 1; 3) = (x ≤ ≤4/1 − 1 = 3) ∧ (y ≤ ≤4/1 − 1 = 3)
box BV (1, 1; 3) = (x ≤ min(3, 7) = 3) ∧ (y ≤ min(3, 7) = 3)
Example 2. Although
box LIA (c; b)
LIA
=
box BV (c; b)
BV
, it does not necessarily
follow that
box LIA (c; b)
LIA
=
box LIA (c; b)
BV
. To illustrate, consider x + y ≤ 7
for d = 2 and m = 4. Thus c = 1, 1 and b = 7. Then L = 14/4 + 1 = 4 and
I 2 ((d − 1)(L + 1)) = I 2 (5) = {{1, 4, 2, 3, 3, 2, 4, 1} hence
box LIA (c; b) = (x ≤ 1 ∧ y ≤ 7) ∨ (x ≤ 3 ∧ y ≤ 5)∨
(x ≤ 5 ∧ y ≤ 3) ∨ (x ≤ 7 ∧ y ≤ 1)
Therefore
box LIA (c; b)
LIA
= M
2 but (2, 2) ∈
box LIA (c; b)
BV
.
The following lemma shows that the solution sets for boxing grow monotonically as the constant of the inequality is relaxed.
Lemma 2. If b ≤ b
then
box LIA (c; b)
LIA
⊆
box LIA (c; b
)
LIA
.
The following results explains how to augment an inequality with a box so
as to align its BV semantics with its LIA semantics.
Theorem 1 (boxing without gapping). Let c ∈ N
d and b ∈ N. If b < m/2
then
d
i=1
c i x i ≤ b
LIA
=
(
d
i=1
c i x i ≤ b) ∧ box BV (c; b)
BV
85
Given m and b ∈ N, it is always possible to find a unique L ∈ N which satisfies
Definition 2 by putting L =
2b
m + 1. Then L − 1 =
2b
m ≤
2b
m <
2b
m + 1 = L
hence (L − 1)(m/2) ≤ b < L(m/2) whence (L − 1)(m/2) ≤ b ≤ L(m/2) − 1
because b and L(m/2) are integral.
One might expect that the cardinality of I d ((d − 1)(L + 1)) becomes large
as d or L grow large. Yet d is the number of variables occurring in the LIA
interpolant, which is typically small. Furthermore, when L is large, the values
of p are also large, so that many terms become equivalent because of the min
operation in equation (2) of Definition 2. Thus the number of terms required to
define box BV (c; b) does not grow excessively large in practice.
The following proposition asserts that the boxing and reduced boxing formulae share the same solution set when interpreted with, respectively, the LIA and
BV semantics.
Proposition 1.
box LIA (c; b)
LIA
=
box BV (c; b)
BV
Example 1. To demonstrate this equivalence, consider again x+y ≤ 3 for m = 8.
Then put L = 6/8 + 1 = 1 and I 2 ((d − 1)(L + 1)) = I 2 (2) = {{1, 1}. Observe
box LIA (1, 1; 3) = box BV (1, 1; 3) since
box LIA (1, 1; 3) = (x ≤ ≤4/1 − 1 = 3) ∧ (y ≤ ≤4/1 − 1 = 3)
box BV (1, 1; 3) = (x ≤ min(3, 7) = 3) ∧ (y ≤ min(3, 7) = 3)
Example 2. Although
box LIA (c; b)
LIA
=
box BV (c; b)
BV
, it does not necessarily
follow that
box LIA (c; b)
LIA
=
box LIA (c; b)
BV
. To illustrate, consider x + y ≤ 7
for d = 2 and m = 4. Thus c = 1, 1 and b = 7. Then L = 14/4 + 1 = 4 and
I 2 ((d − 1)(L + 1)) = I 2 (5) = {{1, 4, 2, 3, 3, 2, 4, 1} hence
box LIA (c; b) = (x ≤ 1 ∧ y ≤ 7) ∨ (x ≤ 3 ∧ y ≤ 5)∨
(x ≤ 5 ∧ y ≤ 3) ∨ (x ≤ 7 ∧ y ≤ 1)
Therefore
box LIA (c; b)
LIA
= M
2 but (2, 2) ∈
box LIA (c; b)
BV
.
The following lemma shows that the solution sets for boxing grow monotonically as the constant of the inequality is relaxed.
Lemma 2. If b ≤ b
then
box LIA (c; b)
LIA
⊆
box LIA (c; b
)
LIA
.
The following results explains how to augment an inequality with a box so
as to align its BV semantics with its LIA semantics.
Theorem 1 (boxing without gapping). Let c ∈ N
d and b ∈ N. If b < m/2
then
d
i=1
c i x i ≤ b
LIA
=
(
d
i=1
c i x i ≤ b) ∧ box BV (c; b)
BV