Z3

Z3 ist ein Theorembeweiser von Microsoft Research. Es ist unter der MIT-Lizenz lizenziert. Windows-Binärverteilungen enthalten C++-Laufzeit-Redistributables

Wenn Sie mit Z3 nicht vertraut sind, können Sie hier beginnen.

Vorgefertigte Binärdateien für stabile und nächtliche Versionen sind hier verfügbar.

Z3 kann mit Visual Studio, einem Makefile, mit CMake, mit vcpkg oder mit Bazel erstellt werden. Es bietet Bindings für mehrere Programmiersprachen.

Siehe die Versionshinweise für Hinweise zu verschiedenen stabilen Versionen von Z3.

Build-Status

Pull Request & Push Workflows

WASM-Build	Windows-Build	CI	OCaml-Binding

Geplante Workflows

Offene Fehler	Android-Build	Pyodide Wheel (PyPI)	Nächtlicher Build	Cross-Build

MSVC Static	MSVC Clang-CL	Build Z3 Cache	Speichersicherheit	PRs als bereit markieren

Manuelle & Release-Workflows

Dokumentation	Release-Build	WASM-Release	NuGet-Build

Spezialisierte Workflows

Nächtliche Validierung	Copilot-Einrichtung	Agentik-Wartung

Agentische Workflows

API-Kohärenz	Code-Vereinfacher	Versionshinweise	Workflow-Vorschlag	Akademische Zitation

Issue Backlog	Speichersicherheitsbericht	QF-S-Benchmark	Specbot-Crash-Analyzer	SMTLIB-Benchmark-Finder

TPTP-Benchmark

Erstellen von Z3 unter Windows mit der Visual Studio-Eingabeaufforderung

Für 32-Bit-Builds beginnen Sie mit:

python scripts/mk_make.py

oder stattdessen für einen 64-Bit-Build:

python scripts/mk_make.py -x

führen Sie dann aus:

cd build
nmake

Z3 verwendet C++20. Die empfohlene Version von Visual Studio ist daher VS2019 oder neuer.

Sicherheitsfunktionen (MSVC): Beim Erstellen mit Visual Studio/MSVC sind standardmäßig einige Sicherheitsfunktionen für Z3 aktiviert:

• Control Flow Guard (/guard:cf) – standardmäßig aktiviert, um Versuche zu erkennen, Ihren Code zu kompromittieren, indem Aufrufe an andere Stellen als Funktions-Einstiegspunkte verhindert werden, was es Angreifern erschwert, durch Umleitung des Kontrollflusses beliebigen Code auszuführen.
• Address Space Layout Randomization (/DYNAMICBASE) – standardmäßig aktiviert für die Randomisierung des Speicherlayouts, erforderlich durch die /GUARD:CF-Linkeroption.
• Diese können bei Bedarf mit python scripts/mk_make.py --no-guardcf (Python-Build) oder cmake -DZ3_ENABLE_CFG=OFF (CMake-Build) deaktiviert werden.

Erstellen von Z3 mit make und GCC/Clang

Führen Sie aus:

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

Beachten Sie, dass standardmäßig g++ als C++-Compiler verwendet wird, falls verfügbar. Wenn Sie Clang bevorzugen, ändern Sie den Aufruf von mk_make.py in:

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

Beachten Sie, dass Clang < 3.7 OpenMP nicht unterstützt.

Sie können Z3 auch für Windows mit Cygwin und dem Mingw-w64-Cross-Compiler erstellen. Stellen Sie in diesem Fall sicher, dass Sie Cygwins eigenes Python und keine Windows-Installation von Python verwenden.

Für einen 64-Bit-Build (von Cygwin64) konfigurieren Sie die Z3-Quellen mit

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

Ein 32-Bit-Build sollte ähnlich funktionieren (ist aber ungetestet); dasselbe gilt für 32/64-Bit-Builds innerhalb von Cygwin32.

Standardmäßig installiert es Z3-Executables in PREFIX/bin, Bibliotheken in PREFIX/lib und Include-Dateien in PREFIX/include, wobei das PREFIX-Installationspräfix vom Skript mk_make.py abgeleitet wird. Es ist normalerweise /usr für die meisten Linux-Distributionen und /usr/local für FreeBSD und macOS. Verwenden Sie die Befehlszeilenoption --prefix=, um das Installationspräfix zu ändern. Zum Beispiel:

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

Um Z3 zu deinstallieren, verwenden Sie

sudo make uninstall

Um Z3 zu bereinigen, können Sie das Build-Verzeichnis löschen und das Skript mk_make.py erneut ausführen.

Erstellen von Z3 mit CMake

Z3 hat ein Build-System mit CMake. Lesen Sie die Datei README-CMake.md für Details. Es wird für die meisten Build-Aufgaben empfohlen, mit Ausnahme des Erstellens von OCaml-Bindungen.

Erstellen von Z3 mit vcpkg

vcpkg ist ein vollständiger Plattform-Paketmanager. Um Z3 mit vcpkg zu installieren, führen Sie aus:

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

Erstellen von Z3 mit Bazel

Z3 kann mit Bazel erstellt werden. Dies funktioniert bekanntermaßen unter Ubuntu mit Clang (kann aber auch anderswo mit anderen Compilern funktionieren):

bazel build //...

Abhängigkeiten

Z3 selbst hat nur wenige Abhängigkeiten. Es verwendet C++-Laufzeitbibliotheken, einschließlich pthreads für Multithreading. Optional kann GMP für mehrfache Genauigkeit bei Ganzzahlen verwendet werden, aber Z3 enthält eine eigene in sich geschlossene Mehrfachgenauigkeitsfunktionalität. Python ist erforderlich, um Z3 zu erstellen. Das Erstellen von Java-, .NET-, OCaml- und Julia-APIs erfordert die Installation relevanter Toolchains.

Z3-Bindungen

Z3 hat Bindungen für verschiedene Programmiersprachen.

.NET

Sie können ein NuGet-Paket für die neueste Z3-Version von nuget.org installieren.

Verwenden Sie das Befehlszeilen-Flag --dotnet mit mk_make.py, um das Erstellen dieser zu aktivieren.

Siehe examples/dotnet für Beispiele.

C

Diese sind immer aktiviert.

Siehe examples/c für Beispiele.

C++

Diese sind immer aktiviert.

Siehe examples/c++ für Beispiele.

Java

Verwenden Sie das Befehlszeilen-Flag --java mit mk_make.py, um das Erstellen dieser zu aktivieren.

Anleitungen zur IDE-Einrichtung (Eclipse, IntelliJ IDEA, Visual Studio Code) und Fehlerbehebung finden Sie im Java IDE Setup Guide.

Siehe examples/java für Beispiele.

Go

Verwenden Sie das Befehlszeilen-Flag --go mit mk_make.py, um das Erstellen dieser zu aktivieren. Beachten Sie, dass Go-Bindungen CGO verwenden und eine Go-Toolchain (Go 1.20 oder neuer) zum Erstellen benötigen.

Verwenden Sie mit CMake die Option -DZ3_BUILD_GO_BINDINGS=ON.

Siehe examples/go für Beispiele und src/api/go/README.md für die vollständige API-Dokumentation.

OCaml

Verwenden Sie das Befehlszeilen-Flag --ml mit mk_make.py, um das Erstellen dieser zu aktivieren.

Siehe examples/ml für Beispiele.

Python

Sie können den Python-Wrapper für Z3 für die neueste Version von pypi mit dem folgenden Befehl installieren:

   pip install z3-solver

Verwenden Sie das Befehlszeilen-Flag --python mit mk_make.py, um das Erstellen dieser zu aktivieren.

Beachten Sie, dass auf bestimmten Plattformen das Python-Paketverzeichnis (site-packages auf den meisten Distributionen und dist-packages auf Debian-basierten Distributionen) unter dem Installationspräfix liegen muss. Wenn Sie ein nicht standardmäßiges Präfix verwenden, können Sie die Option --pypkgdir verwenden, um das für die Installation verwendete Python-Paketverzeichnis zu ändern. Zum Beispiel:

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

Wenn Sie in ein nicht standardmäßiges Präfix installieren müssen, ist ein besserer Ansatz, eine Python virtuelle Umgebung zu verwenden und Z3 dort zu installieren. Python-Pakete funktionieren auch für Python3. Denken Sie unter Windows daran, innerhalb der nativen Visual C++-Befehlsumgebung zu erstellen. Beachten Sie, dass das Verzeichnis build/python/z3 von dem Ort aus zugänglich sein sollte, an dem Python mit Z3 verwendet wird, und dass libz3.dll im Pfad vorhanden sein muss.

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

Siehe examples/python für Beispiele.

Julia

Das Julia-Paket Z3.jl kapselt die C-API von Z3. Eine frühere Version kapselte die C++-API: Informationen zum Aktualisieren und Erstellen der Julia-Bindungen finden Sie in src/api/julia.

WebAssembly / TypeScript / JavaScript

Ein WebAssembly-Build mit zugehörigen TypeScript-Typisierungen wird auf npm als z3-solver veröffentlicht. Informationen zum Erstellen dieser Bindungen finden Sie in src/api/js.

Smalltalk (Pharo / Smalltalk/X)

Das Projekt MachineArithmetic bietet eine Smalltalk-Schnittstelle zur C-API von Z3. Weitere Informationen finden Sie unter MachineArithmetic/README.md.

AIX

Build-Einstellungen für AIX sind hier beschrieben.

Systemübersicht

Schnittstellen

• Standard-Eingabeformat ist SMTLIB2

• Andere native fremde Funktionsschnittstellen:

• C++-API

• .NET-API

• Java-API

• Python-API (auch im pydoc-Format verfügbar)

• Rust

• C

• OCaml

• Julia

• Smalltalk (unterstützt Pharo und Smalltalk/X)

Power-Tools

• Der Axiom Profiler, der derzeit von der ETH Zurich entwickelt wird