z3 Unduh - z3 Unduh kode sumber

z3

Kode sumber lainnya

z3-4.13.3

Unduh

Z3

Z3 adalah pembukti teorema dari Microsoft Research. Ini dilisensikan di bawah lisensi MIT.

Jika Anda belum familiar dengan Z3, Anda bisa mulai dari sini.

Biner yang dibuat sebelumnya untuk rilis stabil dan malam hari tersedia dari sini.

Z3 dapat dibangun menggunakan Visual Studio, Makefile atau menggunakan CMake. Ini menyediakan binding untuk beberapa bahasa pemrograman.

Lihat catatan rilis untuk catatan tentang berbagai rilis stabil Z3.

gambar buruh pelabuhan.

Membangun Z3 di Windows menggunakan Visual Studio Command Prompt

Versi 32-bit, mulailah dengan:

python scripts/mk_make.py

atau sebaliknya, untuk versi 64-bit:

python scripts/mk_make.py -x

Kemudian:

 cd build
nmake

Z3 menggunakan C++20. Oleh karena itu, versi Visual Studio yang direkomendasikan adalah VS2019.

Membangun Z3 menggunakan make dan GCC/Clang

Menjalankan:

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

Catatan secara default g++ digunakan sebagai kompiler C++ jika tersedia. Jika Anda lebih suka menggunakan Dentang, ubah pemanggilan mk_make.py menjadi:

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

Perhatikan bahwa Dentang <3.7 tidak mendukung OpenMP.

Anda juga dapat membuat Z3 untuk Windows menggunakan Cygwin dan kompiler silang Mingw-w64. Untuk mengonfigurasi kasus tersebut dengan benar, pastikan untuk menggunakan python Cygwin sendiri dan bukan instalasi Python Windows.

Untuk versi 64 bit (dari Cygwin64), konfigurasikan sumber Z3 dengan

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

Versi 32 bit seharusnya bekerja dengan cara yang sama (tetapi belum teruji); hal yang sama berlaku untuk versi 32/64 bit dari dalam Cygwin32.

Secara default, ini akan menginstal z3 yang dapat dieksekusi di PREFIX/bin , perpustakaan di PREFIX/lib , dan menyertakan file di PREFIX/include , di mana awalan instalasi PREFIX disimpulkan oleh skrip mk_make.py . Biasanya /usr untuk sebagian besar distro Linux, dan /usr/local untuk FreeBSD dan macOS. Gunakan opsi baris perintah --prefix= untuk mengubah awalan instalasi. Misalnya:

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

Untuk menghapus instalasi Z3, gunakan

sudo make uninstall

Untuk membersihkan Z3 Anda dapat menghapus direktori build dan menjalankan kembali skrip mk_make.py .

Membangun Z3 menggunakan CMake

Z3 memiliki sistem build menggunakan CMake. Baca file README-CMake.md untuk detailnya. Direkomendasikan untuk sebagian besar tugas pembangunan, kecuali untuk membangun pengikatan OCaml.

Membangun Z3 menggunakan vcpkg

vcpkg adalah pengelola paket platform lengkap, Anda dapat dengan mudah menginstal libzmq dengan vcpkg.

Menjalankan:

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

Ketergantungan

Z3 sendiri memiliki sedikit ketergantungan. Ia menggunakan pustaka runtime C++, termasuk pthreads untuk multi-threading. Secara opsional dimungkinkan untuk menggunakan GMP untuk bilangan bulat multi-presisi, tetapi Z3 berisi fungsionalitas multi-presisi mandiri. Python diperlukan untuk membangun Z3. Untuk membangun API Java, .Net, OCaml, Julia memerlukan pemasangan rantai alat yang relevan.

pengikatan Z3

Z3 memiliki binding untuk berbagai bahasa pemrograman.

`.NET`

Anda dapat menginstal paket nuget untuk rilis terbaru Z3 dari nuget.org.

Gunakan tanda baris perintah --dotnet dengan mk_make.py untuk mengaktifkan pembuatannya.

Lihat examples/dotnet untuk contohnya.

`C`

Ini selalu diaktifkan.

Lihat examples/c untuk contohnya.

`C++`

Ini selalu diaktifkan.

Lihat examples/c++ untuk contohnya.

`Java`

Gunakan tanda baris perintah --java dengan mk_make.py untuk mengaktifkan pembuatannya.

Lihat examples/java untuk contohnya.

`OCaml`

Gunakan tanda baris perintah --ml dengan mk_make.py untuk mengaktifkan pembuatannya.

Lihat examples/ml untuk contohnya.

`Python`

Anda dapat menginstal pembungkus Python untuk Z3 untuk rilis terbaru dari pypi menggunakan perintah:

   pip install z3-solver

Gunakan tanda baris perintah --python dengan mk_make.py untuk mengaktifkan pembuatannya.

Perhatikan bahwa pada platform tertentu direktori paket Python ( site-packages pada sebagian besar distribusi dan dist-packages pada distribusi berbasis Debian) harus berada di bawah awalan install. Jika Anda menggunakan awalan non standar, Anda dapat menggunakan opsi --pypkgdir untuk mengubah direktori paket Python yang digunakan untuk instalasi. Misalnya:

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

Jika Anda perlu menginstal ke awalan non standar, pendekatan yang lebih baik adalah menggunakan lingkungan virtual Python dan menginstal Z3 di sana. Paket Python juga berfungsi untuk Python3. Di Windows, ingatlah untuk membangun di dalam lingkungan build perintah asli Visual C++. Perhatikan bahwa direktori build/python/z3 harus dapat diakses dari tempat python digunakan dengan Z3 dan bergantung pada libz3.dll yang berada di jalurnya.

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

Lihat examples/python untuk contohnya.

`Julia`

Paket Julia Z3.jl membungkus C API Z3. Versi sebelumnya membungkus C++ API: Informasi tentang memperbarui dan membangun binding Julia dapat ditemukan di src/api/julia.

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

Build WebAssembly dengan pengetikan TypeScript terkait diterbitkan di npm sebagai z3-solver. Informasi tentang pembuatan binding ini dapat ditemukan di src/api/js.