Relaxed Stratification: A New Approach toPractical Complete Predicate Refinement⋆
Tachio Terauchi1 and Hiroshi Unno2
1

JAIST
terauchi@jaist.ac.jp
2
University of Tsukuba
uhiro@cs.tsukuba.ac.jp

Abstract. In counterexample-guided abstraction refinement, a predicate refinement scheme is said to be complete for a given theory if it
is guaranteed to eventually find predicates sufficient to prove the given
property, when such exist. However, existing complete methods requiredeciding if a proof of the counterexample’s spuriousness exists in some finite language of predicates. Such an exact finite-language-restricted predicate search is quite hard for many theories used in practice and incurs
a heavy overhead. In this paper, we address the issue by showing thatthe language restriction can be relaxed so that the refinement process
is restricted to infer proofs from some finite language Lbase ∪ Lext but
is only required to return a proof when the counterexample’s spuriousness can be proved in Lbase . Then, we show how a proof-based refinement algorithm can be made to satisfy the relaxed requirement and becomplete by restricting only the theory-level reasoning in SMT to emit
Lbase -restricted partial interpolants (while such an approach has been
proposed previously, we show for the first time that it can be done for
languages that are not closed under conjunctions and disjunctions). We
also present a technique that uses a property of counterexample patterns
to further improve the efficiency of the refinement algorithm while stillsatisfying the requirement. We have experimented with a prototype implementation of the new refinement algorithm, and show that it is able
to achieve complete refinement with only a small overhead.

1

Introduction

Predicate abstraction with counterexample-guided abstraction refinement (CEGAR) is a promising approach to automated verification of safety (i.e., reachability) properties (see, e.g., [7] for a survey). Briefly, the CEGAR approach works
as follows. Let T be a first-order logic (FOL) theory. The verifier picks somefinite set of predicates from T as the initial candidate predicate set, and iterates
the following two processes until convergence (here, we use the term “predicate”
for an arbitrary formula, and not limited to just atomic predicates).
⋆

This work was supported by MEXT Kakenhi 23220001, 26330082, 25280023, and25730035.

(1) The abstraction process checks if the current candidates form a sufficient
proof of the program’s safety (i.e., an inductive invariant – sometimes called“safe” inductive invariant). If so, then the program is proved safe and theiteration halts. Otherwise, the process generates a counterexample as anevidence that the current candidates are insufficient, and (2) is invoked.
(2) The refinement process analyzes the given counterexample. If the counterexample cannot be proved spurious by predicates from T (i.e., “the counterexample is real”), then the iteration halts and the program is detected to beunsafe. Otherwise, the predicates inferred as a proof of the counterexample’s
spuriousness are added to the candidates, and we repeat from (1).
Note that the verifier halts either when sufficient predicates are inferred to prove
the program safe, or a real counterexample is discovered.
For an unsafe program, the state-of-the-art CEGAR-based verifiers are usually able to eventually discover a real counterexample and converge, by exploring
the state space in a fair manner (if somewhat slowly for ones requiring large counterexamples). By contrast, when a program is safe and the underlying theory
T is sufficient for proving the safety, most verifiers have no guarantee of convergence and can diverge by having the refinement process indefinitely produce
incorrect candidate proofs.
For example, consider the C-like program shown in Figure 1. Here, ndet()
returns a non-deterministic integer. The goal is to verify that the assertion failure
is unreachable, that is, a = b ⇒ y = x whenever line 10 is reached.
Suppose we start the verification process with the 1: void main(void) {candidate set comprising the 2:
int a = ndet();int b = ndet();boolean closure of the pred- 3:
int x = a;int y = b;int z = 0;
while (ndet()) {icates z = 0, a = b and 4:
y++;z++;
y = x. A possible counterex- 5:}
ample is a path that passes 6:
while (z != 0) {through the first loop (lines 7:
8:y--;z--;
4-6) once, reaching line 79:}with the abstract state (a = 10: if (a=b && y!=x) { assert false; }b ⇒ y ≠ x) ∧ z ≠ 0, and then 11: }passes through the second
loop (lines 7-9) once, reaching line 10 with the abstract Fig. 1. A program on which CEGAR may diverge.
state z = 0, which does not
imply a = b ⇒ y = x. A possible proof of the counterexample’s spuriousness (i.e.,
proof that the path is actually safe) is the predicate a = b ⇒ y = x + z. The predicate turns out to be an inductive invariant for the program, and the verification
process halts in the next iteration.
Unfortunately, the refinement process is not guaranteed to infer such a predicate but may choose any predicates that can prove the counterexample’s safety.
For instance, another possibility is the predicate a = b ⇒ y = x + 1. Adding thisto the candidate set is sufficient for proving the safety of the counterexample

but not that of the program, and the abstraction process in the subsequent iteration would return yet another counterexample. For example, it may return the
counterexample that passes the first loop twice, reaching line 7 with the abstractstate a = b ⇒ y ≠ x + 1, and then passes through the second loop twice, reachingline 10 with the abstract state z = 0 again. Then, the refinement process may
choose the predicate a = b ⇒ y = x + 2 to prove the spuriousness of this new
counterexample, which is still insufficient to prove the whole program correct.
The abstract-and-refine iteration may repeat indefinitely in this manner, adding
to the candidates the predicate a = b ⇒ y = x + i in each i-th run of the refinement process. A refinement process is said to be complete (w.r.t. T ) if the
CEGAR process is guaranteed to converge and eventually discover a proof ofthe program’s safety, when one exists in T .
Previous works [8, 13] have proposed to achieve complete refinement in CEGAR by stratifying T into an infinite sequence of predicate languages L0 ⊆ L1 ⊆. . . Lk . . . such that T = ⋃k∈ω Lk , and requiring each i-th run of the refinement
to only infer predicates from the stratum Llvl(i) where lvl (i) is the stratum levelat the i-th CEGAR iteration. By requiring each Lk to be finite3 and raising
the stratum level just when the refinement process reports that no proof exists
for the given counterexample in the current stratum, the approach guarantees
completeness. However, the approach requires the refinement process to exactly
decide if there is a proof of the given counterexample in the current stratum. Indeed, completeness would be lost if the refinement process was allowed to reportthat the current stratum does not have a proof when it actually does. For many
theories used in practice, such as the theory of linear real arithmetic, such anexact finite-language-restricted proof search incurs heavy overhead and is prohibitive (see Section 4, Section 5, and Appendix F for analysis and discussion).
The first contribution of this paper is the observation that exact finite language restricted proof search is actually unnecessary for completeness. Instead,
we show that the following more relaxed scheme is sufficient: in each i-th run of
the refinement process, we restrict the returned proof to some finite language oflvl(i)
lvl(i)
predicates Lbase ∪ Lext (base and extension) such that the refinement processlvl(i)
may report that no proof exists only when no proof exists in Lbase . There areno further restrictions on the refinement process, and so, the refinement process
may return a proof that is not in Lbase (but in Lbase ∪ Lext ) even if a proof exists
in Lbase , or may report that no proof exists even if a proof exists in Lbase ∪ Lext
(but not in Lbase ). We show that this relaxed approach still ensures completenesswhen the stratum level is raised just when the refinement process reports that
there is no proof in the current stratum, as before, and Lbase grows to eventually
cover T (i.e., L0base ⊆ L1base ⊆ . . . Lkbase . . . such that T = ⋃k∈ω Lkbase ). We formalize this observation in a refinement algorithm scheme called relaxed stratification(contra the exact stratification approach described above) and prove that it isindeed complete.
3

The term “finite predicate language” is used synonymously with “finite set of predicates”.

As the second contribution, we present a concrete refinement algorithm that
implements the relaxed scheme. The algorithm is a modification of the proofbased refinement [6] in which the theory-level reasoning is restricted so thatpartial (tree-)interpolants at that level is restricted to Lbase .4 We also present atechnique that uses a certain property of the counterexample patterns to further
improve the efficiency of the algorithm while still satisfying the requirement of
the scheme. We formalize the refinement algorithm as a constraint solver forrecursion-free Horn-clause constraints [4, 14, 15, 24] which has gained popularity
as the standard format for describing refinement algorithms. We have implemented a prototype of the refinement algorithm, and we show empirically that
it is able to achieve complete predicate refinement with low overhead.
In summary, the paper’s contributions are as follows:– A new scheme for practical complete predicate refinement called relaxedstratification and the proof of its completeness (Section 2).
– A new predicate refinement algorithm as concrete instance of the relaxedstratification scheme (Section 3).
– Experiments with a prototype implementation of the refinement algorithm(Section 4).
The rest of the paper is organized as follows. Section 2 formally defines therelaxed stratification scheme and proves its completeness. Section 3 presents
the concrete refinement algorithm implementing the scheme. Section 4 presents
experimental results with the prototype implementation of the refinement algorithm. We discuss related work in Section 5 and conclude the paper in Section 6.
Appendix contains proofs and extra materials omitted from the main body ofthe paper.

2

The Relaxed Stratification Scheme

Let T be a FOL theory. For a formula θ in the signature of T (a T -formula), wewrite fvs(θ) for the free variables in θ. A predicate in T is of the form λx1 , . . . , xn .θ
where θ is a T -formula such that fvs(θ) ⊆ {x1 , . . . , xn }. For readability, we often
omit the explicit λ abstraction and treat a formula θ as the predicate λx̄.θ where{x̄} = fvs(θ). We overload T for the set of predicates in T .
2.1

Assumptions on the Abstraction Process

Relaxed stratification only concerns the refinement process part of CEGAR.
We show that the scheme is quite general and can be used in a wide rangeof CEGAR-based verifiers. To this end, we delineate the conditions that theabstraction process part needs to satisfy. As we shall show below, the conditions
are quite weak and satisfied by virtually any CEGAR-based verifier.
4

While this approach has already been suggested in [8], they require the restricting
language to be closed under conjunctions and disjunctions (see Section 5 for further
discussion).

We assume that the abstraction process Abs takes as input a program and afinite set of predicates in T (the set of candidate proofs). For a program M anda finite set of predicates F ⊆ T , we require that Abs(M, F ) either returns safe,
indicating that M has been proved safe using the predicates from F , or returns acounterexample. For generality, we assume that a counterexample is also simply
a program so that, for a counterexample M , we write Abs(M, F ) = safe when F issufficient for the abstraction process to prove the spuriousness of M (in practice,a counterexample is not an arbitrary program, but, e.g., an unwound programslice of the input program, and concrete instances of the relaxed stratification
scheme take advantage of the counterexample structure – cf. Section 3). We
sometimes say that F refutes the counterexample M when Abs(M, F ) = safe.
We require Abs to be monotonic on the candidates, that is, if Abs(M, F ) = safe
and F ⊆ F ′ then Abs(M, F ′ ) = safe (i.e., having more predicates can only increase Abs’s ability to prove). We also require that if Abs(M, F ) = cex(M ′ ) thenAbs(M ′ , F ) ≠ safe, that is, the returned counterexample is actually a counterexample and cannot be refuted by the given predicates. Finally, we require that if
Abs(M, F ) = safe and Abs(M, F ′ ) = cex(M ′ ) then Abs(M ′ , F ) = safe, that is, if
a set of predicates is a proof for program’s safety then it is also a proof for any
counterexample of the program. We say that Abs is sound when it only provessafe programs safe, that is, Abs(M, F ) = safe only if M is safe.5
We note that the assumptions on the abstraction process are quite liberaland do not demand, for example, the process uses the given set of predicatesby decomposing them into atomic predicates and taking their boolean closure,taking the cartesian closure, or using them directly as loop invariants. In Example 1 below, we describe an example abstraction process that uses the predicatesdirectly.

int a=ndet();int b=ndet();int x=a;int y=b;int z=0;
a1:assume (ndet());
y++;z++;
a2:assume (ndet());
a3:assume (z != 0);y--;z--;
a4:assume (z == 0);
assume (a=b && y!=x);
assert false;

Mexa

int a=ndet();int b=ndet();int x=a;int y=b;int z=0;b1:assume (ndet());
y++;z++;
b2:assume (ndet());
y++;z++;
b3:assume (ndet());
b4:assume (z != 0);y--;z--;
b5:assume (z != 0);y--;z--;
b6:assume (z == 0);
assume (a=b && y!=x);
assert false;
Mexb

Fig. 2. Counterexamples of the program from Figure 1.
5

Soundness of Abs is not required for completeness of relaxed stratification.

Example 1. Let T be the quantifier-free theory of linear real arithmetic. Let Abs
be the abstraction process that, given a program (or counterexample) M and theset of predicates F ⊆ T , checks if there exists an assignment from each loop-headlocation in M to a predicate in F that forms an inductive invariant of M . Recall
the example from Section 1. Let Mex be the program shown in Figure 1. Then,the map ρ such that ρ(L4) = ρ(L7) = θex1 where θex1 ≡ a = b ⇒ y = x + z is aninductive invariant of Mex , and therefore, Abs(Mex , {θex1 }) = safe.
When given an insufficient set of predicates as the candidates, Abs returns
a counterexample. For instance, as discussed in Section 1, a possible counterexample of Mex is Mexa , shown in Figure 2, that passes through each loop once
to reach line 10. (The semantics of assume (b) is to safely halt if b is false, andproceed otherwise.) Here, a1–a4 label the entry points of the unwound loops.
Viewing them as one-iteration loops where invariants are asserted, it can beseen that ρ such that ρ(ℓ) = θex1 for each ℓ ∈ {a1–a4} is an inductive invariant of Mexa , and therefore Abs(Mexa , {θex1 }) = safe. However, as discussed in
Section 1, asserting θ0 at a1, a4, and θ1 at a2, a3 where θ0 ≡ a = b ⇒ y = x
and θ1 ≡ a = b ⇒ y = x + 1 also constitutes a sufficient loop invariant of Mexa .
Therefore, we also have Abs(Mexa , {θ0 , θ1 }) = safe.
Similarly, Mexb shown in Figure 2 is a counterexample that passes througheach loop twice to reach line 10. By reasoning similar to the above, we haveAbs(Mexb , {θex1 }) = Abs(Mexb , {θ0 , θ1 , θ2 }) = safe where θ2 ≡ a = b ⇒ y = x + 2. ▲2.2

The Relaxed Stratification Scheme

We are now ready to formalize the relaxed stratification scheme. The core of thescheme is the relaxed finite-language-restricted refinement process RlxRef thattakes as input a counterexample and a restricting predicate language (Lbase , Lext ),and returns either unsafe indicating that the counterexample is real, a set of predicates F ⊆ Lbase ∪ Lext that proves the safety of the counterexample, or noproof
indicating that it could not find a proof for the counterexample within the given
restriction.
We prepare strata of restricting predicate languages:(L0base , L0ext ), (L1base , L1ext ), . . . (Lkbase , Lkext ), . . .
We require each restricting predicate language to be finite, and the base-part toeventually cover T . Formally, we impose the following condition on the restricting
predicate languages: 1.) for each k ∈ ω, Lkbase ∪ Lkext is a finite subset of T , 2.) forkeach k ∈ ω, Lkbase ⊆ Lk+1
base , and 3.) T = ⋃k∈ω Lbase .
Figure 3 shows the overview of the relaxed stratification verification process.
The verification procedure RlxCegar takes as input the program M to be verified,
and first initializes the candidate predicate set Cands to ∅ (line 2) and therestricting language stratum k to 0 (line 3). Then, it repeats the abstract-andrefine loop (lines 4-10) until convergence. The loop first calls Abs(M, Cands) tocheck if M can be proved safe with the current candidates. If so, then we exit
the verification process, returning safe (line 6). Otherwise, a counterexample

01: RlxCegar(M ) =02: Cands := ∅;03: k := 0;
04: while true do05:
match Abs(M ,Cands) with06:
safe → return safe
07:
∣ cex(M ′ ) → match RlxRef(M ′ ,Lkbase ,Lkext ) with08:
unsafe → return unsafe
09:∣ prf(F ) → Cands := Cands ∪ F
10:∣ noproof → k := k + 1
Fig. 3. The relaxed stratification verification process.

M ′ is obtained, and we call RlxRef on M ′ and the current restricting language(Lkbase , Lkext ) (line 7). If RlxRef returns unsafe, then the counterexample is real
and we exit the verification process, returning unsafe (line 8). Otherwise, RlxRefeither returns a set of predicates that refutes the counterexample (line 9), or
returns noproof indicating that it has failed to find a proof for the counterexample
in the current language stratum (line 10). In the former case, the returned setof predicates are added to Cands, and in the latter case, the language stratum
is raised to the next level.
We require RlxRef to only report unsafe on a real counterexample, that is,
RlxRef(M, Lbase , Lext ) = unsafe only if ∀F ⊆ T .Abs(M, F ) ≠ safe, and we require the returned proof to be actually a proof of the counterexample, that is
RlxRef(M, Lbase , Lext ) = prf(F ) only if Abs(M, F ) = safe (these conditions are
not particular to relaxed stratification and usually assumed for any refinement
process in CEGAR). In addition, we require RlxRef to only infer proofs from thegiven restricting predicate language and be able to return some proof if the given
counterexample is refutable just in the base part of the language. Formally, we
impose the following additional conditions on RlxRef:– If RlxRef(M, Lbase , Lext ) = prf(F ) then F ⊆ Lbase ∪ Lext ; and– If ∃F ⊆ Lbase .Abs(M, F ) = safe, then RlxRef(M, Lbase , Lext ) = prf(F ′ ) forsome F ′ .
We state and prove the completeness of the relaxed stratification scheme.
Theorem 1 (Completeness). If ∃F ⊆ T .Abs(M, F ) = safe, then RlxCegar(M )terminates and returns safe.
We remind that safety verification is undecidable in general, and our “completeness” only states that the verification terminates under the promise that a proofof the program’s safety exists in T .6
Also, assuming that Abs is sound (cf. Section 2.1), it is easy to see that
RlxCegar is also sound in that it only proves safe programs safe (in fact, thisholds independently of the behavior of RlxRef).
6

This notion of completeness is the same as the one from previous works [8, 13].

Theorem 2 (Soundness). If Abs is sound, then RlxCegar(M ) returns safe only
if M is safe.
Example 2. We show how the relaxed stratification scheme would ensure theconvergence of a verifier on the program Mex from Example 1. Suppose that werun RlxCegar(Mex ), and for contradiction, it diverges by generating the following
infinite series of refinements discussed in Section 1:
a = b ⇒ y = x, a = b ⇒ y = x + 1, . . . a = b ⇒ y = x + i, . . .
By the definition of RlxCegar, it must be the case that the restricting predicate
lvl(i)
lvl(i)
language at the i-th CEGAR iteration is (Lbase , Lext ) such that y = x + i ∈lvl(i)
lvl(i)
Lbase ∪ Lext where lvl (i) is the restricting language stratum level in the i-thlvl(i)
lvl(i)
iteration. Because each Lbase ∪ Lext is finite, the stratum level of the language
must have been raised infinitely many times. Therefore, a = b ⇒ y = x + z ∈ Ljbase
for some j because T = ⋃k∈ω Lkbase .
But, as argued in Example 1, a = b ⇒ y = x + z is a sufficient proof of Mex ’ssafety, and therefore also that of its counterexamples. Therefore, by the fact that
RlxRef refutes any counterexample refutable in the base part of the given restricting language, for any counterexample M ′ of Mex , RlxRef(M ′ , Ljbase , Ljext ) =prf(F ′ ) for some F ′ ⊆ Ljbase ∪ Ljext . Then, because Ljbase ∪ Ljext is finite, RlxCegar
must have eventually inferred a sufficient set of predicates that constitutes a
proof of Mex ’s safety without further raising the language stratum.
▲

3

Concrete Refinement Algorithm Instances

We show how to implement the relaxed finite-language-restricted refinement
process RlxRef. In fact, we describe a technique that takes as module an exact
Lbase -restricted refinement algorithm and turn it into a relaxed (Lbase , Lbase ∧∨ )restricted refinement algorithm. (We write L∧∨ for the closure of L under conjunctions and disjunctions.) We focus on the case where the given counterexample is spurious.7
Following the recent trend [20, 4, 10, 3, 2, 15, 14, 24], we formalize the refinement algorithm as a constraint solver for recursion-free Horn-clause constraints.
Specifically, we present a relaxed (Lbase , Lext )-restricted constraint solver thattakes as module an exact Lbase -restricted constraint solver (cf. Section 3.1 forthe definition of exact/relaxed finite-language-restricted constraint solvers). We
review Horn-clause constraints in Section 3.1, and describe the constraint solver,that we call RlxSolveA, in Section 3.2.
We also present a technique that takes as module a relaxed (Lbase , Lext )restricted constraint solver, an unrestricted constraint solver AU , and a positive
integer parameter ℓ, and turn them into a relaxed (Lbase , LB(Lbase ∪Lext , AU , ℓ))restricted constraint solver where LB(L, AU, ℓ) is a certain finite language of7

Detecting if the counterexample real and returning unsafe if so can be handled via
usual unrestricted refinement (cf. Section 4).

predicates determined by L, AU , and ℓ. We formalize the technique as the constraint solver RlxSolveB, described in Section 3.3. The technique applies the relaxed finite-language-restricted constraint solver provided as the module to onlya small subset of the constraint solving problem, and can be used to improvethe efficiency of the given relaxed finite-language-restricted constraint solver.
We remind that the exact finite-language-restricted proof search is an inherently expensive process (cf. Section 5, Section 4, and Appendix F), and the
key idea in these constraint solvers is to use the expensive exact finite-languagerestricted proof search process (given as a module) only on small subparts of the
problem. This is made possible thanks to the relaxed requirement on the language restriction where the refinement process is not required to exactly decide
the existence of a restricted solution for the whole problem. Informally, the trick
is to choose the subproblems just large enough to guarantee that if a subproblem
is not Lbase solvable then neither is the whole and that there can only be finitely
many solutions for the whole obtainable from Lbase -restricted solutions for the
subproblems.
3.1

Horn Clause Constraints

For concreteness, in what follows, we assume that the underlying theory T is
the quantifier-free theory of linear real arithmetic (QFLRA). However, the techniques presented in Sections 3.2 and 3.3 can be applied to any quantifier-freetheory.
A formula θ in the signature of QFLRA comprises atomic predicate p of theform a1 x1 + a2 x2 ⋅ ⋅ ⋅ + an xn ≤ an+1 where a1 , . . . , an+1 ∈ Z, and is closed under theusual boolean operations ¬, ∧, ∨, and ⇒. As usual, we let ¬ bind the tightest and⇒ the weakest. A literal l is either an atomic predicate or its negation. A clause
C is a disjunction of literals. A conjunctive normal form (CNF) is a conjunctionof clauses. We often use a set to represent a clause or a CNF so that {l1 , . . . , ln }represents l1 ∨ ⋅ ⋅ ⋅ ∨ ln and {C1 , . . . , Cn } represents C1 ∧ ⋅ ⋅ ⋅ ∧ Cn . We write  forcontradiction and ⊺ for tautology. We write ⊧ θ when θ is valid in T .
Horn Clauses and Horn-Clause Constraints. A predicate variable application is of the form P (x̄) where P is a predicate variable of arity ∣x̄∣. A Hornclause hc is of the form θ ∧ B1 ∧ ⋅ ⋅ ⋅ ∧ Bn ⇢ H where θ is a formula in T , each Bi
is a predicate variable application, and H is a predicate variable application or. We call H the head of the Horn clause, and θ ∧ B1 ∧ ⋅ ⋅ ⋅ ∧ Bn the body. A Hornclause whose head is  is called a root clause.
A Horn-clause constraint set (HCCS) H is a finite set of Horn clauses. We
write pvs(H) for the predicate variables in H. We write leaves(H) for the setof predicate variables in H that do not occur as a head in H. We define ↝H to
be the relation {(P, Q) ∣ θ ∧ . . . P (x̄) . . . ⇢ Q(ȳ) ∈ H}. We say that a Horn clauseθ ∧ B1 ∧ ⋅ ⋅ ⋅ ∧ Bn ⇢ H is conjunctive if θ is a conjunction of literals. We say thatan HCCS H is conjunctive if each hc ∈ H is conjunctive.
We say that H is recursion-free if ↝H is acyclic. We say that a recursion-free
HCCS H is tree-like [14, 15] if 1.) there is exactly one root clause in H and everyθp1 ⇢ P (x̄)θp2 ∧ P (x̄) ⇢ P (x̄′ )P (x̄) ⇢ Q(x̄)θp3 ∧ Q(x̄) ⇢ Q(x̄′ )θp4 ∧ Q(x̄) ⇢ 

θp1 ⇢ P1 (x̄)θp2 ∧ P1 (x̄) ⇢ P2 (x̄′ )P2 (x̄) ⇢ Q1 (x̄)θp3 ∧ Q1 (x̄) ⇢ Q2 (x̄′ )θp4 ∧ Q2 (x̄) ⇢ 

θp1 ⇢ P1 (x̄)θp2 ∧ P1 (x̄) ⇢ P2 (x̄′ )θp2 ∧ P2 (x̄) ⇢ P3 (x̄′ )P3 (x̄) ⇢ Q1 (x̄)θp3 ∧ Q1 (x̄) ⇢ Q2 (x̄′ )θp3 ∧ Q2 (x̄) ⇢ Q3 (x̄′ )θp4 ∧ Q3 (x̄) ⇢ 

Hex

Hexa

Hexb

Fig. 4. HCCS examples.

P ∈ pvs(H) can reach a predicate variable occurring in the body of the root clausevia ↝∗H ; and 2.) for any P ∈ pvs(H), at most one hc ∈ H contains P in its body, atmost one hc ∈ H contains P as its head, and no hc ∈ H has multiple occurrences of
P . For a tree-like HCCS H, we define the depth of H, depth(H), to be the lengthof the longest ↝H path. For η a mapping from predicate variables to predicate
variables, we write η(hc) for the Horn clause hc with each predicate variableapplication P (x̄) replaced by η(P )(x̄). We write η(H) for {η(hc) ∣ hc ∈ H}. We
say that a tree-like HCCS H′ is an unwound instance of a (possibly recursive)
HCCS H if there exists a mapping η from pvs(H′ ) to pvs(H) such that η(H′ ) ⊆ H.
Constraint Solutions and Restricted Constraint Solvers. For σ a mapping from predicate variables to predicates in T , we write σ(hc) for hc with eachpredicate variable application P (x̄) replaced by θ[x̄/ȳ] where σ(P ) = λȳ.θ. We
say that the map σ from pvs(H) to predicates in T is a solution of H, writtenσ ⊧ H, if for each hc ∈ H, ⊧ σ(hc), interpreting ⇢ as ⇒. We define ran(σ), therange of σ, to be the set of predicates {σ(P ) ∣ P ∈ dom(σ)}.
We focus on constraint solving algorithms for tree-like HCCSs (they can beextended to arbitrary recursion-free HCCSs by adopting the technique from [15]).
We say that an algorithm is an unrestricted constraint solver if given a tree-like
HCCS H, it returns a solution of H or decides that H has no solution. We saythat an algorithm is an exact L-restricted constraint solver if given a tree-like
HCCS H, it decides if there is a solution σ of H such that ran(σ) ⊆ L and returns
such a solution if so. We say that an algorithm is a relaxed (Lbase , Lext )-restrictedconstraint solver if given a tree-like HCCS H, it either returns a solution σ of H
such that ran(σ) ⊆ Lbase ∪ Lext or returns noproof indicating that it has failed tofind a solution, with the requirement that it returns some solution (whose range
is in Lbase ∪ Lext ) if there exists a solution σ ′ of H such that ran(σ ′ ) ⊆ Lbase .
Example 3. Consider the HCCS Hex shown in Figure 4. Here, x̄ = a, b, x, y, z,x̄′ = a′ , b′ , x′ , y ′ , z ′ , andθp1 ≡ x = a ∧ y = b ∧ z = 0
θp2 ≡ z ′ = z + 1 ∧ y ′ = y + 1 ∧ x′ = x ∧ a′ = a ∧ b′ = bθp3 ≡ z ≠ 0 ∧ z ′ = z − 1 ∧ y ′ = y − 1 ∧ x′ = x ∧ a′ = a ∧ b′ = bθp4 ≡ z = 0 ∧ a = b ∧ x ≠ yHex is not tree-like (in fact, ↝S is cyclic). Figure 4 shows HCCSs Hexa andHexb that are tree-like. In addition, they are unwound instances of Hex becauseηa (Hexa ) ⊆ Hex and ηb (Hexb ) ⊆ Hex where ηa = {P1 ↦ P, P2 ↦ P, Q1 ↦ Q, Q2 ↦ Q}
and ηb = {P1 ↦ P, P2 ↦ P, P3 ↦ P, Q1 ↦ Q, Q2 ↦ Q, Q3 ↦ Q}.
Recall the predicates θext1 , θ0 , θ1 , θ2 from Example 1. Let the maps σa1 , σa2 ,
σb1 , and σb2 be defined as below.
σa1 = {P ↦ θex1 ∣ P ∈ pvs(Hexa )}σb1 = {P ↦ θex1 ∣ P ∈ pvs(Hexb )}σa2 = {P ↦ θ0 ∣ P ∈ {P1 , Q2 }}∪ {P ↦ θ1 ∣ P ∈ {P2 , Q1 }}σb2 = {P ↦ θ0 ∣ P ∈ {P1 , Q3 }}∪ {P ↦ θ1 ∣ P ∈ {P2 , Q2 }}∪ {P ↦ θ2 ∣ P ∈ {P3 , Q1 }}Then, σa1 and σa2 are solutions of Hexa , and σb1 and σb2 are solutions of Hexb .
▲Relating Refinement Process to Constraint Solving. We relate constraint
solving to refinement process. Roughly, the relationship says that, for any counterexample, there is a corresponding tree-like HCCS such that the range of its
solutions are the proofs of the counterexample’s spuriousness. We further assume that such a tree-like HCCS is always an unwound instance of some fixed“generator” HCCS determined by the given program.
We formalize the relationship. Let M be a program. We assume that there
exists an HCCS Hgen(M ) such that for any counterexample M ′ of M (i.e.,Abs(M, F ) = cex(M ′ ) for some F ), there exists an unwound instance HM ′ ofHgen(M ) that satisfies the following:– if σ ⊧ HM ′ then Abs(M ′ , ran(σ)) = safe (i.e., the range of a solution of HM ′is a proof of M ′ ’s spuriousness); and– if Abs(M ′ , F ) = safe then ∃σ. ran(σ) ⊆ F ∧σ ⊧ HM ′ (i.e., if M ′ can be refutedby F , then there is a solution for HM ′ whose range is in F ).
Hence, the task of implementing a relaxed language restricted refinement process
RlxRef for the restricting language (Lbase , Lext ) is now reduced to implementing
a relaxed (Lbase , Lext )-restricted constraint solver.
We remark that the relationship stated above is quite general and many
CEGAR-based verifiers [20, 10, 3, 2, 15, 14, 24] use the relationship to implement
the refinement process as a constraint solver for tree-like HCCSs. For example,
refuting a counterexample in a typical CEGAR-based verification of sequential
imperative programs is equivalent to solving a tree-like HCCS of the form below
where x̄ are the variables in the program, and each θi is a formula on x̄ and x̄′ that
expresses the semantics of symbolically executing the corresponding segment(e.g., basic block) in the path:θ1 ⇢ P1 (x̄)θi ∧ Pi (x̄) ⇢ Pi+1 (x̄′ )′θ2 ∧ P1 (x̄) ⇢ P2 (x̄ )⋮⋮Pn (x̄) ⇢ In such a verification, the generator HCCS Hgen(M ) can be described as follows.
Let x̄ be the variables in the program. For each node a in the program’s control
flow graph (CFG), we associate a predicate variable Pa of arity ∣x̄∣. For eachedge from node a to node b in the CFG, we add to Hgen(M ) the Horn clauseθab ∧ Pa (x̄) ⇢ Pb (x̄′ ) where θab is a formula on x̄ and x̄′ expressing the effectof symbolically executing the CFG path from a to b (with x̄ representing thecurrent and x̄′ representing the post state). For the entry node a, we add theHorn clause θinit ⇢ Pa (x̄) where θinit is a formula on x̄ expressing the program’s
initial state. Finally, for each error node a (i.e., assert false statement), we
add the Horn clause Pa (x̄) ⇢ .
Example 4. Recall the program Mex from Example 1. The corresponding generator HCCS Hgen(Mex) is Hex from Example 3. Roughly, the predicate variable
P in the HCCS represents the program states at the time when the first loop is
entered, and Q represents the states when the second loop is entered.
Recall the counterexamples Mexa and Mexb from Example 1, and the treelike HCCSs Hexa and Hexb from Example 3. Hexa corresponds to Mexa and Hexb
corresponds to Mexb . Indeed, as shown in Example 1, {θex1 } (resp. {θ0 , θ1 }) isa proof of Mexa , and Hexa has the corresponding solution σa1 (resp. σa2 ) from
Example 3. Similarly, the solutions σb1 and σb2 of Hexb and the proofs {θex1 }and {θ0 , θ1 , θ2 } of Mexb correspond.
▲
3.2

The Constraint Solver RlxSolveA

RlxSolveA is a relaxed (Lbase , Lbase ∧∨ )-restricted constraint solver. It is parameterized by an exact Lbase -restricted constraint solver that it takes as module.
Let us fix the exact solver, AE Lbase , and write RlxSolveA[AE Lbase ] for RlxSolveAparameterized by the exact solver. Note that Lbase ∧∨ is finite for a finite Lbase .
We briefly overview the construction of RlxSolveA. First, we leverage theequivalence of solving tree-like HCCS and tree interpolation [15] to reduce theproblem to tree interpolation. Then, we adopt the standard proof-based interpolation technique that obtains interpolants from resolution proofs generated
via SMT solving [12], except that we modify the SMT solver to use the exact
Lbase -restricted solver AE Lbase for the theory solver so as to infer Lbase -restricted(partial) interpolants at the theory level of the resolution proof. As we shall show,
this guarantees that if the SMT solver fails to prove, then no Lbase solution exists, and conversely, any inferred solution is guaranteed to be in Lbase ∧∨ .
We describe the approach more formally. First, we review tree interpolation.
The tree interpolation problem takes as input (V, E, Θ) where (V, E) is a finite
directed tree with the node set V and (v, v ′ ) ∈ E denoting that the node v isa direct child of the node v ′ , and the map Θ labels each node v ∈ V with the
T -formula Θ(v). The goal is to find a map I from V to T -formulas, called a treeinterpolant of (V, E, Θ), that satisfies the following.
– I(vrt ) =  for the root node vrt ;– for each v ∈ V , ⊧ Θ(v) ∧ ⋀(v′ ,v)∈E I(v ′ ) ⇒ I(v); and– for each v ∈ V , fvs(I(v)) ⊆ (⋃(v′ ,v)∈E ∗ fvs(Θ(v ′ ))) ∩ (⋃(v′ ,v)∉E ∗ fvs(Θ(v ′ ))).
We reduce constraint solving for a tree-like HCCS to tree interpolation as follows.8 Let H be the input tree-like HCCS. We transform H to an equivalent
HCCS that satisfies: 1.) for each predicate variable P ∈ pvs(H), there exists a
vector of fresh variables x̄P such that P only occurs in the form P (x̄P ), and 2.)
the only sharing of variables among Horn clauses are x̄P ’s between two Hornclauses both containing P . Then, the transformed H is reduced to the tree interpolation problem (VH , EH , ΘH ) where– VH = pvs(H) ∪ {vrt } where vrt ∉ pvs(H);– EH =↝H ∪{(P, vrt ) ∣ θ ∧ . . . P (x̄P ) . . . ⇢  ∈ H};– For each P , ΘH (P ) = θP if θP ∧⋀i Bi ⇢ P (x̄P ) ∈ H and otherwise ΘH (P ) = ;and– ΘH (vrt ) = θrt where θrt ∧ ⋀i Bi ⇢  ∈ H.
The theorem below follows from the construction, and shows the one-to-one
correspondence between the tree interpolants of (VH , EH , ΘH ) and the solutionsof H.
Theorem 3 ([15]). Let H be a tree-like HCCS. Let σ and I be such that I(vrt ) = and for each P ∈ pvs(S), σ(P ) = λx̄P .I(P ). Then, σ ⊧ H if and only if I is atree interpolant of (VH , EH , ΘH ).
Example 5. Recall the tree-like HCCS Hexa from Example 3. The corresponding
tree interpolation problem (V, E, Θ) is shown below where each x̄P1 , x̄P2 , x̄Q1 ,x̄Q2 is a quintuple of fresh variables.
V = {vrt , P1 , P2 , Q1 , Q2 }E = {(P1 , P2 ), (P2 , Q1 ), (Q1 , Q2 ), (Q2 , vrt )}Θ(P2 ) = θp2 [x̄P1 /x̄][x̄P2 /x̄′ ]Θ(P1 ) = θp1 [x̄P1 /x̄]Θ(Q2 ) = θp3 [x̄Q1 /x̄][x̄Q2 /x̄′ ]Θ(Q1 ) = x̄P2 = x̄Q1
Θ(vrt ) = θp4 [x̄Q2 /x̄]▲Now, the relaxed (Lbase , Lbase ∧∨ )-restricted constraint solving problem is reduced to relaxed (Lbase , Lbase ∧∨ )-restricted tree interpolation. That is, we would
like to find tree interpolants restricted to Lbase ∪ Lbase ∧∨ (i.e., Lbase ∧∨ ), with theguarantee to return one if there exists a Lbase -restricted tree interpolant.
Next, we describe the process of relaxed (Lbase , Lbase ∧∨ )-restricted tree interpolation. In what follows, we assume familiarity with lazy SMT and the proofbased technique for obtaining interpolants from resolution proofs [19, 12]. Let(V, E, Θ) be the tree interpolation instance to be solved. In an ordinary proofbased tree interpolation, one looks for tree interpolants by having the SMT solver
check the unsatisfiability of ⋀v∈V Θ(v) and analyzing the output resolution proof
to compute the interpolant. However, this decides the existence of, and infers,
8

The reduction is adopted from [15].

AE Lbase (Hthy(C ,V ,E ,Θ) ) = σ∀P.λx̄P .I(P ) = σ(P )(V, E, Θ) ⊢itp C ∶ I

ThyC ∈ Θ(v)Hyp

I(vrt ) = ⎧′∗⎪⎪C↑ ′ if (v, v ) ∈ E∀v ′ .I(v ′ ) = ⎨ v⎪otherwise⎪⎩⊺(V, E, Θ) ⊢itp C ∶ I⎧⎪⎪I1 (v) ∧ I2 (v)∀v.I3 (v) = ⎨⎪⎪⎩I1 (v) ∨ I2 (v)(V, E, Θ) ⊢itp C1 ∨ C2 ∶ I3

(V, E, Θ) ⊢itp p ∨ C1 ∶ I1
(V, E, Θ) ⊢itp ¬p ∨ C2 ∶ I2
Res

if p ∈ outs(v)otherwise

Fig. 5. The tree interpolation rules.

a tree interpolant from the entire T , and is unsuitable for our task (i.e., thisresults in an unrestricted constraint solver).
Instead, we modify the SMT solver so that its theory-level reasoning is delegated to the exact Lbase -restricted constraint solver AE Lbase . More specifically,
when the SMT solver builds a model of possible (propositional) satisfying assignment ¬C, instead of passing the model to a theory solver as in ordinary SMT,
we build a “fragment” HCCS Hthy(C ,V ,E ,Θ) that just contains the part of thetree interpolation problem touched by the literals in C. Formally,
Hthy(C ,V ,E ,Θ) = {¬C↡v ∧ ⋀(P,v)∈E P (x̄P ) ⇢ Hv ∣ v ∈ V }where C↡v is the set of literals of C over atomic predicates occurring in Θ(v),and Hv =  if v = vrt and Hv = Q(x̄Q ) if v is a predicate variable Q. We pass
Hthy(C ,V ,E ,Θ) to AE Lbase to decide if it has a Lbase restricted solution, and if
so, we set the obtained solution as the partial tree interpolant for the theorylevel resolution proof nodes where C occurs as the theory lemma. Otherwise,
we can safely reject that the whole problem as having no Lbase -restricted treeinterpolant and return noproof. To generate the tree interpolant for the whole,
we adopt the proof-based approach that builds the tree interpolant in a bottom
up manner following the rules shown in Figure 5.9 Here, outs(v) is the set of
atomic predicates occurring outside of the subtree rooted at v (i.e., outs(v) ={p ∣ p occurs in Θ(v ′ ) where (v ′ , v) ∉ E ∗ }), and C↑v is the set of literals of C
over the atomic predicates occurring outside of the subtree rooted at v (i.e.,C↑v = {p ∈ C ∣ p ∈ outs(v)} ∪ {¬p ∈ C ∣ p ∈ outs(v)}). The rules Hyp for clausesin the input tree and Res for resolution steps extend the analogous rules fromthe standard proof-based interpolation [12] to tree interpolation. As describedabove, Thy uses the Lbase -restricted solution computed by the exact solver for9

We assume that each Θ(v) is CNF (if not, they can be transformed so via the Tseitintransformation [22]).

the partial tree interpolant. As we show in Theorems 4 and 5 below, this achieves
the desired relaxed (Lbase , Lbase ∧∨ )-restricted tree interpolation.
First, we show that any tree interpolant obtained by the method is restricted
to Lbase ∧∨ .
Theorem 4. Let H be a tree-like HCCS and (V, E, Θ) be the corresponding treeinterpolation problem. Suppose (V, E, Θ) ⊢itp  ∶ I. Then, I is a tree interpolantof (V, E, Θ), and for all P ∈ pvs(H), λx̄P .I(P ) ∈ Lbase ∧∨ .
Next, we prove that if there is a Lbase -restricted tree interpolant for the given
tree interpolation instance, then the method infers some tree interpolant (andby Theorem 4 above, such a tree interpolant will be restricted to Lbase ∧∨ ).
Theorem 5. Let H be a tree-like HCCS and (V, E, Θ) be the corresponding treeinterpolation problem. Suppose there is a tree interpolant I of (V, E, Θ) such thatfor all P ∈ pvs(H), λx̄P .I(P ) ∈ Lbase . Then, (V, E, Θ) ⊢itp  ∶ I ′ for some I ′ .
We note that Hthy(C ,V ,E ,Θ) is always a conjunctive HCCS and is often muchsmaller than the input HCCS. Therefore, the expensive exact Lbase -restrictedconstraint solver AE Lbase is only applied to small conjunctive HCCSs, thereby
making its job easier. Also, we note that, while we have presented RlxSolveA to beparameterized by an exact Lbase -restricted constraint solver passed as module,
the algorithm actually works even if a relaxed (Lbase , Lext )-restricted constraint
solver is used in place of the exact Lbase -restricted constraint solver.10 Therefore,
RlxSolveA can actually be parameterized by RlxSolveA itself, but the solvers mustbe “primed” by some exact solver (e.g., RlxSolveA[RlxSolveA[AE Lbase ]]).
Minimizing Theory Lemmas. When ¬C is given as a possible propositionalmodel by the SMT solver, we use the exact finite-language-restricted constraint
solver AE Lbase to find a solution for Hthy(C ,V ,E ,Θ) . But, using C directly as
the theory lemma after AE Lbase finds a solution could result in the SMT solver
producing many propositional models and lead to bad performance. (This isanalogous to using C directly as the theory lemma in an ordinary lazy SMT
solving when the theory solver finds ¬C unsatisfiable.) Instead, we let AE Lbase
return the subset of the literals of C that it used to find the solution, and use it
to obtain a smaller theory lemma. (We refer to Appendix E for more detail.)
3.3

The Constraint Solver RlxSolveB

RlxSolveB is a relaxed (Lbase , LB(Lbase ∪Lext , AU , ℓ))-restricted constraint solver
which takes as module a relaxed (Lbase , Lext )-restricted constraint solver, an unrestricted constraint solver AU, and a positive integer parameter ℓ. LB(L, AU, ℓ)
is a finite language of predicates determined by L, AU , and ℓ.
We informally describe RlxSolveB. We select some fraction of predicate variables in a certain “fair” manner based on the parameter ℓ and use the relaxed
10

More precisely, it becomes a relaxed (Lbase , Lext ∧∨ )-restricted constraint solver when
passed a relaxed (Lbase , Lext )-restricted constraint solver.

(Lbase , Lext )-restricted solver provided as a module to look for solutions to justthe selected predicate variables. After restricted solutions are obtained for theselected predicate variables, we use AU to look for unrestricted solutions to theremaining predicate variables, and return the combined solution as the solution
for the input HCCS. Note that this technique reduces the number of predicate
variables that the given relaxed (Lbase , Lext )-restricted solver needs to solve for,and therefore can be used to improve the performance of a relaxed (Lbase , Lext )restricted solver. The key observation we use here is that HCCSs solved in arefinement process are all unwound instances of a fixed “generator” HCCS (i.e.,
Hgen(M )). As we shall show next, the observation can be used to guaranteethat the result is a relaxed finite-language-restricted solver, when the predicate
variable selection is done in a certain proper way.
We describe the constraint solving algorithm in detail. In what follows, we
extend the definition of a tree-like HCCS (cf. Section 3.1) so that the root clausecan be a Horn clause whose head is of the form P (x̄) where P does not occur
anywhere else in the HCCS. For such an HCCS H, we say that P is the root of
H and write root(H) = P (root(H) =  for H with a -head root clause).
01: RlxSolveB[AR(Lbase ,Lext ) , AU , ℓ](H) =02: let Y = partition(ℓ, H) in
03: let A = ⋃H′ ∈Y {root(H′ )} ∖ {} in
04: let HA = rewrite(H, A) in
05: match AR(Lbase ,Lext ) (HA ) with
06:
noproof → return noproof07:∣ sol(σA ) → return sol(σA ∪ ⋃H′ ∈Y AU (σA (H′ )))Fig. 6. The overview of RlxSolveB.

Let RlxSolveB be parameterized by the relaxed (Lbase , Lext )-restricted constraint solver AR(Lbase ,Lext ) , the unrestricted constraint solver AU , and the positive integer ℓ. Figure 6 shows the overview of RlxSolveB. RlxSolveB first partitions
the input HCCS H into a set of tree-like HCCSs of depth at most ℓ in a top-downmanner (line 2). Formally, partition is defined as follows.
partition(ℓ,H) =if depth(H) ≤ ℓ then {H}else let H′ , X = subtrees(ℓ, H) in{H′ } ∪ ⋃H∈X partition(ℓ, H)
Here, subtrees(ℓ, H) returns the pair (H′ , X) such that 1.) H′ is the largest treelike subset of H containing the root clause of H and depth(H′ ) = ℓ, and 2.) X
is the set of subtrees of H rooted at each leaf of H′ . It is easy to see that Y
partitions H (i.e., H = ⋃ Y and ∀H1 , H2 ∈ Y.H1 ≠ H2 ⇒ H1 ∩ H2 = ∅), and thateach H′ ∈ Y is a tree-like HCCS of depth at most ℓ. In fact, the partition is thecoarsest of such partitions, where the only HCCSs in the partition having depthless than ℓ are the ones whose leaf predicate variables do not appear anywhere
else in the partition.
By construction, only the root predicate variables are shared by different
HCCSs in Y (more precisely, a root of one HCCS appears as a leaf in another
HCCS). RlxSolveB selects these shared predicate variables to be the ones toinfer restricted solutions (line 3). It can be seen that the fraction of the selected
predicate variables, that is ∣A∣/∣pvs(H)∣, is inversely proportional to the size of adepth ℓ tree-like subset of H, and decreases rapidly as ℓ is increased.
To infer restricted solutions to A, RlxSolveB constructs the HCCS HA suchthat pvs(HA ) = A, and solutions of HA correspond exactly to the solutions of
H restricted to A (i.e., σ ⊧ HA if and only if ∃σ ′ .σ ′ ↾A = σ ∧ σ ′ ⊧ H ). This isdone by the operation rewrite(H, A) (line4), defined to be the application of thefollowing rewriting relation ↠ to H until convergence.
H′ ∪ {Φ1 ⇢ P (x̄), Φ2 ∧ P (ȳ) ⇢ H} ↠ H′ ∪ {Φ2 ∧ Φ1 [ȳ/x̄] ⇢ H}
Here, P ∈ pvs(H) ∖ A, and Φi ’s range over Horn clause bodies. (We assume thateach Horn clause in H is over disjoint variables. Otherwise, we transform H intosuch a form by variable renaming.)
Then, RlxSolveB calls AR(Lbase ,Lext ) to find a Lbase ∪ Lext -restricted solutionfor HA (line 5). If AR(Lbase ,Lext ) returns noproof then no Lbase solution exists for
HA by the property of AR(Lbase ,Lext ) , and by the construction above, it can beshown that no Lbase solution exists for the input HCCS H either, and we safely
return noproof (line 6) (see Theorem 7 for the proof). Otherwise, we obtain asolution σA for HA , and RlxSolveB calls AU on each element of the partition
with the solution σA substituted (i.e., AU (σA (H′ )) for each H′ ∈ Y ).11 This
gives solutions for the remaining predicate variables in H, and we return theunion of σA and these solutions as the final solution (line 7).
We argue that the produced solution is indeed a solution of H. Let Y ={H1 , . . . , Hn }. Note that the only predicate variables shared by different elements in Y are A. Therefore, σA (H1 ),. . . ,σA (Hn ), and HA are over disjoint
predicate variables, and their solutions are over disjoint domains. Then, because
Y partitions H, it follows that σA ∪ ⋃H′ ∈Y AU (σA (H′ )) is a solution of H.
To show that RlxSolveB is a relaxed finite-language-restricted constraint solver,
it remains to show that the obtained solution is restricted to a finite languageof predicates. We show that it is restricted to LB(Lbase ∪ Lext , AU , ℓ) which isdefined as follows. Let L be a finite language. We define LB(L, AU, ℓ) as follows.
LB(L, AU, ℓ) = L ∪ ⋃H′ ∈X ran(AU (H′ ))where
X = {σ(H′ ) ∣ H′ ∈ unwds(ℓ, Hgen(M )) and σ ⪰L H′ }Here, M is the program being verified (i.e., the input to the top-level procedure
RlxCegar), unwds(ℓ, H) is the set of unwound instances of H of depth at most ℓ,
11Here, we extend the notion of substitution so that the result is tree-like: for P ∈dom(σA ), σA (Φ ⇢ P (x̄)) = ¬σA (P )[x̄/ν̃(P )] ∧ σA (Φ) ⇢ .

and σ ⪰L H if and only if σ is a map from the leaves and the root of H to thepredicates in L (i.e., dom(σ) = leaves(H)∪{root(H)}∖{} and ran(H) ⊆ L). Notethat Hgen(M ) is a constant for the entire run of RlxCegar(M ), and unwds(ℓ, H)is finite for any H and ℓ. Therefore, LB(L, AU, ℓ) is a finite language that isdetermined by L, AU and ℓ.
We formally prove that RlxSolveB is indeed a relaxed (Lbase , LB(Lbase ∪Lext , AU , ℓ))-restricted constraint solver. First, we prove that the solution returned is indeed a solution of the input HCCS and that it is restricted to
LB(Lbase ∪ Lext , AU , ℓ).
Theorem 6. Suppose RlxSolveB[AR(Lbase ,Lext ) , AU , ℓ](H) returns sol(σ). Then,σ ⊧ H and ran(σ) ⊆ LB(Lbase ∪ Lext , AU, ℓ).
Next, we show that some solution is returned if there exists a Lbase -restricted
solution to the given HCCS (and by Theorem 6, such a solution is restricted to
LB(Lbase ∪ Lext , AU , ℓ)).
Theorem 7. Suppose that there exists σ such that σ ⊧ H and ran(σ) ⊆ Lbase .
Then, RlxSolveB[AR(Lbase ,Lext ) , AU, ℓ](H) infers some σ ′ such that σ ′ ⊧ H.
Example 6. Recall the HCCS Hexa from Example 3. Running RlxSolveB on Hexa
with ℓ = 2, we have Y = partition(2, Hexa ) = {H1 , H2 , H3 } where
H1 = {θp3 ∧ Q1 (x̄) ⇢ Q2 (x̄′ ), θp4 ∧ Q2 (x̄) ⇢ }
H2 = {θp2 ∧ P1 (x̄) ⇢ P2 (x̄′ ), P2 (x̄) ⇢ Q1 (x̄)}
H3 = {θp1 ⇢ P1 (x̄)}
Then, the shared predicate variables that are selected to be restricted are A ={root(H1 ), root(H2 ), root(H3 )} ∖ {} = {P1 , Q1 }. And, HA = rewrite(Hexa , A) is
as shown below.
HA = {θp3 ∧ Q1 (x̄) ∧ θp4 [x̄′ , x̄′′ /x̄, x̄′ ] ⇢ , θp2 ∧ P1 (x̄) ⇢ Q1 (x̄′ ), θp1 ⇢ P1 (x̄)}
where x̄′′ is a quintuple of fresh variables. RlxSolveB then calls AR(Lbase ,Lext )on HA to obtain a restricted solution for A. Suppose the returned solution isσA = {P ↦ a = b ⇒ y = z + x ∣ P ∈ {P1 , Q1 }}. Then, σA is applied to each elementof the partition and we obtain σA (H1 ), σA (H2 ), and σA (H3 ) shown below.
σA (H1 ) = {θp3 ∧ (a = b ⇒ y = x + z) ⇢ Q2 (x̄′ ), θp4 ∧ Q2 (x̄) ⇢ }σA (H2 ) = {θp2 ∧ (a = b ⇒ y = x + z) ⇢ P2 (x̄′ ), a = b ∧ y ≠ x + z ∧ P2 (x̄) ⇢ }σA (H3 ) = {a = b ∧ y ≠ x + z ∧ θp1 ⇢ }
AU is called on σA (H1 ), σA (H2 ), and σA (H3 ) to infer unrestricted solutions
to the remaining predicate variables. Suppose we have obtained the solutions
σ1 = {Q2 ↦ a = b ⇒ z ≠ −1 ∧ y = x + z}, σ2 = {P2 ↦ a = b ⇒ y = x + z}, and σ3 = ∅for σA (H1 ), σA (H2 ), and σA (H3 ) respectively. Finally, RlxSolveB returns the
combined map, σA ∪ σ1 ∪ σ2 ∪ σ3 , as the solution inferred for the input HCCS
Hexa .
▲

4

Implementation and Experiments

We have implemented the new refinement algorithms RlxSolveA and RlxSolveB
described in Section 3. The refinement algorithms require an exact finite-languagerestricted constraint solver and an unrestricted constraint solver to be provided
as modules. An unrestricted constraint solver finds unrestricted solutions to thegiven tree-like HCCS. This is the ordinary constraint solving for tree-like HCCSs
which is a well-studied problem, and we use the existing technique that iteratively solve the constraints one predicate variable at a time by using interpolation
as a blackbox process (see [23, 5, 20] for details).12
Exact Finite-Language-Restricted Constraint Solver. For the exact solver,
we use a simple approach in which the finite predicate languages are represented
by predicate templates containing unknowns of bounded range. We use an SMT
solver13 to find an assignment to the unknowns within the bound that makes
the templates into an actual solution. Below, we informally describe the processby an example, and defer the detailed description to Appendix E.
Example 7. Recall the program Mex from Example 1. Let Lbase be the finite language of predicates consisting of conjunctions of at most two atomic predicateswhose numeric constants are bounded in the range {−1, 0, 1}. We represent thelanguage by the bounded predicate template shown below
λa, b, x, y, z. c1 a + c2 b + c3 x + c4 y + c5 z + c6 ≤ 0∧
c7 a + c8 b + c9 x + c10 y + c11 z + c12 ≤ 0
where ci ’s are unknown constants each associated with the bound {−1, 0, 1}.
Bounded predicate templates can concisely represent a finite language of predicates.14
Let ξ be a bounded predicate template. To check if the given HCCS H has asolution in the language represented by ξ, we make a solution template σξ thatmaps each predicate variable in H to a copy of ξ with fresh unknowns. Then,
we check if there exists an assignment to the unknowns within the bounds thatmakes the solution template into an actual solution of H, that is, we look for
assignments to the unknowns within the bounds that satisfy ∀hc ∈ σξ (H). ⊧ hc.
For QFLRA, the latter can be done by applying the Motzkin’s transposition
theorem [18] to reduce the problem to the satisfiability problem for quantifierfree non-linear real arithmetic, and using an SMT solver to solve the resulting
problem.
▲
We note that the exact finite-language-restricted constraint solving is a highly
expensive process and using it directly solve the whole HCCS is prohibitive.
Indeed, as we show in the experiments, the exact solver fails to scale even on
12

The implementation uses MathSAT 5 (http://mathsat.fbk.eu/) for the backend
interpolation process.
13
The implementation uses Z3 (http://z3.codeplex.com/).
14
Note that such a language is generally not closed under conjunctions or disjunctions.

relatively small constraint sets (see also the discussion in Section 5 and thecomplexity theoretic analysis in Appendix F).
Experiment Setup. We have experimented with the new refinement algorithms
by using them in the refinement process of MoCHi [10]. MoCHi is a state-of-theart software model checker for higher-order functional programs based on predicate abstraction, CEGAR, and higher-order-recursion-scheme (HORS) model
checking. MoCHi verifies assertion safety of OCaml programs. A verifier for
functional programs such as MoCHi is suited for experimenting with the newrefinement algorithm because Horn-clause constraints generated in such a verifier often contain non-trivial tree-like structure. (Intuitively, this is because theconstraints express the flow of data in the program, and data often flow in a complex way in a functional program, e.g., passed to and returned from recursivefunctions, captured in closures, etc.)
The new refinement algorithms RlxSolveA and RlxSolveB are parametric. For
this experiment, we parameterize them as follows to obtain a single refinement
algorithm:
RlxSolveB[RlxSolveA[AE Lbase ], AU , 4]Here, the exact Lbase -restricted constraint solver AE Lbase and the unrestricted
solver AU are the ones described above. That is, we use RlxSolveB parameterized to use as modules the relaxed (Lbase , (Lbase )∧∨ )-restricted constraint solver
RlxSolveA (itself parameterized by the exact Lbase -restricted constraint solver
AE Lbase ) and the unrestricted constraint solver AU , and with the parameterℓ = 4. The strata of restricting predicate languages are built “dynamically” as
the CEGAR iteration progresses, by starting from a small fixed (L0base , L0ext )and enlarging the current (Lbase , Lext ) whenever the refinement algorithm returns noproof by using the unrestricted refinement process.15
We compare the new refinement algorithm with two other refinement methods: 1.) the ordinary (incomplete) unrestricted predicate search, and 2.) exact
finite-language-restricted predicate search. The unrestricted predicate search algorithm is AU , and the exact finite-language restricted predicate search algorithm is AE. For AE, we give (the Lbase part of) the same restricting predicate
language given to the new algorithm when solving the corresponding HCCS.
We have ran the three refinement algorithms on 318 HCCSs generated byrunning MoCHi on 139 programs, measuring the time spent in each run of therefinement process. The benchmark programs are mostly taken from the previous
work on MoCHi [10, 16, 25, 11]. To obtain the benchmark HCCS set, we ran
MoCHi on each benchmark program with the new refinement algorithm until
completion or timeout and recorded the HCCS given as the input to each run of
the refinement process. We also compare the overall verification speed of MoCHi
when using the three refinement algorithms. This is done by running MoCHi
with each of the refinement algorithm on the 139 benchmark programs. We have15

Formally, this is done by having a non-decreasing preorder of restricting predicate
languages where the limit of any ω-chain is T , and when noproof is returned, thelanguage raised to the least one containing the predicate inferred by AU.

run the experiments on a machine with 2.69 GHz i7-4600U processor with 16
GB of RAM, with the time limit of 100 seconds. The benchmark programs, thebenchmark HCCSs and the experiment results data are available online [21].
Experiment Aim and Hypothesis. Because of the overhead from computing
restricted proofs, we expect the individual refinement runs to be slower with
the new refinement algorithm compared to an ordinary incomplete approach
which only does unrestricted refinement, but faster than the more naı̈ve complete
approach that directly applies the exact finite-language-restricted proof search
to the entire refinement problem. The main purpose of the experiment is totest this hypothesis. We also compare the overall verification speeds, but we
do not expect a significant improvement on this aspect because of the inherent
complexity of the verification problem. (For any sound and QFLRA-complete
verifier, one can always find a program on which the verifier takes arbitrarily
long time.)

100

100

10

10

1

1

Exact

Unrestricted

Experiment Results and Analysis. Figure 7 shows the plots comparing thethe run times of the new refinement algorithm (New Algorithm), the unrestrictedrefinement algorithm (Unrestricted), and the exact finite-language-restricted refinement algorithm (Exact) on each of the 318 benchmark HCCSs. As we haveexpected, the unrestricted refinement algorithm is the fastest of the three. The
new algorithm performs quite competitively, however, and shows that it is able
to achieve completeness with only a low overhead. Also, the plots show thatthe exact finite-language-restricted refinement algorithm is significantly slower,
timing out on many instances that the other two algorithms were able to solve
quickly.

0.1

0.1

0.01

0.01

0.001
0.001

0.01

0.1

1

NewAlgorithm

10

100

0.001
0.001

0.01

0.1

1

10

100

NewAlgorithm

Fig. 7. Run time comparison of the refinement algorithms on benchmarks HCCSs

Figure 8 shows the plots comparing the run times of the overall verification
process on each of the 139 benchmark programs for each refinement algorithm.

100

10

10

1

1

Exact

Unrestricted

100

0.1

0.1

0.01

0.01

0.001
0.001

0.01

0.1

1

NewAlgorithm

10

100

0.001
0.001

0.01

0.1

1

10

100

NewAlgorithm

Fig. 8. Run time comparison of the refinement algorithms on benchmarks programs

The plots show that there is no clear winner in this comparison and none of
the three outperformed the others on all benchmarks (while the unrestrictedrefinement edged out in the number of instances solved within the time limit,
it also timed out on some instances the complete methods were able to solve).
This is due to the inherent undecidability of the program verification problem,
and the fact that the speed of overall verification depends heavily on subtle
heuristic choices made by MoCHi. Such issues are largely outside of the scopeof this paper, but they give interesting insights into what would be the goodheuristics to use with the new refinement algorithm. For instance, an interesting
behavior we have observed is that the stratified approaches (New Algorithm andExact) sometimes infer more useless predicates than the ordinary unrestrictedrefinement because a stratified approach needs to add predicates to raise the language stratum till it reaches the level where a proof of the given program exists.
Because MoCHi does eager predicate abstraction, its performance degrades exponentially in the number of predicates that are added to the candidate predicate
set. This seems to have had a large negative impact on the stratified approaches.
A possible way to address the issue maybe is to have MoCHi take a more lazy
approach to predicate abstraction, or allow the language strata “coarseness” tobe dynamically adjustable so that we can immediately jump to a large predicate
language when it seems beneficial.

5

Related Work

Previous work [8, 13] has considered an exact stratification approach which requires the refinement process to exactly decide if a proof of the given counterexample’s spuriousness exists in the current finite language stratum. As remarked before, an issue with exact stratification is the high cost of exact finitelanguage-restricted proof search. As we have shown empirically in Section 4,
the exact finite-language-restricted proof search suffers from high overhead. (Wealso show complexity theoretic evidences for the inherent hardness of the exact
search in Appendix F.) We note that relaxed stratification is a generalizationof exact stratification. That is, exact stratification is a special case of relaxedstratification where Lext = ∅.
We note that the interpolation technique that limits the theory-level reasoning to only emit restricted partial interpolants (cf. Section 3.2) has also been
proposed in [8]. But, they target exact stratification and therefore requires the
restricting language to be closed under conjunctions and disjunctions (so thatL∧∨ = L), which substantially reduces the applicability of the technique.16

6

Conclusion

We have presented a new approach to complete predicate refinement, called
relaxed stratification, where the background theory is stratified into a sequenceof finite predicate languages(L0base , L0ext ), (L1base , L1ext ), . . . (Lkbase , Lkext ), . . .
such that each run of the refinement process is restricted to only infer predicates from the current stratum Lbase ∪ Lext . Contrary to previous approaches
to complete refinement, the refinement process is neither required to decide theexistence of a proof for the given counterexample in Lbase ∪Lext nor in Lbase , but
is only required to return some proof if one exists in Lbase . We have proved thatthe approach is complete despite the relaxed requirement, assuming that thestrata of Lbase ’s grow to eventually cover the predicates of the underlying theory. We have shown that the relaxed requirement can be used to build practicalrefinement algorithms that have low overhead and the completeness guarantee.

References
1. M. Colón, S. Sankaranarayanan, and H. Sipma. Linear invariant generation using
non-linear constraint solving. In W. A. H. Jr. and F. Somenzi, editors, CAV, volume2725 of Lecture Notes in Computer Science, pages 420–432. Springer, 2003.
2. S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko. Synthesizing
software verifiers from proof rules. In J. Vitek, H. Lin, and F. Tip, editors, PLDI,
pages 405–416. ACM, 2012.
3. A. Gupta, C. Popeea, and A. Rybalchenko. Predicate abstraction and refinement
for verifying multi-threaded programs. In T. Ball and M. Sagiv, editors, POPL,
pages 331–344. ACM, 2011.
16

Contrary to [8], in QFLRA, it is insufficient to only look for an atomic interpolant(i.e., a separating hyperplane) when interpolating between even just conjunctionsof literals (i.e., polytopes) under a finite-language restriction. For example, consider
interpolating between y ≤ 1 ∧ 2x + y ≤ −3 ∧ x ≤ −1 and y + x ≥ 1 under the restrictionthat interpolants’ constants are in {−1, 0, 1}.

4. A. Gupta, C. Popeea, and A. Rybalchenko. Solving recursion-free horn clauses over
LI+UIF. In H. Yang, editor, APLAS, volume 7078 of Lecture Notes in Computer
Science, pages 188–203. Springer, 2011.
5. M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In M. V.
Hermenegildo and J. Palsberg, editors, POPL, pages 471–482. ACM, 2010.
6. T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions fromproofs. In N. D. Jones and X. Leroy, editors, POPL, pages 232–244. ACM, 2004.
7. R. Jhala and R. Majumdar. Software model checking. ACM Computing Surveys,
41(4), 2009.
8. R. Jhala and K. L. McMillan. A practical and complete approach to predicate
refinement. In H. Hermanns and J. Palsberg, editors, TACAS, volume 3920 ofLecture Notes in Computer Science, pages 459–473. Springer, 2006.
9. D. Jovanovic and L. M. de Moura. Solving non-linear arithmetic. In B. Gramlich, D. Miller, and U. Sattler, editors, IJCAR, volume 7364 of Lecture Notes in
Computer Science, pages 339–354. Springer, 2012.
10. N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for
higher-order model checking. In M. W. Hall and D. A. Padua, editors, PLDI,
pages 222–233. ACM, 2011.
11. T. Kuwahara, T. Terauchi, H. Unno, and N. Kobayashi. Automatic termination
verification for higher-order functional programs. In Z. Shao, editor, ESOP, volume8410 of Lecture Notes in Computer Science, pages 392–411. Springer, 2014.
12. K. L. McMillan. An interpolating theorem prover. Theoretical Computer Science,
345(1):101–121, 2005.
13. K. L. McMillan. Quantified invariant generation using an interpolating saturation
prover. In C. R. Ramakrishnan and J. Rehof, editors, TACAS, volume 4963 of
Lecture Notes in Computer Science, pages 413–427. Springer, 2008.
14. P. Rümmer, H. Hojjat, and V. Kuncak. Classifying and solving horn clauses forverification. In E. Cohen and A. Rybalchenko, editors, VSTTE, volume 8164 of
Lecture Notes in Computer Science, pages 1–21. Springer, 2013.
15. P. Rümmer, H. Hojjat, and V. Kuncak. Disjunctive interpolants for Horn-clauseverification. In N. Sharygina and H. Veith, editors, CAV, volume 8044 of Lecture
Notes in Computer Science, pages 347–363. Springer, 2013.
16. R. Sato, H. Unno, and N. Kobayashi. Towards a scalable software model checker
for higher-order programs. In E. Albert and S. Mu, editors, PEPM, pages 53–62.
ACM, 2013.
17. M. Schaefer and C. Umans. Completeness in the polynomial-time hierarchy: A
compendium. SIGACT news, 33(3):32–49, 2002.
18. A. Schrijver. Theory of linear and integer programming. Wiley, 1998.
19. R. Sebastiani. Lazy satisability modulo theories. JSAT, 3(3-4):141–224, 2007.
20. T. Terauchi. Dependent types from counterexamples. In M. V. Hermenegildo and
J. Palsberg, editors, POPL, pages 119–130. ACM, 2010.
21. T. Terauchi and H. Unno. Relaxed stratification: A new approach to practicalcomplete predicate refinement. 2015. http://www.jaist.ac.jp/~ terauchi.
22. G. S. Tseitin. On the complexity of derivation in propositional calculus. Studies
in constructive mathematics and mathematical logic, 2(115-125):10–13, 1968.
23. H. Unno and N. Kobayashi. Dependent type inference with interpolants. In
A. Porto and F. J. López-Fraguas, editors, PPDP, pages 277–288. ACM, 2009.
24. H. Unno and T. Terauchi. Inferring simple solutions to recursion-free horn clauses
via sampling. In TACAS, 2015. To appear.

25. H. Unno, T. Terauchi, and N. Kobayashi. Automating relatively complete verification of higher-order functional programs. In R. Giacobazzi and R. Cousot, editors,
POPL, pages 75–86. ACM, 2013.

A

Proof of Theorem 1

The following lemma states that the candidates returned by the refinement process must contain a new predicate.
Lemma 1 (Progress). Let Abs(M, F ) = cex(M ′ ) and RlxRef(M ′ , Lbase , Lext ) =prf(F ′ ). Then, F ′ ⊆/ F .
Proof. Because RlxRef(M ′ , Lbase , Lext ) = prf(F ′ ), Abs(M ′ , F ′ ) = safe. Also, because Abs(M, F ) = cex(M ′ ), Abs(M ′ , F ) ≠ safe. Therefore, F ≠ F ′ , and by themonotonicity of Abs, it follows that F ′ ⊆/ F .
⊔⊓Theorem 1 (Completeness). If ∃F ⊆ T .Abs(M, F ) = safe, then RlxCegar(M )terminates and returns safe.
Proof. Let F ⊆ T be such that Abs(M, F ) = safe. Because Abs(M, F ) = safe,
for any counterexample M ′ of M (i.e., Abs(M, F ′ ) = cex(M ′ ) for some F ′ ),RlxRef(M ′ , Lbase , Lext ) ≠ unsafe for any (Lbase , Lext ). Therefore, it suffices toshow that RlxCegar(M ) terminates.
For contradiction, suppose that RlxCegar(M ) does not terminate. Let j ∈ ω
be such that F ⊆ Ljbase (by the definition of the restricting language strata, suchlvl(i)
lvl(i)
j exists). Let (Lbase , Lext ) be the restricting predicate language at the i-th
CEGAR iteration. By Lemma 1, infinitely many predicates must have been returned as candidates. Therefore, at some iteration, the language stratum musthave reached level j, because RlxRef at each lvl (i)-th language stratum is relvl(i)lvl(i)
stricted to only infer predicates from the finite set Lbase ∪ Lext .
By the fact that RlxRef refutes any counterexample refutable in the Lbasepart of the given restricting language and the fact that F is sufficient to refute any counterexample of M , for any counterexample M ′ of M , we have
RlxRef(M ′ , Ljbase , Ljext ) = prf(F ′ ) for some F ′ . Therefore, by Lemma 1 and thefiniteness of Ljbase ∪ Ljext , it follows that a sufficient proof of M ’s safety musthave been inferred without further raising the language stratum, and we obtaina contradiction.
⊔⊓

B

Proofs of Theorem 4 and Theorem 5

Let ins(v) be the atomic predicates occurring in the subtree rooted at v, thatis, ins(v) = {p ∣ p occurs in Θ(v ′ ) where (v ′ , v) ∈ E ∗ }. Let C↓v = C ∖ C↑v , that
is, C↓v are the literals of C over atomic predicates not occurring outside of thesubtree rooted at v.

We state the following assumptions regarding the input tree interpolation
instance and the theory lemmas, which can be enforced by making each atomic
predicate in the input syntactically distinct.17(A1) For C a theory lemma, for each p occurring in C, there is a unique v ∈ Vsuch that p occurs in Θ(v).
(A2) For C a theory lemma, for each v ∈ V , ¬C↡v ⇒ Θ(v).
(A3) For each v, v ′ ∈ V and C ∈ Θ(v), C↓v ′ = C if (v, v ′ ) ∈ E ∗ and otherwiseC↓v ′ = .
(A1) says that theory lemmas are used only to “communicate” atomic predicatesacross nodes. This follows from the observation that a lazy SMT solver interprets the atomic predicates in the input tree interpolation instance as distinct
propositional variables. (A2) is a consequence of the fact that the negation of atheory lemma is a possible satisfying assignment of ⋀v∈V Θ(v) with the atomic
predicates interpreted as distinct propositional variables.
The following lemma states that any atomic predicate occurring in the derivation is from the input tree interpolation instance.
Lemma 2. Let (V, E, Θ) ⊢itp C ∶ I. Then, for any p occurring in C, and anyv ∈ V , p ∈ outs(v) or p ∈ ins(v).
Proof. By induction on the derivation of (V, E, Θ) ⊢itp C ∶ I.
B.1

⊔
⊓

Proof of Theorem 4

Theorem 4. Let H be a tree-like HCCS and (V, E, Θ) be the corresponding treeinterpolation problem. Suppose (V, E, Θ) ⊢itp  ∶ I. Then, I is a tree interpolantof (V, E, Θ), and for all P ∈ pvs(H), λx̄P .I(P ) ∈ Lbase ∧∨ .
We define a C-partial tree interpolant to be a map I from V to formulas inT such that
(pitp-1) I(vrt ) =  for the root node vrt ;(pitp-2) for each v ∈ V , ⊧ Θ(v) ∧ ¬C↓v ∧ ⋀(v′ ,v)∈E I(v ′ ) ⇒ I(v); and(pitp-3) for each v ∈ V , fvs(I(v)) ⊆ (⋃(v′ ,v)∈E ∗ fvs(Θ(v ′ )))∩(⋃(v′ ,v)∉E ∗ fvs(Θ(v ′ ))).
Note that only the second condition, (pitp-2), differs from the definition of (nonpartial) tree interpolant. Essentially, the condition (pitp-2) is the corresponding
condition from the tree interpolant definition except that the labeling Θ(v) isstrengthened by ¬C↓v . Clearly, a -partial tree interpolant is a tree interpolant.
Therefore, Theorem 4 follows from the following lemma.
Lemma 3. Let H be a tree-like HCCS and (V, E, Θ) be the corresponding treeinterpolation problem. Suppose (V, E, Θ) ⊢itp C ∶ I. Then, I is a C-partial treeinterpolant of (V, E, Θ), and (♣) for all P ∈ pvs(H), λx̄P .I(P ) ∈ Lbase ∧∨ .
17

In practice, we label the atomic predicate occurring in the different nodes of the
input tree interpolation instance with disjoint sets of labels, and define C↑v and C↡v
to distinguish the atomic predicates by the labels.

Proof. By induction on the derivation of (V, E, Θ) ⊢itp C ∶ I. We prove by a caseanalysis on the last rule.
Thy
Conditions (♣), (pitp-1), and (pitp-3) are trivially satisfied. We show condition (pitp-2) for each v. By (A1), we have that ¬C↓v ⇒ ¬C↡v . Therefore, byTheorem 3 and the property of AE, if v is a predicate variable P , thenΘ(P ) ∧ ¬C↓P ∧ ⋀(Q,P )∈E φQ ⇒ φP
And, for v = vrt , we haveΘ(vrt ) ∧ ¬C↓vrt ∧ ⋀(Q,vrt )∈E φQ ⇒ 
HypConditions (♣) and (pitp-1) are trivially satisfied. Condition (pitp-3) follows
from (A3). We show condition (pitp-2) for each v ′ . For v ′ such that (v, v ′ ) ∉E ∗ , the condition is trivial. Let (v, v ′ ) ∈ E ∗ . Because C↓v′ ∨ C↑v′ = C, thecondition is equivalent to Θ(v ′ ) ∧ ⋀(v′′ ,v′ )∈E I(v ′′ ) ⇒ C. If v ′ = v, then the
result follows from Θ(v) ⇒ C. Otherwise, for some v ′′ such that (v ′′ , v ′ ) ∈ E,
we have that I(v ′′ ) = C↑v′′ , and the result follows from C↑v′′ ⇒ C.
Res
Conditions (♣), (pitp-1), and (pitp-3) follow immediately from induction
hypothesis. We show condition (pitp-2) for each v. We split the argumenton whether p ∈ outs(v) or not.
Case p ∈ outs(v)We have I3 (v) = I1 (v) ∧ I2 (v). For any v ′ such that (v ′ , v) ∈ E, we havep ∈ outs(v ′ ). Therefore, I3 (v ′ ) = I1 (v ′ )∧I2′ (v ′ ) for any such v ′ . Therefore,
it suffices to show that
Θ(v) ∧ ¬(C1 ∨ C2 )↓v ∧ ⋀(v′ ,v)∈E I1 (v ′ ) ∧ I2 (v ′ )⇒ I1 (v) ∧ I2 (v)By induction hypothesis, we haveΘ(v) ∧ ¬(p ∨ C1 )↓v ∧ ⋀(v′ ,v)∈E I1 (v ′ ) ⇒ I1 (v)and,Θ(v) ∧ ¬(¬p ∨ C2 )↓v ∧ ⋀(v′ ,v)∈E I2 (v ′ ) ⇒ I2 (v)Because (p ∨ C1 )↓v = C1 ↓v and (¬p ∨ C2 )↓v = C2 ↓v , the result follows.
Case p ∉ outs(v)We have I3 (v) = I1 (v) ∨ I2 (v). By Lemma 2, there is at most one v ′ suchthat (v ′ , v) ∈ E and p ∉ outs(v ′ ). Let v ′ be such a node. (The argument issimilar for the case when no such v ′ exists, i.e., when p occurs in Θ(v).)
Let
V ′′ = {v ′′ ∣ (v ′′ , v) ∈ E and p ∈ outs(v ′′ )}Then, it suffices to show that
Θ(v) ∧ ¬(C1 ∨ C2 )↓v ∧(I1 (v ′ ) ∨ I2 (v ′ )) ∧ ⋀v′′ ∈V ′′ I1 (v ′′ ) ∧ I2 (v ′′ )⇒ I1 (v) ∨ I2 (v)By induction hypothesis, we haveΘ(v) ∧ ¬(p ∨ C1 )↓v ∧ ⋀(v′ ,v)∈E I1 (v ′ ) ⇒ I1 (v)and,Θ(v) ∧ ¬(¬p ∨ C2 )↓v ∧ ⋀(v′ ,v)∈E I2 (v ′ ) ⇒ I2 (v)Because (p ∨ C1 )↓v = p ∨ C1 ↓v and (¬p ∨ C2 )↓v = ¬p ∨ C2 ↓v , the result
follows from the fact
(I1 (v ′ ) ∨ I2 (v ′ )) ∧ ⋀v′′ ∈V ′′ I1 (v ′′ ) ∧ I2 (v ′′ ) ⇒(⋀(v′ ,v)∈E I1 (v ′ )) ∨ (⋀(v′ ,v)∈E I2 (v ′ ))and a resolution on p.
⊔⊓
B.2

Proof of Theorem 5

Theorem 5. Let H be a tree-like HCCS and (V, E, Θ) be the corresponding treeinterpolation problem. Suppose there is a tree interpolant I of (V, E, Θ) such thatfor all P ∈ pvs(H), λx̄P .I(P ) ∈ Lbase . Then, (V, E, Θ) ⊢itp  ∶ I ′ for some I ′ .
The theorem follows from the lemma below and the refutation completenessof resolution (for CNF).
Lemma 4. Let H be a tree-like HCCS and (V, E, Θ) be the corresponding treeinterpolation problem. Suppose that there exists a tree interpolant I of (V, E, Θ)such that for all P ∈ pvs(H), λx̄P .I(P ) ∈ Lbase . Suppose that C is a theory
lemma. Then, (V, E, Θ) ⊢itp C ∶ I ′ for some I ′ .
Proof. We derive (V, E, Θ) ⊢itp C ∶ I ′ via Thy. It suffices to show that σ suchthat σ(P ) = λx̄P .I(P ) for each P is a Lbase solution of Hthy(C ,V ,E ,Θ) . By
construction, ran(σ) ⊆ Lbase . Therefore, it suffices to show that ⊧ σ(hc) for eachhc ∈ Hthy(C ,V ,E ,Θ) .
Because I is a tree interpolant of (V, E, Θ), we have⋀¬Θ(vrt ) ∧σ(Q) ⇒ (Q,vrt )∈E

and for each P ,¬Θ(P ) ∧⋀(Q,vrt )∈E

σ(Q) ⇒ σ(P )Therefore, by (A2), for the root clause of Hthy(C ,V ,E ,Θ) , we have¬C↡vrt ∧⋀σ(Q) ⇒ (Q,vrt )∈E

And, for each non-root clause in Hthy(C ,V ,E ,Θ) , we have
¬C↡P ∧⋀

σ(Q) ⇒ σ(P )(Q,P )∈E⊔⊓C

Proof of Theorem 6

Theorem 6. Suppose RlxSolveB[AR(Lbase ,Lext ) , AU , ℓ](H) returns sol(σ). Then,σ ⊧ H and ran(σ) ⊆ LB(Lbase ∪ Lext , AU, ℓ).
Proof. The solution σ inferred is of the form σA ∪ ⋃i∈{1,...,n} σi where– σA is a solution of HA ; and– each σi is a solution of σA (Hi ) such that {H1 , . . . , Hn } = Y partitions the
input HCCS H.
By construction, we have that σA ∪ σi ⊧ Hi for each Hi ∈ Y . Therefore, by
disjointness of σA and each σi , we have σ ⊧ H.
Next, we show that ran(σ) ⊆ LB(Lbase ∪ Lext , AU , ℓ). For each Hi , we haveHi ∈ unwds(ℓ, Hgen(M ) ) and σA ⪰Lbase ∪Lext Hi . Therefore, for each Hi ,ran(σi ) = ran(AU (σA (Hi ))) ⊆ ⋃H′ ∈X ran(AU(H′ ))where X = {σ(H′ ) ∣ H′ ∈ unwds(ℓ, Hgen(M )) and σ ⪰L H′ }. Therefore, we haveran(σ) ⊆ LB(Lbase ∪ Lext , AU , ℓ) because ran(σA ) ⊆ Lbase ∪ Lext .
⊔⊓D

Proof of Theorem 7

Theorem 7. Suppose that there exists σ such that σ ⊧ H and ran(σ) ⊆ Lbase .
Then, RlxSolveB[AR(Lbase ,Lext ) , AU, ℓ](H) infers some σ ′ such that σ ′ ⊧ H.
Proof. Let Y , A and HA be as constructed in Figure 6. Let σ↾A be σ restricted
to A. Then, by construction, σ↾A ⊧ HA . Therefore, HA has a Lbase solution, andAR(Lbase ,Lext ) (HA ) returns some solution σA of HA .
By construction, there exists σ ′ ⊇ σA such that σ ′ ⊧ H. Therefore, eachσA (Hi ) for Hi ∈ Y is solvable because σ ′ ↾pvs(σA (Hi )) ⊧ σA (Hi ). Then, because
AU returns some solution of the given solvable HCCS, it follows that RlxSolveB
returns some solution of H.
⊔⊓

E

Exact L-restricted Constraint Solving for QFLRA

A term t in the signature of QFLRA is either a variable x or an affine expression
a1 t1 +⋅ ⋅ ⋅+an tn +an+1 where a1 , . . . , an+1 are integer constants. We define a bounded
term template to be an expression of the form cb t where t is a term and cb isan bounded unknown constant annotated with a finite set b ⊆ Z as its bound. We
define a bounded formula template to be a QFLRA formula that contain bounded
{0,1}
{1,2}
{0,1}
+ c2 x + c3 y ≤ z isterm templates as (ordinary) terms. For example, c1
a bounded formula template. We define bounded predicate template to be of theform λx̄.φ where φ is a bounded formula template and fvs(φ) ⊆ {x̄}.
For a bounded predicate template ξ, we define Lξ to be the set of (nontemplate) predicates obtained by replacing each cb in ξ by an integer a ∈ b.
Clearly, Lξ is finite for any ξ.
We describe the exact Lξ -restricted constraint solver AE Lξ . It takes a treelike HCCS H as input and looks for a solution σ such that σ ⊧ H and ran(σ) ⊆ Lξ .
AE Lξ does this as follows. First, by variable renaming, we transform H into aform such that each Horn clause is over disjoint variables. Then, we translate
H to σξ (H) where σξ maps each predicate variable P ∈ pvs(S) to ξP such that
ξP is a copy of ξ with the unknowns replaced fresh unknowns with the same
bounds. 18
Note that σξ (S) has no predicate variable. Let Ψ = ⋀ σξ (S). Ψ is a bounded
formula template, interpreting ⇢ as ⇒. Let cb11 , . . . , cbnn be the bounded unknowns
occurring in Ψ , and x̄ be the variables occurring in Ψ . Now, to find an assignment
to the unknowns that make the bounded formula templates into a solution ofH, it suffices to find an assignment to each cbi i within the bound bi that satisfy∀x̄.Ψ .
We convert Ψ to an equivalent formula ⋀i ϕi via a CNF conversion so thateach ϕi is of the form ¬(Ax̄ ≤ a ∧ B x̄ < b) where A and B (resp. a and b) arematrices (resp. vectors) whose elements are polynomials on cb11 , . . . , cbnn . Then,
we translate each ϕi by applying Motzkin’s transposition theorem [18]:Theorem 8 (Motkin’s transposition theorem). Consider the following system of linear inequalities over real-valued variables x̄.
Ax̄ ≤ a ∧ B x̄ < b
The system is unsatisfiable if and only if there exist non-negative real-valued
vectors r and p such thatrA + pB = 0 ∧ (ra + pb < 0 ∨ (p ≠ 0 ∧ ra + pb ≤ 0))
Applying the Motzkin’s transposition theorem, the satisfiability of ∀x̄. ⋀i ϕi
is reduced to that of Ψ ′ where Ψ ′ is a quantifier-free non-linear real arithmetic
18

For simplicity, we assumes that the predicate variables in H have same arities. Otherwise, the restricting language is represented by a bounded predicate template pera predicate variable of different arities.

formula on variables r̄, p̄, and cb11 , . . . , cbnn where the variables r̄ and p̄ are factor
variables that are introduced in the translation. Finally, we conjunct Ψ ′ withthe formula encoding the bound information for each cbi i , and apply a decision
procedure for quantifier-free non-linear real arithmetic [9] to find a satisfying
assignment to the unknowns. If no satisfying assignments are found, then we
return noproof. Otherwise, the assignments found for the unknowns cb11 , . . . , cbnn
are substituted to σξ to obtain a solution for the input HCCS.
Note that, contrary to the template-based program verification [1] that use
the templates directly as a solution for a recursive constraint set (i.e., one withcyclic ↝H if expressed as Horn-clause constraints), we use the templates to solve
only recursion-free constraints. The role of templates here is only for restricting
the solution to a finite language.
Returning Small Models to Minimize Theory Lemmas. Recall that the
input to AE given by RlxSolveA is a HCCS HC that consists of Horn clausesof the form ¬C↡v ∧ ⋀(Q,v)∈E Q(x̄Q ) ⇢ H where ¬C is the possible model foundby the SMT solver (cf. Section 3.2). To minimize the model, we wish to find asmall subset C ′ ⊆ C such that HC ′ is still Lξ solvable where HC ′ is HC with each
formula part of the body ¬C↡v replaced with ¬C ′ ↡v . To this end, we solve HC as
described above and obtain a solution σ for HC . Then, we check the assignment
inferred for the factor variables r̄ and p̄ and remove from C any literal whose
associated factor has 0 inferred as the assignment (note that each literal of C
is associated with some row of [A∣a] or [B∣b]) and return the resulting model
along with σ. The correctness of the approach follows from the fact that such
literals do not contribute to the solution σ obtained for HC .

F

Computational Complexity of Exact Finite-LanguageRestricted Predicate Search

Formally, the decision version of exact finite-language-restricted predicate searchis the problem of deciding, given a tree-like HCCS S and repl (L) representing
a finite language, whether there exists a solution for S in L. We investigate theproblem’s computational complexity for QFLRA.19
First, we note that the unrestricted version of the problem is coNP-complete.
This follows from the equivalence of tree-like HCCS solving and tree interpolation(cf. Section 3.2) and the fact that (the decision version of) tree interpolation for
QFLRA is coNP-complete.
Next, we consider the case when repl (L) is given as a bounded predicate
template as described in Section 4. Then, the exact finite-language-restrictedpredicate search problem can be shown to be Σ2 -complete. The result shows a
gap from the unrestricted case, assuming that the polynomial hierarchy does notcollapse at the first level.
19

A similar analysis can be applied to other FOL theories whose TAUT and (unrestricted) interpolation are coNP-complete.

Theorem 9. The exact finite-language-restricted predicate search problem isΣ2 -complete for repl (L) given as a bounded predicate template.
Proof.
In Σ2This is immediate from the fact that checking whether a given assignmentσ ∶ pvs(S) → L is a solution of S is in coNP.
Σ2 -hard
We reduce from the Σ2 -complete problem of deciding if a quantified propositional formula of the form ∃x̄.∀ȳ.Φ is true, where Φ is a propositional formulaon variables x̄, ȳ. Let ∃x̄.∀ȳ.Φ be the given formula. Let x1 , ..., xn = x̄, andy1 , ..., ym = ȳ Let c1 , ..., cn = c̄ be unknowns each having the bound {0, 1}. We
construct a bounded predicate template repl (L) of the form λȳ.φ where φis a bounded formula template on variables ȳ and unknowns c̄ such that for
all v¯x ∈ {0, 1}n and v¯y ∈ Rm , ¬φ[v¯x /c̄][v¯y /ȳ] if and only if v¯y ∈ {0, 1}m andΦ[v¯x /x̄][v¯y /ȳ]. Formally, ¬φ can be constructed from Φ by replacing eachvariable occurrence xi ∈ x̄ (resp. yi ∈ ȳ) by ci = 1 (resp. yi = 1), and conjuncting the formula xi = 0 ∨ xi = 1 for each variable xi ∈ x̄. Let S = {P (ȳ) ⇢ }.
Then, S has a solution in L if and only if ∃x̄.∀ȳ.Φ is true.
⊔⊓
We note that, in general (for QFLRA), the problem of exact finite-languagerestricted predicate search is in Σ2 for any language representation where thesize of formulas in the language is polynomial in the size of the representation.
Next, we consider the case when repl (L) represents the maximum size of
formulas in L. We consider three definitions of “formula size”. We show that the
problem is Σ2 -hard when the size is defined to be the number of literals in CNF
or DNF, and is Σ2 -hard under Turing-reductions when the size is defined to be
the number of literals (in arbitrary form). (Here, we assume that the constants
appearing in L are finitely bounded, so that L is finite.)
Theorem 10. For repl (L) given as the size of the maximum formula in L, theexact finite-language-restricted predicate search problem is– Σ2 -hard when the size is defined to be the number of literals in CNF;
– Σ2 -hard when the size is defined to be the number of literals in DNF; and– Σ2 -hard under Turing-reductions when the size is defined to be the numberof literals.
Proof. Σ2 -hardness for the CNF case is shown by a reduction from SHORT
CNF, and by a reduction from MIN DNF for the DNF case, and by a reduction
from MINIMUM EQUIVALENT EXPRESSION for the general case [17]. The
reduction in each case has the same structure: we use the observation that exact
finite-language-restricted predicate search contains the problem of finding anequivalent formula in the restricting language. That is, checking if there exists a
formula in L equivalent to the given formula θ can be reduced to checking if the
HCCS {θ ⇢ P (x̄), P (x̄) ∧ ¬θ ⇢ } has a solution in L where x̄ are the variables
occurring in θ.
⊔⊓