The problem of computing Craig interpolants in SAT and SMT has recentlyreceived a lot of interest, mainly for its applications in formal verification.Efficient algorithms for interpolant generation have been presented for sometheories of interest ---including that of equality and uninterpreted functions,linear arithmetic over the rationals, and their combination--- and they aresuccessfully used within model checking tools. For the theory of lineararithmetic over the integers (LA(Z)), however, the problem of finding aninterpolant is more challenging, and the task of developing efficientinterpolant generators for the full theory LA(Z) is still the objective ofongoing research. In this paper we try to close this gap. We build on previouswork and present a novel interpolation algorithm for SMT(LA(Z)), which exploitsthe full power of current state-of-the-art SMT(LA(Z)) solvers. We demonstratethe potential of our approach with an extensive experimental evaluation of ourimplementation of the proposed algorithm in the MathSAT SMT solver.
展开▼
