Interpolant Generation for UTVPI

The problem of computing Craig interpolants in SMT has recently received a lot of interest, mainly for its applications in formal verification. Efficient algorithms for interpolant generation have been presented for some theories of interest -including that of equality and uninterpreted functions (ε Uℱ), linear arithmetic over the rationals (LA(ℚ)), and some fragments of linear arithmetic over the integers (LA(ℤ))- and they are successfully used within model checking tools. In this paper we address the problem of computing interpolants in the theory of Unit-Two-Variable-Per-Inequality (UTVPI). This theory is a very useful fragment of LA(Zdbl;), since it is expressive enough to encode many hardware and software verification queries while still admitting a polynomial time decision procedure. We present an efficient graph-based algorithm for interpolant generation in UTVPI, which exploits the power of modern SMT techniques. We have implemented our new algorithm within the MathSAT SMT solv...