Z3

Z3 هو مبرهن نظري من Microsoft Research. مرخص بموجب رخصة MIT. تتضمن التوزيعات الثنائية لنظام Windows مكتبات C++ وقت التشغيل القابلة لإعادة التوزيع

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

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

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

راجع ملاحظات الإصدار للحصول على ملاحظات حول الإصدارات المستقرة المختلفة لـ Z3.

حالة البناء

سير عمل طلبات السحب والدفع

سير العمل المجدولة

سير العمل اليدوية والإصدارات

سير العمل المتخصصة

Nightly Validation	Copilot Setup	Agentics Maintenance

سير العمل الوكيلية

TPTP Benchmark

بناء 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 أو أحدث.

ميزات الأمان (MSVC): عند البناء باستخدام Visual Studio/MSVC، يتم تمكين ميزتين أمنيتين افتراضيًا لـ Z3:

• Control Flow Guard (/guard:cf) - مفعل افتراضيًا لاكتشاف محاولات اختراق الكود الخاص بك عن طريق منع الاستدعاءات لمواقع أخرى غير نقاط دخول الدوال، مما يجعل من الصعب على المهاجمين تنفيذ كود عشوائي عبر إعادة توجيه تدفق التحكم
• Address Space Layout Randomization (/DYNAMICBASE) - مفعل افتراضيًا لترتيب عشوائي لتخطيط الذاكرة، وهو مطلوب بواسطة خيار الرابط /GUARD:CF
• يمكن تعطيل هذه باستخدام python scripts/mk_make.py --no-guardcf (بناء Python) أو cmake -DZ3_ENABLE_CFG=OFF (بناء CMake) إذا لزم الأمر

بناء 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 ومترجم Mingw-w64 cross-compiler. في هذه الحالة، تأكد من استخدام 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 بواسطة script 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، يمكنك حذف دليل البناء وتشغيل script mk_make.py مرة أخرى.

بناء Z3 باستخدام CMake

Z3 لديه نظام بناء باستخدام CMake. اقرأ ملف README-CMake.md للحصول على التفاصيل. يُوصى به لمعظم مهام البناء، باستثناء بناء روابط OCaml.

بناء Z3 باستخدام vcpkg

vcpkg هو مدير حزم كامل المنصة. لتثبيت Z3 باستخدام vcpkg، قم بتنفيذ:

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

بناء Z3 باستخدام Bazel

يمكن بناء Z3 باستخدام Bazel. هذا معروف بأنه يعمل على Ubuntu مع Clang (لكن قد يعمل في أماكن أخرى مع مترجمات أخرى):

bazel build //...

التبعيات

Z3 نفسه لديه تبعيات قليلة فقط. يستخدم مكتبات C++ وقت التشغيل، بما في ذلك pthreads للتعددية الخيطية. من الممكن اختياريًا استخدام GMP للأعداد الصحيحة متعددة الدقة، ولكن Z3 يحتوي على وظائف متعددة الدقة ذاتية الاكتفاء. Python مطلوب لبناء Z3. يتطلب بناء واجهات Java و .NET و OCaml و Julia تثبيت سلاسل أدوات ذات صلة.

روابط Z3

Z3 لديه روابط للعديد من لغات البرمجة.

.NET

يمكنك تثبيت حزمة NuGet لأحدث إصدار من Z3 من nuget.org.

استخدم علامة سطر الأوامر --dotnet مع mk_make.py لتمكين بناء هذه.

انظر examples/dotnet للحصول على أمثلة.

C

هذه دائمًا مفعلة.

انظر examples/c للحصول على أمثلة.

C++

هذه دائمًا مفعلة.

انظر examples/c++ للحصول على أمثلة.

Java

استخدم علامة سطر الأوامر --java مع mk_make.py لتمكين بناء هذه.

للحصول على إعدادات IDE (Eclipse، IntelliJ IDEA، Visual Studio Code) واستكشاف الأخطاء وإصلاحها، راجع دليل إعداد Java IDE.

انظر examples/java للحصول على أمثلة.

Go

استخدم علامة سطر الأوامر --go مع mk_make.py لتمكين بناء هذه. لاحظ أن روابط Go تستخدم CGO وتتطلب سلسلة أدوات Go (Go 1.20 أو أحدث) للبناء.

مع CMake، استخدم الخيار -DZ3_BUILD_GO_BINDINGS=ON.

انظر examples/go للحصول على أمثلة و src/api/go/README.md للحصول على توثيق كامل لواجهة API.

OCaml

استخدم علامة سطر الأوامر --ml مع mk_make.py لتمكين بناء هذه.

انظر examples/ml للحصول على أمثلة.

Python

يمكنك تثبيت غلاف Python لـ 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 virtual environment وتثبيت 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
# ستجد Z3 وروابط Python مثبتة في البيئة الافتراضية
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.

WebAssembly / TypeScript / JavaScript

يتم نشر بناء WebAssembly مع كتابة TypeScript المرتبطة على npm كـ z3-solver. يمكن العثور على معلومات حول بناء هذه الروابط في src/api/js.

Smalltalk (Pharo / Smalltalk/X)

يوفر مشروع MachineArithmetic واجهة Smalltalk لواجهة C لـ Z3. لمزيد من المعلومات، راجع MachineArithmetic/README.md.

AIX

إعدادات البناء لـ AIX موصوفة هنا.

نظرة عامة على النظام

الواجهات

• تنسيق الإدخال الافتراضي هو SMTLIB2

• واجهات الوظائف الخارجية الأصلية الأخرى:

• C++ API

• .NET API

• Java API

• Python API (متاح أيضًا بتنسيق pydoc)

• Rust

• C

• OCaml

• Julia

• Smalltalk (يدعم Pharo و Smalltalk/X)

أدوات القوة

• Axiom Profiler الذي تم تطويره حاليًا بواسطة ETH Zurich