Z3

Z3 é um provador de teoremas da Microsoft Research. Está licenciado sob a licença MIT. Distribuições binárias para Windows incluem redistribuíveis de tempo de execução C++

Se você não está familiarizado com o Z3, pode começar aqui.

Binários pré-construídos para versões estáveis e noturnas estão disponíveis aqui.

O Z3 pode ser construído usando Visual Studio, um Makefile, CMake, vcpkg ou Bazel. Ele fornece bindings para várias linguagens de programação.

Consulte as notas de lançamento para obter notas sobre várias versões estáveis do Z3.

Status da compilação

Fluxos de trabalho de Pull Request & Push

WASM Build	Windows Build	CI	OCaml Binding

Fluxos de trabalho agendados

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

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

Fluxos de trabalho manuais e de lançamento

Documentation	Release Build	WASM Release	NuGet Build

Fluxos de trabalho especializados

Nightly Validation	Copilot Setup	Agentics Maintenance

Fluxos de trabalho agênticos

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

Construindo Z3 no Windows usando o Prompt de Comando do Visual Studio

Para compilações de 32 bits, comece com:

python scripts/mk_make.py

ou, em vez disso, para uma compilação de 64 bits:

python scripts/mk_make.py -x

depois execute:

cd build
nmake

Z3 usa C++20. A versão recomendada do Visual Studio é, portanto, VS2019 ou posterior.

Recursos de segurança (MSVC): Ao construir com Visual Studio/MSVC, alguns recursos de segurança são habilitados por padrão para Z3:

• Control Flow Guard (/guard:cf) - habilitado por padrão para detectar tentativas de comprometer seu código, impedindo chamadas para locais diferentes dos pontos de entrada de funções, tornando mais difícil para invasores executarem código arbitrário por meio de redirecionamento de fluxo de controle
• Address Space Layout Randomization (/DYNAMICBASE) - habilitado por padrão para randomização de layout de memória, exigido pela opção de vinculador /GUARD:CF
• Esses podem ser desabilitados usando python scripts/mk_make.py --no-guardcf (compilação Python) ou cmake -DZ3_ENABLE_CFG=OFF (compilação CMake) se necessário

Construindo Z3 usando make e GCC/Clang

Execute:

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

Observe que, por padrão, g++ é usado como compilador C++ se estiver disponível. Se você preferir usar Clang, altere a invocação de mk_make.py para:

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

Observe que o Clang < 3.7 não suporta OpenMP.

Você também pode construir Z3 para Windows usando Cygwin e o compilador cruzado Mingw-w64. Nesse caso, certifique-se de usar o Python do próprio Cygwin e não alguma instalação do Windows do Python.

Para uma compilação de 64 bits (a partir do Cygwin64), configure as fontes do Z3 com

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

Uma compilação de 32 bits deve funcionar de forma semelhante (mas não testada); o mesmo vale para compilações de 32/64 bits a partir do Cygwin32.

Por padrão, ele instalará executáveis do Z3 em PREFIX/bin, bibliotecas em PREFIX/lib e arquivos de inclusão em PREFIX/include, onde o prefixo de instalação PREFIX é inferido pelo script mk_make.py. Geralmente é /usr para a maioria das distribuições Linux e /usr/local para FreeBSD e macOS. Use a opção de linha de comando --prefix= para alterar o prefixo de instalação. Por exemplo:

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

Para desinstalar o Z3, use

sudo make uninstall

Para limpar o Z3, você pode excluir o diretório de compilação e executar o script mk_make.py novamente.

Construindo Z3 usando CMake

Z3 tem um sistema de compilação usando CMake. Leia o arquivo README-CMake.md para obter detalhes. É recomendado para a maioria das tarefas de compilação, exceto para construir os bindings OCaml.

Construindo Z3 usando vcpkg

vcpkg é um gerenciador de pacotes de plataforma completo. Para instalar o Z3 com vcpkg, execute:

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

Construindo Z3 usando Bazel

Z3 pode ser construído usando Bazel. Isso é conhecido por funcionar em Ubuntu com Clang (mas pode funcionar em outros lugares com outros compiladores):

bazel build //...

Dependências

O próprio Z3 tem poucas dependências. Ele usa bibliotecas de tempo de execução C++, incluindo pthreads para multithreading. Opcionalmente, é possível usar GMP para inteiros de precisão múltipla, mas Z3 contém sua própria funcionalidade de precisão múltipla independente. Python é necessário para construir Z3. Construir APIs Java, .NET, OCaml e Julia requer instalar os conjuntos de ferramentas relevantes.

Bindings Z3

Z3 tem bindings para várias linguagens de programação.

.NET

Você pode instalar um pacote NuGet para a versão mais recente do Z3 em nuget.org.

Use o sinalizador de linha de comando --dotnet com mk_make.py para ativar a compilação desses.

Veja examples/dotnet para exemplos.

C

Estes estão sempre ativados.

Veja examples/c para exemplos.

C++

Estes estão sempre ativados.

Veja examples/c++ para exemplos.

Java

Use o sinalizador de linha de comando --java com mk_make.py para ativar a compilação desses.

Para instruções de configuração de IDE (Eclipse, IntelliJ IDEA, Visual Studio Code) e solução de problemas, consulte o Guia de Configuração de IDE Java.

Veja examples/java para exemplos.

Go

Use o sinalizador de linha de comando --go com mk_make.py para ativar a compilação desses. Observe que os bindings Go usam CGO e exigem um conjunto de ferramentas Go (Go 1.20 ou posterior) para compilar.

Com CMake, use a opção -DZ3_BUILD_GO_BINDINGS=ON.

Veja examples/go para exemplos e src/api/go/README.md para documentação completa da API.

OCaml

Use o sinalizador de linha de comando --ml com mk_make.py para ativar a compilação desses.

Veja examples/ml para exemplos.

Python

Você pode instalar o wrapper Python para Z3 para a versão mais recente do pypi usando o comando:

   pip install z3-solver

Use o sinalizador de linha de comando --python com mk_make.py para ativar a compilação desses.

Observe que é necessário em certas plataformas que o diretório de pacotes Python (site-packages na maioria das distribuições e dist-packages em distribuições baseadas em Debian) esteja sob o prefixo de instalação. Se você usar um prefixo não padrão, pode usar a opção --pypkgdir para alterar o diretório de pacotes Python usado para instalação. Por exemplo:

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

Se você precisar instalar em um prefixo não padrão, uma abordagem melhor é usar um ambiente virtual Python e instalar Z3 lá. Pacotes Python também funcionam para Python3. No Windows, lembre-se de construir dentro do ambiente de compilação de comando nativo do Visual C++. Observe que o diretório build/python/z3 deve estar acessível a partir de onde o Python é usado com Z3 e requer que libz3.dll esteja no caminho.

virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# Você encontrará o Z3 e os bindings Python instalados no ambiente virtual
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...

Veja examples/python para exemplos.

Julia

O pacote Julia Z3.jl envolve a API C do Z3. Uma versão anterior dele envolvia a API C++: informações sobre como atualizar e construir os bindings Julia podem ser encontradas em src/api/julia.

WebAssembly / TypeScript / JavaScript

Uma compilação WebAssembly com tipagens TypeScript associadas é publicada no npm como z3-solver. Informações sobre como construir esses bindings podem ser encontradas em src/api/js.

Smalltalk (Pharo / Smalltalk/X)

O projeto MachineArithmetic fornece uma interface Smalltalk para a API C do Z3. Para mais informações, veja MachineArithmetic/README.md.

AIX

Configurações de compilação para AIX estão descritas aqui.

Visão geral do sistema

Interfaces

• O formato de entrada padrão é SMTLIB2

• Outras interfaces de funções nativas estrangeiras:

• API C++

• API .NET

• API Java

• API Python (também disponível no formato pydoc)

• Rust

• C

• OCaml

• Julia

• Smalltalk (suporta Pharo e Smalltalk/X)

Ferramentas Poderosas

• O Axiom Profiler atualmente desenvolvido pela ETH Zurique