Z3, also known as the Z3 Theorem Prover, is a cross-platform

satisfiability modulo theories In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvin ...

(SMT) solver by

Microsoft Microsoft Corporation is an American multinational corporation, multinational technology company, technology corporation producing Software, computer software, consumer electronics, personal computers, and related services headquartered at th ...

Overview

Z3 was developed in the ''Research in Software Engineering'' (RiSE) group at

Microsoft Research Microsoft Research (MSR) is the research subsidiary of Microsoft. It was created in 1991 by Richard Rashid, Bill Gates and Nathan Myhrvold with the intent to advance state-of-the-art computing and solve difficult world problems through technologi ...

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. In 2015, it received the ''Programming Languages Software Award'' from

ACM ACM or A.C.M. may refer to: Aviation * AGM-129 ACM, 1990–2012 USAF cruise missile * Air chief marshal * Air combat manoeuvring or dogfighting * Air cycle machine * Arica Airport (Colombia) (IATA: ACM), in Arica, Amazonas, Colombia Computing * ...

SIGPLAN. In 2018, Z3 received the ''Test of Time Award'' from the European Joint Conferences on Theory and Practice of Software (ETAPS). 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. Z3 was open sourced in the beginning of 2015. The source code is licensed under

MIT License The MIT License is a permissive free software license originating at the Massachusetts Institute of Technology (MIT) in the late 1980s. As a permissive license, it puts only very limited restriction on reuse and has, therefore, high license co ...

and hosted on

GitHub GitHub, Inc. () is an Internet hosting service for software development and version control using Git. It provides the distributed version control of Git plus access control, bug tracking, software feature requests, task management, co ...

. The solver can be built using

Visual Studio Visual Studio is an integrated development environment (IDE) from Microsoft. It is used to develop computer programs including websites, web apps, web services and mobile apps. Visual Studio uses Microsoft software development platforms such ...

, a

Makefile In software development, Make is a build automation tool that automatically builds executable programs and libraries from source code by reading files called ''Makefiles'' which specify how to derive the target program. Though integrated deve ...

or using CMake and runs on

Windows Windows is a group of several proprietary graphical operating system families developed and marketed by Microsoft. Each family caters to a certain sector of the computing industry. For example, Windows NT for consumers, Windows Server for ...

FreeBSD FreeBSD is a free and open-source Unix-like operating system descended from the Berkeley Software Distribution (BSD), which was based on Research Unix. The first version of FreeBSD was released in 1993. In 2005, FreeBSD was the most popular ...

Linux Linux ( or ) is a family of open-source Unix-like operating systems based on the Linux kernel, an operating system kernel first released on September 17, 1991, by Linus Torvalds. Linux is typically packaged as a Linux distribution, which i ...

, and

macOS macOS (; previously OS X and originally Mac OS X) is a Unix operating system developed and marketed by Apple Inc. since 2001. It is the primary operating system for Apple's Mac (computer), Mac computers. Within the market of ...

. It has bindings for various

programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming l ...

s including C, C++,

Java Java (; id, Jawa, ; jv, ꦗꦮ; su, ) is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea to the north. With a population of 151.6 million people, Java is the world's mo ...

Julia Julia is usually a feminine given name. It is a Latinate feminine form of the name Julio and Julius. (For further details on etymology, see the Wiktionary entry "Julius".) The given name ''Julia'' had been in use throughout Late Antiquity (e ...

, Haskell,

Rust Rust is an iron oxide, a usually reddish-brown oxide formed by the reaction of iron and oxygen in the catalytic presence of water or air moisture. Rust consists of hydrous iron(III) oxides (Fe2O3·nH2O) and iron(III) oxide-hydroxide (FeO(OH), ...

OCaml OCaml ( , formerly Objective Caml) is a general-purpose, multi-paradigm programming language which extends the Caml dialect of ML with object-oriented features. OCaml was created in 1996 by Xavier Leroy, Jérôme Vouillon, Damien Doligez, D ...

, Python, WebAssembly, and .NET/ Mono. The default input format is SMTLIB2.

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 \equiv \overline \lor \overline

: (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 laws In propositional logic and Boolean algebra, De Morgan's laws, also known as De Morgan's theorem, are a pair of transformation rules that are both valid rules of inference. They are named after Augustus De Morgan, a 19th-century British mathem ...

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) )

References

External links

*
Z3 online playground

The inner magic behind the Z3 theorem prover
{{Microsoft Research Free and open-source software Free software programmed in C++ Microsoft free software Microsoft Research SMT solvers Software using the MIT license 2012 software