ดาวน์โหลด z3 - ดาวน์โหลดซอร์สโค้ด z3

z3

ซอร์สโค้ดอื่น ๆ

z3-4.13.3

ดาวน์โหลด

Z3

Z3 เป็นผู้พิสูจน์ทฤษฎีบทจาก Microsoft Research ได้รับอนุญาตภายใต้ใบอนุญาต MIT

หากคุณไม่คุ้นเคยกับ Z3 คุณสามารถเริ่มต้นได้ที่นี่

ไบนารีที่สร้างไว้ล่วงหน้าสำหรับการเผยแพร่ที่เสถียรและทุกคืนมีให้จากที่นี่

สามารถสร้าง Z3 ได้โดยใช้ Visual Studio, Makefile หรือใช้ CMake มันมีการเชื่อมโยงสำหรับภาษาการเขียนโปรแกรมหลายภาษา

ดูบันทึกประจำรุ่นสำหรับหมายเหตุเกี่ยวกับ Z3 รุ่นต่างๆ ที่เสถียร

ภาพนักเทียบท่า

การสร้าง Z3 บน Windows โดยใช้ Visual Studio Command Prompt

รุ่น 32 บิต เริ่มต้นด้วย:

python scripts/mk_make.py

หรือสำหรับรุ่น 64 บิตแทน:

python scripts/mk_make.py -x

แล้ว:

 cd build
nmake

Z3 ใช้ C++20 Visual Studio เวอร์ชันที่แนะนำคือ VS2019

การสร้าง Z3 โดยใช้ make และ GCC/Clang

ดำเนินการ:

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.py

โปรดทราบว่า Clang < 3.7 ไม่รองรับ OpenMP

คุณยังสามารถสร้าง Z3 สำหรับ Windows โดยใช้ Cygwin และ cross-compiler Mingw-w64 หากต้องการกำหนดค่าเคสนั้นอย่างถูกต้อง ตรวจสอบให้แน่ใจว่าใช้ Python ของ Cygwin เอง ไม่ใช่การติดตั้ง Python บน Windows

สำหรับบิลด์ 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.py

รุ่น 32 บิตควรทำงานในลักษณะเดียวกัน (แต่ยังไม่ผ่านการทดสอบ) เช่นเดียวกับการสร้าง 32/64 บิตจากภายใน Cygwin32

โดยค่าเริ่มต้น มันจะติดตั้งไฟล์ปฏิบัติการ z3 ที่ PREFIX/bin ไลบรารีที่ PREFIX/lib และรวมไฟล์ที่ PREFIX/include โดยที่คำนำหน้าการติดตั้ง PREFIX ถูกอนุมานโดยสคริปต์ mk_make.py โดยปกติจะเป็น /usr สำหรับ Linux distros ส่วนใหญ่ และ /usr/local สำหรับ FreeBSD และ macOS ใช้ตัวเลือกบรรทัดคำสั่ง --prefix= เพื่อเปลี่ยนคำนำหน้าการติดตั้ง ตัวอย่างเช่น:

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

หากต้องการถอนการติดตั้ง Z3 ให้ใช้

sudo make uninstall

หากต้องการล้าง Z3 คุณสามารถลบไดเร็กทอรี build และรันสคริปต์ mk_make.py อีกครั้ง

การสร้าง Z3 โดยใช้ CMake

Z3 มีระบบบิลด์โดยใช้ CMake อ่านรายละเอียดในไฟล์ README-CMake.md ขอแนะนำสำหรับงานสร้างส่วนใหญ่ ยกเว้นการสร้างการเชื่อมโยง OCaml

การสร้าง Z3 โดยใช้ vcpkg

vcpkg เป็นตัวจัดการแพ็คเกจแพลตฟอร์มเต็มรูปแบบ คุณสามารถติดตั้ง libzmq ด้วย vcpkg ได้อย่างง่ายดาย

ดำเนินการ:

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

การพึ่งพาอาศัยกัน

Z3 นั้นมีการพึ่งพาน้อย ใช้ไลบรารีรันไทม์ C++ รวมถึง pthreads สำหรับมัลติเธรด คุณสามารถเลือกใช้ GMP สำหรับจำนวนเต็มที่มีความแม่นยำหลายระดับได้ แต่ Z3 มีฟังก์ชันการทำงานที่มีความแม่นยำหลายระดับในตัวเอง ต้องใช้ Python เพื่อสร้าง Z3 หากต้องการสร้าง Java, .Net, OCaml, Julia API จำเป็นต้องติดตั้งกลุ่มเครื่องมือที่เกี่ยวข้อง

การผูก Z3

Z3 มีการเชื่อมโยงสำหรับภาษาการเขียนโปรแกรมต่างๆ

`.NET`

คุณสามารถติดตั้งแพ็คเกจ nuget สำหรับ Z3 รุ่นล่าสุดได้จาก nuget.org

ใช้แฟล็กบรรทัดคำสั่ง --dotnet กับ mk_make.py เพื่อเปิดใช้งานการสร้างสิ่งเหล่านี้

ดู examples/dotnet สำหรับตัวอย่าง

`C`

สิ่งเหล่านี้จะเปิดใช้งานอยู่เสมอ

ดู examples/c สำหรับตัวอย่าง

`C++`

สิ่งเหล่านี้จะเปิดใช้งานอยู่เสมอ

ดู examples/c++ สำหรับตัวอย่าง

`Java`

ใช้แฟล็กบรรทัดคำสั่ง --java กับ mk_make.py เพื่อเปิดใช้งานการสร้างสิ่งเหล่านี้

ดู examples/java สำหรับตัวอย่าง

`OCaml`

ใช้แฟล็กบรรทัดคำสั่ง --ml กับ mk_make.py เพื่อเปิดใช้งานการสร้างสิ่งเหล่านี้

ดู examples/ml . สำหรับตัวอย่าง

`Python`

คุณสามารถติดตั้ง Python wrapper สำหรับ Z3 สำหรับรุ่นล่าสุดจาก pypi โดยใช้คำสั่ง:

   pip install z3-solver

ใช้แฟล็กบรรทัดคำสั่ง --python กับ mk_make.py เพื่อเปิดใช้งานการสร้างสิ่งเหล่านี้

โปรดทราบว่าจำเป็นต้องมีในบางแพลตฟอร์มที่ไดเร็กทอรีแพ็คเกจ Python ( site-packages สำหรับการแจกแจงส่วนใหญ่และ dist-packages สำหรับการแจกแจงแบบ Debian) อยู่ภายใต้คำนำหน้าการติดตั้ง หากคุณใช้คำนำหน้าที่ไม่ใช่มาตรฐาน คุณสามารถใช้ตัวเลือก --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 สำหรับตัวอย่าง

`Julia`

แพ็คเกจ Julia Z3.jl ล้อม C API ของ Z3 เวอร์ชันก่อนหน้านี้รวม C++ API: ข้อมูลเกี่ยวกับการอัปเดตและการสร้างการเชื่อมโยง Julia สามารถพบได้ใน src/api/julia

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

โครงสร้าง WebAssembly ที่มีการพิมพ์ TypeScript ที่เกี่ยวข้องถูกเผยแพร่บน npm เป็น z3-solver ข้อมูลเกี่ยวกับการสร้างการเชื่อมโยงเหล่านี้มีอยู่ใน src/api/js