z3
z3-4.13.3
Z3은 Microsoft Research의 정리 증명자입니다. MIT 라이선스에 따라 라이선스가 부여됩니다.
Z3에 익숙하지 않다면 여기에서 시작해 보세요.
안정적인 릴리스와 야간 릴리스를 위해 사전 구축된 바이너리를 여기에서 사용할 수 있습니다.
Z3은 Visual Studio, Makefile 또는 CMake를 사용하여 빌드할 수 있습니다. 여러 프로그래밍 언어에 대한 바인딩을 제공합니다.
Z3의 다양한 안정 릴리스에 대한 정보는 릴리스 노트를 참조하세요.
도커 이미지.
32비트 빌드는 다음으로 시작합니다.
python scripts/mk_make.py또는 대신 64비트 빌드의 경우:
python scripts/mk_make.py -x그 다음에:
cd build
nmakeZ3은 C++20을 사용합니다. 따라서 권장되는 Visual Studio 버전은 VS2019입니다.
실행하다:
python scripts/mk_make.py
cd build
make
sudo make install 참고 기본적으로 g++ 사용 가능한 경우 C++ 컴파일러로 사용됩니다. Clang을 사용하려면 mk_make.py 호출을 다음과 같이 변경하세요.
CXX=clang++ CC=clang python scripts/mk_make.pyClang < 3.7은 OpenMP를 지원하지 않습니다.
Cygwin 및 Mingw-w64 크로스 컴파일러를 사용하여 Windows용 Z3을 빌드할 수도 있습니다. 해당 사례를 올바르게 구성하려면 일부 Windows 설치 Python이 아닌 Cygwin 자체 Python을 사용해야 합니다.
64비트 빌드(Cygwin64)의 경우 다음을 사용하여 Z3의 소스를 구성합니다.
CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.py32비트 빌드도 비슷하게 작동해야 합니다(그러나 테스트되지 않았습니다). Cygwin32 내에서 32/64비트 빌드의 경우에도 마찬가지입니다.
기본적으로 z3 실행 파일은 PREFIX/bin 에, 라이브러리는 PREFIX/lib 에, 포함 파일은 PREFIX/include 에 설치됩니다. 여기서 PREFIX 설치 접두사는 mk_make.py 스크립트에 의해 유추됩니다. 일반적으로 대부분의 Linux 배포판에서는 /usr 이고 FreeBSD 및 macOS에서는 /usr/local 입니다. --prefix= 명령줄 옵션을 사용하여 설치 접두사를 변경합니다. 예를 들어:
python scripts/mk_make.py --prefix=/home/leo
cd build
make
make installZ3을 제거하려면 다음을 사용하십시오.
sudo make uninstall Z3을 정리하려면 빌드 디렉터리를 삭제하고 mk_make.py 스크립트를 다시 실행할 수 있습니다.
Z3에는 CMake를 사용하는 빌드 시스템이 있습니다. 자세한 내용은 README-CMake.md 파일을 읽어보세요. OCaml 바인딩 빌드를 제외한 대부분의 빌드 작업에 권장됩니다.
vcpkg는 전체 플랫폼 패키지 관리자이므로 vcpkg를 사용하여 libzmq를 쉽게 설치할 수 있습니다.
실행하다:
git clone https://github.com/microsoft/vcpkg.git
./bootstrap-vcpkg.bat # For powershell
./bootstrap-vcpkg.sh # For bash
./vcpkg install z3Z3 자체에는 종속성이 거의 없습니다. 멀티스레딩을 위한 pthread를 포함한 C++ 런타임 라이브러리를 사용합니다. 다중 정밀도 정수에 GMP를 사용하는 것이 선택적으로 가능하지만 Z3에는 자체 다중 정밀도 기능이 포함되어 있습니다. Z3을 빌드하려면 Python이 필요합니다. Java, .Net, OCaml, Julia API를 구축하려면 관련 도구 체인을 설치해야 합니다.
Z3에는 다양한 프로그래밍 언어에 대한 바인딩이 있습니다.
.NETnuget.org에서 최신 릴리스 Z3용 너겟 패키지를 설치할 수 있습니다.
mk_make.py 와 함께 --dotnet 명령줄 플래그를 사용하여 이를 빌드할 수 있습니다.
예제는 examples/dotnet 참조하세요.
C이는 항상 활성화되어 있습니다.
예제는 examples/c 참조하세요.
C++이는 항상 활성화되어 있습니다.
예제는 examples/c++ 참조하세요.
Java mk_make.py 와 함께 --java 명령줄 플래그를 사용하여 이를 빌드할 수 있습니다.
예제는 examples/java 참조하세요.
OCaml mk_make.py 와 함께 --ml 명령줄 플래그를 사용하여 이를 빌드할 수 있습니다.
예제는 examples/ml 참조하세요.
Python다음 명령을 사용하여 pypi의 최신 릴리스용 Z3용 Python 래퍼를 설치할 수 있습니다.
pip install z3-solver mk_make.py 와 함께 --python 명령줄 플래그를 사용하여 이를 빌드할 수 있습니다.
특정 플랫폼에서는 Python 패키지 디렉터리(대부분의 배포판에서는 site-packages , Debian 기반 배포판에서는 dist-packages )가 install 접두사 아래에 있어야 한다는 점에 유의하세요. 비표준 접두사를 사용하는 경우 --pypkgdir 옵션을 사용하여 설치에 사용되는 Python 패키지 디렉터리를 변경할 수 있습니다. 예를 들어:
python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages 비표준 접두사에 설치해야 하는 경우 더 나은 접근 방식은 Python 가상 환경을 사용하고 거기에 Z3을 설치하는 것입니다. Python 패키지는 Python3에서도 작동합니다. Windows에서는 Visual C++ 기본 명령 빌드 환경 내에서 빌드하는 방법을 기억하세요. build/python/z3 디렉터리는 Python이 Z3와 함께 사용되는 위치에서 액세스할 수 있어야 하며 경로에 있는 libz3.dll 에 따라 달라집니다.
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()) '
... 예제는 examples/python 참조하세요.
JuliaJulia 패키지 Z3.jl은 Z3의 C API를 래핑합니다. 이전 버전은 C++ API를 래핑했습니다. Julia 바인딩 업데이트 및 빌드에 대한 정보는 src/api/julia에서 찾을 수 있습니다.
Web Assembly / TypeScript / JavaScript연결된 TypeScript 입력이 포함된 WebAssembly 빌드는 npm에 z3-solver로 게시됩니다. 이러한 바인딩 구축에 대한 정보는 src/api/js에서 찾을 수 있습니다.
Pharo / Smalltalk/X )Project MachineArithmetic은 Z3의 C API에 Smalltalk 인터페이스를 제공합니다. 자세한 내용은 MachineArithmetic/README.md를 참조하세요.
기본 입력 형식은 SMTLIB2입니다.
기타 기본 외부 함수 인터페이스:
C++ API
.NET API
자바 API
Python API(pydoc 형식으로도 사용 가능)
녹
기음
OCaml
줄리아
스몰토크(Pharo 및 Smalltalk/X 지원)
