Advertisement

Programming Z3

  • Nikolaj BjørnerEmail author
  • Leonardo de Moura
  • Lev Nachmanson
  • Christoph M. Wintersteiger
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11430)

Abstract

This tutorial provides a programmer’s introduction to the Satisfiability Modulo Theories Solver Z3. It describes how to use Z3 through scripts, provided in the Python scripting language, and it describes several of the algorithms underlying the decision procedures within Z3. It aims to broadly cover almost all available features of Z3 and the essence of the underlying algorithms.

References

  1. 1.
    Alviano, M.: Model enumeration in propositional circumscription via unsatisfiable core analysis. TPLP 17(5–6), 708–725 (2017)MathSciNetzbMATHGoogle Scholar
  2. 2.
    Bacchus, F., Katsirelos, G.: Finding a collection of MUSes incrementally. In: Quimper, C.-G. (ed.) CPAIOR 2016. LNCS, vol. 9676, pp. 35–44. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-33954-2_3CrossRefzbMATHGoogle Scholar
  3. 3.
    Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)
  4. 4.
    Biere, A.: Bounded model checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 457–481. IOS Press (2009).  https://doi.org/10.3233/978-1-58603-929-5-457
  5. 5.
    Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24–51. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-23534-9_2CrossRefGoogle Scholar
  6. 6.
    Bjørner, N., Janota, M.: Playing with alternating quantifier satisfaction. In: LPAR Short Presentation Papers (2015)Google Scholar
  7. 7.
    Bjørner, N., Nachmanson, L.: Theorem recycling for theorem proving. In: Kovács, L., Voronkov, A. (eds.) Vampire 2017, Proceedings of the 4th Vampire Workshop. EPiC Series in Computing, vol. 53, pp. 1–8. EasyChair (2018).  https://doi.org/10.29007/r58f, https://easychair.org/publications/paper/qGfG
  8. 8.
    Bonacina, M.P., Lynch, C., de Moura, L.M.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47(2), 161–189 (2011)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: Formal Methods in Computer-Aided Design, 7th International Conference, FMCAD 2007, Austin, Texas, USA, 11–14 November 2007, Proceedings, pp. 173–180 (2007).  https://doi.org/10.1109/FAMCAD.2007.15
  10. 10.
    Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, 8–10 January 2006, Proceedings, pp. 427–442 (2006).  https://doi.org/10.1007/11609773_28Google Scholar
  11. 11.
    Bromberger, M., Weidenbach, C.: New techniques for linear arithmetic: cubes and equalities. Form. Methods Syst. Des. 51(3), 433–461 (2017).  https://doi.org/10.1007/s10703-017-0278-7CrossRefzbMATHGoogle Scholar
  12. 12.
    Chockler, H., Ivrii, A., Matsliah, A.: Computing interpolants without proofs. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 72–85. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39611-3_12CrossRefGoogle Scholar
  13. 13.
    Christ, J., Hoenicke, J.: Cutting the mix. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 37–52. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21668-3_3CrossRefGoogle Scholar
  14. 14.
    Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Experimenting on solving nonlinear integer arithmetic with incremental linearization. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 383–398. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-94144-8_23CrossRefzbMATHGoogle Scholar
  15. 15.
    Cohen, E., Megiddo, N.: Improved algorithms for linear inequalities with two variables per inequality. SIAM J. Comput. 23(6), 1313–1347 (1994).  https://doi.org/10.1137/S0097539791256325MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Colmerauer, A., Dao, T.-B.-H.: Expressiveness of full first order constraints in the algebra of finite or infinite trees. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, pp. 172–186. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-45349-0_14CrossRefzbMATHGoogle Scholar
  17. 17.
    Costan, A., Gaubert, S., Goubault, E., Martel, M., Putot, S.: A policy iteration algorithm for computing fixed points in static analysis of programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 462–475. Springer, Heidelberg (2005).  https://doi.org/10.1007/11513988_46CrossRefGoogle Scholar
  18. 18.
    Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5, 394–397 (1962)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 233–247. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_20CrossRefGoogle Scholar
  20. 20.
    Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4), 758–771 (1980).  https://doi.org/10.1145/322217.322228MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006).  https://doi.org/10.1007/11817963_11CrossRefGoogle Scholar
  22. 22.
    Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_25CrossRefGoogle Scholar
  23. 23.
    Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012, Beijing, China, 11–16 June 2012, pp. 405–416 (2012).  https://doi.org/10.1145/2254064.2254112
  24. 24.
    Heule, M., Järvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. 53, 127–168 (2015).  https://doi.org/10.1613/jair.4694MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50–65. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-34188-5_8CrossRefGoogle Scholar
  26. 26.
    Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31612-8_13CrossRefGoogle Scholar
  27. 27.
    Hoder, K., Bjørner, N., de Moura, L.: \(\mu \)z– an efficient engine for fixed points with constraints. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 457–462. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_36CrossRefGoogle Scholar
  28. 28.
    Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265–281. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_19CrossRefGoogle Scholar
  29. 29.
    Janota, M., Lynce, I., Marques-Silva, J.: Algorithms for computing backbones of propositional formulae. AI Commun. 28(2), 161–177 (2015).  https://doi.org/10.3233/AIC-140640MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25–31 July 2015, pp. 325–331 (2015). http://ijcai.org/Abstract/15/052
  31. 31.
    John, A.K., Chakraborty, S.: A quantifier elimination algorithm for linear modular equations and disequations. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 486–503. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_39CrossRefGoogle Scholar
  32. 32.
    John, A.K., Chakraborty, S.: A layered algorithm for quantifier elimination from linear modular constraints. Form. Methods Syst. Des. 49(3), 272–323 (2016).  https://doi.org/10.1007/s10703-016-0260-9CrossRefzbMATHGoogle Scholar
  33. 33.
    Jovanović, D.: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 330–346. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-52234-0_18CrossRefGoogle Scholar
  34. 34.
    Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339–354. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31365-3_27CrossRefGoogle Scholar
  35. 35.
    Kapur, D., Zarba, C.: A reduction approach to decision procedures. Technical report, University of New Mexico (2006). https://www.cs.unm.edu/~kapur/mypapers/reduction.pdf
  36. 36.
    Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17–34. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08867-9_2CrossRefGoogle Scholar
  37. 37.
    Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible mus enumeration. Constraints 21(2), 223–250 (2016)MathSciNetCrossRefGoogle Scholar
  38. 38.
    Lopes, N.P., Menendez, D., Nagarakatte, S., Regehr, J.: Practical verification of peephole optimizations with alive. Commun. ACM 61(2), 84–91 (2018).  https://doi.org/10.1145/3166064CrossRefGoogle Scholar
  39. 39.
    McMillan, K.L.: Lazy annotation revisited. In: Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 18–22 July 2014, Proceedings, pp. 243–259 (2014).  https://doi.org/10.1007/978-3-319-08867-9_16Google Scholar
  40. 40.
    Mencía, C., Previti, A., Marques-Silva, J.: Literal-based MCS extraction. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25–31 July 2015, pp. 1973–1979 (2015). http://ijcai.org/Abstract/15/280
  41. 41.
    Monniaux, D.: A quantifier elimination algorithm for linear real arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 243–257. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-89439-1_18CrossRefzbMATHGoogle Scholar
  42. 42.
    de Moura, L.M., Bjørner, N.: Proofs and refutations, and Z3. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, 22 November 2008, CEUR Workshop Proceedings, vol. 418. CEUR-WS.org (2008). http://ceur-ws.org/Vol-418/paper10.pdf
  43. 43.
    de Moura, L.M., Bjørner, N.: Generalized, efficient array decision procedures. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15–18 November 2009, Austin, Texas, USA, pp. 45–52 (2009).  https://doi.org/10.1109/FMCAD.2009.5351142
  44. 44.
    de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1–12. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-35873-9_1CrossRefGoogle Scholar
  45. 45.
    de Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 15–44. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-36675-8_2CrossRefGoogle Scholar
  46. 46.
    de Moura, L., Bjørner, N.: Efficient E-Matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183–198. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73595-3_13CrossRefGoogle Scholar
  47. 47.
    de Moura, L., Bjørner, N.: Bugs, moles and skeletons: symbolic reasoning for software development. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 400–411. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14203-1_34CrossRefzbMATHGoogle Scholar
  48. 48.
    Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSat resolution. In: Brodley, C.E., Stone, P. (eds.) AAAI 2014, 27–31 July 2014, Quebec City, Quebec, Canada, pp. 2717–2723. AAAI Press (2014)Google Scholar
  49. 49.
    Narodytska, N., Bjørner, N., Marinescu, M., Sagiv, M.: Core-guided minimal correction set and core enumeration. In: Lang, J. (ed.) Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, 13–19 July 2018, Stockholm, Sweden, pp. 1353–1361. ijcai.org (2018).  https://doi.org/10.24963/ijcai.2018/188
  50. 50.
    Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979).  https://doi.org/10.1145/357073.357079CrossRefzbMATHGoogle Scholar
  51. 51.
    Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Solving quantified bit-vectors using invertibility conditions. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 236–255. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-96142-2_16CrossRefGoogle Scholar
  52. 52.
    Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)MathSciNetCrossRefGoogle Scholar
  53. 53.
    Previti, A., Mencía, C., Järvisalo, M., Marques-Silva, J.: Improving MCS enumeration via caching. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 184–194. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66263-3_12CrossRefGoogle Scholar
  54. 54.
    Ramakrishnan, I.V., Sekar, R.C., Voronkov, A.: Term indexing. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 1853–1964. Elsevier and MIT Press (2001)Google Scholar
  55. 55.
    Seidl, M., Lonsing, F., Biere, A.: qbf2epr: a tool for generating EPR formulas from QBF. In: Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012, Manchester, UK, 30 June–1 July 2012, pp. 139–148 (2012). http://www.easychair.org/publications/paper/145184
  56. 56.
    Silva, J.P.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)MathSciNetCrossRefGoogle Scholar
  57. 57.
    Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2), 215–225 (1975).  https://doi.org/10.1145/321879.321884MathSciNetCrossRefzbMATHGoogle Scholar
  58. 58.
    Veanes, M., Bjørner, N., Nachmanson, L., Bereg, S.: Monadic decomposition. J. ACM 64(2), 14:1–14:28 (2017).  https://doi.org/10.1145/3040488MathSciNetCrossRefzbMATHGoogle Scholar
  59. 59.
    Wintersteiger, C.M., Hamadi, Y., de Moura, L.M.: Efficiently solving quantified bit-vector formulas. Form. Methods Syst. Des. 42(1), 3–23 (2013)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Microsoft ResearchRedmondUSA
  2. 2.Microsoft ResearchCambridgeUK

Personalised recommendations