هل تبحث عن أمثلة عملية لـ SMT Z3 Usecases (مثل DBC) وبديل المصدر المفتوح لـ Z3؟ [مغلق

Question

لقد اهتمت بالبحث عن أمثلة عملية لاستخدام SMT Z3 (مثل DBC) مع رمز وبدائل مفتوحة المصدر لهذه الأداة. لذلك ، في الواقع ، أنا مهتم بأدوات حل رسمية Z3 مماثلة ، ولكن:

• يجب أن يكون مفتوح المصدر
• توفير كل من المستوى المنخفض (API) والتفاعل عالي المستوى (النصوص)
• دعم SMT-LIB
• مناسبة (قابلة للاستخدام) في الأدوات/مكتوبة في/للغات مثل Java و Python و Ruby و Vala و ليس هاسكل
• لديه أدوات مستقرة (قابلة للاستخدام في الممارسة) بناءً على ذلك ، مثل التصميم حسب العقد (DBC) ، والتحقق من النوع الثابت ، إلخ.

وفقًا لـ SMT-LIB Homepage (انظر Bit.ly Bundle للحصول على التفاصيل) ، فإن قائمة SMT Solvers 2010 هي: "alt-ergo ، Barcelogic ، Beaver ، Boolector ، CVC3 ، DPT ، Mathsat ، Opensmt ، Sateen ، Spear ، STP ، Sword ، Uclid ، verit ، yices ، Z3. "

يرجى تقديم أي ملاحظات حول استخدام أي منها في الممارسة (أمثلة الرمز هي الأفضل)؟

أخيرًا ، ستكون أي معلومات حول المقارنة مع إمكانيات GHC مفيدة ، ولكن فقط في حالة وجود مثال للتنفيذ (وليس "ميزة" اللغة).

المزيد من المعلومات السريعة على Z3 هنا http://bit.ly/bundles/ewiger/1

Answer 1

على حد علمي ، يأتي CVC3 الأقرب إلى متطلباتك ، من خلال ذلك:

1. يحتوي على مجموعة ميزات تشبه Z3.
2. لديه ترخيص على غرار BSD
3. هو الحلال الأساسي لعدد من المشاريع الحالية.

CVC3 لديه روابط لـ C ++ و Java ، وربما لغات أخرى. بشكل عام ، أعتقد أن واجهة برمجة التطبيقات أكثر صعوبة بكثير من استخدامها (النص) لغة الإدخال. هذا له فائدة إضافية ، إذا تم التمسك بلغة SMT-LIB2 ، فقد تتمكن من التبديل إلى أداة مختلفة لاحقًا إذا كان ذلك ضروريًا. تتوفر عينة كبيرة من الأمثلة على موقع SMT-LIB.

Answer 2

لقد سألت عن بدائل OpenSource لـ Z3:

وفق SMT-Wikipedia في 2011-08 ، لدينا:

استنادًا إلى هذه التدابير ، يبدو أن المشاريع الأكثر حيوية وتنظيمها هي OpenSMT و STP و CVC4.

أنا فقط أتحقق من هذه الأشياء - حتى الآن ، يبدو الثلاثة معقولون ، بالإضافة إلى CVC الأقدم -> أعني CVC3.