z3

The Z3 Theorem Prover

10,260

1,477

10,260

151

View on GitHub

Top Related Projects

verona

3,574

Research programming language for concurrent ownership

cvc5

1,004

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

Quick Overview

Z3 is a high-performance theorem prover developed by Microsoft Research. It is used for software verification, constraint solving, and automated theorem proving. Z3 supports a wide range of theories and can be integrated into various programming languages.

Pros

Powerful and efficient constraint solving capabilities
Supports multiple theories and logics (e.g., arithmetic, arrays, bit-vectors)
Extensive language bindings (Python, C++, Java, .NET, etc.)
Active development and community support

Cons

Steep learning curve for beginners
Documentation can be challenging for non-experts
Performance can vary depending on the complexity of the problem
Limited support for certain specialized domains

Code Examples

Solving a simple arithmetic constraint:

from z3 import *

x = Int('x')
y = Int('y')
s = Solver()
s.add(x + y > 5)
s.add(x > 0)
s.add(y > 0)
print(s.check())
print(s.model())

Checking satisfiability of boolean formulas:

from z3 import *

p = Bool('p')
q = Bool('q')
r = Bool('r')
s = Solver()
s.add(Implies(p, q))
s.add(Implies(q, r))
s.add(p)
s.add(Not(r))
print(s.check())

Solving an optimization problem:

from z3 import *

x = Real('x')
y = Real('y')
opt = Optimize()
opt.add(x + y <= 10)
opt.add(x >= 0)
opt.add(y >= 0)
h1 = opt.maximize(3*x + 2*y)
h2 = opt.minimize(x - y)
print(opt.check())
print(opt.lower(h1), opt.upper(h1))
print(opt.lower(h2), opt.upper(h2))

Getting Started

To get started with Z3, follow these steps:

Install Z3:
```
pip install z3-solver
```
Import Z3 in your Python script:
```
from z3 import *
```

Create variables, add constraints, and solve:

x = Int('x')
s = Solver()
s.add(x > 0)
s.add(x < 10)
if s.check() == sat:
    print(s.model())

For more advanced usage and integration with other languages, refer to the official Z3 documentation.

Competitor Comparisons

verona

3,574

Research programming language for concurrent ownership

Pros of Verona

Focuses on concurrent programming and memory safety
Designed for building highly scalable, low-latency systems
Introduces novel concepts like concurrent ownership and regions

Cons of Verona

Still in early development stages, not production-ready
Smaller community and ecosystem compared to Z3
Limited documentation and learning resources

Code Comparison

Verona example (concurrent ownership):

class Counter
{
  var count: U64;

  public create(): Counter & mut
  {
    Counter{ count: 0 }
  }

  public increment(self: Counter & mut)
  {
    self.count = self.count + 1;
  }
}

Z3 example (constraint solving):

from z3 import *

x = Int('x')
y = Int('y')
s = Solver()
s.add(x > 2, y < 10, x + 2*y == 7)
print(s.check())
print(s.model())

While Z3 is a mature theorem prover and constraint solver, Verona is a new programming language focusing on concurrent systems. Z3 is widely used in formal verification and program analysis, whereas Verona aims to provide safer and more efficient concurrent programming models. The code examples highlight their different purposes: Verona for writing concurrent programs, and Z3 for solving logical constraints.

cvc5

1,004

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

Pros of cvc5

More active development and frequent updates
Better support for quantifiers and non-linear arithmetic
Stronger performance in certain SMT-LIB categories

Cons of cvc5

Smaller user community and less extensive documentation
Fewer language bindings and integrations
Less mature codebase compared to Z3

Code Comparison

Z3:

Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2) {
    Z3_TRY;
    RESET_ERROR_CODE();
    api::context * ctx = mk_c(c);
    ast_manager & m = ctx->m();
    expr * _t1 = to_expr(t1);
    expr * _t2 = to_expr(t2);
    return of_ast(m.mk_app(m.get_family_id("bv"), OP_BADD, _t1, _t2));
    Z3_CATCH_RETURN(nullptr);
}

cvc5:

Node BVRewriter::rewriteAdd(TNode node)
{
  Assert(node.getKind() == kind::BITVECTOR_ADD);
  NodeManager* nm = NodeManager::currentNM();
  std::vector<Node> children;
  for (const Node& c : node)
  {
    children.push_back(c);
  }
  return nm->mkNode(kind::BITVECTOR_ADD, children);
}

Convert designs to code with AI

Introducing Visual Copilot: A new AI model to turn Figma designs to high quality code using your components.

Try Visual Copilot

README

Z3

Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license.

If you are not familiar with Z3, you can start here.

Pre-built binaries for stable and nightly releases are available from here.

Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for several programming languages.

See the release notes for notes on various stable releases of Z3.

Build status

Azure Pipelines	Code Coverage	Open Bugs	Android Build	WASM Build	Windows Build

Docker image.

Building Z3 on Windows using Visual Studio Command Prompt

32-bit builds, start with:

python scripts/mk_make.py

or instead, for a 64-bit build:

python scripts/mk_make.py -x

then:

cd build
nmake

Z3 uses C++17. The recommended version of Visual Studio is therefore VS2019.

Building Z3 using make and GCC/Clang

Execute:

python scripts/mk_make.py
cd build
make
sudo make install

Note by default g++ is used as the C++ compiler if it is available. If you would prefer to use Clang change the mk_make.py invocation to:

CXX=clang++ CC=clang python scripts/mk_make.py

Note that Clang < 3.7 does not support OpenMP.

You can also build Z3 for Windows using Cygwin and the Mingw-w64 cross-compiler. To configure that case correctly, make sure to use Cygwin's own python and not some Windows installation of Python.

For a 64 bit build (from Cygwin64), configure Z3's sources with

CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.py

A 32 bit build should work similarly (but is untested); the same is true for 32/64 bit builds from within Cygwin32.

By default, it will install z3 executable at PREFIX/bin, libraries at PREFIX/lib, and include files at PREFIX/include, where PREFIX installation prefix is inferred by the mk_make.py script. It is usually /usr for most Linux distros, and /usr/local for FreeBSD and macOS. Use the --prefix= command line option to change the install prefix. For example:

python scripts/mk_make.py --prefix=/home/leo
cd build
make
make install

To uninstall Z3, use

sudo make uninstall

To clean Z3 you can delete the build directory and run the mk_make.py script again.

Building Z3 using CMake

Z3 has a build system using CMake. Read the README-CMake.md file for details. It is recommended for most build tasks, except for building OCaml bindings.

Building Z3 using vcpkg

vcpkg is a full platform package manager, you can easily install libzmq with vcpkg.

Execute:

git clone https://github.com/microsoft/vcpkg.git
./bootstrap-vcpkg.bat # For powershell
./bootstrap-vcpkg.sh # For bash
./vcpkg install z3

Dependencies

Z3 itself has few dependencies. It uses C++ runtime libraries, including pthreads for multi-threading. It is optionally possible to use GMP for multi-precision integers, but Z3 contains its own self-contained multi-precision functionality. Python is required to build Z3. To build Java, .Net, OCaml, Julia APIs requires installing relevant tool chains.

Z3 bindings

Z3 has bindings for various programming languages.

`.NET`

You can install a nuget package for the latest release Z3 from nuget.org.

Use the --dotnet command line flag with mk_make.py to enable building these.

See examples/dotnet for examples.

`C`

These are always enabled.

See examples/c for examples.

`C++`

These are always enabled.

See examples/c++ for examples.

`Java`

Use the --java command line flag with mk_make.py to enable building these.

See examples/java for examples.

`OCaml`

Use the --ml command line flag with mk_make.py to enable building these.

See examples/ml for examples.

`Python`

You can install the Python wrapper for Z3 for the latest release from pypi using the command:

   pip install z3-solver

Use the --python command line flag with mk_make.py to enable building these.

Note that it is required on certain platforms that the Python package directory (site-packages on most distributions and dist-packages on Debian based distributions) live under the install prefix. If you use a non standard prefix you can use the --pypkgdir option to change the Python package directory used for installation. For example:

python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages

If you do need to install to a non standard prefix a better approach is to use a Python virtual environment and install Z3 there. Python packages also work for Python3. Under Windows, recall to build inside the Visual C++ native command build environment. Note that the build/python/z3 directory should be accessible from where python is used with Z3 and it depends on libz3.dll to be in the path.

virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# You will find Z3 and the Python bindings installed in the virtual environment
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...

See examples/python for examples.

`Julia`

The Julia package Z3.jl wraps the C API of Z3. A previous version of it wrapped the C++ API: Information about updating and building the Julia bindings can be found in src/api/julia.

`Web Assembly` / `TypeScript` / `JavaScript`

A WebAssembly build with associated TypeScript typings is published on npm as z3-solver. Information about building these bindings can be found in src/api/js.

Smalltalk (`Pharo` / `Smalltalk/X`)

Project MachineArithmetic provides Smalltalk interface to Z3's C API. For more information, see MachineArithmetic/README.md

System Overview

System Diagram

Interfaces

Default input format is SMTLIB2
Other native foreign function interfaces:
C++ API
.NET API
Java API
Python API (also available in pydoc format)
Rust
C
OCaml
Julia
Smalltalk (supports Pharo and Smalltalk/X)

Power Tools

The Axiom Profiler currently developed by ETH Zurich

Top Related Projects

verona

3,574

Research programming language for concurrent ownership

cvc5

1,004

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

Convert designs to code with AI

Introducing Visual Copilot: A new AI model to turn Figma designs to high quality code using your components.

Try Visual Copilot

z3

Top Related Projects

verona

cvc5

Quick Overview

Pros

Cons

Code Examples

Getting Started

Competitor Comparisons

verona

Pros of Verona

Cons of Verona

Code Comparison

cvc5

Pros of cvc5

Cons of cvc5

Code Comparison

Convert designs to code with AI

README

Z3

Build status

Building Z3 on Windows using Visual Studio Command Prompt

Building Z3 using make and GCC/Clang

Building Z3 using CMake

Building Z3 using vcpkg

Dependencies

Z3 bindings

.NET

C

C++

Java

OCaml

Python

Julia

Web Assembly / TypeScript / JavaScript

Smalltalk (Pharo / Smalltalk/X)

System Overview

Interfaces

Power Tools

Top Related Projects

verona

cvc5

Convert designs to code with AI

`.NET`

`C`

`C++`

`Java`

`OCaml`

`Python`

`Julia`

`Web Assembly` / `TypeScript` / `JavaScript`

Smalltalk (`Pharo` / `Smalltalk/X`)