View source for Z3 Theorem Prover

{{Short description|Software for solving satisfiability problems}}
{{Infobox software
| name = Z3 Theorem Prover
| logo = Z3 Theorem Prover Logo 329x329.jpg
| logo size = 75px
| author = [[Microsoft Research]]
| developer = [[Microsoft]]
| released = {{Start date and age|2012}}
| latest release version = {{wikidata|property|edit|reference|P348}}
| latest release date    = {{start date and age|{{wikidata|qualifier|P348|P577}}}}
| programming language = [[C++]]
| operating system = [[Microsoft Windows|Windows]], [[FreeBSD]], [[Linux]] ([[Debian]], [[Ubuntu]]), [[macOS]]
| platform = [[IA-32]], [[x86-64]], [[WebAssembly]], [[arm64]]
| genre = [[Automated theorem proving|Theorem prover]]
| license = [[MIT License]]
| website = {{URL|https://github.com/Z3Prover}}
}}
'''Z3''', also known as the '''Z3 Theorem Prover''', is a [[satisfiability modulo theories]] (SMT) solver developed by [[Microsoft]].<ref>{{Cite web |url=http://lim.univ-reunion.fr/staff/fred/Enseignement/AlgoAvancee/Exos/Z3-exercises.pdf |title=Using the SMT solver Z3 |access-date=2019-12-01 |archive-date=2020-11-17 |archive-url=https://web.archive.org/web/20201117164223/http://lim.univ-reunion.fr/staff/fred/Enseignement/AlgoAvancee/Exos/Z3-exercises.pdf |url-status=dead}}</ref>

==Overview==
Z3 was developed in the ''Research in Software Engineering'' (RiSE) group at [[Microsoft Research Redmond]] and is targeted at solving problems that arise in [[software verification]] and [[program analysis]]. Z3 supports arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, and [[quantifier (logic)|quantifier]]s. Its main applications are [[extended static checking]], test case generation, and [[predicate abstraction]].{{citation needed|date=May 2023}}

Z3 was open sourced in the beginning of 2015.<ref>{{Cite web|url=https://sdtimes.com/android/microsofts-visual-studio-timeline-and-z3-theorem-prover-google-cloud-launcher-facebooks-fresco-sd-times-news-digest-march-27-2015/|title=Microsoft's Visual Studio timeline and Z3 Theorem Prover, Google Cloud Launcher, Facebook's Fresco—SD Times news digest: March 27, 2015|date=March 27, 2015}}</ref> The source code is licensed under [[MIT License]] and hosted on [[GitHub]].<ref>{{Cite web|url=https://github.com/Z3Prover/z3|title=GitHub - Z3Prover/z3: The Z3 Theorem Prover|date=December 1, 2019|via=GitHub}}</ref>
The solver can be built using [[Visual Studio]], a [[makefile]] or using [[CMake]] and runs on [[Microsoft Windows|Windows]], [[FreeBSD]], [[Linux]], and [[macOS]].

The default input format for Z3 is [[Smt2 (file format)|SMTLIB2]].
It also has officially supported [[Language binding|bindings]] for several [[programming language]]s, including [[C (programming language)|C]], [[C++]], [[Python (programming language)|Python]], [[.NET]], [[Java (programming language)|Java]], and [[OCaml]].<ref>{{Cite web |last=Bjørner |first=Nikolaj |last2=de Moura |first2=Leonardo |last3=Nachmanson |first3=Lev |last4=Wintersteiger |first4=Christoph |date=2019 |title=Programming Z3 |url=https://z3prover.github.io/papers/programmingz3.html |url-status=live |archive-url=https://web.archive.org/web/20230209065233/https://z3prover.github.io/papers/programmingz3.html |archive-date=February 9, 2023 |access-date=May 21, 2023 |website=Programming Z3}}</ref>

==Examples==
===Propositional and predicate logic===
In this example propositional logic assertions are checked using functions to represent the propositions a and b. The following Z3 script checks to see if <math>\overline{a \land b} \equiv \overline{a} \lor \overline{b}</math>:

 (declare-fun a () Bool)
 (declare-fun b () Bool)
 (assert (not (= (not (and a b)) (or (not a)(not b)))))
 (check-sat)

Result:
 unsat

Note that the script asserts the ''negation'' of the proposition of interest. The ''unsat'' result means that the negated proposition is not satisfiable, thus proving the desired result ([[De Morgan's law]]).

===Solving equations===
The following script solves the two given equations, finding suitable values for the variables a and b:

 (declare-const a Int)
 (declare-const b Int)
 (assert (= (+ a b) 20))
 (assert (= (+ a (* 2 b)) 10))
 (check-sat)
 (get-model)

Result:
 sat
 (model 
   (define-fun b () Int
     -10)
   (define-fun a () Int
     30)
 )

==Awards==

In 2015, Z3 received the ''Programming Languages Software Award'' from [[Association for Computing Machinery|ACM]] [[SIGPLAN]].<ref>{{Cite web|url=http://www.sigplan.org/Awards/Software/|title=Programming Languages Software Award|website=www.sigplan.org}}</ref><ref>[https://www.i-programmer.info/news/112-theory/8722-microsoft-z3-theorem-prover-wins-award-.html Microsoft Z3 Theorem Prover Wins Award]</ref> In 2018, Z3 received the ''Test of Time Award'' from the [[European Joint Conferences on Theory and Practice of Software]] (ETAPS).<ref>[https://www.etaps.org/about/test-of-time-award/test-of-time-award-2018 ETAPS 2018 Test of Time Award]</ref> Microsoft researchers Nikolaj Bjørner and Leonardo de Moura received the 2019 [[Herbrand Award|Herbrand Award for Distinguished Contributions to Automated Reasoning]] in recognition of their work in advancing theorem proving with Z3.<ref>[https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/ The inner magic behind the Z3 theorem prover - Microsoft Research]</ref><ref>[http://www.cadeinc.org/Herbrand-Award Herbrand Award]</ref>

==See also==
{{Portal|Free and open-source software}}
* [[Formal verification]]

==References==
{{Reflist}}

==Further reading==
* {{Cite journal|author1=Leonardo De Moura |author2=Nikolaj Bjørner |title=Z3: an efficient SMT solver|year=2008 |journal=Tools and Algorithms for the Construction and Analysis of Systems |volume=4963 |pages=337–340}}
* [https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/ The inner magic behind the Z3 theorem prover]

==External links==
* {{Official website|https://github.com/Z3Prover}}
* [https://microsoft.github.io/z3guide/playground/Freeform%20Editing/ Official playground]

{{Microsoft FOSS}}
{{Microsoft Research}}

[[Category:Free and open-source software]]
[[Category:Free software programmed in C++]]
[[Category:Microsoft free software]]
[[Category:Microsoft Research]]
[[Category:Satisfiability modulo theories solvers]]
[[Category:Software using the MIT license]]
[[Category:2012 software]]