z3

Z3

Z3 ist ein Theorembeweis von Microsoft Research. Es ist unter der MIT-Lizenz lizenziert.

Wenn Sie Z3 noch nicht kennen, können Sie hier beginnen.

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

Z3 kann mit Visual Studio, einem Makefile oder mit CMake erstellt werden. Es stellt Bindungen für mehrere Programmiersprachen bereit.

Hinweise zu verschiedenen stabilen Versionen von Z3 finden Sie in den Versionshinweisen.

Docker-Image.

Erstellen von Z3 unter Windows mithilfe der Visual Studio-Eingabeaufforderung

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

Dann:

 cd build
nmake

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

Erstellen von Z3 mit make und GCC/Clang

Ausführen:

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

Hinweis: Standardmäßig wird g++ als C++-Compiler verwendet, sofern verfügbar. Wenn Sie lieber Clang verwenden möchten, ändern Sie den mk_make.py -Aufruf wie folgt:

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

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

Sie können Z3 für Windows auch mit Cygwin und dem Cross-Compiler Mingw-w64 erstellen. Um diesen Fall richtig zu konfigurieren, stellen Sie sicher, dass Sie Cygwins eigenes Python und keine Windows-Installation von Python verwenden.

Konfigurieren Sie für einen 64-Bit-Build (von Cygwin64) die Quellen von Z3 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 jedoch ungetestet); Das Gleiche gilt für 32/64-Bit-Builds aus Cygwin32.

Standardmäßig werden die ausführbaren z3-Dateien unter PREFIX/bin , Bibliotheken unter PREFIX/lib und Include-Dateien unter PREFIX/include installiert, wobei das PREFIX Installationspräfix vom mk_make.py -Skript abgeleitet wird. Normalerweise ist es /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 verfügt über ein Build-System, das CMake verwendet. Weitere Informationen finden Sie in der Datei README-CMake.md. Es wird für die meisten Build-Aufgaben empfohlen, mit Ausnahme der Erstellung von OCaml-Bindungen.

Erstellen von Z3 mit vcpkg

vcpkg ist ein vollständiger Plattform-Paketmanager. Sie können libzmq einfach mit vcpkg installieren.

Ausführen:

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

Abhängigkeiten

Z3 selbst hat wenige Abhängigkeiten. Es verwendet C++-Laufzeitbibliotheken, einschließlich Pthreads für Multithreading. Es ist optional möglich, GMP für Ganzzahlen mit mehreren Genauigkeiten zu verwenden, Z3 enthält jedoch eine eigene, eigenständige Multigenauigkeitsfunktionalität. Zum Erstellen von Z3 ist Python erforderlich. Um Java-, .Net-, OCaml- und Julia-APIs zu erstellen, müssen entsprechende Toolketten installiert werden.

Z3-Bindungen

Z3 verfügt über Bindungen für verschiedene Programmiersprachen.

.NET

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

Verwenden Sie das Befehlszeilenflag --dotnet mit mk_make.py um die Erstellung dieser zu ermöglichen.

examples/dotnet “.

C

Diese sind immer aktiviert.

Beispiele finden Sie unter examples/c .

C++

Diese sind immer aktiviert.

Beispiele finden Sie unter examples/c++ .

Java

Verwenden Sie das Befehlszeilenflag --java mit mk_make.py um die Erstellung dieser zu ermöglichen.

Beispiele finden Sie unter examples/java .

OCaml

Verwenden Sie das Befehlszeilenflag --ml mit mk_make.py um deren Erstellung zu ermöglichen.

Beispiele finden Sie unter examples/ml .

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 Befehlszeilenflag --python mit mk_make.py um die Erstellung dieser zu ermöglichen.

Beachten Sie, dass es auf bestimmten Plattformen erforderlich ist, dass das Python-Paketverzeichnis ( site-packages bei den meisten Distributionen und dist-packages bei Debian-basierten Distributionen) unter dem Installationspräfix läuft. 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 auf ein nicht standardmäßiges Präfix installieren müssen, ist es besser, eine virtuelle Python-Umgebung zu verwenden und Z3 dort zu installieren. Python-Pakete funktionieren auch für Python3. Denken Sie unter Windows daran, innerhalb der nativen Befehlserstellungsumgebung von Visual C++ zu erstellen. Beachten Sie, dass das Verzeichnis build/python/z3 von dort aus zugänglich sein sollte, wo Python mit Z3 verwendet wird, und es davon abhängt, dass sich libz3.dll im Pfad befindet.

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

Beispiele finden Sie unter examples/python .

Julia

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

Web Assembly / 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 )

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

Systemübersicht

Schnittstellen

• Das Standardeingabeformat ist SMTLIB2

• Andere native Fremdfunktionsschnittstellen:

• C++-API

• .NET-API

• Java-API

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

• Rost

• C

• OCaml

• Julia

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

Elektrowerkzeuge

• Der derzeit von der ETH Zürich entwickelte Axiom Profiler