Z3

Z3 è un dimostratore di teoremi di Microsoft Research. È concesso in licenza sotto la licenza MIT. Le distribuzioni binarie per Windows includono file ridistribuibili del runtime C++

Se non conosci Z3, puoi iniziare qui.

I binari precompilati per le versioni stabili e notturne sono disponibili qui.

Z3 può essere compilato utilizzando Visual Studio, un Makefile, CMake, vcpkg o Bazel. Fornisce binding per diversi linguaggi di programmazione.

Vedi le note di rilascio per le note sulle varie versioni stabili di Z3.

Stato di compilazione

Workflow di Pull Request e Push

WASM Build	Windows Build	CI	OCaml Binding

Workflow Pianificati

Open Bugs	Android Build	Pyodide Wheel (PyPI)	Nightly Build	Cross Build

MSVC Static	MSVC Clang-CL	Build Z3 Cache	Memory Safety	Mark PRs Ready

Workflow Manuali e di Rilascio

Documentation	Release Build	WASM Release	NuGet Build

Workflow Specializzati

Nightly Validation	Copilot Setup	Agentics Maintenance

Workflow Agenti

API Coherence	Code Simplifier	Release Notes	Workflow Suggestion	Academic Citation

Issue Backlog	Memory Safety Report	QF-S Benchmark	Specbot Crash Analyzer	SMTLIB Benchmark Finder

TPTP Benchmark

Compilare Z3 su Windows con il Prompt dei comandi di Visual Studio

Per build a 32 bit, inizia con:

python scripts/mk_make.py

oppure, per una build a 64 bit:

python scripts/mk_make.py -x

poi esegui:

cd build
nmake

Z3 utilizza C++20. La versione raccomandata di Visual Studio è quindi VS2019 o successiva.

Funzionalità di sicurezza (MSVC): Quando si compila con Visual Studio/MSVC, alcune funzionalità di sicurezza sono abilitate di default per Z3:

• Control Flow Guard (/guard:cf) - abilitato di default per rilevare tentativi di compromettere il codice impedendo chiamate a posizioni diverse dai punti di ingresso delle funzioni, rendendo più difficile per gli aggressori eseguire codice arbitrario attraverso il reindirizzamento del flusso di controllo
• Address Space Layout Randomization (/DYNAMICBASE) - abilitato di default per la randomizzazione del layout di memoria, richiesto dall'opzione del linker /GUARD:CF
• Queste possono essere disabilitate usando python scripts/mk_make.py --no-guardcf (build Python) o cmake -DZ3_ENABLE_CFG=OFF (build CMake) se necessario

Compilare Z3 usando make e GCC/Clang

Esegui:

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

Nota che di default viene usato g++ come compilatore C++ se disponibile. Se preferisci usare Clang, cambia l'invocazione di mk_make.py in:

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

Nota che Clang < 3.7 non supporta OpenMP.

Puoi anche compilare Z3 per Windows usando Cygwin e il cross-compilatore Mingw-w64. In tal caso, assicurati di usare il Python di Cygwin e non qualche installazione Windows di Python.

Per una build a 64 bit (da Cygwin64), configura le sorgenti di Z3 con

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

Una build a 32 bit dovrebbe funzionare in modo simile (ma non testata); lo stesso vale per build a 32/64 bit da Cygwin32.

Per impostazione predefinita, installerà gli eseguibili Z3 in PREFIX/bin, le librerie in PREFIX/lib e i file di inclusione in PREFIX/include, dove il prefisso di installazione PREFIX è dedotto dallo script mk_make.py. Di solito è /usr per la maggior parte delle distribuzioni Linux, e /usr/local per FreeBSD e macOS. Usa l'opzione --prefix= per cambiare il prefisso di installazione. Ad esempio:

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

Per disinstallare Z3, usa

sudo make uninstall

Per pulire Z3, puoi eliminare la directory build ed eseguire di nuovo lo script mk_make.py.

Compilare Z3 usando CMake

Z3 ha un sistema di build che utilizza CMake. Leggi il file README-CMake.md per i dettagli. È consigliato per la maggior parte dei compiti di build, tranne che per la compilazione dei binding OCaml.

Compilare Z3 usando vcpkg

vcpkg è un gestore di pacchetti multipiattaforma. Per installare Z3 con vcpkg, esegui:

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

Compilare Z3 usando Bazel

Z3 può essere compilato usando Bazel. È noto per funzionare su Ubuntu con Clang (ma potrebbe funzionare altrove con altri compilatori):

bazel build //...

Dipendenze

Z3 stesso ha solo poche dipendenze. Utilizza librerie runtime C++, inclusi pthreads per il multi-threading. È opzionalmente possibile usare GMP per interi a precisione multipla, ma Z3 contiene la propria funzionalità a precisione multipla auto-contenuta. Python è necessario per compilare Z3. La compilazione delle API Java, .NET, OCaml e Julia richiede l'installazione delle toolchain pertinenti.

Binding di Z3

Z3 dispone di binding per vari linguaggi di programmazione.

.NET

Puoi installare un pacchetto NuGet per l'ultima versione di Z3 da nuget.org.

Usa il flag --dotnet della riga di comando con mk_make.py per abilitarne la compilazione.

Vedi examples/dotnet per esempi.

C

Questi sono sempre abilitati.

Vedi examples/c per esempi.

C++

Questi sono sempre abilitati.

Vedi examples/c++ per esempi.

Java

Usa il flag --java della riga di comando con mk_make.py per abilitarne la compilazione.

Per istruzioni di configurazione dell'IDE (Eclipse, IntelliJ IDEA, Visual Studio Code) e risoluzione dei problemi, vedi la Guida di configurazione IDE Java.

Vedi examples/java per esempi.

Go

Usa il flag --go della riga di comando con mk_make.py per abilitarne la compilazione. Nota che i binding Go usano CGO e richiedono una toolchain Go (Go 1.20 o successiva) per la compilazione.

Con CMake, usa l'opzione -DZ3_BUILD_GO_BINDINGS=ON.

Vedi examples/go per esempi e src/api/go/README.md per la documentazione API completa.

OCaml

Usa il flag --ml della riga di comando con mk_make.py per abilitarne la compilazione.

Vedi examples/ml per esempi.

Python

Puoi installare il wrapper Python per Z3 per l'ultima release da pypi usando il comando:

   pip install z3-solver

Usa il flag --python della riga di comando con mk_make.py per abilitarne la compilazione.

Nota che è richiesto su alcune piattaforme che la directory dei pacchetti Python (site-packages sulla maggior parte delle distribuzioni e dist-packages sulle distribuzioni basate su Debian) si trovi sotto il prefisso di installazione. Se usi un prefisso non standard puoi usare l'opzione --pypkgdir per cambiare la directory dei pacchetti Python usata per l'installazione. Ad esempio:

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

Se devi installare in un prefisso non standard, un approccio migliore è usare un ambiente virtuale Python e installare Z3 lì. I pacchetti Python funzionano anche per Python3. Su Windows, ricordati di compilare all'interno dell'ambiente di compilazione nativo di Visual C++. Nota che la directory build/python/z3 deve essere accessibile da dove Python viene usato con Z3 e richiede che libz3.dll sia nel percorso.

virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# Troverai Z3 e i binding Python installati nell'ambiente virtuale
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...

Vedi examples/python per esempi.

Julia

Il pacchetto Julia Z3.jl racchiude l'API C di Z3. Una versione precedente racchiudeva l'API C++: le informazioni sull'aggiornamento e la compilazione dei binding Julia possono essere trovate in src/api/julia.

WebAssembly / TypeScript / JavaScript

Una build WebAssembly con tipizzazioni TypeScript associate è pubblicata su npm come z3-solver. Le informazioni sulla compilazione di questi binding possono essere trovate in src/api/js.

Smalltalk (Pharo / Smalltalk/X)

Il progetto MachineArithmetic fornisce un'interfaccia Smalltalk all'API C di Z3. Per maggiori informazioni, vedi MachineArithmetic/README.md.

AIX

Le impostazioni di build per AIX sono descritte qui.

Panoramica del sistema

Interfacce

• Il formato di input predefinito è SMTLIB2

• Altre interfacce native per funzioni esterne:

• API C++

• API .NET

• API Java

• API Python (disponibile anche in formato pydoc)

• Rust

• C

• OCaml

• Julia

• Smalltalk (supporta Pharo e Smalltalk/X)

Strumenti Avanzati

• Axiom Profiler attualmente sviluppato dall'ETH Zurich