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 involvi ...

(SMT) solver by

Microsoft Microsoft Corporation is an American multinational technology corporation producing computer software, consumer electronics, personal computers, and related services headquartered at the Microsoft Redmond campus located in Redmond, Washin ...

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

program analysis In computer science, program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas: program op ...

. 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

SIGPLAN SIGPLAN is the Association for Computing Machinery's Special Interest Group on programming languages. Conferences * Principles of Programming Languages (POPL) * Programming Language Design and Implementation (PLDI) * International Symposium on ...

. 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 comp ...

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, continu ...

. 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 devel ...

or using

CMake In software development, CMake is cross-platform free and open-source software for build automation, testing, packaging and installation of software by using a compiler-independent method. CMake is not a build system itself; it generates an ...

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 ser ...

, FreeBSD,

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, w ...

, 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 computers. Within the market of desktop and lapt ...

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

s including C,

C++ C++ (pronounced "C plus plus") is a high-level general-purpose programming language created by Danish computer scientist Bjarne Stroustrup as an extension of the C programming language, or "C with Classes". The language has expanded significan ...

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 mos ...

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.g ...

Haskell Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lan ...

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( ...

, OCaml,

Python Python may refer to: Snakes * Pythonidae, a family of nonvenomous snakes found in Africa, Asia, and Australia ** ''Python'' (genus), a genus of Pythonidae found in Africa and Asia * Python (mythology), a mythical serpent Computing * Python (pro ...

WebAssembly WebAssembly (sometimes abbreviated Wasm) defines a portable binary-code format and a corresponding text format for executable programs as well as software interfaces for facilitating interactions between such programs and their host environment ...

, and .NET/

Mono Mono may refer to: Common meanings * Infectious mononucleosis, "the kissing disease" * Monaural, monophonic sound reproduction, often shortened to mono * Mono-, a numerical prefix representing anything single Music Performers * Mono (Japanese b ...

. 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 math ...

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