90
T. Okudono and A. King
shows
7x + 3y − 21 ≤ −4
LIA
=
7x + 3y ≤ 17
LIA
and so building on example 6
7x + 3y ≤ 17
LIA
=
φ 0 ∨ φ 1 ∨ φ 2
BV
. By corollary 3 it follows
φ
LIA
=
F y (φ 0 ) ∨ F y (φ 1 ) ∨ F y (φ 2 )
BV
where F y (φ 0 ), F y (φ 1 ) and F y (φ 2 ) are
given in Fig. 4(b), (c) and (d) respectively. Finally, to illustrate the handling
of boxing, recall box BV (c; 11) from example 6 and
box BV (c; 11) = (x ≤ 0 ∧ y ≤ 3)
∨ (x ≤ 1 ∧ y ≤ 2)
∨ (x ≤ 1 ∧ y ≤ 1)
F y (box BV (c; 11)) = (x ≤ 0 ∧ (−y + 7 ≤ 3))
∨ (x ≤ 1 ∧ (−y + 7 ≤ 2))
∨ (x ≤ 1 ∧ (−y + 7 ≤ 1))
Finally observe
x ≤ 0 ∧ (−y + 7 ≤ 3)
LIA
= {(0, y) ∈ M
2
| 4 ≤ y ≤ 7}
x ≤ 1 ∧ (−y + 7 ≤ 2)
LIA
= {(x, y) ∈ M
2
| 0 ≤ x ≤ 1 ∧ 5 ≤ y ≤ 7}
and that the disjunct (x ≤ 1 ∧ (−y + 7 ≤ 1)) is actually redundant.
3.4 Boxing, Gapping, Flipping and Demoding
Griggio [16] gives a procedure for encoding machine arithmetic in LIA, illustrating that the resulting LIA interpolants can include inequalities such as
−x 2 +x 3 −256−x 2 /256 ≤ 255 [16, Example 5]. Relaxing inequalities to include
ceiling (or floor) functions can reduce the size of interpolants whilst simplifying
their derivation [17]. These more general forms of interpolant include inequalities of the form c · x + n
c
· x/n ≤ b [9] or c · x + n
c
· x/n ≤ b [17],
though for our purposes it is sufficient to consider c · x + n
2
n
c
· x/2
n
≤ b or
c · x + n
2
n
c
· x/2
n
≤ b, where the divisors are powers of 2, stemming from the
way they model wrap-around in machine arithmetic. To extend boxing to these
generalised interpolants we extend the LIA and BV semantics two new types of
atomic constraint (though the definitions are almost vacuous):
Definition 5. If ≡ c · x + n
c
· x/2
n
≤ b then
LIA
=
x ∈ M
d
|c · x + n
c
· x/2
n
≤ b
BV
=
x ∈ M
d
|(c · x + n
c
· x/2
n
) mod m ≤ b mod m
The following proposition shows generalised LIA interpolants are not an obstacle
to boxing. These inequalities are handled through a transformation scheme which
exploits the property that if n ≤ w then (c · x mod 2
n ) mod m = c · x mod 2
n .
We informally call this transformation tactic demoding, because like gapping
and flipping, it is designed to increase the general applicability of boxing.
Proposition 3. Suppose 0 ≤ n ≤ w and
(c + n
c
) · x − n
y ≤ b
LIA
=
φ
BV
.
If y does not occur in x then
c · x + n
2
n
c
· x/2
n
≤ b
LIA
=
φ[y → c
· x mod 2
n ]
BV
T. Okudono and A. King
shows
7x + 3y − 21 ≤ −4
LIA
=
7x + 3y ≤ 17
LIA
and so building on example 6
7x + 3y ≤ 17
LIA
=
φ 0 ∨ φ 1 ∨ φ 2
BV
. By corollary 3 it follows
φ
LIA
=
F y (φ 0 ) ∨ F y (φ 1 ) ∨ F y (φ 2 )
BV
where F y (φ 0 ), F y (φ 1 ) and F y (φ 2 ) are
given in Fig. 4(b), (c) and (d) respectively. Finally, to illustrate the handling
of boxing, recall box BV (c; 11) from example 6 and
box BV (c; 11) = (x ≤ 0 ∧ y ≤ 3)
∨ (x ≤ 1 ∧ y ≤ 2)
∨ (x ≤ 1 ∧ y ≤ 1)
F y (box BV (c; 11)) = (x ≤ 0 ∧ (−y + 7 ≤ 3))
∨ (x ≤ 1 ∧ (−y + 7 ≤ 2))
∨ (x ≤ 1 ∧ (−y + 7 ≤ 1))
Finally observe
x ≤ 0 ∧ (−y + 7 ≤ 3)
LIA
= {(0, y) ∈ M
2
| 4 ≤ y ≤ 7}
x ≤ 1 ∧ (−y + 7 ≤ 2)
LIA
= {(x, y) ∈ M
2
| 0 ≤ x ≤ 1 ∧ 5 ≤ y ≤ 7}
and that the disjunct (x ≤ 1 ∧ (−y + 7 ≤ 1)) is actually redundant.
3.4 Boxing, Gapping, Flipping and Demoding
Griggio [16] gives a procedure for encoding machine arithmetic in LIA, illustrating that the resulting LIA interpolants can include inequalities such as
−x 2 +x 3 −256−x 2 /256 ≤ 255 [16, Example 5]. Relaxing inequalities to include
ceiling (or floor) functions can reduce the size of interpolants whilst simplifying
their derivation [17]. These more general forms of interpolant include inequalities of the form c · x + n
c
· x/n ≤ b [9] or c · x + n
c
· x/n ≤ b [17],
though for our purposes it is sufficient to consider c · x + n
2
n
c
· x/2
n
≤ b or
c · x + n
2
n
c
· x/2
n
≤ b, where the divisors are powers of 2, stemming from the
way they model wrap-around in machine arithmetic. To extend boxing to these
generalised interpolants we extend the LIA and BV semantics two new types of
atomic constraint (though the definitions are almost vacuous):
Definition 5. If ≡ c · x + n
c
· x/2
n
≤ b then
LIA
=
x ∈ M
d
|c · x + n
c
· x/2
n
≤ b
BV
=
x ∈ M
d
|(c · x + n
c
· x/2
n
) mod m ≤ b mod m
The following proposition shows generalised LIA interpolants are not an obstacle
to boxing. These inequalities are handled through a transformation scheme which
exploits the property that if n ≤ w then (c · x mod 2
n ) mod m = c · x mod 2
n .
We informally call this transformation tactic demoding, because like gapping
and flipping, it is designed to increase the general applicability of boxing.
Proposition 3. Suppose 0 ≤ n ≤ w and
(c + n
c
) · x − n
y ≤ b
LIA
=
φ
BV
.
If y does not occur in x then
c · x + n
2
n
c
· x/2
n
≤ b
LIA
=
φ[y → c
· x mod 2
n ]
BV