--- name: z3-prover description: مُثبِت قيود حتمي (Z3 SMT). UNSAT=إثبات صوري، SAT=مثال مضادّ/حلّ فوري. يُثري math-foundation + lean-verify + engineering-design-stack. ---

Z3 SMT Prover (Deterministic Constraint Solving)

متى تُستخدم (auto-trigger)

• إثبات/دحض عبارة منطقية أو رياضية (claim) بسرعة + مثال مضادّ فوري عند الدحض.
• حلّ نظام قيود/معادلات (خطي/لاخطي/أعداد صحيحة/منطق).
• فحص تناقض قيود تصميم هندسي (constraints feasibility).

القوة الفريدة (تسدّ ثغرة Lean/Wolfram)

• UNSAT = إثبات صوري (لا مثال ينقض) — أخفّ من Lean (لا تحتاج mathlib) وأسرع.
• SAT = مثال مضادّ ملموس فوراً — Wolfram لا يُرجع counterexample؛ Z3 يُرجعه (x=0.5 ينقض x²>x).
• حتمي 100% (لا هلوسة) — طبقة تحقّق فوق opus5-executor/math-foundation.

الأوامر

python3 skills/z3-prover/z3_prover.py selftest
python3 skills/z3-prover/z3_prover.py solve '<قيود؛ مفصولة بـ ; >'
python3 skills/z3-prover/z3_prover.py prove '<claim>' '<assumptions>'
python3 skills/z3-prover/z3_prover.py check '<expr>'

المتغيّرات تُعرّف تلقائياً: افتراضي Real · سابقة int_ = عدد صحيح · bool_ = منطقي. دوال متاحة: And/Or/Not/Implies/If/Sqrt/ForAll/Exists.

أمثلة:

solve 'x + y == 10; x - y == 2'        → x=6, y=4
prove 'xx >= 0' ''                     → PROVEN
prove 'xx > x' ''                      → DISPROVEN (مثال مضادّ x=0)
solve 'int_n > 2; int_n < 4'            → n=3

التكامل (أماكن الاستخدام)

• math-foundation → تحقّق صوري + أمثلة مضادّة للبراهين/المسائل.
• lean-verify → طبقة أخفّ/أسرع للتحقّق المنطقي (Z3 أولاً، Lean للعميق).
• opus5-clean-executor → double-check حتمي لأي حلّ رياضي نظيف.
• engineering-design-stack → فحص جدوى قيود التصميم (هل القيود متناقضة؟).

مُختبَر E2E (2026-10-08)

selftest 6/6: نظام معادلات (x=6,y=4) · إثبات x²≥0 · مثال مضادّ x²>x→x=0 · تناقض UNSAT · تبديلية · قيد صحيح n=3 → SELFTEST_OK.

🔴 القيد (صادق)

• للبراهين العميقة بالحثّ/mathlib → lean-verify أقوى؛ Z3 للقرارية (decidable) والقيود.
• التعابير بصيغة Python/z3 (eval آمن مقيّد — لا builtins).