A new interpolation algorithm

For the theory of Equality with Uninterpreted Functions

Jose Abel Castellanos Joo, Deepak Kapur
CS Colloquium @ University of New Mexico

Outline

What is an interpolant?

Craig Interpolant

Definition: Given two logical formulas $A$ and $B$ such that $\vdash A \land B \rightarrow \bot$, an interpolant $I$ for $(A, B)$ satisfies:

  • $\vdash A \rightarrow I$
  • $\vdash B \land I \rightarrow \bot$
  • $vars(I) \subseteq vars(A) \cap vars(B)$

Applications:

  • Guide bounded model checking algorithms [ 6 ]
  • Invariant generation for quantifier-free theories [ 5 ]

Example

$A := f(z_1, v) = s_1 \land f(z_2, v) = s_2 \land f(f(y_1, v), f(y_2, v)) = t$

$B := z_1 = y_1 \land z_1 = y_2 \land f(s_1, s_1) \neq t$

Discussing the example (1)

$A := f(z_1, v) = s_1 \land f(z_2, v) = s_2 \land f(f(y_1, v), f(y_2, v)) = t$

$B := z_1 = y_1 \land z_1 = y_2 \land f(s_1, s_1) \neq t$

$I := f(s_1, s_1) = t \lor z_1 \neq y_1 \lor y_2 \neq y_1$ contains only common symbols

Discussing the example (2)

$A := f(z_1, v) = s_1 \land f(z_2, v) = s_2 \land f(f(y_1, v), f(y_2, v)) = t$

$I := f(s_1, s_1) = t \lor z_1 \neq y_1 \lor y_2 \neq y_1$

$\vdash A \rightarrow I$ because:

$I \cong (z_1 = y_1 \land y_2 = y_1) \rightarrow f(s_1, s_1) = t $

Discussing the example (3)

$B := z_1 = y_1 \land z_1 = y_2 \land f(s_1, s_1) \neq t$

$I := f(s_1, s_1) = t \lor z_1 \neq y_1 \lor y_2 \neq y_1$

$\vdash B \land I \rightarrow \bot$ because:

b_part_check

Problem (Statement)

Problem statement: Given a pair of inconsistent conjunctive formulas in the EUF theory, find the interpolating formula

Current approaches mainly rely on unsatisfiability proofs [4–7]

z3_proof

Prof. Kapur Algorithm

It finds an interpolant by eliminating uncommon symbols.

  • Preprocessing: Flatten formula by introducing new constants

  • Phase I: Elimination of uncommon constants

  • Phase II: Elimination of uncommon function symbols

  • Phase III: Elimination of uncommon symbols conditionally

  • Phase IV: Interpolant generation

Preprocessing

The algorithm introduces new constants by equating each subexpression in the AST of the original input

Subterms with function symbols $f$ with produce f-equations of the form:

(1)
\[f(a_1, \dots, a_n) = b \]

where each $a_1, \dots, a_n, b$ are constants

New terms preserve the common property

My implementation renames terms to work internally with particular methods to distinguish terms

This steps rewrites disequations of the form $a \neq b$ into Horn clauses of the form $a = b \rightarrow \bot$

Elimination of uncommon constants

This steps computes the congruence closure [2, 8, 9] of the initial set of equations an keeps as representatives of the underlying union-find data structure common terms whenever possible

Elimination of uncommon function symbols

There are two cases:

  • Uncommon terms because function symbol is uncommon

For all pairs of f-equations

  • $f(a_1, \dots, a_n) = c_1$, and
  • $f(b_1, \dots, b_n) = c_2$

generate a Horn clause of the form $\bigwedge_{i=1}^n repr(a_i) = repr(b_i) \rightarrow repr(c_1) = repr(c_2)$

  • Uncommon terms because function application contains uncommon terms

Follow the same rule as above

Elimination of uncommon symbols conditionally

If there are Horn clauses which antecedent is completely common and it contains at least an uncommon term in the consequent equation,

then use these Horn clauses to conditionally eliminate the uncommon term in other Horn clauses which contain this uncommon term

Dependency analysis can improve the possible exponential behaviour of this step by choose a right ordering of reduction

Interpolant generation

This step outputs all the common Horn clauses generated, the existing common equations, and it generates new Horn clauses by eliminating uncommon terms appearing in uncommon equations similarly to the conditional elimination approach

Additionally, the algorithm removes the constants introduced in the problem

My implementation

My implementation modifies the Phase III of the original formulation

The idea is to use a separate (conditional) equivalence relation that includes the theory implied by the common equations appearing inside the antecedent of the Horn clauses produced in Phase II

Additionally, the implementation requires an explanation operator to produce Horn clauses with antecedents constructed using such operator using the original equations and the Horn clauses produced in Phase II

Data Structures

Linear-time algorithm for propositional Horn formulae [ 1 ]

Horn unsatisfiability with grounded equations [ 3 ]

Congruence closure with explanations [ 9 ]

Modification: only add into the equivalence relation common equations using a congruence closure with explanations to keep track of these common equations

Modified algorithms

modified_gallier

modified_gallier_2

New Conditional Elimination Step (1)

  • Processing equations

new_cond_elimination_1

new_cond_elimination_2

New Conditional Elimination Step (2)

  • Processing Horn clauses

There are four cases:

Antecedent : Common, Consequent : Common

Antecedent : Common, Consequent : Uncommon

Antecedent : Uncommon, Consequent : Common

Antecedent : Uncommon, Consequent : Uncommon

Some theorems

Lemma 1.
numargs is always 0 or a positive number.

Lemma 2.
Explain for the modified Gallier data structure always returns a set of common equations

Theorem 1.
The new conditional elimination step always produce common Horn clauses

Conclusions

Unsatisfiabilit proofs for conjunctive inconsistencies in the theory of EUF can be exponentially large

An unsatisfiability proof is not needed to compute the interpolant for the EUF theory

The implementation provides an additional mechanism for working with interpolating related problems

Contributions

References

[1]William F. Dowling, and Jean H. Gallier. “Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae.” The Journal of Logic Programming 1 (3): 267–284. 1984. doi:10.1016/0743-1066(84)90014-1. 🔎
[2]Peter J. Downey, Ravi Sethi, and Robert Endre Tarjan. “Variations on the Common Subexpression Problem.” J. ACM 27 (4). Association for Computing Machinery, New York, NY, USA: 758–771. Oct. 1980. doi:10.1145/322217.322228. 🔎
[3]Jean H. Gallier. “Fast Algorithms for Testing Unsatisfiability of Ground Horn Clauses with Equations.” Journal of Symbolic Computation 4 (2): 233–254. 1987. doi:10.1016/S0747-7171(87)80067-6. 🔎
[4]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. “Abstractions from Proofs.” SIGPLAN Not. 39 (1). Association for Computing Machinery, New York, NY, USA: 232–244. Jan. 2004. doi:10.1145/982962.964021. 🔎
[5]Kenneth McMillan. “Interpolants from Z3 Proofs.” In Formal Methods in Computer-Aided Design, Formal Methods in Computer-Aided Design. Oct. 2011. https://​www.​microsoft.​com/​en-​us/​research/​publication/​interpolants-​from-​z3-​proofs/​. 🔎
[6]K. L. McMillan. “Interpolation and SAT-Based Model Checking.” In Computer Aided Verification, edited by Warren A. Hunt and Fabio Somenzi, 1–13. Springer Berlin Heidelberg, Berlin, Heidelberg. 2003. 🔎
[7]K. L. McMillan. “An Interpolating Theorem Prover.” In Tools and Algorithms for the Construction and Analysis of Systems, edited by Kurt Jensen and Andreas Podelski, 16–30. Springer Berlin Heidelberg, Berlin, Heidelberg. 2004. 🔎
[8]Greg Nelson, and Derek C. Oppen. “Fast Decision Procedures Based on Congruence Closure.” J. ACM 27 (2). Association for Computing Machinery, New York, NY, USA: 356–364. Apr. 1980. doi:10.1145/322186.322198. 🔎
[9]Robert Nieuwenhuis, and Albert Oliveras. “Proof-Producing Congruence Closure.” In Term Rewriting and Applications, edited by Jürgen Giesl, 453–468. Springer Berlin Heidelberg, Berlin, Heidelberg. 2005. 🔎