Téléchargement z3 - Téléchargement du code source z3

z3

Autre code source

z3-4.13.3

Télécharger

Z3

Z3 est un prouveur de théorèmes de Microsoft Research. Il est sous licence MIT.

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

Des binaires prédéfinis pour les versions stables et nocturnes sont disponibles ici.

Z3 peut être construit à l'aide de Visual Studio, d'un Makefile ou en utilisant CMake. Il fournit des liaisons pour plusieurs langages de programmation.

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

Image Docker.

Construire Z3 sur Windows à l'aide de l'invite de commande Visual Studio

Versions 32 bits, commencez par :

python scripts/mk_make.py

ou à la place, pour une version 64 bits :

python scripts/mk_make.py -x

alors:

 cd build
nmake

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

Construire Z3 en utilisant make et GCC/Clang

Exécuter:

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 mk_make.py par :

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

Notez que Clang < 3.7 ne prend pas en charge OpenMP.

Vous pouvez également créer Z3 pour Windows à l'aide de Cygwin et du compilateur croisé Mingw-w64. Pour configurer ce cas correctement, assurez-vous d'utiliser le propre python de Cygwin et non une installation Windows de Python.

Pour une version 64 bits (à partir de 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 la même manière (mais n'a pas été testée) ; il en va de même pour les builds 32/64 bits à partir de Cygwin32.

Par défaut, il installera l'exécutable z3 sur PREFIX/bin , les bibliothèques sur PREFIX/lib et inclura les fichiers sur PREFIX/include , où le préfixe d'installation PREFIX est déduit par le script mk_make.py . Il s'agit généralement /usr pour la plupart des distributions Linux et /usr/local pour FreeBSD et macOS. Utilisez l'option de ligne de commande --prefix= pour modifier 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 réexécuter le script mk_make.py .

Construire Z3 à l'aide de CMake

Z3 dispose d'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 build, à l'exception de la création de liaisons OCaml.

Construire Z3 en utilisant vcpkg

vcpkg est un gestionnaire de packages de plateforme complète, vous pouvez facilement installer libzmq avec vcpkg.

Exécuter:

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

Dépendances

Z3 lui-même a peu de dépendances. Il utilise les bibliothèques d'exécution C++, notamment pthreads pour le multithreading. Il est éventuellement possible d'utiliser GMP pour les entiers multi-précision, mais le Z3 contient sa propre fonctionnalité multi-précision autonome. Python est requis pour construire Z3. Pour créer des API Java, .Net, OCaml, Julia nécessite l'installation de chaînes d'outils pertinentes.

Fixations Z3

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

`.NET`

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

Utilisez l'indicateur de ligne de commande --dotnet avec mk_make.py pour permettre leur construction.

Voir examples/dotnet pour des exemples.

`C`

Ceux-ci sont toujours activés.

Voir examples/c pour des exemples.

`C++`

Ceux-ci sont toujours activés.

Voir examples/c++ pour des exemples.

`Java`

Utilisez l'indicateur de ligne de commande --java avec mk_make.py pour permettre leur construction.

Voir examples/java pour des exemples.

`OCaml`

Utilisez l'indicateur de ligne de commande --ml avec mk_make.py pour permettre leur construction.

Voir examples/ml pour des exemples.

`Python`

Vous pouvez installer le wrapper Python pour Z3 pour la dernière version de pypi à l'aide de la commande :

   pip install z3-solver

Utilisez l'indicateur de ligne de commande --python avec mk_make.py pour permettre 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) réside sous le préfixe d'installation. Si vous utilisez un préfixe non standard, vous pouvez utiliser l'option --pypkgdir pour modifier le répertoire du package 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 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, n'oubliez pas de créer dans l'environnement de génération de commandes natif Visual C++. Notez que le répertoire build/python/z3 doit être accessible à partir de l'endroit où python est utilisé avec Z3 et cela dépend de la présence libz3.dll dans le chemin.

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

Voir examples/python pour des exemples.

`Julia`

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

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

Une version WebAssembly avec les typages TypeScript associés est publiée sur npm en tant que z3-solver. Des informations sur la création de ces liaisons peuvent être trouvées dans src/api/js.