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 = Windows, FreeBSD, Linux (Debian, Ubuntu), macOS

| platform = IA-32, x86-64, WebAssembly, arm64

| genre = 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.{{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}}

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|date=May 2023}}

Z3 was open sourced in the beginning of 2015.{{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}} The source code is licensed under MIT License and hosted on GitHub.{{Cite web|url=https://github.com/Z3Prover/z3|title=GitHub - Z3Prover/z3: The Z3 Theorem Prover|date=December 1, 2019|via=GitHub}}

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.{{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}}

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 $\overline{a \land b} \equiv \overline{a} \lor \overline{b}$ :

(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.{{Cite web|url=http://www.sigplan.org/Awards/Software/|title=Programming Languages Software Award|website=www.sigplan.org}}[https://www.i-programmer.info/news/112-theory/8722-microsoft-z3-theorem-prover-wins-award-.html Microsoft Z3 Theorem Prover Wins Award] In 2018, Z3 received the Test of Time Award from the European Joint Conferences on Theory and Practice of Software (ETAPS).[https://www.etaps.org/about/test-of-time-award/test-of-time-award-2018 ETAPS 2018 Test of Time Award] 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.[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][http://www.cadeinc.org/Herbrand-Award Herbrand Award]