تحميل z3 - تنزيل كود المصدر z3

z3

شفرة المصدر الأخرى

z3-4.13.3

تنزيل

Z3

Z3 هو مثبت نظرية من أبحاث Microsoft. وهو مرخص بموجب ترخيص MIT.

إذا لم تكن على دراية بـ Z3، فيمكنك البدء من هنا.

تتوفر الثنائيات المعدة مسبقًا للإصدارات المستقرة والليلية من هنا.

يمكن إنشاء Z3 باستخدام Visual Studio أو Makefile أو باستخدام CMake. يوفر روابط للعديد من لغات البرمجة.

راجع ملاحظات الإصدار للحصول على ملاحظات حول الإصدارات الثابتة المتنوعة من Z3.

صورة عامل الميناء.

بناء Z3 على نظام التشغيل Windows باستخدام موجه أوامر Visual Studio

إصدارات 32 بت، تبدأ بـ:

python scripts/mk_make.py

أو بدلاً من ذلك، لبناء 64 بت:

python scripts/mk_make.py -x

ثم:

 cd build
nmake

يستخدم Z3 C++ 20. وبالتالي فإن الإصدار الموصى به من Visual Studio هو VS2019.

بناء Z3 باستخدام make وGC/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 والمترجم المتقاطع Mingw-w64. لتكوين هذه الحالة بشكل صحيح، تأكد من استخدام python الخاص بـ Cygwin وليس بعض تثبيتات Windows لـ 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.py

يجب أن يعمل الإصدار 32 بت بشكل مشابه (لكن لم يتم اختباره)؛ وينطبق الشيء نفسه على إصدارات 32/64 بت من داخل Cygwin32.

افتراضيًا، سيتم تثبيت z3 القابل للتنفيذ في PREFIX/bin ، والمكتبات في PREFIX/lib ، ويتضمن الملفات في PREFIX/include ، حيث يتم استنتاج بادئة تثبيت PREFIX بواسطة البرنامج النصي mk_make.py . عادةً ما يكون /usr لمعظم توزيعات Linux، و /usr/local لـ FreeBSD وmacOS. استخدم خيار سطر الأوامر --prefix= لتغيير بادئة التثبيت. على سبيل المثال:

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

لإلغاء تثبيت Z3، استخدم

sudo make uninstall

لتنظيف Z3، يمكنك حذف دليل البناء وتشغيل البرنامج النصي 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 يحتوي على وظائف متعددة الدقة قائمة بذاتها. مطلوب بايثون لبناء Z3. لإنشاء Java، و.Net، وOCaml، وJulia APIs، يلزم تثبيت سلاسل الأدوات ذات الصلة.

روابط 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 لـ Z3 لأحدث إصدار من pypi باستخدام الأمر:

   pip install z3-solver

استخدم علامة سطر الأوامر --python مع mk_make.py لتمكين إنشاء هذه العناصر.

لاحظ أنه مطلوب في بعض الأنظمة الأساسية أن يكون دليل حزمة Python ( site-packages في معظم التوزيعات dist-packages على التوزيعات المستندة إلى دبيان) موجودًا تحت بادئة التثبيت. إذا كنت تستخدم بادئة غير قياسية، فيمكنك استخدام خيار --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 لـ Z3. تم تغليف إصدار سابق منه بواجهة برمجة تطبيقات C++: يمكن العثور على معلومات حول تحديث وبناء روابط Julia في src/api/julia.