Advertisement

Interpolants for Linear Arithmetic in SMT

  • Christopher Lynch
  • Yuefeng Tang
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)

Abstract

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.

Keywords

Free Variable Active Bound Predicate Abstraction Linear Arithmetic Extension Equation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The Software Model Checker Blast: Applications to Software Engineering. International Journal on Software Tools for Technology Transfer (STTT) 9(5-6), 505–525 (2007)CrossRefGoogle Scholar
  2. 2.
    Chvatal, V.: Linear Programming. W. H. Freeman, New York (1983)zbMATHGoogle Scholar
  3. 3.
    Cimatti, A., Griggio, A., Sebastiani, R.: Efficient Interpolant Generation in Satisfiability Modulo Theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  4. 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
  5. 5.
    Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbolic Logic 22(3), 269–285 (1957)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Dantzig, G.B., Curtis, B.: Fourier-Motzkin elimination and its dual. Journal of Combinatorial Theory, 288–297 (1973)Google Scholar
  7. 7.
    Dickson, L.E.: History of the Theory of Numbers, vol. 2. Chelsea, New York (1957)Google Scholar
  8. 8.
    Dutertre, B., de Moura, L.: Integrating Simplex with DPLL(T). CSL Technical Report SRI-CSL-06-01 (2006)Google Scholar
  9. 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
  10. 10.
    McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  12. 12.
    McMillan, K.L.: Applications of Craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1–12. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Rybalchenko, A., Stokkermans, V.S.: Constraint Solving for Interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346–362. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  14. 14.
    Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 353–368. Springer, Heidelberg (2005)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Christopher Lynch
    • 1
  • Yuefeng Tang
    • 1
  1. 1.Department of Mathematics and Computer ScienceClarkson UniversityPotsdamUSA

Personalised recommendations