Interpolation of SMT formulas is dificult, especially in the presence of quantifiers since quantifier instantiations introduce mixed terms, i.e., terms containing symbols that belong to diferent partitions of the input formula. Existing interpolation algorithms for quantified formulas require proof modifications or syntactical restrictions on the generated proof trees. We present a non-restrictive, proof tree preserving approach to compute inductive sequences of interpolants for quantified formulas in the theory of equality with uninterpreted functions using a single proof tree.
We present an interpolation procedure for quantified formulas in the theory of equality with
uninterpreted functions. Interpolants have various applications in model checking, for example,
during abstraction refinement or invariant generation [
Many verification problems require the ability to reason about quantifiers, which are, among
others, needed in user-added assertions, for the modeling of unsupported theories or memory
modeling [
Our method is based on the proof tree preserving interpolation approach [
The contributions of this paper are a proof tree and satisfiability preserving scheme for the virtual modification of mixed terms, a scheme to interpolate instantiation clauses generated by a quantifier solver, and modifications of interpolation rules for theory lemmas and resolvents to generate valid inductive sequences of interpolants from a single proof tree.
Related Work. Interpolation goes back to Craig [
Gleiss et al. [
Bonacina and Johansson [
The method presented by Kovács and Voronkov [
A basis for our work is the interpolation method by Christ and Hoenicke [
Finally, Christ et al. [
We assume the usual notions of first-order logic. A theory is defined by a signature that contains interpreted and uninterpreted constant, function, and predicate symbols, and by a set of axioms that settle the meaning for its interpreted symbols. We consider the theory of equality (with uninterpreted functions), whose axioms state reflexivity, symmetry, and transitivity for the single interpreted symbol, the equality predicate =, and congruence for each uninterpreted function symbol.
As usual, a term is a variable, a constant, or an application of an -ary function symbol to terms. An atom is the formula that is always true (⊤), an equality between two terms, or the application of an -ary predicate to terms. A literal is an atom or its negation. A clause is a disjunction of literals, and a formula is in conjunctive normal form (CNF) if it is a conjunction of clauses. We assume that formulas are in CNF where each clause can be preceded by universal quantifiers only. This can be accomplished by Skolemization.
We usually denote functions by , , ℎ, terms by , , , , variables by , , , , literals by ℓ, clauses by , the empty clause by ⊥, and formulas by , , , , . For two formulas and , we use |= to denote that is a logical consequence of in the theory of equality. Formula is unsatisfiable if and only if |= ⊥. We denote the equivalence of two formulas by ≡ . A formula is said to be ground if it does not contain any variable.
A substitution maps variables to terms. We denote the result of substituting the terms ¯ for the variables ¯ in a formula (¯) by (¯). We call a substitution ground if the terms ¯ are ground. By [ℓ] we denote a formula in negation normal form where the literal ℓ only occurs positively, and by [ ] the same formula where all occurrences of ℓ are replaced by the formula .
The basis for our interpolation procedure is an instantiation-based resolution proof for the unsatisfiability of a given formula. We shortly describe the structure of such proofs and how interpolants can be computed from ground resolution proofs.
the result of applying a ground substitution for the variables ¯ to the body , i.e., the formula (¯) for ground terms ¯. Most SMT solvers treat problems containing quantified formulas by successively adding instances of the quantified formulas to the ground part which is then solved in the usual way (e.g., with the DPLL( )/CDCL algorithm). This approach is mainly suitable to show unsatisfiability of a formula, but it can also show satisfiability in some restricted fragments.
A resolution proof for the unsatisfiability of a formula in CNF is a derivation of the empty clause ⊥ using the rule 1 ∨ ℓ 2 ∨ ¬ℓ
1 ∨ 2
where 1 and 2 are clauses, and ℓ is a literal called the pivot (literal). A resolution proof can
be represented by a tree. For a formula in a theory that contains quantified subformulas,
the tree has three types of leaves: input clauses, theory lemmas, i.e., clauses that are valid in
the theory , and instantiation clauses of the form ¬(∀¯.(¯)) ∨ (¯). Note that we treat the
quantified formula as a literal which also occurs positively as an input clause. The inner nodes
are clauses obtained by resolution, and the unique root node is the empty clause ⊥.
Interpolation. A Craig interpolant [
We call the formulas the partitions2 of the interpolation problem. If a symbol occurs in two partitions and , we can assume that it also occurs in all partitions between and without changing the symbol condition of the sequence interpolants. Therefore, we say a symbol virtually occurs in if it occurs in some with ≤ and in some with ≤ .
Each interpolant in a sequence interpolant is also a binary interpolant of :≡ 1 ∧ · · · ∧ and :≡ +1 ∧ · · · ∧ . Note that not every sequence of binary interpolants obtained by such partitioning is a sequence interpolant. A literal is mixed if there is no partition where all symbols of the literal virtually occur. All literals of the input problem are obviously not mixed, but mixed literals can be introduced by Nelson-Oppen equality propagation.
Interpolants can be computed from resolution proofs, e.g., with the interpolation systems by
Pudlák [
2The word partition can be used in English for the sections, or the boundaries, or the whole partitioning. In this
paper we use the word partition for one section of the partitioning.
least one color and that all symbols in the literal occur in the corresponding partition. Mixed
literals require a diferent interpolation scheme where projections ℓ ⇂ are defined diferently.
Proof Tree Preserving Interpolation. The proof tree preserving interpolation framework
allows for computing binary [
A mixed equality literal = or ̸= is a literal where is colored with [′, ] and is colored with [, ′] where these intervals are disjoint. W.l.o.g., we assume that < . We also say that this literal is , -mixed. The basic idea is to use a fresh auxiliary variable for each mixed equality literal. When projecting a , -mixed literal, we split it into two literals using the auxiliary variable.
( = ) ⇂ :≡ ( = ) ( = ) ⇂ :≡ ( = ) ( = ) ⇂ :≡ ⊤ ( ̸= ) ⇂ :≡ EQ (, ) ( ̸= ) ⇂ :≡ ¬ EQ (, ) ( ̸= ) ⇂ :≡ ⊤ for ̸= , for ̸= , Here, EQ is an uninterpreted predicate that forces the interpolant to have a certain shape. The interpolation procedure treats EQ and as shared symbols, which may occur in the interpolant. Note that ℓ ⇂ ∧ ℓ ⇂ is equisatisfiable to ℓ and has the same models for the symbols in ℓ.
Again, we define the partial interpolants of a clause as the sequence interpolant for the
sequence 1 ∧ ¬ ⇂ 1, . . . , ∧ ¬ ⇂ . If the negation ¬ of a clause contains a mixed
equality = , the partial interpolants for with ≤ < may contain the auxiliary
variable . If ¬ contains ̸= , we require that the variable in the interpolant only occurs
in atoms of the form EQ (, ) which must occur positively in . This is not really a restriction
as interpolants naturally have this shape. The are shared terms, which are closely related to
equality-interpolating terms in the sense of [
As mentioned earlier, an interpolant is computed by annotating each clause in the proof tree, starting with the leaves, by a partial interpolant 0, . . . , . We denote this by : 1, . . . , − 1 (we omit 0 ≡ ⊤ and ≡ ⊥ ). Resolution combines the partial interpolants of the involved clauses. To resolve on a mixed literal = , we combine the partial interpolants of the input clauses using the following function that replaces all occurrences of EQ (, ) in by a copy of ′ where all occurrences of are replaced by .
ruleEq ( = , [EQ (, 1)]...[EQ (, )], ′()) :≡ [′(1)]...[′()] The following rule is used to compute the partial interpolants for the resolvent of a resolution rule from the partial interpolants of the antecedents.
1 ∨ ℓ : 1, . . . , − 1
2 ∨ ¬ℓ : 1′, . . . , ′− 1 1 ∨ 2 : ′′, . . . , ′′− 1 1 with ′′ :≡ ⎧ ⎪ ∨ ′ ⎪ ⎪ ⎪⎨ ∧ (resolution) ⎪ruleEq (ℓ, , ′) ⎪ ⎪ ⎪⎩( ∨ ℓ) ∧ (′ ∨ ¬ℓ) if ℓ has colors [, ] with ≤ < .
if ℓ has only colors ≤ , if ℓ has only colors > , if ℓ is , -mixed, ≤ < , Example 1 (Mixed Literals). Consider the following two (tautological) clauses :≡ = ∨ ̸= ∨ ̸=
′ :≡ ̸= ∨ ̸= () ∨ = (), where is 1-local, is 2-local, and the remaining symbols are shared. A partial interpolant of is the formula EQ (, ), since it is an interpolant of ¬ ⇂ 1 ≡ EQ (, ) ∧ = and ¬ ⇂ 2 ≡ ¬
EQ (, ) ∧ = .
This interpolant can be obtained by using well-known interpolation techniques for the theory
of equality. Note that EQ (, ) captures the equality-interpolating term of = in the sense
of [
The interpolant for the resolvent of and ′ can now be obtained using the resolution rule: = ∨ ̸= ∨ ̸= : EQ (, ) ̸= ∨ ̸= () ∨ = () : = () ̸= ∨ ̸= () ∨ ̸= ∨ = () : = () The interested reader is invited to check that the annotated partial interpolant is correct.
One obstacle to use proof tree preserving interpolation in the presence of quantifiers are mixed terms. To illustrate the problem, let us consider the following example.
Example 2 (Running Example). Take the sequence of formulas 1, 2, 3 with 1 : ∀.(ℎ()) = 2 : ∀. (()) ̸= 3 : ∀. () = .
The conjunction of the three formulas is unsatisfiable, which can be seen as follows. Instantiating 1 with gives (ℎ()) = . Instantiating 2 with ℎ() gives ((ℎ())) ̸= . Substituting (ℎ()) using the first equality yields () ̸= , which is clearly a contradiction to 3.
A mixed term is a term that uses symbols from at least two diferent partitions. In the example above, a mixed term is ℎ(), because ℎ only occurs in 1 and only occurs in 2. Mixed terms may be generated during the instantiation process of quantified formulas. They can thus appear in a resolution proof within instantiation clauses and theory lemmas but not in input clauses. A resolution node may contain a mixed term if it was already contained in one of its antecedents. Interpolation algorithms based on resolution proofs usually rely upon non-mixed terms. We do not want to restrict the instantiation procedure to local terms as this would negatively efect the performance of the solver. Transforming the proofs into localized proofs in the context of sequence interpolation can break the inductivity property if not done in a consistent manner. So it would require to either localize the proof for all partitions at once or to compute the interpolants by repeated binary interpolation, which requires a new proof for each interpolant.
We propose a method to handle mixed terms, simply by coloring them with some input partition. This partition does not contain all symbols occurring in the term. Thus, we replace subterms of the wrong color by fresh variables to purify the term. Each variable is defined by adding an auxiliary equation to all partitions where the subterm’s outer function symbol occurs.
We proceed by first assigning a color to each term, and purify mixed terms afterwards. As a symbol may appear in several partitions, we can assign one or multiple of these partitions as its color. However, this decision may afect the number of quantifiers within the final interpolant. We use the following coloring scheme to obtain as few quantifiers as possible. To color a term, we start by coloring its subterms from bottom up. The color of a constant symbol corresponds to the partitions it occurs in. For a function application (1, . . . , ), we compute the intersection of the partitions where occurs and the colors of the terms 1, . . . , . If the intersection is non-empty, it is used to color the term. Otherwise, if it is empty, meaning that the term contains symbols for which there is no common partition. We color the term by all partitions in which the function symbol occurs. The whole literal is then colored as if the top-level terms occurred in the partitions corresponding to the terms’ colors.
If the literal ℓ colored with partition contains a mixed term, it contains some constant or function application (1, . . . , ) where or does not occur in the partition . In the projection ℓ ⇂ , these constants and function applications are replaced by fresh variables (1,...,). Each fresh variable is set equal to the term it stands for by an auxiliary equation of the form (1,...,) = (1 , . . . , ). The arguments of the function application are also replaced by fresh variables and the corresponding auxiliary equations are added to their corresponding partitions, i.e., the term is flattened.
Example 3 (Purification) . Take the sequence of formulas 1, 2, 3 from the running example (Example 2). Consider the literal ℓ ≡ (ℎ()) = that stems from instantiating 1. The subterm occurs only in partition 2. The term ℎ() is mixed since ℎ only occurs in partition 1. We assign it partition 1. The term (ℎ()) is now also assigned partition 1 as it is the intersection where occurs (1, 2) and what its argument ℎ() was assigned. The whole literal is treated as mixed equality, since the left-hand side (ℎ()) of ℓ is colored 1 and the right-hand side is colored 2.
When computing the projection of the mixed equality ℓ ⇂ , we split ℓ first into (ℎ()) = and = , as we explained in Section 3. In the projection, we further replace the subterm on the left-hand side (that does not match partition 1) with a fresh variable. The auxiliary equation is added to partition 2, since this is the partition where occurs.
ℓ ≡ (ℎ()) = :
ℓ ⇂ 1 ≡ (ℎ()) = , ℓ ⇂ 2 ≡ = ∧ = , ℓ ⇂ 3 ≡ ⊤ Consider the literal ℓ ≡ ((ℎ())) = that stems from instantiating 2. As before, the term (ℎ()) is assigned partition 1. The term ((ℎ())) is mixed as is only in partition 2, 3. So the whole term gets assigned partitions 2, 3. Since the right-hand side of the equality appears only in partition 2, the whole literal is assigned partition 2.
When computing the projection, we replace all subterms not occurring in partition 2 with fresh variables, as well as their subterms. The auxiliary equations are added to the partitions where the corresponding function symbol appears. ℓ ≡ ((ℎ())) = :
ℓ ⇂ 1 ≡ ℎ = ℎ(), ℓ ⇂ 2 ≡ ((ℎ)) = ∧ = , ℓ ⇂ 3 ≡ ⊤ Note that if ℎ occurred in multiple partitions, the auxiliary equation ℎ = ℎ() would be added to all projections where ℎ occurs in the partition.
As mentioned in Section 3, our algorithm computes for each clause in the resolution proof a partial interpolant of 1 ∧ ¬ ⇂ 1, . . . , ∧ ¬ ⇂ . Interpolation of leaf clauses is performed based on the color of literals, i.e., the interpolants are computed as if the literal occurred in the partition corresponding to its color. This may introduce symbols from the wrong partition in the interpolant, i.e., the resulting interpolant may violate the symbol condition. The algorithm then replaces all terms containing symbols that are not allowed in the interpolant by their auxiliary variable. In many cases, these auxiliary variables are allowed to occur in the partial interpolant, since they satisfy the symbol condition with respect to the corresponding interpolation problem 1 ∧ ¬ ⇂ 1, . . . , ∧ ¬ ⇂ .
We say that a variable is supported by a clause if the term that it replaced occurs within a mixed term in , that is, if the auxiliary equation defining is part of one of the projections ¬ ⇂ . Note that a variable may be unsupported even if the corresponding subterm occurs in the clause, e.g., is not supported by () ̸= , because the literal contains no mixed term and thus there is no auxiliary equation for . A variable may only appear unbound in the partial interpolant of a clause if it is supported by . Thus, in a post-processing step, we bind variables that are not supported by the current clause but still occur in a partial interpolant. An existential quantifier is introduced around the interpolant for each unsupported variable where the head function symbol appears in . Similarly, a universal quantifier is introduced for if appears in . If multiple variables become unsupported at the same time, we need to be careful to add the quantifiers in the right order. If one of the variables corresponds to a subterm of the other, then the variable for the outer term is defined using the variable of the subterm. Hence its quantifier needs to appear after the quantifier for the variable of the outer term. Since we add quantifiers from inside to outside, we need to add the quantifiers in inverse dependency order, i.e., the quantifier for the variable corresponding to the outermost term needs to be added first.
In this section, we show how to compute partial sequence interpolants for the diferent clause types involved in a proof of unsatisfiability for quantified input formulas. The overall algorithm follows a simple common theme: first compute the interpolants using only the colors we assigned to literals and ignore the symbol condition. Then introduce the fresh variable for every term that violates the symbol condition. Finally, introduce quantifiers for each variable that is unsupported by the current clause, as outlined in Section 4.2. In the following, we concretize this for the diferent kind of clauses in the resolution proof.
Input Clauses. Input clauses cannot contain mixed terms. The interpolant of an input clause is either ¬(¬ ∖ ) if the clause is part of , or ¬ ∖ if is part of . Here ¬ ∖ removes all literals from that do not have any color from . For Pudlák’s algorithm where each literal is colored with all partitions it occurs in, all literals are removed and the interpolants are always either ⊤ or ⊥. Instantiation Clauses. We say that an instantiation clause originates from the partition in which its quantified formula occurs in. We extend the definition of ¬ ∖ to handle a , -mixed equality = as follows: if both , are in , then (ℓ ∖ ) ≡ ⊤ , if both are in , then (ℓ ∖ ) ≡ ℓ, and if is in and in , then ( = ∖ ) ≡ = and ( ̸= ∖ ) ≡ ¬ EQ (, ). Analogously, we define ¬ ∖ . The partial sequence interpolant is then computed in three steps.
1. Set to ¬(¬ ∖ ) if originates from , and to ¬ ∖ , otherwise. 2. Replace every subterm in that must not occur in according to the symbol condition by its corresponding fresh variable .
3. Introduce quantifiers for each variable that is not supported by .
Theory Lemmas. Our proof tree can contain theory lemmas for transitivity and congruence. 1 ̸= 2 ∨ · · · ∨ 1 ̸= ′1 ∨ · · · ∨ − 1 ̸= ∨ 1 = ̸= ′ ∨ (1, . . . , ) = (′1, . . . , ′) (transitivity) (congruence) Transitivity lemmas are interpolated by summarizing equality chains involving -colored literals in the negation of the lemma. If the single equality of the transitivity lemma is mixed, the chain EQ (, 1) ∧ 1 = · · · = is summarized by EQ (, ). As the ends of the -colored chains are also -colored (the boundary terms appear in -colored literals), this satisfies the symbol condition except when a mixed term contains a subterm from a diferent partition. To ifx the interpolant, all subterms from the wrong partition are replaced by their corresponding variable . Our construction guarantees that these variables are supported by .
For congruence lemmas, the interpolant depends on the color of the equality (1, . . . , ) = (′1, . . . , ′). If it is colored with a partition from , the interpolant is ¬(¬ ∖ ) and if it is colored with a partition from , the interpolant is ¬ ∖ . If the equality is a mixed equality where (1, . . . , ) is from , then is shared and the interpolant is EQ (, (1, . . . , )) where is the variable for the projection of the mixed equality, and for = 1, . . . , the term is the auxiliary variable of = ′ , if that equality is mixed, or if the equality is colored with , or ′ if it is colored with . Again, the subterms from the wrong partition are replaced by their corresponding variable , which is supported by .
Resolution Clauses. The partial interpolant for a resolution node is computed by the rule (resolution) in Section 3. Since the resolution rule removes a literal from both antecedent clauses, the resolvent may no longer support all variables occurring in the interpolant. So in the last step, we add quantifiers for all unsupported variables as outlined in Section 4.2. Example 4. We illustrate the algorithm on our running example (Example 2).
1 : ∀.(ℎ()) = 2 : ∀. (()) ̸= 3 : ∀. () = The symbol occurs in partitions 2–3, in 1–2, ℎ in 1, in 2. Our goal is to compute sequence interpolants 1, 2 where 1 implies 1, and 1 and 2 imply 2, and 2 and 3 imply ⊥. Also 1 may only contain the symbol and 2 only the symbol . ⊤ The first input clause on the top left of the proof tree is from 1, i.e., it is in 1 and 2. By the rule for input clauses its interpolants are ⊥, ⊥. The projections of the negated instantiation clause Inst on the top right are ¬Inst ⇂ 1 ≡ (1∧EQ (, (ℎ()))) ¬Inst ⇂ 2 ≡ (¬ EQ (, )∧ = ) ¬Inst ⇂ 3 ≡ ⊤ .
For 1, the quantified formula is in 1, and the interpolant is first set to ¬(¬ ∖ 1). Since (ℎ()) = is 1, 2-mixed, ((ℎ()) ̸= ∖ 1) is ¬ EQ (, ) and 1 is set to EQ (, ). In the ifnal step, the forbidden symbol is replaced by its shared variable yielding EQ (, ). The variable is supported by the clause and therefore not quantified. The interpolant 2 is just ⊥ as it contains only literals with colors 1–2. Resolving the first two clauses builds the disjunction of the corresponding interpolants, because the literal is colored with partition 1.
The equality in the congruence lemma, in the second row in Figure 1, is colored with partition 2. Therefore, interpolant 1 is first set to ¬ ∖ 1, which is (ℎ()) = . As the function symbol ℎ may not occur in the interpolant, the term ℎ() is replaced by its auxiliary variable ℎ. The interpolant 2 is set to ⊥ since the lemma involves no literal colored with partition 2. The result is (ℎ) = , ⊥, which is indeed a sequence interpolant of ℎ = ℎ() ∧ (ℎ()) = , ((ℎ)) ̸= () ∧ = ∧ = , ⊤. The next resolution step involves a 1, 2-mixed literal. Therefore, we use the third case (ruleEq ) of rule (resolution). The first interpolants of the antecedents are combined by replacing EQ (, ) with (ℎ) = , yielding (ℎ) = . All literals in the transitivity lemma (third row) are colored with partition 2. Therefore the resulting interpolants are ⊤, ⊥. The resolution step combines the interpolants with conjunction or disjunction, respectively, as the literal is colored with partition 2.
The second instantiation clause is completely colored with partition 2 as is the corresponding input clause. The interpolants are just ⊤, ⊥ and resolving them with the other branch does not change the previous interpolants. However, since the literal ((ℎ())) ̸= gets removed in the resolution step, ℎ and are no longer supported. Therefore, quantifiers are introduced: the inner existential quantifier for the 1-colored outermost term ℎ = ℎ() and the outer universal quantifier for the 2-colored inner term = . Note that although the clause still contains in the literal () ̸= , this literal is not mixed and therefore does not support .
The last instantiation clause is originating from 3, hence 1 is set to ¬ ∖ 1 (which is ⊤) and 2 is set to ¬ ∖ 2. Since () ̸= is colored with partition 2, the second interpolant is ∀.(ℎ()) = ⊥, ⊥
¬(∀.(ℎ()) = ), (ℎ()) = EQ(, ), ⊥ (ℎ()) = EQ(, ), ⊥
(ℎ()) ̸= , ((ℎ())) = () (ℎ) = , ⊥ ((ℎ())) = () (ℎ) = , ⊥
((ℎ())) ̸= (), () ̸= , ((ℎ())) = ⊤, ⊥ () ̸= , ((ℎ())) = (ℎ) = , ⊥ ∀. (()) ̸= ⊤, ⊥
¬(∀. (()) ̸= ), ((ℎ())) ̸= ⊤, ⊥ ((ℎ())) ̸= ⊤, ⊥ () ̸= ∀.∃ℎ.(ℎ) = , ⊥
Input Clause Instantiation Clause
Theory Lemma
Resolvent ∀. () = ⊤, ⊤
¬(∀. () = ), () = ⊤, ∃. () ̸= () = ⊤, ∃. () ̸= ⊥ ∀.∃ℎ.(ℎ) = , ∃. () ̸= () ̸= . In the next step, is replaced by its auxiliary variable and since this is not supported by the clause, an existential quantifier must be introduced. So the partial sequence interpolant is ⊤, ∃. () ̸= . This is indeed a valid interpolant for the sequence ⊤, () ̸= , ∀. () = .
In the last two resolution steps, the interpolants are combined with conjunction or disjunction. Since for each resolution step one of the interpolants is ⊤ or ⊥, the other interpolant is not changed. The final sequence interpolant, i.e., ∀∃ℎ.(ℎ) = , ∃. () ̸= , can be found in the annotation of the empty clause.
We presented an algorithm to obtain inductive sequences of interpolants from instantiationbased refutation proofs of quantified formulas in the theory of equality. In contrast to most existing algorithms that allow for interpolation of quantified formulas, our approach works on non-local proofs. It neither requires to restrict the inference done by the SMT solver, nor does it require transformations of the proof tree. Mixed terms occurring in a proof tree due to quantifier instantiations are directly treated using virtual purification. To obtain (partial) interpolants satisfying the symbol condition, local terms are replaced by auxiliary variables that are eventually bound by quantifiers.
Our algorithm computes sequence interpolants from a single proof of unsatisfiability instead
of repeatedly performing binary interpolation on several proof trees. Implementation of the
algorithm in SMTInterpol [
This work was partially supported by the German Research Council (DFG) under HO 5606/1-2.