Download z3 - download do código-fonte z3

z3

Outro código-fonte

z3-4.13.3

Baixar

Z3

Z3 é um provador de teoremas da Microsoft Research. É licenciado sob a licença do MIT.

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.

Z3 pode ser construído usando Visual Studio, Makefile ou CMake. Ele fornece ligações para diversas linguagens de programação.

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

Imagem do Docker.

Construindo Z3 no Windows usando o prompt de comando do Visual Studio

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

então:

 cd build
nmake

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

Construindo Z3 usando make e GCC/Clang

Executar:

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 o Clang, altere a invocação mk_make.py para:

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

Observe que Clang <3.7 não oferece suporte a OpenMP.

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

Para uma compilação de 64 bits (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 foi testada); o mesmo se aplica a compilações de 32/64 bits no Cygwin32.

Por padrão, ele instalará o executável z3 em PREFIX/bin , bibliotecas em PREFIX/lib e incluirá arquivos 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 construção e executar o script mk_make.py novamente.

Construindo Z3 usando CMake

Z3 possui um sistema de compilação usando CMake. Leia o arquivo README-CMake.md para obter detalhes. É recomendado para a maioria das tarefas de construção, exceto para construção de ligações OCaml.

Construindo Z3 usando vcpkg

vcpkg é um gerenciador de pacotes de plataforma completo, você pode instalar facilmente o libzmq com vcpkg.

Executar:

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

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 números inteiros de multiprecisão, mas Z3 contém sua própria funcionalidade de multiprecisão independente. Python é necessário para construir o Z3. Para construir APIs Java, .Net, OCaml, Julia requer a instalação de cadeias de ferramentas relevantes.

Ligações Z3

Z3 possui ligações 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 permitir a construção deles.

Veja examples/dotnet para exemplos.

`C`

Eles estão sempre habilitados.

Veja examples/c para exemplos.

`C++`

Eles estão sempre habilitados.

Veja examples/c++ para exemplos.

`Java`

Use o sinalizador de linha de comando --java com mk_make.py para permitir a construção deles.

Veja examples/java para exemplos.

`OCaml`

Use o sinalizador de linha de comando --ml com mk_make.py para permitir a construção deles.

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 permitir a construção deles.

Observe que é necessário em certas plataformas que o diretório do pacote Python ( site-packages na maioria das distribuições e dist-packages nas distribuições baseadas em Debian) resida sob o prefixo install. Se você usar um prefixo não padrão, poderá usar a opção --pypkgdir para alterar o diretório do pacote 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 o Z3 lá. Os pacotes Python também funcionam para Python3. No Windows, lembre-se de compilar dentro do ambiente de compilação de comandos nativos do Visual C++. Observe que o diretório build/python/z3 deve estar acessível de onde python é usado com Z3 e depende de libz3.dll estar no caminho.

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

Veja examples/python para exemplos.

`Julia`

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

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

Uma construção WebAssembly com tipificações TypeScript associadas é publicada no npm como z3-solver. Informações sobre como construir essas ligações podem ser encontradas em src/api/js.