84
T. Okudono and A. King
Furthermore, the LIA semantics can be lifted from inequalities to LIA formulae
by:
f 1 ∨ f 2
LIA
=
f 1
LIA
∪
f 2
LIA
,
f 1 ∧ f 2
LIA
=
f 1
LIA
∩
f 2
LIA
and
¬f
LIA
=
M
d
\
f
LIA
. Likewise for BV formulae.
In the sequel, N denotes the set of (strictly) positive integers, R the set of
real numbers, and R ≥0 the set of non-negative real numbers. We extend the
floor and ceiling function for the sequences in R
d in a component-wise manner:
x i = x i and x i = x i . If x ∈ R
d then |x| = d. The partial order ≤ on R
d
is defined by x ≤ y if and only if x i ≤ y i for all i = 1, . . . , d.
3.1 Boxing
Boxing is founded on the following result and its corollary in which sets of
solutions to inequalities which describe hyper-rectangles are pinched, above and
below, by inclusions to systems of inequalities with positive, unary coefficients:
Lemma 1. Let d > 1 and L ∈ N. Then:
x ∈ R
d
≥0
d
i=1 x i ≤ L · (m/2) − 1
⊆
p∈I d ((d−1)(L+1))
d
i=1
x ∈ R
d
≥0 | x i <
pi·(m/2)
d−1
⊆
x ∈ R
d
≥0
d
i=1 x i < (L + 1) · (m/2)
where I d (n) =
(i 1 , . . . , i d ) ∈ N
d
| i 1 + · · · + i d = n
.
Corollary 1. Let d > 1, L ∈ N and c ∈ N
d . Then:
x ∈ Z
d
≥0 |
d
i=1 c i x i ≤ L · (m/2) − 1
⊆
p∈I d ((d−1)(L+1))
d
j=1
x ∈ Z
d
≥0 | x j ≤ ≤
pj ·(m/2)
ci(d−1) − 1
⊆
x ∈ Z
d
≥0 |
d
i=1 c i x i ≤ (L + 1) · (m/2) − 1
The corollary leads to two types of box constraint: one for LIA and the other,
reducing boxing, for BV. Boxing formulae are purely conceptual and are used
to reason about correctness; reduced boxing formulae are deployed within BV
interpolants.
Definition 2. Let c ∈ N
d , b ∈ N and L ∈ N be the unique natural number
such that (L − 1) · (m/2) ≤ b ≤ L · (m/2) − 1. The boxing and reduced boxing of
d
i=1 c i x i ≤ b are formulae defined as follows:
box LIA (c; b) ≡
p∈I d ((d−1)(L+1))
d
j=1
x j ≤ ≤
p j · (m/2)
c j (d − 1)
− 1
(1)
box BV (c; b) ≡
p∈I d ((d−1)(L+1))
d
j=1
x j ≤ min
p j · (m/2)
c j (d − 1)
− 1, m − 1
(2)
T. Okudono and A. King
Furthermore, the LIA semantics can be lifted from inequalities to LIA formulae
by:
f 1 ∨ f 2
LIA
=
f 1
LIA
∪
f 2
LIA
,
f 1 ∧ f 2
LIA
=
f 1
LIA
∩
f 2
LIA
and
¬f
LIA
=
M
d
\
f
LIA
. Likewise for BV formulae.
In the sequel, N denotes the set of (strictly) positive integers, R the set of
real numbers, and R ≥0 the set of non-negative real numbers. We extend the
floor and ceiling function for the sequences in R
d in a component-wise manner:
x i = x i and x i = x i . If x ∈ R
d then |x| = d. The partial order ≤ on R
d
is defined by x ≤ y if and only if x i ≤ y i for all i = 1, . . . , d.
3.1 Boxing
Boxing is founded on the following result and its corollary in which sets of
solutions to inequalities which describe hyper-rectangles are pinched, above and
below, by inclusions to systems of inequalities with positive, unary coefficients:
Lemma 1. Let d > 1 and L ∈ N. Then:
x ∈ R
d
≥0
d
i=1 x i ≤ L · (m/2) − 1
⊆
p∈I d ((d−1)(L+1))
d
i=1
x ∈ R
d
≥0 | x i <
pi·(m/2)
d−1
⊆
x ∈ R
d
≥0
d
i=1 x i < (L + 1) · (m/2)
where I d (n) =
(i 1 , . . . , i d ) ∈ N
d
| i 1 + · · · + i d = n
.
Corollary 1. Let d > 1, L ∈ N and c ∈ N
d . Then:
x ∈ Z
d
≥0 |
d
i=1 c i x i ≤ L · (m/2) − 1
⊆
p∈I d ((d−1)(L+1))
d
j=1
x ∈ Z
d
≥0 | x j ≤ ≤
pj ·(m/2)
ci(d−1) − 1
⊆
x ∈ Z
d
≥0 |
d
i=1 c i x i ≤ (L + 1) · (m/2) − 1
The corollary leads to two types of box constraint: one for LIA and the other,
reducing boxing, for BV. Boxing formulae are purely conceptual and are used
to reason about correctness; reduced boxing formulae are deployed within BV
interpolants.
Definition 2. Let c ∈ N
d , b ∈ N and L ∈ N be the unique natural number
such that (L − 1) · (m/2) ≤ b ≤ L · (m/2) − 1. The boxing and reduced boxing of
d
i=1 c i x i ≤ b are formulae defined as follows:
box LIA (c; b) ≡
p∈I d ((d−1)(L+1))
d
j=1
x j ≤ ≤
p j · (m/2)
c j (d − 1)
− 1
(1)
box BV (c; b) ≡
p∈I d ((d−1)(L+1))
d
j=1
x j ≤ min
p j · (m/2)
c j (d − 1)
− 1, m − 1
(2)