Proof Tree Preserving Interpolation

TL;DR

This paper introduces a novel scheme for computing Craig interpolants in SMT solving that preserves proof trees and handles mixed literals without limiting inferences or transforming proof structures.

Contribution

It presents a proof tree preserving interpolation scheme for SMT solvers that efficiently manages mixed literals without restricting inference steps.

Findings

Implemented in SMTInterpol solver

Handles uninterpreted functions and linear arithmetic

Extensible to other theories

Abstract

Craig interpolation in SMT is difficult because, e. g., theory combination and integer cuts introduce mixed literals, i. e., literals containing local symbols from both input formulae. In this paper, we present a scheme to compute Craig interpolants in the presence of mixed literals. Contrary to existing approaches, this scheme neither limits the inferences done by the SMT solver, nor does it transform the proof tree before extracting interpolants. Our scheme works for the combination of uninterpreted functions and linear arithmetic but is extendable to other theories. The scheme is implemented in the interpolating SMT solver SMTInterpol.

Equations

$$\left(\underset{i\in \{1,\dots ,n\}}{\bigwedge }(G_i\to G_i^{\prime })\right)\to (F[G_1]\dots [G_n]\to F[G_1^{\prime }]\dots [G_n^{\prime }])$$

$$F_1[G_1]\dots [G_n]\wedge F_2[G_1]\dots [G_n]$$

$$F_1[G_1]\dots [G_n]\vee F_2[G_1]\dots [G_n]$$

$${\hbox{$\displaystyle\displaystyle{\hbox{\hskip 49.19846pt\vbox{\hbox{\hskip-49.19844pt\hbox{\hbox{$\displaystyle\displaystyle C_{1}\lor\ell:I_{1}\quad C_{2}\lor\lnot\ell:I_{2}$}}}\vbox{}}}\over\hbox{\hskip 21.87494pt\vbox{\vbox{}\hbox{\hskip-21.87494pt\hbox{\hbox{$\displaystyle\displaystyle C_{1}\lor C_{2}:I_{3}$}}}}}}$}}\quad\text{where }I_{3}=\begin{cases}I_{1}\lor I_{2}&\text{if }\ell\downharpoonright B=\top\\ I_{1}\land I_{2}&\text{if }\ell\downharpoonright A=\top\\ \begin{array}[]{l}(I_{1}\lor\ell)\land{}\\ (I_{2}\lor\lnot\ell)\end{array}&\text{otherwise}\end{cases}$$

$$A\wedge \neg C_1\downharpoonright A\wedge \neg C_2\downharpoonright A\models I_3.$$

$$A\wedge \neg C_1\downharpoonright A\wedge \neg \ell \downharpoonright A\models I_1$$

$$A\wedge \neg C_2\downharpoonright A\wedge \ell \downharpoonright A\models I_2$$

$$B\wedge \neg C_1\downharpoonright B\wedge \neg C_2\downharpoonright B\wedge I_3\models \perp$$

$$B\wedge \neg C_1\downharpoonright B\wedge \neg \ell \downharpoonright B\wedge I_1\models \perp$$

$$B\wedge \neg C_2\downharpoonright B\wedge \ell \downharpoonright B\wedge I_2\models \perp$$

$$(a=b)\downharpoonright A$$

$$(a\ne b)\downharpoonright A$$

$$(a+b\le c)\downharpoonright A$$

$$(\forall \vec{x}.(\neg \ell \downharpoonright A\to I_1)\wedge (\ell \downharpoonright A\to I_2))\to I_3$$

$$I_3\to (\exists \vec{x}.(\neg \ell \downharpoonright B\wedge I_1)\vee (\ell \downharpoonright B\wedge I_2))$$

$$A\wedge \neg C_1\downharpoonright A\wedge \neg \ell \downharpoonright A\models I_1$$

$$A\wedge \neg C_2\downharpoonright A\wedge \ell \downharpoonright A\models I_2$$

$$A\wedge \neg C_1\downharpoonright A\models \forall \vec{x}.\neg \ell \downharpoonright A\to I_1$$

$$A\wedge \neg C_2\downharpoonright A\models \forall \vec{x}.\ell \downharpoonright A\to I_2$$

$$A\wedge \neg C_1\downharpoonright A\wedge \neg C_2\downharpoonright A\models \forall \vec{x}.(\neg \ell \downharpoonright A\to I_1)\wedge (\ell \downharpoonright A\to I_2)$$

$$A\wedge \neg C_1\downharpoonright A\wedge \neg C_2\downharpoonright A\models I_3.$$

$$B\wedge \neg C_1\downharpoonright B\wedge \neg C_2\downharpoonright B\wedge I_3\models \perp .$$

$$(\neg \ell \downharpoonright B\wedge I_1)\vee (\ell \downharpoonright B\wedge I_2)$$

$$B\wedge \neg C_1\downharpoonright B\wedge \neg \ell \downharpoonright B\wedge I_1\models \perp$$

$$B\wedge \neg C_2\downharpoonright B\wedge \ell \downharpoonright B\wedge I_2\models \perp$$

$$F_1[G_{11}]\dots [G_{1n}]\wedge F_2[G_{21}]\dots [G_{2m}]\to$$

$$F_1[F_2[G_{311}]\dots [G_{31m}]]\dots [F_2[G_{3n1}]\dots [G_{3nm}]].$$

$$\underset{i\in \{1,\dots ,n\}}{\bigwedge }\underset{j\in \{1,\dots ,m\}}{\bigwedge }((G_{1i}\wedge G_{2j})\to G_{3ij})$$

$$\iff \underset{i\in \{1,\dots ,n\}}{\bigwedge }\underset{j\in \{1,\dots ,m\}}{\bigwedge }(G_{1i}\to (G_{2j}\to G_{3ij}))$$

$$\iff \underset{i\in \{1,\dots ,n\}}{\bigwedge }(G_{1i}\to \underset{j\in \{1,\dots ,m\}}{\bigwedge }(G_{2j}\to G_{3ij}))$$

$$\Rightarrow \underset{i\in \{1,\dots ,n\}}{\bigwedge }(G_{1i}\to (F_2[G_{21}]\dots [G_{2m}]\to F_2[G_{3i1}]\dots [G_{3im}]))$$

$$\iff \underset{i\in \{1,\dots ,n\}}{\bigwedge }(F_2[G_{21}]\dots [G_{2m}]\to (G_{1i}\to F_2[G_{3i1}]\dots [G_{3im}]))$$

$$\iff (F_2[G_{21}]\dots [G_{2m}]\to \underset{i\in \{1,\dots ,n\}}{\bigwedge }(G_{1i}\to F_2[G_{3i1}]\dots [G_{3im}]))$$

$$\Rightarrow (F_2[G_{21}]\dots [G_{2m}]\to (F_1[G_{11}]\dots [G_{1n}]\to$$

$$F_1[F_2[G_{311}]\dots [G_{31m}]]\dots [F_2[G_{3n1}]\dots [G_{3nm}]]))$$

$$\iff (F_1[G_{11}]\dots [G_{1n}]\wedge F_2[G_{21}]\dots [G_{2m}])\to$$

$$F_1[F_2[G_{311}]\dots [G_{31m}]]\dots [F_2[G_{3n1}]\dots [G_{3nm}]]))$$

$$EQ(x,s)$$

$$\frac{\text{vbox}{C}_1\vee a=b:I_1[EQ(x,s_1)]\dots [EQ(x,s_n)]C_2\vee a\ne b:I_2(x)\text{vbox}}{\text{vbox}\text{vbox}{C}_1\vee C_2:I_1[I_2(s_1)]\dots [I_2(s_n)]}$$

Full text

1 Introduction

A Craig interpolant for a pair of formulae $A$ and $B$ whose conjunction is unsatisfiable is a formula $I$ that follows from $A$ and whose conjunction with $B$ is unsatisfiable. Furthermore, $I$ only contains symbols common to $A$ and $B$. Model checking and state space abstraction [16, 21] make intensive use of interpolation to achieve a higher degree of automation. This increase in automation stems from the ability to fully automatically generate interpolants from proofs produced by modern theorem provers.

For propositional logic, a SAT solver typically produces resolution-based proofs that show the unsatisfiability of an error path. Extracting Craig interpolants from such proofs is a well understood and easy task that can be accomplished, e. g., using the algorithms of Pudlák [25] or McMillan [20]. An essential property of the proofs generated by SAT solvers is that every proof step only involves literals that occur in the input.

This property does not hold for proofs produced by SMT solvers for formulae in a combination of first order theories. Such solvers produce new literals for different reasons. First, to combine two theory solvers, SMT solvers exchange (dis-)equalities between the symbols common to these two theories in a Nelson-Oppen-style theory combination. Second, various techniques dynamically generate new literals to simplify proof generation. Third, new literals are introduced in the context of a branch-and-bound or branch-and-cut search for non-convex theories. The theory of linear integer arithmetic for example is typically solved by searching a model for the relaxation of the formula to linear rational arithmetic and then using branch-and-cut with Gomory cuts or extended branches [8] to remove the current non-integer solution from the solution space of the relaxation.

The literals produced by either of these techniques only contain symbols that are already present in the input. However, a literal produced by one of these techniques may be mixed111Mixed literals sometimes are called uncolourable. in the sense that it may contain symbols occurring only in $A$ and symbols occurring only in $B$. These literals pose the major difficulty when extracting interpolants from proofs produced by SMT solvers.

In this paper, we present a scheme to compute Craig interpolants in the presence of mixed literals. Our interpolation scheme is based on syntactical restrictions of partial interpolants and specialised rules to interpolate resolution steps on mixed literals. This enables us to compute interpolants in the context of a state-of-the-art SMT solver without manipulating the proof tree or restricting the solver in any way. We base our presentation on the quantifier-free fragment of the combined theory of uninterpreted functions and linear arithmetic over the rationals or the integers. The interpolation scheme is used in the interpolating SMT solver SMTInterpol [4].

Related Work.

Craig [6] shows in his seminal work on interpolation that for every inconsistent pair of first order formulae an interpolant can be derived. In the proof of the corresponding theorem he shows how to construct interpolants without proofs by introducing quantifiers in the interpolant. For Boolean circuits, Pudlák [25] shows how to construct quantifier-free interpolants from resolution proofs of unsatisfiability.

A different proof-based interpolation system is given by McMillan [20] in his seminal paper on interpolation for SMT. The presented method combines the theory of equality and uninterpreted functions with the theory of linear rational arithmetic. Interpolants are computed from partial interpolants by annotating every proof step. The partial interpolants have a specific form that carries information needed to combine the theories. The proof system is incomplete for linear integer arithmetic as it cannot deal with arbitrary cuts and mixed literals introduced by these cuts.

Brillout et al. [2] present an interpolating sequent calculus that can compute interpolants for the combination of uninterpreted functions and linear integer arithmetic. The interpolants computed using their method might contain quantifiers since they do not use divisibility predicates. Furthermore their method limits the generation of Gomory cuts in the integer solver to prevent some mixed cuts. The method presented in this paper combines the two theories without quantifiers and, furthermore, does not restrict any component of the solver.

Yorsh and Musuvathi [26] show how to combine interpolants generated by an SMT solver based on Nelson-Oppen combination. They define the concept of equality-interpolating theories. These are theories that can provide a shared term $t$ for a mixed literal $a=b$ that is derivable from an interpolation problem. A troublesome mixed interface equality $a=b$ is rewritten into the conjunction $a=t\land t=b$. They show that both, the theory of uninterpreted functions and the theory of linear rational arithmetic are equality-interpolating. We do not explicitly split the proof. Additionally, our method can handle the theory of linear integer arithmetic without any restriction on the solver. The method of Yorsh and Musuvathi, however, cannot deal with cuts used by most modern SMT solvers to decide linear integer arithmetic.

Cimatti et al. [5] present a method to compute interpolants for linear rational arithmetic and difference logic. The method presented in this paper builds upon their interpolation technique for linear rational arithmetic. For theories combined via delayed theory combination, they show how to compute interpolants by transforming a proof into a so-called ie-local proof. In these proofs, mixed equalities are close to the leaves of the proof tree and splitting them is cheap since the proof trees that have to be duplicated are small. A variant of this restricted search strategy is used by MathSAT [13] and CSIsat [1].

Goel et al. [12] present a generalisation of equality-interpolating theories. They define the class of almost-colourable proofs and an algorithm to generate interpolants from such proofs. Furthermore they describe a restricted DPLL system to generate almost-colourable proofs. This system does not restrict the search if convex theories are used. Their procedure is incomplete for non-convex theories like linear arithmetic over integers since it prohibits the generation of mixed branches and cuts.

Recently, techniques to transform proofs gained a lot of attention. Bruttomesso et al. [3] present a framework to lift resolution steps on mixed literals into the leaves of the resolution tree. Once a subproof only resolves on mixed literals, they replace this subproof with the conclusion removing the mixed inferences. The newly generated lemmas however are mixed between different theories and require special interpolation procedures. Even though these procedures only have to deal with conjunctions of literals in the combined theories it is not obvious how to compute interpolants in this setting. Similar to our algorithm, they do not restrict or interact with the SMT solver but take the proof as produced by the solver. In contrast to our approach, they manipulate the proof in a way that is worst-case exponential and rely on an interpolant generator for the conjunctive fragment of the combined theories.

McMillan [22] presents a technique to compute interpolants from Z3 proofs. Whenever a sub-proof contains mixed literals, he extracts lemmas from the proof tree and delegates them to a second (possibly slower) interpolating solver.

For the theory of linear integer arithmetic $\mathcal{LA}\left(\mathbb{Z}\right)$ a lot of different techniques were proposed. Lynch et al. [19] present a method that produces interpolants as long as no mixed cuts were introduced. In the presence of such cuts, their interpolants might contain symbols that violate the symbol condition of Craig interpolants.

For linear Diophantine equations and linear modular equations, Jain et al. [17] present a method to compute linear modular equations as interpolants. Their method however is limited to equations and, thus, not suitable for the whole theory $\mathcal{LA}\left(\mathbb{Z}\right)$.

Griggio [14] shows how to compute interpolants for $\mathcal{LA}\left(\mathbb{Z}\right)$ based on the $\mathcal{LA}\left(\mathbb{Z}\right)$-solver from MathSAT [13]. This solver uses branch-and-bound and the cuts from proofs [8] technique. Similar to the technique presented by Kroening et al. [18] the algorithm prevents generating mixed cuts and, hence, restricts the inferences done by the solver.

2 Preliminaries

In this section, we give an overview of what is needed to understand the procedure we will propose in the later sections. We will briefly introduce the logic and the theories used in this paper. Furthermore, we define key terms like Craig interpolants and symbol sets.

Logic, Theories, and SMT.

We assume standard first-order logic. We operate within the quantifier-free fragments of the theory of equality with uninterpreted functions $\mathcal{EUF}$ and the theories of linear arithmetic over rationals $\mathcal{LA}\left(\mathbb{Q}\right)$ and integers $\mathcal{LA}\left(\mathbb{Z}\right)$. The quantifier-free fragment of $\mathcal{LA}\left(\mathbb{Z}\right)$ is not closed under interpolation. Therefore, we augment the signature with division by constant functions $\left\lfloor\frac{\cdot}{k}\right\rfloor$ for all integers $k\geq 1$.

We use the standard notations $\models_{T},\bot,\top$ to denote entailment in the theory $T$, contradiction, and tautology. In the following, we drop the subscript $T$ as it always corresponds to the combined theory of $\mathcal{EUF}$, $\mathcal{LA}\left(\mathbb{Q}\right)$, and $\mathcal{LA}\left(\mathbb{Z}\right)$.

The literals in $\mathcal{LA}\left(\mathbb{Z}\right)$ are of the form $s\leq c$, where $c$ is an integer constant and $s$ a linear combination of variables. For $\mathcal{LA}\left(\mathbb{Q}\right)$ we use constants $c\in\mathbb{Q}_{\varepsilon}$, $\mathbb{Q}_{\varepsilon}:=\mathbb{Q}\cup\{q-\varepsilon|q\in\mathbb{Q}\}$ where the meaning of $s\leq q-\varepsilon$ is $s<q$. For better readability we use, e. g., $x\leq y$ resp. $x>y$ to denote $x-y\leq 0$ resp. $y-x\leq-\varepsilon$. In the integer case we use $x>y$ to denote $y-x\leq-1$.

Our algorithm operates on a proof of unsatisfiability generated by an SMT solver based on DPLL$(T)$ [24]. Such a proof is a resolution tree with the $\bot$-clause at its root. The leaves of the tree are either clauses from the input formulae222W. l. o. g. we assume input formulae are in conjunctive normal form. or theory lemmas that are produced by one of the theory solvers. The negation of a theory lemma is called a conflict.

The theory solvers for $\mathcal{EUF}$, $\mathcal{LA}\left(\mathbb{Q}\right)$, and $\mathcal{LA}\left(\mathbb{Z}\right)$ are working independently and exchange (dis-)equality literals through the DPLL engine in a Nelson-Oppen style [23]. Internally, the solver for linear arithmetic uses only inequalities in theory conflicts. In the proof tree, the (dis-)equalities are related to inequalities by the (valid) clauses $x=y\lor x<y\lor x>y$, and $x\neq y\lor x\leq y$. We call these leaves of the proof tree theory combination clauses.

Interpolants and Symbol Sets.

For a formula $F$, we use $\mathop{\mathit{symb}}(F)$ to denote the set of non-theory symbols occurring in $F$. An interpolation problem is given by two formulae $A$ and $B$ such that $A\land B\models\bot$. An interpolant of $A$ and $B$ is a formula $I$ such that (i) $A\models I$, (ii) $B\land I\models\bot$, and (iii) $\mathop{\mathit{symb}}(I)\subseteq\mathop{\mathit{symb}}(A)\cap\mathop{\mathit{symb}}(B)$.

We call a symbol $s\in\mathop{\mathit{symb}}(A)\cup\mathop{\mathit{symb}}(B)$ shared if $s\in\mathop{\mathit{symb}}(A)\cap\mathop{\mathit{symb}}(B)$, $A$-local if $s\in\mathop{\mathit{symb}}(A)\setminus\mathop{\mathit{symb}}(B)$, and $B$-local if $s\in\mathop{\mathit{symb}}(B)\setminus\mathop{\mathit{symb}}(A)$. Similarly, we call a term $A$-local ($B$-local) if it contains at least one $A$-local ($B$-local) and no $B$-local ($A$-local) symbols. We call a term ($AB$-)shared if it contains only shared symbols and ($AB$-)mixed if it contains $A$-local as well as $B$-local symbols. The same terminology applies to formulae.

Substitution in Formulae and Monotonicity.

By $F[G_{1}]\ldots[G_{n}]$ we denote a formula in negation normal form with sub-formulae $G_{1},\ldots,G_{n}$ that occur positively in the formula. Substituting these sub-formulae by formula $G_{1}^{\prime},\ldots,G_{n}^{\prime}$ is denoted by $F[G_{1}^{\prime}]\ldots[G_{n}^{\prime}]$. By $F(t)$ we denote a formula with a sub-term $t$ that can appear anywhere in $F$. The substitution of $t$ with a term $t^{\prime}$ is denoted by $F(t^{\prime})$.

The following lemma is important for the correctness proofs in the remainder of this technical report. It also represents a concept that is important for the understanding of the proposed procedure.

Lemma 1 (Monotonicity)

Given a formula $F[G_{1}]\ldots[G_{n}]$ in negation normal form with sub-formulae $G_{1},\ldots,G_{n}$ occurring only positively in the formula and formulae $G_{1}^{\prime},\ldots,G_{n}^{\prime}$, it holds that

[TABLE]

Proof

We prove the claim by induction over the number of $\land$ and $\lor$ connectives in $F[\cdot]\ldots[\cdot]$. If $F[G_{1}]\ldots[G_{n}]$ is a literal different from $G_{1},\ldots,G_{n}$ the implication holds trivially. Also for the other base case $F[G_{1}]\ldots[G_{n}]\equiv G_{i}$ for some $i\in\{1,\dots,n\}$ the property holds. For the induction step observe that if $F_{1}[G_{1}]\ldots[G_{n}]\rightarrow F_{1}[G^{\prime}_{1}]\ldots[G^{\prime}_{n}]$ and $F_{2}[G_{1}]\ldots[G_{n}]\rightarrow F_{2}[G^{\prime}_{1}]\ldots[G^{\prime}_{n}]$, then

[TABLE]

∎

3 Proof Tree-Based Interpolation

Interpolants can be computed from proofs of unsatisfiability as Pudlák and McMillan have already shown. In this section we will introduce their algorithms. Then, we will discuss the changes necessary to handle mixed literals introduced, e. g., by theory combination.

3.1 Pudlák’s and McMillan’s Interpolation Algorithms

Pudlák’s and McMillan’s algorithms assume that the pivot literals are not mixed. We will remove this restriction later. We define a common framework that is more general and can be instantiated to obtain Pudlák’s or McMillan’s algorithm to compute interpolants. For this, we use two projection functions on literals $\cdot\downharpoonright A$ and $\cdot\downharpoonright B$ as defined below. They have the properties (i) $\mathop{\mathit{symb}}(\ell\downharpoonright A)\subseteq\mathop{\mathit{symb}}(A)$, (ii) $\mathop{\mathit{symb}}(\ell\downharpoonright B)\subseteq\mathop{\mathit{symb}}(B)$, and (iii) $\ell\iff(\ell\downharpoonright A\land\ell\downharpoonright B)$. Other projection functions are possible and this allows for varying the strength of the resulting interpolant as shown in [9]. We extend the projection function to conjunctions of literals component-wise.

Pudlák McMillan

$\ell\downharpoonright A$ $\ell\downharpoonright B$ $\ell\downharpoonright A$ $\ell\downharpoonright B$

$\ell$ is $A$-local $\ell$ $\top$ $\ell$ $\top$

$\ell$ is $B$-local $\top$ $\ell$ $\top$ $\ell$

$\ell$ is shared $\ell$ $\ell$ $\top$ $\ell$

Given an interpolation problem $A$ and $B$, a partial interpolant of a clause $C$ is an interpolant of the formulae $A\land(\lnot C\downharpoonright A)$ and $B\land(\lnot C\downharpoonright B)$333Note that $\lnot C$ is a conjunction of literals. Thus, $\lnot C\downharpoonright A$ is well defined.. Partial interpolants can be computed inductively over the structure of the proof tree. A partial interpolant of a theory lemma $C$ can be computed by a theory-specific interpolation routine as an interpolant of $\lnot C\downharpoonright A$ and $\lnot C\downharpoonright B$. Note that the conjunction is equivalent to $\lnot C$ and therefore unsatisfiable. For an input clause $C$ from the formula $A$ (resp. $B$), a partial interpolant is $\lnot(\lnot C\setminus A)$ (resp. $\lnot C\setminus B$) where $\lnot C\setminus A$ is the conjunction of all literals of $\lnot C$ that are not in $\lnot C\downharpoonright A$ and analogously for $\lnot C\setminus B$. For a resolution step, a partial interpolant can be computed using (rule-res), which is given below. For this rule, it is easy to show that $I_{3}$ is a partial interpolant of $C_{1}\lor C_{2}$ given that $I_{1}$ and $I_{2}$ are partial interpolants of $C_{1}\lor\ell$ and $C_{2}\lor\lnot\ell$, respectively. Note that the “otherwise” case never triggers in McMillan’s algorithm.

[TABLE]

As the partial interpolant of the root of the proof tree (which is labelled with the clause $\bot$) is an interpolant of the input formulae $A$ and $B$, this algorithm can be used to compute interpolants.

Theorem 3.1

The above-given partial interpolants are correct, i.e., if $I_{1}$ is a partial interpolant of $C_{1}\lor\ell$ and $I_{2}$ is a partial interpolant of $C_{2}\lor\lnot\ell$ then $I_{3}$ is a partial interpolant of the clause $C_{1}\vee C_{2}$.

Proof

The third property, i.e., $\mathop{\mathit{symb}}(I_{3})\subseteq\mathop{\mathit{symb}}(A)\cap\mathop{\mathit{symb}}(B)$, clearly holds if we assume it holds for $I_{1}$ and $I_{2}$. Note that in the “otherwise” case, $\ell$ is shared. We prove the other two partial interpolant properties separately.

Inductivity.

We have to show

[TABLE]

For this we use the inductivity of $I_{1}$ and $I_{2}$:

[TABLE]

Assume $A$, $\lnot C_{1}\downharpoonright A$, and $\lnot C_{2}\downharpoonright A$. Then, (ind1) simplifies to $\lnot\ell\downharpoonright A\rightarrow I_{1}$ and (ind2) simplifies to $\ell\downharpoonright A\rightarrow I_{2}$. We show that $I_{3}$ holds under these assumptions.

Case $\ell\downharpoonright B=\top$.

Then by the definition of the projection function, $\ell\downharpoonright A=\ell$ and $\lnot\ell\downharpoonright A=\lnot\ell$ hold. If $\ell$ holds, (ind2) gives us $I_{2}$, otherwise (ind1) gives us $I_{1}$, thus $I_{3}=I_{1}\lor I_{2}$ holds in both cases.

Case $\ell\downharpoonright A=\top$.

Then (ind1) gives us $I_{1}$ because $\lnot\ell\downharpoonright A=\top$ (the negation of $\ell$ is still not in $A$), and (ind2) gives us $I_{2}$. So $I_{3}=I_{1}\land I_{2}$ holds.

Case “otherwise”.

By the definition of the projection function $\ell\downharpoonright A=\ell\downharpoonright B=\ell$ and $\lnot\ell\downharpoonright A=\lnot\ell\downharpoonright B=\lnot\ell$. If $\ell$ holds, the left conjunct $(I_{1}\lor\ell)$ of $I_{3}$ holds and the right conjunct $(I_{2}\lor\lnot\ell)$ of $I_{3}$ is fulfilled because (ind2) gives us $I_{2}$. If $\lnot\ell$ holds, (ind1) gives us $I_{1}$ and both conjuncts of $I_{3}$ hold.

Contradiction.

We have to show:

[TABLE]

We use the contradiction properties of $I_{1}$ and $I_{2}$:

[TABLE]

If we assume $B$, $\lnot C_{1}\downharpoonright B$, and $\lnot C_{2}\downharpoonright B$, (cont1) simplifies to $\lnot\ell\downharpoonright B\land I_{1}\rightarrow\bot$ and (cont2) simplifies to $\ell\downharpoonright B\land I_{2}\rightarrow\bot$. We show $I_{3}\rightarrow\bot$.

Case $\ell\downharpoonright B=\top$.

Then (cont1) and $\lnot\ell\downharpoonright B=\top$ give us $I_{1}\rightarrow\bot$, and (cont2) and $\ell\downharpoonright B=\top$ give us $I_{2}\rightarrow\bot$. Thus $I_{3}\equiv I_{1}\lor I_{2}$ is contradictory.

Case $\ell\downharpoonright A=\top$.

Then $\ell\downharpoonright B=\ell$ and $\lnot\ell\downharpoonright B=\lnot\ell$. Then, if $\ell$ holds, (cont2) gives us $I_{2}\rightarrow\bot$. If $\lnot\ell$ holds, (cont1) gives us $I_{1}\rightarrow\bot$ analogously. In both cases, $I_{3}\equiv I_{1}\land I_{2}$ is contradictory.

Case “otherwise”.

By the definition of the projection function $\ell\downharpoonright A=\ell\downharpoonright B=\ell$ and $\lnot\ell\downharpoonright A=\lnot\ell\downharpoonright B=\lnot\ell$ hold. Assuming $I_{3}\equiv(I_{1}\lor\ell)\land(I_{2}\lor\lnot\ell)$ holds, we prove a contradiction. If $\ell$ holds, the second conjunct of $I_{3}$ implies $I_{2}$. Then, (cont2) gives us a contradiction. If $\lnot\ell$ holds, the first conjunct of $I_{3}$ implies $I_{1}$ and (cont1) gives us a contradiction. ∎

3.2 Purification of Mixed Literals

The proofs generated by state-of-the-art SMT solvers may contain mixed literals. We tackle them by extending the projection functions to these literals. The problem here is that there is no projection function that satisfies the conditions stated in the previous section. Therefore, we relax the conditions by allowing fresh auxiliary variables to occur in the projections.

We consider two different kinds of mixed literals: First, (dis-)equalities of the form $a=b$ or $a\neq b$ for an $A$-local variable $a$ and a $B$-local variable $b$ are introduced, e. g., by theory combination or Ackermannization. Second, inequalities of the form $a+b\leq c$ are introduced, e. g., by extended branches [8] or bound propagation. Here, $a$ is a linear combination of $A$-local variables, $b$ is a linear combination of $B$-local and shared variables, and $c$ is a constant. Adding the shared variable to the $B$-part is an arbitrary choice. One gets interpolants of different strengths by assigning some shared variables to the $A$-part. It is only important to keep the projection of each literal consistent throughout the proof.

We split mixed literals using auxiliary variables, which we denote by $x$ or $p_{x}$ in the following. The variable $p_{x}$ has the type Boolean, while $x$ has the same type as the variables in the literal. One or two fresh variables are introduced for each mixed literal. We count these variables as shared between $A$ and $B$. The purpose of the auxiliary variable $x$ is to capture the shared value that needs to be propagated between $A$ and $B$. When splitting a literal $\ell$ into $A$- and $B$-part, we require that $\ell\Leftrightarrow\exists x,p_{x}.(\ell\downharpoonright A)\land(\ell\downharpoonright B)$. We need the additional Boolean variable $p_{x}$ to split the literal $a\neq b$ into two (nearly) symmetric parts. This is achieved by the definitions below.

[TABLE]

Since the mixed variables are considered to be shared, we allow them to occur in the partial interpolant of a clause $C$. However, a variable may only occur if $C$ contains the corresponding literal. This is achieved by a special interpolation rule for resolution steps where the pivot literal is mixed. The rules for the different mixed literals are the core of our proposed algorithm and will be introduced in the following sections.

Lemma 2 (Partial Interpolation)

Given a mixed literal $\ell$ with auxiliary variable(s) $\vec{x}$ and clauses $C_{1}\lor\ell$ and $C_{2}\lor\lnot\ell$ with corresponding partial interpolants $I_{1}$ and $I_{2}$. Let $C_{3}=C_{1}\lor C_{2}$ be the result of a resolution step on $C_{1}\lor\ell$ and $C_{2}\lor\lnot\ell$ with pivot $\ell$. If a partial interpolant $I_{3}$ satisfies the symbol condition, and

[TABLE]

then $I_{3}$ is a partial interpolant of $C_{3}$.

Proof

We need to show inductivity and contradiction for the partial interpolants.

Inductivity.

For this we use inductivity of $I_{1}$ and $I_{2}$:

[TABLE]

Since $\vec{x}$ does not appear in $C_{1}\downharpoonright A$, $C_{2}\downharpoonright A$ nor $A$, we can conclude

[TABLE]

Combining these and pulling the quantifier over the conjunction gives

[TABLE]

Using (ind), this shows that inductivity for $I_{3}$ holds:

[TABLE]

Contradiction.

First, we show the contradiction property for $I_{3}$:

[TABLE]

Assume the formulae on the left-hand side hold. From (cond) we can conclude that there is some $\vec{x}$ such that

[TABLE]

If the first disjunct is true we can derive the contradiction using the contradiction property of $I_{1}$:

[TABLE]

Otherwise, the second disjunct holds and we can use the contradiction property of $I_{2}$

[TABLE]

This shows the contradiction property for $I_{3}$. ∎

It is important to state here that the given purification of a literal into two new literals is not a modification of the proof tree or any of its nodes. The proof tree would no longer be well-formed if we replaced a mixed literal by the disjunction or conjunction of the purified parts. The purification is only used to define partial interpolants of clauses. In fact, it is only used in the correctness proof of our method and is not even done explicitly in the implementation.

3.3 Lemma Used in the Correctness Proof

The following lemma will help us prove the correctness of our proposed new interpolation rules.

Lemma 3 (Deep Substitution)

Let $F_{1}[G_{11}]\dots[G_{1n}]$ and $F_{2}[G_{21}]\dots[G_{2m}]$ be two formulae with sub-formulae $G_{1i}$ for $1\leq i\leq n$ and $G_{2j}$ for $1\leq j\leq m$ occurring positively in $F_{1}$ and $F_{2}$.

If $\bigwedge_{i\in\{1,\dots,n\}}\bigwedge_{j\in\{1,\dots,m\}}G_{1i}\land G_{2j}\rightarrow G_{3ij}$ holds, then

[TABLE]

Proof

[TABLE]

∎

4 Uninterpreted Functions

In this section we will present the part of our algorithm that is specific to the theory $\mathcal{EUF}$. The only mixed atom that is considered by this theory is $a=b$ where $a$ is $A$-local and $b$ is $B$-local.

4.1 Leaf Interpolation

The $\mathcal{EUF}$ solver is based on the congruence closure algorithm [7]. The theory lemmas are generated from conflicts involving a single disequality that is in contradiction to a path of equalities. Thus, the clause generated from such a conflict consists of a single equality literal and several disequality literals.

When computing the partial interpolants of the theory lemmas, we internally split the mixed literals according to Section 3.2. Then we use an algorithm similar to [11] to compute an interpolant. This algorithm basically summarises the $A$-equalities that are adjacent on the path of equalities.

If the theory lemma contains a mixed equality $a=b$ (without negation), it corresponds to the single disequality in the conflict. This disequality is split into $p_{x}\mathrel{\mbox{xor}}a=x$ and $\lnot p_{x}\mathrel{\mbox{xor}}x=b$ and the resulting interpolant depends on the value of $p_{x}$. If $p_{x}=\bot$, the disequality is part of the $B$-part and $x$ is the end of an equality path summing up the equalities from $A$. Thus, the computed interpolant contains a literal of the form $x=s$. If $p_{x}=\top$, then the $A$-part of the literal is $a\neq x$, and the resulting interpolant contains the literal $x\neq s$ instead. Thus, the resulting interpolant can be put into the form $I[p_{x}\mathrel{\mbox{xor}}x=s]$. Note that the formula $p_{x}\mathrel{\mbox{xor}}x=s$ occurs positively in the interpolant and is the only part of the interpolant containing $x$ and $p_{x}$. We define

[TABLE]

and require that the partial interpolant of a clause containing the literal $a=b$ always has the form $I[EQ(x,s)]$ where $x$ and $p_{x}$ do not occur anywhere else.

For theory lemmas containing the literal $a\neq b$, the corresponding auxiliary variable $x$ may appear anywhere in the partial interpolant, even under a function symbol. A simple example is the theory conflict $s\neq f(a)\land a=(x=)b\land f(b)=s$, which has the partial interpolant $s\neq f(x)$. In general the partial interpolant of such a clause has the form $I(x)$.

When two partial interpolants for clauses containing $a=b$ are combined using (rule-res), i. e., the pivot literal is a non-mixed literal but the mixed literal $a=b$ occurs in $C_{1}$ and $C_{2}$, the resulting partial interpolant may contain $EQ(x,s_{1})$ and $EQ(x,s_{2})$ for different shared terms $s_{1},s_{2}$. In general, we allow the partial interpolants to have the form $I[EQ(x,s_{1})]\dots[EQ(x,s_{n})]$.

4.2 Pivoting of Mixed Equalities

We require that every clause $C$ containing $a=b$ with auxiliary variables $x,p_{x}$ is always labelled with a formula of the form $I[EQ(x,s_{1})]\dots[EQ(x,s_{n})]$. As discussed above, the partial interpolants computed for conflicts in the congruence closure algorithm are of the form $I[EQ(x,s_{1})]\dots[EQ(x,s_{n})]$. This property is also preserved by (rule-res), and by Theorem 1 this rule also preserves the property of being a partial interpolant. On the other hand, a clause containing the literal $a\neq b$ is labelled with a formula of the form $I(x)$, i. e., the auxiliary variable $x$ can occur at arbitrary positions. Again, the form $I(x)$ and the property of being a partial interpolant is also preserved by (rule-res).

We use the following rule to interpolate the resolution step on the mixed literal $a=b$.

[TABLE]

The rule replaces every literal $EQ(x,s_{i})$ in $I_{1}$ with the formula $I_{2}(s_{i})$, in which every $x$ is substituted by $s_{i}$. Therefore, the auxiliary variable introduced for the mixed literal $a=b$ is removed.

Theorem 4.1 (Soundness of (rule-eq))

Let $a=b$ be a mixed literal with auxiliary variable $x$. If $I_{1}[EQ(x,s_{1})]\dots[EQ(x,s_{n})]$ is a partial interpolant of $C_{1}\lor a=b$ and $I_{2}(x)$ a partial interpolant of $C_{2}\lor a\neq b$ then $I_{1}[I_{2}(s_{1})]\dots[I_{2}(s_{n})]$ is a partial interpolant of the clause $C_{1}\vee C_{2}$.

Proof

The symbol condition for $I_{1}[I_{2}(s_{1})]\dots[I_{2}(s_{n})]$ clearly holds if we assume that it holds for $I_{1}[EQ(x,s_{1})]\dots[EQ(x,s_{n})]$ and $I_{2}(x)$. Hence, after we show (ind) and (cont), we can apply Lemma 2.

Inductivity.

We assume

[TABLE]

and show $I_{1}[I_{2}(s_{1})]\dots[I_{2}(s_{n})]$. Instantiating $x:=s_{i}$ for all $i\in\{1,\dots,n\}$ and taking the second conjunct gives $\bigwedge_{i\in\{1,\dots,n\}}(a=s_{i}\rightarrow I_{2}(s_{i}))$. Instantiating $p_{x}:=\bot$ and $x:=a$ and taking the first conjunct gives $I_{1}[a=s_{1}]\dots[a=s_{n}]$. With monotonicity we get $I_{1}[I_{2}(s_{1})]\dots[I_{2}(s_{n})]$ as desired.

Contradiction.

We have to show

[TABLE]

We show the implication for $p_{x}:=\top$ and $x:=b$. It simplifies to

[TABLE]

If $I_{2}(b)$ holds the implication is true. If $I_{2}(b)$ does not hold, we have

[TABLE]

With monotonicity we get $I_{1}[I_{2}(s_{1})]\dots[I_{2}(s_{n})]\rightarrow I_{1}[b\neq s_{1}]\dots[b\neq s_{n}]$. ∎

4.3 Example

We demonstrate our algorithm on the following example:

[TABLE]

The conjunction $A\land B$ is unsatisfiable. In this example, $a$ is $A$-local, $b$ is $B$-local and the remaining symbols are shared.

Assume the theory solver for $\mathcal{EUF}$ introduces the mixed literal $a=b$ and provides the lemmas (i) $f(a)\neq t\lor a\neq b\lor f(b)=t$, (ii) $a\neq s_{1}\lor b\neq s_{1}\lor a=b$, and (iii) $a\neq s_{2}\lor b\neq s_{2}\lor a=b$. Let the variable $x$ be associated with the equality $a=b$. Then, we label the lemmas with (i) $f(x)=t$, (ii) $EQ(x,s_{1})$, and (iii) $EQ(x,s_{2})$.

We compute an interpolant for $A$ and $B$ using Pudlák’s algorithm. Since the input is already in conjunctive normal form, we can directly apply resolution. Note that for Pudlák’s algorithm every input clause has the partial interpolant $\bot$ ($\top$) if it is part of $A$ ($B$). In the following derivation trees we apply the following simplifications without explicitely stating them:

[TABLE]

From lemma (ii) and the input clauses $\lnot q\lor a=s_{1}$ and $\lnot q\lor b=s_{1}$ we can derive the clause $\lnot q\lor a=b$. The partial interpolant of the derived clause is still $EQ(x,s_{1})$.

[TABLE]

Similarly, from lemma (iii) and the input clauses $q\lor a=s_{2}$ and $q\lor b=s_{2}$ we can derive the clause $q\lor a=b$ with partial interpolant $EQ(x,s_{2})$.

[TABLE]

A resolution step on these two clauses with $q$ as pivot yields the clause $a=b$. Since $q$ is a shared literal, Pudlák’s algorithm introduces the case distinction. Hence, we get the partial interpolant $(EQ(x,s_{2})\lor q)\land(EQ(x,s_{1})\lor\lnot q)$. Note that this interpolant has the form $I_{1}[EQ(x,s_{1})][EQ(x,s_{2})]$ and, therefore, satisfies the syntactical restrictions.

[TABLE]

From the $\mathcal{EUF}$-lemma (i) and the input clauses $f(a)=t$ and $f(b)\neq t$, we can derive the clause $a\neq b$ with partial interpolant $f(x)=t$. Note that this interpolant has the form $I_{2}(x)$ which also corresponds to the syntactical restrictions needed for our method.

[TABLE]

If we apply the final resolution step on the mixed literal $a=b$ using (rule-eq), we get the interpolant $I_{1}[I_{2}(s_{1})][I_{2}(s_{2})]$ which corresponds to the interpolant $(f(s_{2})=t\lor q)\land(f(s_{1})=t\lor\lnot q)$.

[TABLE]

When resolving on $q$ in the derivations above, the mixed literal $a=b$ occurs in both antecedents. This leads to the form $I[EQ(x,s_{1})][EQ(x,s_{2})]$. We can prevent this by resolving in a different order. We could first resolve the clause $q\lor a=b$ with the clause $a\neq b$ and obtain the partial interpolant $f(s_{2})=t$ using (rule-eq).

[TABLE]

Then we could resolve the clause $\lnot q\lor a=b$ with the clause $a\neq b$ and obtain the partial interpolant $f(s_{1})=t$ again using (rule-eq).

[TABLE]

The final resolution step on $q$ will then introduce the case distinction according to Pudlák’s algorithm. This results in the same interpolant.

[TABLE]

5 Linear Real and Integer Arithmetic

Our solver for linear arithmetic is based on a variant of the Simplex approach [10]. A theory conflict is a conjunction of literals $\ell_{j}$ of the form $\sum_{i}a_{ij}x_{i}\leq b_{j}$. The proof of unsatisfiability is given by Farkas coefficients $k_{j}\geq 0$ for each inequality $\ell_{j}$. These coefficients have the properties $\sum_{j}k_{j}a_{ij}=0$ and $\sum_{j}k_{j}b_{j}<0$. In the following we use the notation of adding inequalities (provided the coefficients are positive). Thus, we write $\sum_{j}k_{j}\ell_{j}$ for $\sum_{i}(\sum_{j}k_{j}a_{ij})x_{i}\leq\sum_{j}k_{j}b_{j}$. With the property of the Farkas coefficients we get a contradiction ($0<0$) and this shows that the theory conflict is unsatisfiable.

A conjunction of literals may have rational but no integer solutions. In this case, there are no Farkas coefficients that can prove the unsatisfiability. So for the integer case, our solver may introduce extended branches [8], which are just branches of the DPLL engine on newly introduced literals. In the proof tree this results in resolution steps with these literals as pivots.

Example 1

The formula $t\leq 2a\leq r\leq 2b+1\leq t$ has no integer solution but a rational solution. Introducing the branch $a\leq b\lor b<a$ leads to the theory conflicts $t\leq 2a\leq 2b\leq t-1$ and $r\leq 2b+1\leq 2a-1\leq r-1$ (note that $b<a$ is equivalent to $b+1\leq a$). The corresponding proof tree is given below. The Farkas coefficients in the theory lemmas are given in parenthesis. Note that the proof tree shows the clauses, i. e., the negated conflicts. A node with more than two parents denotes that multiple applications of the resolution rule are taken one after another.

\begin{array}[]{r}\lnot(r\leq 2b+1)\;(\cdot 1)\\ \lnot(b+1\leq a)\;(\cdot 2)\\ \lnot(2a\leq r)\;(\cdot 1)\end{array}$$\begin{array}[]{r}\lnot(t\leq 2a)\;(\cdot 1)\\ \lnot(a\leq b)\;(\cdot 2)\\ \lnot(2b+1\leq t)\;(\cdot 1)\end{array}$$r\leq 2b+1$$2a\leq r$$t\leq 2a$$2b+1\leq t$$a\leq b$$\lnot(a\leq b)$$\bot

Now consider the problem of deriving an interpolant between $A\equiv t\leq 2a\leq r$ and $B\equiv r\leq 2b+1\leq t$. We can obtain an interpolant by annotating the above resolution tree with partial interpolants. To compute a partial interpolant for the theory lemma $\lnot(r\leq 2b+1)\lor\lnot(b+1\leq a)\lor\lnot(2a\leq r)$, we purify the negated clause according to the definition in Section 3.2, which gives

[TABLE]

Then, we sum up the $A$-part of the conflict (the second and fourth literal) multiplied by their corresponding Farkas coefficients. This yields the interpolant $2x_{1}\leq r$. Similarly, the negation of the theory lemma $\lnot(t\leq 2a)\lor\lnot(a\leq b)\lor\lnot(2b+1\leq t)$ is purified to

[TABLE]

which yields the partial interpolant $2x_{2}+t\leq 0$. Note, that we have to introduce different variables for each literal. Intuitively, the variable $x_{1}$ stands for $a$ and $x_{2}$ for $-a$. Using Pudlák’s algorithm we can derive the same interpolants for the clause $a\leq b$ resp. $\lnot(a\leq b)$.

For the final resolution step, the two partial interpolants $2x_{1}\leq r$ and $2x_{2}+t\leq 0$ are combined into the final interpolant of the problem. Summing up these inequalities with $x_{1}=-x_{2}$ we get $t\leq r$. While this follows from $A$, it is not inconsistent with $B$. We need an additional argument that, given $r=t$, $r$ has to be an even integer. This also follows from the partial interpolants when setting $x_{1}=-x_{2}$: $t\leq-2x_{2}=2x_{1}\leq r$. The final interpolant computed by our algorithm is $t\leq 2\left\lfloor\frac{r}{2}\right\rfloor$.

In general, we can derive additional constraints on the variables if the constraint resulting from summing up the two partial interpolants holds very tightly. We know implicitly that $x_{1}=-x_{2}$ is an integer value between $t/2$ and $r/2$. If $t$ equals $r$ or almost equals $r$ there are only a few possible values which we can explicitly express using the division function as in the example above. We assume that the (partial) interpolant $F$ always has a certain property. There is some term $s$ and some constant $k$, such that for $s>0$ the interpolant is always false and for $s<-k$ the interpolant is always true (in our case $s=t-r$ and $k=0$). For a partial interpolant that still contains auxiliary variables $\vec{x}$, we additionally require that $s$ contains them with a positive coefficient and that $F$ is monotone on $\vec{x}$, i. e., $\vec{x}\geq\vec{x}^{\prime}$ implies $F(\vec{x})\rightarrow F(\vec{x}^{\prime})$.

To mechanise the reasoning used in the example above, our resolution rule for mixed inequality literals requires that the interpolant patterns that label the clauses have a certain shape. An auxiliary variable of a mixed inequality literal may only occur in the interpolant pattern if the negated literal appears in the clause. Let $\vec{x}$ denote the set of auxiliary variables that occur in the pattern. We require that these variables only occur inside a special sub-formula of the form $LA(s(\vec{x}),k,F(\vec{x}))$. The first parameter $s$ is a linear term over the variables in $\vec{x}$ and arbitrary other terms not involving $\vec{x}$. The coefficients of the variables $\vec{x}$ in $s$ must all be positive. The second parameter $k\in\mathbb{Q}_{\varepsilon}$ is a constant value. In the real case we only allow the values [math] and $-\varepsilon$. In the integer case we allow $k\in\mathbb{Z},k\geq-1$. To simplify the presentation, we sometimes write $-\varepsilon$ for $-1$ in the integer case. The third parameter $F(\vec{x})$ is a formula that contains the variables from $\vec{x}$ at arbitrary positions. We require that $F$ is monotone, i. e., $\vec{x}\geq\vec{x}^{\prime}$ implies $F(\vec{x})\rightarrow F(\vec{x}^{\prime})$. Moreover, $F(\vec{x})=\bot$ for $s(\vec{x})>0$ and $F(\vec{x})=\top$ for $s(\vec{x})<-k$. The sub-formula $LA(s(\vec{x}),k,F(\vec{x}))$ stands for $F(\vec{x})$ and it is only used to remember what the values of $s$ and $k$ are.

The intuition behind the formula $LA(s(\vec{x}),k,F(\vec{x}))$ is that $s(\vec{x})\leq 0$ summarises the inequality chain that follows from the $A$-part of the formula. On this chain there may be some constraints on intermediate values. In the example above the $A$-part contains the chain $t\leq 2a\leq r$, which is summarised to $s\leq 0$ (with $s=t-r$). Furthermore the $A$-part implies that there is an even integer value between $t$ and $r$. If $s<-k$ (with $k=0$ in this case), $t$ and $r$ are distinct, and there always is an even integer between them. However, if $-k\leq s\leq 0$, the truth value of the interpolant depends on whether $t$ is even.

In the remainder of the section, we will give the interpolants for the leaves produced by the linear arithmetic solver and for the resolvent of the resolution step where the pivot is a mixed linear inequality.

5.1 Leaf Interpolation

As mentioned above, our solver produces for a clause $C\equiv\lnot\ell_{1}\lor\dots\lor\lnot\ell_{m}$ some Farkas coefficients $k_{1},\dots,k_{m}\geq 0$ such that $\sum_{j}k_{j}\ell_{j}$ yields a contradiction $0<0$. A partial interpolant for a theory lemma can be computed by summing up the $A$-part of the conflict: $I$ is defined as $\sum_{j}k_{j}(\ell_{j}\downharpoonright A)$ (if $\ell_{j}\downharpoonright A=\top$ we regard it as $0\leq 0$, i. e., it is not added to the sum). It is a valid interpolant as it clearly follows from $\lnot C\downharpoonright A\iff\ell_{1}\downharpoonright A\land\dots\land\ell_{m}\downharpoonright A$. Moreover, we have that $I+\sum_{j}k_{j}(\ell_{j}\downharpoonright B)$ yields $0<0$, since for every literal, even for mixed literals, $\ell_{j}\downharpoonright A+\ell_{j}\downharpoonright B=\ell_{j}$ holds444Strictly speaking this does not hold for shared literals, where $\ell\downharpoonright A=\ell\downharpoonright B=\ell$. In that case use $k_{j}=0$ in $I+\sum_{j}k_{j}(\ell_{j}\downharpoonright B)$ to see that $I$ is indeed a partial interpolant.. This shows that $I\land\lnot C\downharpoonright B$ is unsatisfiable.

The linear constraint $\sum_{j}k_{j}(\ell_{j}\downharpoonright A)$ can be expressed as $s(\vec{x})\leq 0$. Thus, we can equivalently write this interpolant in our pattern as $LA(s(\vec{x}),-\varepsilon,s(\vec{x})\leq 0)$. Since the Farkas coefficients are all positive and the auxiliary variables introduced to define $\ell\downharpoonright A$ for mixed literals contain $x$ positively, the resulting term $s(\vec{x})$ will also always contain $x$ with a positive coefficient.

Theory combination lemmas.

As mentioned in the preliminaries, we use theory combination clauses to propagate equalities from and to the Simplex core of the linear arithmetic solver. These clauses must also be labelled with partial interpolants. In the following we give interpolants for those theory combination lemmas. We will start with the case where no mixed literals occur, and treat lemmas containing mixed literals afterwards.

Interpolation of Non-Mixed Theory Combination Lemmas.

If a theory combination lemma $t=u\lor t<u\lor t>u$ or $t\neq u\lor t\leq u$ contains no mixed literal, we can compute partial interpolants as follows. If all literals in the clause are $A$-local, the formula $\bot$ is a partial interpolant. If all literals are $B$-local, the formula $\top$ is a partial interpolant. These are the same interpolants Pudlák’s algorithm would give for input clauses from $A$ resp. $B$.

Otherwise, one of the literals belongs to $A$ and one to $B$. The symbols $t$ and $u$ have to be shared between $A$ and $B$ since they appear in all literals. We can derive a partial interpolant by conjoining the negated literals projected to the $A$ partition.

[TABLE]

Since we defined $I$ as $\lnot C\downharpoonright A$, the first property of the partial interpolant holds trivially. Also $I\land\lnot C\downharpoonright B$ is equivalent to $\lnot C$ and therefore false. The symbol condition is satisfied as $t$ and $u$ are shared symbols.

Interpolation of AB-Mixed Theory Combination Lemmas.

If we are in the mixed case, all three literals are mixed. One of the two terms must be $A$-local (in the following we denote this term by $a$) the other term $B$-local (which we denote by $b$). To purify the literals, we introduce a fresh auxiliary variable for each literal. Table 1 depicts all possible mixed theory lemmas together with the projections $\lnot C\downharpoonright A$ and $\lnot C\downharpoonright B$ and a partial interpolant of the clause.

Lemma 4

The interpolants shown in Table 1 are correct partial interpolants of their respective clauses.

Proof

First, we convince ourselves that these interpolants are of the right form: The variables $x_{1}$ and $x_{2}$ appear in the first parameter of $LA$ with positive coefficients. For the first two clauses that contain the literal $a\neq b$, the interpolant is allowed to contain $x$ at arbitrary positions. Note that in the first interpolant $x_{1}\leq x$ is false for $-x+x_{1}>0$ and true for $-x+x_{1}<\varepsilon$, i. e., $-x+x_{1}\leq 0$. Also, $x_{1}\geq x_{1}^{\prime}$ implies $x_{1}\leq x\rightarrow x_{1}^{\prime}\leq x$. Similarly, for the second interpolant.

In the third clause, $F(x_{1},x_{2})=x_{1}\leq-x_{2}\land(x_{1}\geq-x_{2}\rightarrow EQ(x,x_{1}))$ is false for $x_{1}+x_{2}>0$ (because of the first conjunct) and true for $x_{1}+x_{2}<0$ (because the implication holds vacuously). Also, $x_{1}\geq x_{1}^{\prime}$ and $x_{2}\geq x_{2}^{\prime}$ implies $F(x_{1},x_{2})\rightarrow F(x_{1}^{\prime},x_{2}^{\prime})$. To see this, note that $F(x_{1},x_{2})$ is false if $x_{1}^{\prime}\geq-x_{2}^{\prime}$ and $x_{1}^{\prime}\neq x_{1}$. The variable $x$ appears only in an $EQ$-term which occurs positively in the partial interpolant.

Next we show

[TABLE]

Inductivity.

For the clause $a\neq b\lor a\leq b$, the interpolant follows from $\lnot C\downharpoonright A$, as $a=x$ and $-a+x_{1}\leq 0$ imply $x_{1}\leq x$. Similarly for the clause $a\neq b\lor a\geq b$, $\lnot C\downharpoonright A$ contains $a=x$ and $a+x_{2}\leq 0$, which implies $x\leq-x_{2}$. Now consider the clause $a=b\lor a<b\lor b<a$. Here, $\lnot C\downharpoonright A$ implies $x_{1}\leq-x_{2}$ and that if $x_{1}\geq-x_{2}$ holds, then $x_{1}=a=-x_{2}$. Hence, $x_{1}\leq-x_{2}\land x_{1}\geq-x_{2}\rightarrow EQ(x,x_{1})$ holds.

Contradiction.

Again we only show the first and third case. For the clause $C\equiv a\neq b\lor a\leq b$, note that $\lnot C\downharpoonright B$ and $LA(-x+x_{1},-\varepsilon,x_{1}\leq x)$ give the contradiction $x_{1}>b=x>x_{1}$. For the clause $C\equiv a=b\lor a<b\lor b<a$, $\lnot C\downharpoonright B$ implies $x_{1}\geq b\geq-x_{2}$. With $x_{1}\leq-x_{2}$ from the interpolant this gives $x_{1}=b$. Also, $x_{1}\geq-x_{2}\rightarrow EQ(x,x_{1})$ from the interpolant gives $p_{x}\mathrel{\mbox{xor}}x=b$. This is in contradiction with $\lnot p_{x}\mathrel{\mbox{xor}}x=b$ from $\lnot C\downharpoonright B$.

∎

5.2 Pivoting of Mixed Literals

In this section we give the resolution rule for a step involving a mixed inequality $a+b\leq c$ as pivot element. In the following we denote the auxiliary variable of the negated literal $\lnot(a+b\leq c)$ with $x_{1}$ and the auxiliary variable of $a+b\leq c$ with $x_{2}$. The intuition here is that $x_{1}$ and $-x_{2}$ correspond to the same value between $a$ and $c-b$. The resolution rule for pivot element $a+b\leq c$ is as follows where the values for $s_{3}$, $k_{3}$ and $F_{3}$ are given later.

[TABLE]

The basic idea is to find for $\exists x_{1}.F_{1}(x_{1},\vec{x})\land F_{2}(-x_{1},\vec{x})$ an equivalent quantifier free formula $F_{3}(\vec{x})$. To achieve this we note that we only have to look on the value of $F_{1}$ for $-k_{1}\leq c_{1}x_{1}+s_{1}(\vec{x})\leq 0$, since outside of this interval $F_{1}$ is guaranteed to be true resp. false. The formula $F_{3}$ must also be monotone and satisfy the range condition. We choose

[TABLE]

and then $F_{3}$ will be false for $s_{3}(\vec{x})>0$, since either $F_{1}(x_{1},\vec{x})$ or $F_{2}(-x_{1},\vec{x})$ is false. The value of $k_{3}$ must be chosen such that $s_{3}(\vec{x})<-k_{3}$ guarantees the existence of a value $x_{1}$ with $c_{1}x_{1}+s_{1}(\vec{x})<-k_{1}$ and $-c_{2}x_{1}+s_{2}(\vec{x})<-k_{2}$. Hence, in the integer case, the gap between $\frac{s_{2}(\vec{x})+k_{2}}{c_{2}}$ and $\frac{-s_{1}(\vec{x})-k_{1}}{c_{1}}$ should be bigger than one. Then, $c_{1}c_{2}<c_{2}(-s_{1}(\vec{x})-k_{1})-c_{1}(s_{2}(\vec{x})+k_{2})$. So if we define

[TABLE]

then there is a suitable $x_{1}$ for $s_{3}(\vec{x})<-k_{3}$. For $F_{3}$ we can then use a finite case distinction over all values where the truth value of $F_{1}$ is not determined. This suggests defining

[TABLE]

In the real case, if $k_{1}=-\varepsilon$, the best choice is $x_{1}=\frac{-s_{1}(\vec{x})}{c_{1}}$, for which $F_{1}(x_{1})$ is guaranteed to be true. If $k_{1}=0$, we need to consider two cases:

[TABLE]

Note that the formula of the integer case is asymmetric. If $\left\lceil\frac{k_{2}+1}{c_{2}}\right\rceil<\left\lceil\frac{k_{1}+1}{c_{1}}\right\rceil$ we can replace $-s_{1}$ by $s_{2}$, $k_{1}$ by $k_{2}$, and $c_{1}$ by $c_{2}$. This leads to a fewer number of disjuncts in $F_{3}$. Also note that we can remove $F_{1}$ from the last disjunct of $F_{3}$, as it will always be true.

With these definitions we can state the following lemma.

Lemma 5

Let for $i=1,2$, $s_{i}(\vec{x})$ be linear terms over $\vec{x}$, $c_{i}\geq 0$, $k_{i}\in\mathbb{Z}_{\geq-1}$ (integer case) or $k_{i}\in\{0,-\varepsilon\}$ (real case), $F_{i}(x_{i},\vec{x})$ monotone formulas with $F_{i}(x_{i},\vec{x})=\bot$ for $c_{i}x_{i}+s_{i}(\vec{x})>0$ and $F_{i}(x_{i},\vec{x})=\top$ for $c_{i}x_{i}+s_{i}(\vec{x})<-k_{i}$. Let $s_{3},k_{3},F_{3}$ be as defined above. Then $F_{3}$ is monotone, $F_{3}(\vec{x})=\bot$ for $s_{3}(\vec{x})>0$ and $F_{3}(\vec{x})=\top$ for $s_{3}(\vec{x})<-k_{i}$.

Proof

Since $F_{1}$ and $F_{2}$ are monotone and they occur only positively in $F_{3}$, $F_{3}$ must also be monotone. If $s_{3}(\vec{x})>0$, then $\frac{-s1(\vec{x})}{c_{1}}<\frac{s_{2}}{c_{2}}$. Hence, for every $x\leq\frac{-s(\vec{x})}{c_{1}}$, $F_{2}(-x,\vec{x})$ is false since $-c_{2}x+s_{2}(\vec{x})>0$. By definition, every disjunct of $F_{3}$ (except $s_{3}(\vec{x})<0$) contains $F_{2}(-x,\vec{x})$ for such an $x$, so $F_{3}(\vec{x})$ is false.

Now assume $s_{3}(\vec{x})<-k_{3}$. For $k_{1}=-\varepsilon$ in the real case, $F_{3}(\vec{x})=F_{2}(-\frac{s_{1}(\vec{x})}{c_{1}})$ is true since $s_{1}(\vec{x})+s_{2}(\vec{x})<-k_{2}$. For $k_{1}=0$, $F_{3}$ is true by definition. In the integer case define $y:=\left\lfloor\frac{-s_{1}(\vec{x})}{c_{1}}\right\rfloor-\left\lceil\frac{k_{1}+1}{c_{1}}\right\rceil$. This implies $c_{1}y\leq-s_{1}(\vec{x})-k_{1}-1$, hence $F_{1}(y,\vec{x})$ holds. Also $c_{1}y\geq-s_{1}(\vec{x})-k_{1}-c_{1}$, hence

[TABLE]

Therefore, $F_{2}(-y,\vec{x})$ holds. Since $y$ is included in the big disjunction of $F_{3}$, $F_{3}(\vec{x})$ is true.

Lemma 6

Let for $i=1,2$, $s_{i}(\vec{x})$ be linear terms over $\vec{x}$, $c_{i}\geq 0$, $k_{i}\in\mathbb{Z}_{\geq-1}$ (integer case) or $k_{i}\in\{0,-\varepsilon\}$ (real case), $F_{i}(x_{i},\vec{x})$ monotone formulas with $F_{i}(x_{i},\vec{x})=\bot$ for $c_{i}x_{i}+s_{i}(\vec{x})>0$ and $F_{i}(x_{i},\vec{x})=\top$ for $c_{i}x_{i}+s_{i}(\vec{x})<-k_{i}$. Let $F_{3}$ be as defined above. Then

[TABLE]

Proof (for $\mathcal{LA}\left(\mathbb{Z}\right)$)

Since $F_{3}$ is a disjunction of $F_{1}(x,\vec{x})\land F_{2}(-x,\vec{x})$ for different values of $x$, the implication from left to right is obvious. We only need to show the other direction. For this, choose $x_{1}$ such that $F_{1}(x_{1},\vec{x})\land F_{2}(-x_{1},\vec{x})$ holds. We show $F_{3}(\vec{x})$. We define $y:=\left\lfloor\frac{-s_{1}(\vec{x})}{c_{1}}\right\rfloor-\left\lceil\frac{k_{1}+1}{c_{1}}\right\rceil$. This implies $y\leq\frac{-s_{1}(\vec{x})-k_{1}-1}{c_{1}}$. We show $F_{3}$ by a case split on $x_{1}<y$.

Case $x_{1}<y$.

Since $F_{2}$ is monotone and $-x_{1}>-y$, we have $F_{2}(-y,\vec{x})$. Also $F_{1}(y,\vec{x})$ holds since $c_{1}y+s_{1}(\vec{x})<-k_{1}$. This implies $F_{3}(\vec{x})$, since $F_{1}(y,\vec{x})\land F_{2}(-y,\vec{x})$ is a disjunct of $F_{3}$.

Case $y\leq x_{1}$.

Since $F_{1}(x_{1},\vec{x})$ holds, $c_{1}x_{1}+s_{1}(\vec{x})\leq 0$, hence $x_{1}\leq\left\lfloor\frac{-s_{1}(\vec{x})}{c_{1}}\right\rfloor$. Thus, $x_{1}$ is one of the values $\left\lfloor\frac{-s_{1}(\vec{x})}{c_{1}}\right\rfloor-i$ for $0\leq i\leq\left\lceil\frac{k_{1}+1}{c_{1}}\right\rceil$. This means the disjunction $F_{3}(\vec{x})$ includes $F_{1}(x_{1},\vec{x})\land F_{2}(-x_{1},\vec{x})$.∎

Proof (for $\mathcal{LA}\left(\mathbb{Q}\right)$)

In the case $k_{1}=-\varepsilon$, $F_{1}(\frac{-s_{1}}{c_{1}},\vec{x})$ is true. From the definition of $F_{3}$, we get the implication $F_{3}(\vec{x})\rightarrow\exists x_{1}.F_{1}(x_{1},\vec{x})\land F_{2}(-x_{1},\vec{x})$ for $x_{1}=\frac{-s_{1}}{c_{1}}$. If $k_{1}=0$ and $s_{3}(x)<0$, then $\frac{s_{2}}{c_{2}}<\frac{-s_{1}}{c_{1}}$ and for any value $x_{1}$ in between, $F_{1}(x_{1},\vec{x})\land F_{2}(-x_{1},\vec{x})$ are true.

For the other direction assume that $F_{1}(x_{1},\vec{x})\land F_{2}(-x_{1},\vec{x})$ holds. Since $F_{1}$ is not false, $x_{1}\leq\frac{-s_{1}}{c_{1}}$ holds. If $x_{1}=\frac{-s_{1}}{c_{1}}$ then $F_{3}$ holds by definition. In the case $k_{1}=0$ where $x_{1}<\frac{-s_{1}}{c_{1}}$, we have $s_{3}(\vec{x})<0$, since $F_{2}(-x_{1},\vec{x})$ is not false. In the case $k_{1}=-\varepsilon$, we need to show that $F_{2}(\frac{s_{1}}{c_{1}},\vec{x})$ holds. This follows from $x_{1}\leq\frac{-s_{1}}{c_{1}}$ and monotonicity of $F_{2}$. ∎

This lemma can be used to show that (rule-la) is correct.

Theorem 5.1 (Soundness of (rule-la))

Let $a+b\leq c$ be a mixed literal with the auxiliary variable $x_{2}$, and $x_{1}$ be the auxiliary variable of the negated literal. If $I_{1}[LA(c_{1}x_{1}+s_{1},k_{1},F_{1})]$ is a partial interpolant of $C_{1}\lor a+b\leq c$ and $I_{2}[LA(c_{2}x_{2}+s_{2},k_{2},F_{2})]$ is a partial interpolant of $C_{2}\lor\lnot(a+b\leq c)$ then $I_{1}[I_{2}[LA(s_{3},k_{3},F_{3})]]$ is a partial interpolant of the clause $C_{1}\vee C_{2}$.

To ease the presentation, we gave the rule (rule-la) with only one $LA$ term per partial interpolant. The generalised rule requires the partial interpolants of the premises to have the shapes $I_{1}[LA_{11}]\dots[LA_{1n}]$ and $I_{2}[LA_{21}]\dots[LA_{2m}]$. The resulting interpolant is

[TABLE]

where $LA_{3ij}$ is computed from $LA_{1i}$ and $LA_{2j}$ as explained above.

Proof

The symbol condition holds for $I_{3}$ if it holds for $I_{1}$ and $I_{2}$, which can be seen as follows. The only symbol that is allowed to occur in $I_{1}$ resp. $I_{2}$ but not in $I_{3}$ is the auxiliary variable introduced by the literal, i.e., $x_{1}$ resp. $x_{2}$. This variable may only occur inside the $LA_{1}$ resp. $LA_{2}$ terms as indicated and, by construction, $x_{1}$ and $x_{2}$ do not occur in $LA_{3}$. Furthermore, the remaining variables from $\vec{x}$ occur in $s_{3}(\vec{x})$ with a positive coefficient as required by our pattern and occur only inside the $LA$ pattern in $s_{3}$ and $F_{3}$. Thus $I_{3}$ has the required form. We will use Lemma 2 to show that $I_{3}$ is a partial interpolant. For this we need to show inductivity (ind) and contradiction (cont).

In this proof we will use $I_{1}[LA_{1i}(x_{1})]$ to denote the first interpolant

[TABLE]

and similarly $I_{2}[LA_{2j}(x_{2})]$ and $I_{1}[I_{2}[LA_{3ij}]]$, the latter standing for

[TABLE]

where

[TABLE]

Inductivity.

We apply Lemma 6 on $x_{1}=a$, which gives us

[TABLE]

Using the deep substitution lemma, we obtain

[TABLE]

Now assume the left-hand-side of (ind), which in this case is

[TABLE]

Instantiating $x_{1}$ with $a$ and $x_{2}$ with $-a$ gives us $I_{1}[LA_{1i}(a)]$ and $I_{2}[LA_{2j}(-a)]$. Thus by $(*)$, $I_{3}\equiv I_{1}[I_{2}[LA_{3ij}]]$ holds as desired.

Contradiction.

We assume $I_{1}[I_{2}[LA_{3ij}]]$ and show

[TABLE]

We do a case distinction on

[TABLE]

If it holds, then we may get a different value for $x_{1}$ for every $i$. However, if $LA_{1i}(x_{1})$ holds for some value, it also holds for any smaller value of $x_{1}$. Take $x$ as the minimum of these values (or $x=c-b+1$ if the implication holds vacuously for every $i$). Then, $-x-b<-c$ and $\bigwedge_{i}(I_{2}[LA_{3ij}]\rightarrow LA_{1i}(x))$. With monotonicity we get from $I_{1}[I_{2}[LA_{3ij}]]$ that $I_{1}[LA_{1i}(x)]$ holds. Hence, the left disjunct of formula $(*)$ holds.

In the other case there is some $i$ with

[TABLE]

The second part of Lemma 6 gives us

[TABLE]

Then, $x_{1}\leq c-b$ by $(**)$. But if $LA_{2j}(-x_{1})$ holds, then $LA_{2j}$ also holds for the smaller value $b-c$. This gives us

[TABLE]

We obtain $I_{2}[LA_{2j}(b-c)]$ by applying monotonicity on the left conjunct of formula $(**)$. Thus the right disjunct of formula $(*)$ holds for $x_{2}=b-c$. ∎

6 An Example for the Combined Theory

The previous examples showed how to use our technique to compute an interpolant in the theory of uninterpreted functions, or the theory of linear arithmetic. We will now present an example in the combination of these theories by applying our scheme to a proof of unsatisfiability of the interpolation problem

[TABLE]

where $a$, $b$, $s$, and $t$ are integer constants, $q$ is a constant of the uninterpreted sort $U$, and $f$ is a function from integer to $U$.

We derive the interpolant using Pudlák’s algorithm and the rules shown in this paper. Note that the formula is already in conjunctive normal form. Since we use Pudlák’s algorithm, every input clause is labelled with $\bot$ if it is an input clause from $A$, and $\top$ if it is an input clause from $B$. We will simplify the interpolants by removing neutral elements of Boolean connectives.

Since the variables $a$ and $b$ are shared between the theory of uninterpreted functions and the theory of linear arithmetic, we get some theory combination clauses for $a$ and $b$. The only theory combination clause needed to prove unsatisfiability of $A\land B$ is $a=b\lor\lnot(b\leq a)\lor\lnot(a\leq b)$ which has the partial interpolant $LA(x_{1}+x_{2},0,F[EQ(x,x_{1})])$ where $F[G]\equiv x_{1}\leq-x_{2}\land(x_{1}\geq-x_{2}\rightarrow G)$. Here, $x_{1}$ is used to purify555Note that we purify the conflict, i. e., the negated clause $b\leq a$ and $x_{2}$ is used to purify $a\leq b$.

We get two lemmas from $\mathcal{LA}\left(\mathbb{Z}\right)$: The first one, $\lnot(2a\leq s)\lor\lnot(s\leq 2b)\lor a\leq b$, states that we can derive $a\leq b$ from $2a\leq s$ and $s\leq 2b$. Let $x_{3}$ be the variable used to purify $\lnot(a\leq b)$. Note that we purify the literals in the conflict, i. e., the negation of the lemma. Then, this lemma can be annotated with the partial interpolant $LA(2x_{3}-s,-1,2x_{3}\leq s)$. We can resolve this lemma with the unit clauses from the input to get $a\leq b$.

The second $\mathcal{LA}\left(\mathbb{Z}\right)$-lemma, $\lnot(t\leq 2a)\lor\lnot(2b\leq t+1)\lor b\leq a$, states that we can derive $b\leq a$ from $t\leq 2a$ and $2b\leq t+1$. Let $x_{4}$ be the variable used to purify $\lnot(b\leq a)$. Then, we can annotate the lemma with the partial interpolant $LA(2x_{4}+t,-1,2x_{4}+t\leq 0)$ and propagate this partial interpolant to the unit clause $b\leq a$ by resolution with input clauses.

Additionally, we get one lemma from $\mathcal{EUF}$, $f(b)=q\lor\lnot(f(a)=q)\lor\lnot(a=b)$, that states that, given $f(a)=q$ and $a=b$, by congruence, $f(b)=q$ has to hold. Let $x$ be the variable used to purify $a=b$. Then, we can label this lemma with the partial interpolant $f(x)=q$. Note that this interpolant has the form $I(x)$ as required by our interpolation scheme. We propagate this partial interpolant to the unit clause $\lnot(a=b)$ by resolving the lemma with the input clauses.

[TABLE]

From the theory combination clause $a=b\lor\lnot(b\leq a)\lor\lnot(a\leq b)$ and the three unit clauses derived above, we show a contradiction. We start by resolving with the unit clause $a=b$ using (rule-eq) and produce the partial interpolant $LA(x_{1}+x_{2},0,f(x_{1})=q)$.

[TABLE]

The next step resolves on $b\leq a$ using (rule-la). Note that we used $x_{1}$ to purify $b\leq a$ and $x_{4}$ to purify $\lnot(b\leq a)$. Hence, these variables will be removed from the resulting partial interpolant. From the partial interpolants of the antecedents, $LA(2x_{4}+t,-1,2x_{4}+t\leq 0)$ and $LA(x_{1}+x_{2},0,F[f(x_{1})=q])$, we get the following components:

[TABLE]

These components yield $k_{3}=1\cdot(-1)+2\cdot 0+2\cdot 1=1$. Furthermore, $\left\lceil\frac{k_{1}+1}{c_{1}}\right\rceil=0$ leads to one disjunct in $F_{3}$. The corresponding values are $\left\lfloor\frac{-t}{2}\right\rfloor$, resp. $-\left\lfloor\frac{-t}{2}\right\rfloor$. $F_{1}(\left\lfloor\frac{-t}{2}\right\rfloor)$ is always true and can be omitted. The resulting formula $G(x_{2}):=F_{3}(\vec{x})$ is

[TABLE]

The partial interpolant for the clause $\lnot(a\leq b)$ is $LA(t+2x_{2},1,G(x_{2}))$.

[TABLE]

In the final resolution step, we resolve $a\leq b$ labelled with partial interpolant $LA(2x_{3}-s,-1,2x_{3}\leq s)$ against $\lnot(a\leq b)$ labelled with $LA(t+2x_{2},1,G(x_{2}))$. Note that the literals have been purified with $x_{3}$ and $x_{2}$, respectively. We get the components

[TABLE]

We get $k_{3}=2\cdot(-1)+2\cdot 1+2\cdot 2=4$. Again, $\left\lceil\frac{k_{1}+1}{c_{1}}\right\rceil=0$ yields one disjunct in $F_{3}$ with the values $\left\lfloor\frac{s}{2}\right\rfloor$, and $-\left\lfloor\frac{s}{2}\right\rfloor$, respectively. Again, $F_{1}(\left\lfloor\frac{s}{2}\right\rfloor)$ is always true and can be omitted. The resulting formula is

[TABLE]

The final resolution step yields an interpolant for this problem.

[TABLE]

Thus $H$ is the final interpolant. Now we argue validity of this interpolant.

Interpolant follows from the $A$-part.

The $A$-part contains $2a\leq s$, which implies $a\leq\left\lfloor\frac{s}{2}\right\rfloor$. From $t\leq 2a$ we get $-\left\lfloor\frac{-t}{2}\right\rfloor\leq a$. Hence, $-\left\lfloor\frac{-t}{2}\right\rfloor\leq\left\lfloor\frac{s}{2}\right\rfloor$. Moreover, $-\left\lfloor\frac{-t}{2}\right\rfloor\geq\left\lfloor\frac{s}{2}\right\rfloor$ implies $-\left\lfloor\frac{-t}{2}\right\rfloor=a$. So with the $A$-part we get $f(-\left\lfloor\frac{-t}{2}\right\rfloor)=q$.

Interpolant is inconsistent with the $B$-part.

The $B$-part implies $s\leq 2b\leq t+1$. Hence, we have $\left\lfloor\frac{s}{2}\right\rfloor\leq b\leq\left\lfloor\frac{t+1}{2}\right\rfloor$. A case distinction on whether $t$ is even or odd yields $\left\lfloor\frac{t+1}{2}\right\rfloor=-\left\lfloor\frac{-t}{2}\right\rfloor$. Therefore, $\left\lfloor\frac{s}{2}\right\rfloor\leq b\leq-\left\lfloor\frac{-t}{2}\right\rfloor$ holds. Hence, the interpolant guarantees $f(-\left\lfloor\frac{-t}{2}\right\rfloor)=q$ and $-\left\lfloor\frac{-t}{2}\right\rfloor\leq\left\lfloor\frac{s}{2}\right\rfloor$. Hence, $b=-\left\lfloor\frac{-t}{2}\right\rfloor$ and with $f(b)\neq q$ from the $B$-part we get a contradiction.

Symbol condition is satisfied.

The symbol condition is trivially satisfied since $\mathop{\mathit{symb}}(A)=\{a,t,s,f,q\}$ and $\mathop{\mathit{symb}}(B)=\{b,t,s,f,q\}$. The shared symbols are $t$, $s$, $f$, and $q$ which are exactly the symbols occurring in the interpolant.

7 Conclusion and Future Work

We presented a novel interpolation scheme to extract Craig interpolants from resolution proofs produced by SMT solvers without restricting the solver or reordering the proofs. The key ingredients of our method are virtual purifications of troublesome mixed literals, syntactical restrictions of partial interpolants, and specialised interpolation rules for pivoting steps on mixed literals.

In contrast to previous work, our interpolation scheme does not need specialised rules to deal with extended branches as commonly used in state-of-the-art SMT solvers to solve $\mathcal{LA}\left(\mathbb{Z}\right)$-formulae. Furthermore, our scheme can deal with resolution steps where a mixed literal occurs in both antecedents, which are forbidden by other schemes [5, 12].

Our scheme works for resolution based proofs in the DPLL(T) context provided there is a procedure that generates partial interpolants with our syntactic restrictions for the theory lemmas. We sketched these procedures for the theory lemmas generated by either congruence closure or linear arithmetic solvers producing Farkas proofs. In this paper, we limited the presentation to the combination of the theory of uninterpreted functions, and the theory of linear arithmetic over the integers or the reals. Nevertheless, the scheme could be extended to support other theories. This requires defining the projection functions for mixed literals in the theory, defining a pattern for partial interpolants, and proving a corresponding resolution rule.

We plan to produce interpolants of different strengths using the technique from D’Silva et al. [9]. This is orthogonal to our interpolation scheme (particularly to the partial interpolants used for mixed literals). Furthermore, we want to extend the correctness proof to show that our scheme works with inductive sequences of interpolants [21] and tree interpolants [15]. We also plan to extend this scheme to other theories including arrays and quantifiers.