Z3 Theorem Prover: Difference between revisions
(28 intermediate revisions by 17 users not shown) | |||
Line 1: | Line 1: | ||
{{Short description|Software for solving satisfiability problems}} |
|||
{{Infobox software |
{{Infobox software |
||
| name = Z3 Theorem Prover |
| name = Z3 Theorem Prover |
||
Line 6: | Line 7: | ||
| developer = [[Microsoft]] |
| developer = [[Microsoft]] |
||
| released = {{Start date and age|2012}} |
| released = {{Start date and age|2012}} |
||
| latest release version = {{wikidata|property|edit|reference|P348}} |
|||
| latest_release_version = z3-4.8.12 |
|||
| latest release date = {{start date and age|{{wikidata|qualifier|P348|P577}}}} |
|||
| latest_release_date = {{Start date and age|2021|07|13}}<ref>https://github.com/Z3Prover/z3/releases/tag/z3-4.8.12</ref> |
|||
| repo = {{URL|https://github.com/Z3Prover/z3}} |
|||
| programming language = [[C++]] |
| programming language = [[C++]] |
||
| operating system = [[Microsoft Windows|Windows]], [[FreeBSD]], [[Linux]] ([[Debian]], [[Ubuntu]]), [[macOS]] |
| operating system = [[Microsoft Windows|Windows]], [[FreeBSD]], [[Linux]] ([[Debian]], [[Ubuntu]]), [[macOS]] |
||
| platform = [[IA-32]], [[x86-64]] |
| platform = [[IA-32]], [[x86-64]], [[WebAssembly]], [[arm64]] |
||
| genre = [[Automated theorem proving|Theorem prover]] |
| genre = [[Automated theorem proving|Theorem prover]] |
||
| license = [[MIT License]] |
| license = [[MIT License]] |
||
| website = {{URL|https://github.com/Z3Prover}} |
| website = {{URL|https://github.com/Z3Prover}} |
||
}} |
}} |
||
'''Z3 Theorem Prover''' is a |
'''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== |
==Overview== |
||
Z3 was developed in the ''Research in Software Engineering'' (RiSE) group at [[Microsoft Research]] and is targeted at solving problems that arise in [[software verification]] and [[ |
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> |
||
⚫ | In 2015, |
||
⚫ | |||
The default input format for Z3 is [[Smt2 (file format)|SMTLIB2]]. |
|||
⚫ | 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> |
||
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> |
|||
⚫ | |||
It has bindings for various [[programming language]]s including [[C (programming language)|C]], [[C++]], [[Java (programming language)|Java]], [[Julia (programming language)|Julia]], [[Haskell (programming language)|Haskell]], [[OCaml]], [[Python (programming language)|Python]], [[WebAssembly]], and [[.NET Framework|.NET]]/[[Mono (software)|Mono]]. The default input format is [[Smt2 (file format)|SMTLIB2]]. |
|||
==Examples== |
==Examples== |
||
Line 40: | Line 39: | ||
unsat |
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 |
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=== |
===Solving equations=== |
||
Line 60: | Line 59: | ||
30) |
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== |
==See also== |
||
{{Portal|Free and open-source software}} |
{{Portal|Free and open-source software}} |
||
* [[Formal verification]] |
* [[Formal verification]] |
||
* [[Alt-Ergo]] |
|||
==References== |
==References== |
||
Line 70: | Line 72: | ||
==Further reading== |
==Further reading== |
||
* {{Cite journal| |
* {{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://yurichev.com/writings/SAT_SMT_by_example.pdf Dennis Yurichev - SAT/SMT by Example] - With many examples using Z3Py. |
|||
* [https://www.researchgate.net/publication/341822510_Sudoku_and_Giant_Sudoku Solving Classic, Giant and other Sudoku using an SMT (Integer)] Using a SMT (Integer) solver like Z3 |
|||
* [https://www.researchgate.net/publication/341266227_Chess_Queens_social_distancing_problem_using_an_SMT_Solver Solving Queens placement puzzle on chess board] Using an SMT (Integer) solver like Z3. |
|||
==External links== |
==External links== |
||
* {{Official website|https://github.com/Z3Prover}} |
* {{Official website|https://github.com/Z3Prover}} |
||
* [https://jfmc.github.io/z3-play/ Z3 online playground] |
|||
⚫ | |||
* [https://rise4fun.com/Z3 Z3 @ rise4fun from Microsoft] |
|||
{{Microsoft FOSS}} |
{{Microsoft FOSS}} |
Revision as of 03:35, 21 April 2024
Original author(s) | Microsoft Research |
---|---|
Developer(s) | Microsoft |
Initial release | 2012 |
Stable release | 4.13.0[1]
/ 7 March 2024 |
Repository | |
Written in | C++ |
Operating system | Windows, FreeBSD, Linux (Debian, Ubuntu), macOS |
Platform | IA-32, x86-64, WebAssembly, arm64 |
Type | Theorem prover |
License | MIT License |
Website | github |
Z3, also known as the Z3 Theorem Prover, is a satisfiability modulo theories (SMT) solver developed by Microsoft.[2]
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 quantifiers. Its main applications are extended static checking, test case generation, and predicate abstraction.[citation needed]
Z3 was open sourced in the beginning of 2015.[3] The source code is licensed under MIT License and hosted on GitHub.[4] The solver can be built using Visual Studio, a makefile or using CMake and runs on Windows, FreeBSD, Linux, and macOS.
The default input format for Z3 is SMTLIB2. It also has officially supported bindings for several programming languages, including C, C++, Python, .NET, Java, and OCaml.[5]
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 :
(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 ACM SIGPLAN.[6][7] In 2018, Z3 received the Test of Time Award from the European Joint Conferences on Theory and Practice of Software (ETAPS).[8] Microsoft researchers Nikolaj Bjørner and Leonardo de Moura received the 2019 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of their work in advancing theorem proving with Z3.[9][10]
See also
References
- ^ "Release 4.13.0". 7 March 2024. Retrieved 26 March 2024.
- ^ "Using the SMT solver Z3" (PDF). Archived from the original (PDF) on 2020-11-17. Retrieved 2019-12-01.
- ^ "Microsoft's Visual Studio timeline and Z3 Theorem Prover, Google Cloud Launcher, Facebook's Fresco—SD Times news digest: March 27, 2015". March 27, 2015.
- ^ "GitHub - Z3Prover/z3: The Z3 Theorem Prover". December 1, 2019 – via GitHub.
- ^ Bjørner, Nikolaj; de Moura, Leonardo; Nachmanson, Lev; Wintersteiger, Christoph (2019). "Programming Z3". Programming Z3. Archived from the original on February 9, 2023. Retrieved May 21, 2023.
- ^ "Programming Languages Software Award". www.sigplan.org.
- ^ Microsoft Z3 Theorem Prover Wins Award
- ^ ETAPS 2018 Test of Time Award
- ^ The inner magic behind the Z3 theorem prover - Microsoft Research
- ^ Herbrand Award
Further reading
- Leonardo De Moura; Nikolaj Bjørner (2008). "Z3: an efficient SMT solver". Tools and Algorithms for the Construction and Analysis of Systems. 4963: 337–340.
- The inner magic behind the Z3 theorem prover