64
F. Frohn
Thus, it then suffices to find some ψ 2 ∈ Prop(C (y)) such that
x −→
n
q
ϕ,a x
∧ ψ 2 =⇒ x −→
n
ϕ,a x
.
(1)
The reason is that we have −→ q
ϕ,a ∩ −→
ϕ,a = −→ q
ϕ∧
ϕ,a = −→ ϕ,a and thus
ψ 1 ∧ ψ 2 =⇒ x −→
n
ϕ,a x
,
i.e., ψ 1 ∧ ψ 2 approximates T loop .
Note that the acceleration techniques presented so far would map
ϕ, a to
some ψ 2 ∈ Prop(C (y)) such that
ψ 2 =⇒ x −→
n
ϕ,a x
,
(2)
which is more restrictive than (1). In Sec. 5, we will adapt all acceleration
techniques from Sec. 3 to search for some ψ 2 ∈ Prop(C (y)) that satisfies (1)
instead of (2), i.e., we will turn them into conditional acceleration techniques.
Definition 4 (Conditional Acceleration). We call a partial function
accel : Loop × Prop(C (x)) Prop(C (y)).
a conditional acceleration technique. It is sound if
x −→
n
q
ϕ,a x
∧ accel (χ, a, q
ϕ) implies x −→
n
χ,a x
for all (χ, a, q
ϕ) ∈ dom(accel ), x, x
∈ Z
d , and n > 0. It is exact if additionally
x −→
n
χ∧ q
ϕ,a x
implies accel (χ, a, q
ϕ)
for all (χ, a, q
ϕ) ∈ dom(accel ), x, x
∈ Z
d , and n > 0.
We are now ready to present our acceleration calculus, which combines loop
acceleration techniques in a modular way. In the following, w.l.o.g. we assume
that propositional formulas are in CNF and we identify the formula
k
i=1 C i with
the set of clauses {C i | 1 ≤ i ≤ k}.
Definition 5 (Acceleration Calculus). The relation on acceleration problems is defined by the following rule:
∅ ∅ = χ ⊆
ϕ accel (χ, a, q
ϕ) = ψ 2
ψ 1 | q
ϕ |
ϕ | a (e) ψ 1 ∪ ψ 2 | q
ϕ ∪ χ |
ϕ \ χ | a
accel is a sound conditional acceleration technique
A -step is exact (written e ) if accel is exact.
So our calculus allows us to pick a subset χ (of clauses) from the yet unprocessed condition
ϕ and “move” it to q
ϕ, which has already been processed
successfully. To this end, χ, a needs to be accelerated by a conditional acceleration technique, i.e., when accelerating χ, a we may assume x −→
n
q
ϕ,a x
.
Note that every acceleration technique trivially gives rise to a conditional
acceleration technique (by disregarding the second argument q
ϕ of accel in Def. 4).
Thus, our calculus allows for combining arbitrary existing acceleration techniques
without adapting them. However, many acceleration techniques can easily be
turned into more sophisticated conditional acceleration techniques (cf. Sec. 5),
which increases the power of our approach.
F. Frohn
Thus, it then suffices to find some ψ 2 ∈ Prop(C (y)) such that
x −→
n
q
ϕ,a x
∧ ψ 2 =⇒ x −→
n
ϕ,a x
.
(1)
The reason is that we have −→ q
ϕ,a ∩ −→
ϕ,a = −→ q
ϕ∧
ϕ,a = −→ ϕ,a and thus
ψ 1 ∧ ψ 2 =⇒ x −→
n
ϕ,a x
,
i.e., ψ 1 ∧ ψ 2 approximates T loop .
Note that the acceleration techniques presented so far would map
ϕ, a to
some ψ 2 ∈ Prop(C (y)) such that
ψ 2 =⇒ x −→
n
ϕ,a x
,
(2)
which is more restrictive than (1). In Sec. 5, we will adapt all acceleration
techniques from Sec. 3 to search for some ψ 2 ∈ Prop(C (y)) that satisfies (1)
instead of (2), i.e., we will turn them into conditional acceleration techniques.
Definition 4 (Conditional Acceleration). We call a partial function
accel : Loop × Prop(C (x)) Prop(C (y)).
a conditional acceleration technique. It is sound if
x −→
n
q
ϕ,a x
∧ accel (χ, a, q
ϕ) implies x −→
n
χ,a x
for all (χ, a, q
ϕ) ∈ dom(accel ), x, x
∈ Z
d , and n > 0. It is exact if additionally
x −→
n
χ∧ q
ϕ,a x
implies accel (χ, a, q
ϕ)
for all (χ, a, q
ϕ) ∈ dom(accel ), x, x
∈ Z
d , and n > 0.
We are now ready to present our acceleration calculus, which combines loop
acceleration techniques in a modular way. In the following, w.l.o.g. we assume
that propositional formulas are in CNF and we identify the formula
k
i=1 C i with
the set of clauses {C i | 1 ≤ i ≤ k}.
Definition 5 (Acceleration Calculus). The relation on acceleration problems is defined by the following rule:
∅ ∅ = χ ⊆
ϕ accel (χ, a, q
ϕ) = ψ 2
ψ 1 | q
ϕ |
ϕ | a (e) ψ 1 ∪ ψ 2 | q
ϕ ∪ χ |
ϕ \ χ | a
accel is a sound conditional acceleration technique
A -step is exact (written e ) if accel is exact.
So our calculus allows us to pick a subset χ (of clauses) from the yet unprocessed condition
ϕ and “move” it to q
ϕ, which has already been processed
successfully. To this end, χ, a needs to be accelerated by a conditional acceleration technique, i.e., when accelerating χ, a we may assume x −→
n
q
ϕ,a x
.
Note that every acceleration technique trivially gives rise to a conditional
acceleration technique (by disregarding the second argument q
ϕ of accel in Def. 4).
Thus, our calculus allows for combining arbitrary existing acceleration techniques
without adapting them. However, many acceleration techniques can easily be
turned into more sophisticated conditional acceleration techniques (cf. Sec. 5),
which increases the power of our approach.