نام (NAME)

cvc4, pcvc4 - یک اثبات‌کننده خودکار قضیه

خلاصه دستور (SYNOPSIS)

cvc4 [ گزینه‌ها ] [ فایل ]

pcvc4 [ گزینه‌ها ] [ فایل ]

توضیحات (DESCRIPTION)

cvc4 یک اثبات‌کننده خودکار قضیه برای فرمول‌های مرتبه اول با در نظر گرفتن نظریه‌های پس‌زمینه مورد نظر است. pcvc4 گونه «پورتفولیو» (portfolio) از CVC4 است که قادر است چندین نمونه CVC4 را با پیکربندی‌های متفاوت به‌طور همزمان اجرا کند.

همراه با فایل ، دستورها از فایل خوانده و اجرا می‌شوند. CVC4 از قالب ورودی SMT-LIB (نسخه‌های 1.2 و 2.0) و همچنین «زبان نمایش» اختصاصی خود (نگاه کنید به cvc4(5) ) پشتیبانی می‌کند که از جهات بسیاری به زبان نمایش CVC3 شباهت دارد، اما با آن یکسان نیست.

اگر فایل مشخص نشود، ورودی استاندارد خوانده می‌شود (و زبان نمایش CVC4 فرض می‌گردد). اگر فایل مشخص نشود و CVC4 به یک ترمینال متصل باشد، حالت تعاملی در نظر گرفته می‌شود.

گزینه‌های رایج (COMMON OPTIONS)

هر گزینه علامت‌گذاری‌شده با [*] دارای یک گونه --no-OPTIONNAME است که عملکرد گزینه را معکوس می‌کند.

$

$

هر گزینه علامت‌گذاری‌شده با [*] دارای یک گونه --no-OPTIONNAME است که عملکرد گزینه را معکوس می‌کند.

عیب‌یابی (DIAGNOSTICS)

CVC4 تمام خطاهای نحوی و معنایی را در خروجی خطای استاندارد گزارش می‌کند.

تاریخچه (HISTORY)

تلاش CVC4 نقطه اوج پانزده سال پژوهش در زمینه اثبات قضیه است که با Stanford Validity Checker (SVC) در سال ۱۹۹۶ آغاز شد.

جانشین SVC، یعنی Cooperating Validity Checker (CVC)، دارای طراحی داخلی بهینه‌تری بود، برهان‌ها را تولید می‌کرد، از حل‌کننده SAT با نام Chaff استفاده می‌کرد و بهبودهای متعددی در زمینه قابلیت استفاده داشت. نام آن از ماهیت همکارانه رویه‌های تصمیم در ترکیب نظریه‌های نلسون-اوپن (Nelson-Oppen) گرفته شده است که برابری‌های میان عبارت‌های مشترک را بین یکدیگر به اشتراک می‌گذارند.

نسخه CVC Lite که نخستین بار در سال ۲۰۰۳ عرضه شد، بازنویسی CVC بود که تلاش می‌کرد CVC را منعطف‌تر کند (از این رو «lite» نامیده شد) و در عین حال مجموعه قابلیت‌ها را گسترش دهد: CVCLite بر خلاف پیشینیان خود از سورها (quantifiers) پشتیبانی می‌کرد. CVC3 یک بازنگری اساسی در بخش‌هایی از CVC Lite بود: پیاده‌سازی‌های بهتری از رویه‌های تصمیم‌گیری اضافه کرد، پشتیبانی از MiniSat را در هسته افزود و به‌طور کلی عملکرد بهتری داشت.

نسخه CVC4 نسل جدید و نسل پنجم این خانواده بررسی‌کننده اعتبار است که اکنون میراثی پانزده‌ساله را جشن می‌گیرد. این نسخه نشان‌دهنده ارزیابی و بازطراحی کامل معماری هسته است تا هم کارآمد باشد و هم به عنوان بستری برای پژوهش‌های پیشرفته در چندین سال آینده به کار رود. به جای استفاده از CVC3 و بازطراحی بخش‌های مشکل‌دار، ما رویکرد اتاق پاک (clean-room) را در پیش گرفتیم و از صفر شروع کردیم. پیش از به‌کارگیری هر طرحی از CVC3، ما آن‌ها را به دقت بررسی، بازبینی و به‌روزرسانی کرده‌ایم. بسیاری از بخش‌های CVC4 تنها شباهتی ظاهری، در صورت وجود، به بخش‌های متناظر در CVC3 دارند.

با این حال، CVC4 اساساً مشابه CVC3 و بسیاری دیگر از حل‌کننده‌های مدرن SMT است: این ابزار یک حل‌کننده DPLL( T ) با یک حل‌کننده SAT در هسته خود و مسیری برای واگذاری وظایف به پیاده‌سازی‌های مختلف رویه‌های تصمیم‌گیری است که هر کدام مسئول حل فرمول‌ها در یک نظریه پس‌زمینه خاص هستند.

ما احساس کردیم که ارزیابی مجدد و بازنویسی کامل از پایه، به دلیل ویژگی‌های کارایی CVC3 ضروری بود. CVC3 ویژگی‌های مفید بسیاری دارد، اما برخی از جنبه‌های اصلی طراحی آن منجر به مصرف بالای حافظه شد، و استفاده از محاسبات سنگین (در جایی که رویکردهای مهندسی چابک‌تر می‌توانست کافی باشد) باعث شد CVC3 اثبات‌کننده‌ای بسیار کندتر از سایر ابزارها باشد. از آنجا که این طرح‌ها در CVC3 محوری بودند، ایجاد یک نسخه جدید بر مهندسی مجدد گزینشی که به سرعت از کنترل خارج می‌شد، ترجیح داده شد.

نسخه (VERSION)

این صفحه راهنما مربوط به CVC4 نسخه CVC4_RELEASE_STRING است.

اشکالات (BUGS)

سامانه پیگیری مشکلات پروژه CVC4 در نشانی زیر نگهداری می‌شود: https://github.com/CVC4/CVC4/issues

نویسندگان (AUTHORS)

CVC4 توسط تیمی از پژوهشگران دانشگاه استنفورد و دانشگاه آیووا توسعه یافته است. برای مشاهده فهرست کامل مشارکت‌کنندگان، به فایل AUTHORS در بسته انتشار مراجعه کنید.

همچنین ببینید (SEE ALSO)

libcvc4(3), libcvc4parser(3)

علاوه بر این، ویکی CVC4 حاوی اطلاعات مفیدی درباره طراحی و سازوکار داخلی CVC4 است. این ویکی در نشانی زیر نگهداری می‌شود: http://cvc4.cs.stanford.edu/wiki