Z3

Z3 est un prouveur de théorèmes de Microsoft Research. Il est sous licence MIT. Les distributions binaires Windows incluent les redistribuables du runtime C++

Si vous n'êtes pas familier avec Z3, vous pouvez commencer ici.

Des binaires pré-construits pour les versions stables et nightly sont disponibles ici.

Z3 peut être construit en utilisant Visual Studio, un Makefile, CMake, vcpkg, ou Bazel. Il fournit des liaisons pour plusieurs langages de programmation.

Consultez les notes de version pour les notes sur les différentes versions stables de Z3.

Statut de construction

Workflows Pull Request & Push

Workflows planifiés

Workflows manuels & de version

Workflows spécialisés

Validation Nightly	Configuration Copilot	Maintenance Agentics

Workflows agentiques

Référence TPTP

Construction de Z3 sur Windows avec l'invite de commandes Visual Studio

Pour les versions 32 bits, commencez par :

python scripts/mk_make.py

ou, pour une version 64 bits :

python scripts/mk_make.py -x

puis exécutez :

cd build
nmake

Z3 utilise C++20. La version recommandée de Visual Studio est donc VS2019 ou ultérieure.

Fonctionnalités de sécurité (MSVC) : Lors de la construction avec Visual Studio/MSVC, quelques fonctionnalités de sécurité sont activées par défaut pour Z3 :

• Control Flow Guard (/guard:cf) – activée par défaut pour détecter les tentatives de compromission de votre code en empêchant les appels vers des emplacements autres que les points d'entrée des fonctions, rendant plus difficile l'exécution de code arbitraire par les attaquants via une redirection du flux de contrôle.
• Address Space Layout Randomization (/DYNAMICBASE) – activée par défaut pour la randomisation de la disposition de la mémoire, requise par l'option de l'éditeur de liens /GUARD:CF.
• Ces options peuvent être désactivées en utilisant python scripts/mk_make.py --no-guardcf (construction Python) ou cmake -DZ3_ENABLE_CFG=OFF (construction CMake) si nécessaire.

Construction de Z3 avec make et GCC/Clang

Exécutez :

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

Notez que par défaut g++ est utilisé comme compilateur C++ s'il est disponible. Si vous préférez utiliser Clang, modifiez l'invocation de mk_make.py comme suit :

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

Notez que Clang < 3.7 ne supporte pas OpenMP.

Vous pouvez également construire Z3 pour Windows en utilisant Cygwin et le compilateur croisé Mingw-w64. Dans ce cas, assurez-vous d'utiliser le propre Python de Cygwin et non une installation Windows de Python.

Pour une version 64 bits (depuis Cygwin64), configurez les sources de Z3 avec

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

Une version 32 bits devrait fonctionner de manière similaire (mais n'est pas testée) ; il en va de même pour les versions 32/64 bits depuis Cygwin32.

Par défaut, les exécutables z3 seront installés dans PREFIX/bin, les bibliothèques dans PREFIX/lib et les fichiers d'en-tête dans PREFIX/include, où le préfixe d'installation PREFIX est déduit par le script mk_make.py. Il s'agit généralement de /usr pour la plupart des distributions Linux, et /usr/local pour FreeBSD et macOS. Utilisez l'option --prefix= pour changer le préfixe d'installation. Par exemple :

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

Pour désinstaller Z3, utilisez

sudo make uninstall

Pour nettoyer Z3, vous pouvez supprimer le répertoire de construction et relancer le script mk_make.py.

Construction de Z3 avec CMake

Z3 possède un système de construction utilisant CMake. Lisez le fichier README-CMake.md pour plus de détails. Il est recommandé pour la plupart des tâches de construction, sauf pour la construction des liaisons OCaml.

Construction de Z3 avec vcpkg

vcpkg est un gestionnaire de paquets complet multiplateforme. Pour installer Z3 avec vcpkg, exécutez :

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

Construction de Z3 avec Bazel

Z3 peut être construit en utilisant Bazel. Cela fonctionne sur Ubuntu avec Clang (mais peut fonctionner ailleurs avec d'autres compilateurs) :

bazel build //...

Dépendances

Z3 lui-même a peu de dépendances. Il utilise les bibliothèques d'exécution C++, y compris pthreads pour le multi-threading. Il est possible d'utiliser GMP pour les entiers multi-précision, mais Z3 possède sa propre fonctionnalité de multi-précision autonome. Python est nécessaire pour construire Z3. La construction des API Java, .NET, OCaml et Julia nécessite l'installation des chaînes d'outils correspondantes.

Liaisons Z3

Z3 offre des liaisons pour différents langages de programmation.

.NET

Vous pouvez installer un package NuGet pour la dernière version de Z3 depuis nuget.org.

Utilisez l'option --dotnet avec mk_make.py pour activer leur construction.

Consultez examples/dotnet pour des exemples.

C

Cellessont toujours activées.

Consultez examples/c pour des exemples.

C++

Celles-ci sont toujours activées.

Consultez examples/c++ pour des exemples.

Java

Utilisez l'option --java avec mk_make.py pour activer leur construction.

Pour les instructions de configuration IDE (Eclipse, IntelliJ IDEA, Visual Studio Code) et le dépannage, consultez le Guide de configuration IDE Java.

Consultez examples/java pour des exemples.

Go

Utilisez l'option --go avec mk_make.py pour activer leur construction. Notez que les liaisons Go utilisent CGO et nécessitent une chaîne d'outils Go (Go 1.20 ou ultérieur) pour la construction.

Avec CMake, utilisez l'option -DZ3_BUILD_GO_BINDINGS=ON.

Consultez examples/go pour des exemples et src/api/go/README.md pour la documentation complète de l'API.

OCaml

Utilisez l'option --ml avec mk_make.py pour activer leur construction.

Consultez examples/ml pour des exemples.

Python

Vous pouvez installer l'interface Python pour Z3 de la dernière version depuis pypi en utilisant la commande :

   pip install z3-solver

Utilisez l'option --python avec mk_make.py pour activer leur construction.

Notez qu'il est requis sur certaines plates-formes que le répertoire des packages Python (site-packages sur la plupart des distributions et dist-packages sur les distributions basées sur Debian) se trouve sous le préfixe d'installation. Si vous utilisez un préfixe non standard, vous pouvez utiliser l'option --pypkgdir pour changer le répertoire des packages Python utilisé pour l'installation. Par exemple :

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

Si vous devez installer dans un préfixe non standard, une meilleure approche consiste à utiliser un environnement virtuel Python et y installer Z3. Les packages Python fonctionnent également pour Python3. Sous Windows, pensez à construire dans l'environnement de commande natif de Visual C++. Notez que le répertoire build/python/z3 doit être accessible depuis l'endroit où Python est utilisé avec Z3 et nécessite que libz3.dll soit dans le chemin.

virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# Vous trouverez Z3 et les liaisons Python installés dans l'environnement virtuel
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...

Consultez examples/python pour des exemples.

Julia

Le package Julia Z3.jl enveloppe l'API C de Z3. Une version précédente enveloppait l'API C++ : des informations sur la mise à jour et la construction des liaisons Julia peuvent être trouvées dans src/api/julia.

WebAssembly / TypeScript / JavaScript

Une construction WebAssembly avec les typages TypeScript associés est publiée sur npm sous le nom z3-solver. Des informations sur la construction de ces liaisons peuvent être trouvées dans src/api/js.

Smalltalk (Pharo / Smalltalk/X)

Le projet MachineArithmetic fournit une interface Smalltalk à l'API C de Z3. Pour plus d'informations, consultez MachineArithmetic/README.md.

AIX

Les paramètres de construction pour AIX sont décrits ici.

Aperçu du système

Interfaces

• Le format d'entrée par défaut est SMTLIB2

• Autres interfaces de fonctions étrangères natives :

• API C++

• API .NET

• API Java

• API Python (également disponible au format pydoc)

• Rust

• C

• OCaml

• Julia

• Smalltalk (supporte Pharo et Smalltalk/X)

Outils avancés

• Le Axiom Profiler actuellement développé par l'ETH Zurich