Z3 Theorem Prover

Z3 Theorem Prover

Original author(s)	Microsoft Research
Developer(s)	Microsoft
Initial release	2012; 10 years ago (2012)
Stable release	z3-4.8.12 / July 13, 2021; 6 months ago (2021-07-13)[1]
Repository	github.com/Z3Prover/z3
Written in	C++
Operating system	Windows, FreeBSD, Linux (Debian, Ubuntu), macOS
Platform	IA-32, x86-64
Type	Theorem prover
License	MIT License
Website	github.com/Z3Prover

Z3, also known as the Z3 Theorem Prover, is a cross-platform satisfiability modulo theories (SMT) solver by Microsoft.^[2]

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 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.^[3][4] In 2018, Z3 received the Test of Time Award from the European Joint Conferences on Theory and Practice of Software (ETAPS).^[5] 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.^[6][7]

Z3 was open sourced in the beginning of 2015.^[8] The source code is licensed under MIT License and hosted on GitHub.^[9] The solver can be built using Visual Studio, a Makefile or using CMake and runs on Windows, FreeBSD, Linux, and macOS.

It has bindings for various programming languages including C, C++, Java, Julia, Haskell, OCaml, 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 ${\displaystyle {\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 laws).

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

See also[]

• Formal verification
• Alt-Ergo

References[]

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.CS1 maint: uses authors parameter (link)
• Dennis Yurichev - SAT/SMT by Example - With many examples using Z3Py.
• Solving Classic, Giant and other Sudoku using an SMT (Integer) Using a SMT (Integer) solver like Z3
• Solving Queens placement puzzle on chess board Using an SMT (Integer) solver like Z3.

External links[]

• Official website
• The inner magic behind the Z3 theorem prover
• Z3 @ rise4fun from Microsoft