Z3 Theorem Prover

Z3 Theorem Prover
Original author(s)	Microsoft Research
Developer(s)	Microsoft
Initial release	2012
Stable release	z3-4.8.8 / May 8, 2020
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 Theorem Prover is a cross-platform satisfiability modulo theories (SMT) solver by Microsoft.[1]

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

Z3 was open sourced in the beginning of 2015.[7] The source code is licensed under MIT License and hosted on GitHub.[8] 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, 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 ¬(a ∧ b ) ≡ (¬ a ∨ ¬ b):

(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (= (not(and a b)) (or (not a)(not b))))
(check-sat)

Result:

sat

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

gollark: I've decided to settle for bothering that person about it via their web logs, which is admittedly unlikely to go anywhere since they have the default Apache site up.

gollark: Their IP reverse-DNSes to what looks like some Russian hosting company and nmap says they have a bunch of ports open.

gollark: I'm trying to figure out if there's a way I can bother whoever is doing stuff from the IP which tried to use `Telerik.Web.UI.WebResource.axd` on search.osmarks.tk (which doesn't exist).

gollark: Your space terminated strings can't contain spaces, so...

gollark: Nope.

References

External links

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.

[1] ttp://lim.univ-reunion.fr/staff/fred/Enseignement/AlgoAvancee/Exos/Z3-exercises.pdf

[2] "Programming Languages Software Award". www.sigplan.org.

[3] Microsoft Z3 Theorem Prover Wins Award

[4] ETAPS 2018 Test of Time Award

[5] The inner magic behind the Z3 theorem prover - Microsoft Research

[6] Herbrand Award

[7] "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.

[8] "GitHub - Z3Prover/z3: The Z3 Theorem Prover". December 1, 2019 – via GitHub.