Interpolants for Linear Arithmetic in SMT
The linear arithmetic solver in Yices was specifically designed for SMT provers, providing fast support for operations like adding and deleting constraints. We give a procedure for developing interpolants based on the results of the Yices arithmetic solver. For inequalities over real numbers, the interpolant is computed directly from the one contradictory equation and associated bounds. For integer inequalities, a formula is computed from the contradictory equation, the bounds, and the Gomory cuts. The formula is not exactly an interpolant because it may contain local variables. But local variables only arise from Gomory cuts, so there will not be many local variables, and the formula should thereby be useful for applications like predicate abstraction. For integer equalities, we designed a new procedure. It accepts equations and congruence equations, and returns an interpolant. We have implemented our method and give experimental results.
KeywordsFree Variable Active Bound Predicate Abstraction Linear Arithmetic Extension Equation
Unable to display preview. Download preview PDF.
- 4.Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 2nd edn., pp. 856–862. MIT Press and McGraw-Hill (2001)Google Scholar
- 6.Dantzig, G.B., Curtis, B.: Fourier-Motzkin elimination and its dual. Journal of Combinatorial Theory, 288–297 (1973)Google Scholar
- 7.Dickson, L.E.: History of the Theory of Numbers, vol. 2. Chelsea, New York (1957)Google Scholar
- 8.Dutertre, B., de Moura, L.: Integrating Simplex with DPLL(T). CSL Technical Report SRI-CSL-06-01 (2006)Google Scholar
- 9.Jain, H., Clarke, E.M., Grumberg, O.: Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. In: Proc. CAV (2008)Google Scholar