صدق‌پذیری در پیمانه نظریات

یک مسئله صدق‌پذیری در پیمانه نظریات الگو:به انگلیسی با کوته‌نوشت SMT در علوم رایانه و منطق ریاضیاتی، یک «مسئله تصمیم» برای فرمول‌های منطقی در ارتباط با ترکیبی از نظریات پیش‌زمینه‌ای که به صورت منطق مرتبه اول کلاسیک دارای تساوی بیان شده‌اند، است. مثال‌هایی از این نظریات که معمولاً در علوم رایانه استفاده می‌شوند از این قرار است: نظریه اعداد حقیقی، نظریه اعداد صحیح، و نظریات ساختمان داده‌های متنوع مثل لیست، آرایه، بردار بیتی، و غیره. مسئله SMT را می‌توان نوعی مسئله ارضای محدودیت در نظر گرفت، و از این رو یک دیدگاه صوری‌شده معین به برنامه‌نویسی محدودیت است.

اصطلاح‌شناسی اولیه

به صورت صوری، یک مسئله SMT یک فرمول در منطق مرتبه اول است، که در آن بعضی از نمادهای تابعی و گزاره‌ای تفسیرهای اضافی دارند، و SMT همان مسئله تعیین این سوال است که آیا چنین فرمولی «صدق‌پذیر» هست یا نه. به عبارت دیگر، یک نمونه از مسئله صدق‌پذیری دودویی (SAT) را درنظر بگیرید، که در آن بعضی از متغیرهای دودویی با محمول‌ها جایگزین شده‌اند و این موضوع در محدوده مجموعه مناسبی از متغیرهای غیردودویی رخ داده‌است. یک گزاره یک تابع دودویی از متغیرهای غیردودویی است. چند مثال از گزاره شامل، نابرابری خطی (مثل $3x+2y-z\ge 4$) یا تساوی‌های شامل ترم‌های تفسیرنشده و نمادهای تابعی (مثل $f(f(u,v),v)=f(u,v)$ که در آن $f$ یک تابع تعیین نشده از دو آرگومان است). این گزاره‌ها براساس هر نظریه منتسب‌شده مرتبط رده‌بندی می‌شوند. برای مثال، نابرابری خطی روی متغیرهای حقیقی توسط قواعد نظریه حساب حقیقی خطی ارزیابی می‌شود، که در آن گزاره‌ها درگیر ترم‌های تفسیرنشده اند و نمادهای تابعی توسط قواعد نظریه توابع تفسیرنشده با تساوی ارزیابی می‌شوند (که گاهی به آن نظریه پوچ هم می‌گویند). نظریه‌های دیگر شامل نظریه‌های ساختمان آرایه‌ها و لیست‌ها می‌شود (که برای مدل‌سازی و راستی‌آزمایی برنامه‌های رایانه‌ای مفید است)، و نیز شامل نظریه آرایه بیتی است (که در مدل‌سازی و راستی‌آزمایی طراحی‌های سخت‌افزاری مفید است). زیرنظریه‌هایی دیگری هم ممکن است موجود باشد: مثل «منطق تفاوتی» که یک زیرنظریه از حساب خطی است که در آن هر نابرابری باید محدودیت فرمی $x-y>c$ را برای متغیرهای $x$ و $y$ و ثابت $c$ داشته باشد.

بیشتر حل‌کننده‌های مسئله SAT فقط از قسمت‌های فاقد سور از منطق‌شان پشتیبانی می‌کنند.

قدرت بیان

یک نمونه از مسئله SMT در واقع یک تعمیم برای نمونه مسئله SAT دودویی است، که در آن مجموعه‌های متنوعی از متغیرها با گزاره‌هایی از انواع متنوعی از نظریه‌های بنیادین جایگزین شده‌اند. فرمول‌های SMT قدرت زبان مدل‌سازی بیشتری نسبت به فرمول‌های دودویی SAT دارند. برای مثال، یک فرمول SMT به ما امکان مدل‌سازی عملیات دیتاپد (مسیرداده) برای یک ریزپردازنده را در سطح کلمه (و نه سطح بیت) می‌دهد.

برای مقایسه، برنامه‌نویسی مجموعه جواب نیز براساس گزاره‌ها است (به صورت دقیق‌تر، بر اساس جمله‌های اتمی است که از فرمول‌های اتمی ساخته شده‌است). برخلاف SMT، برنامه‌های مجموعه جواب، «سور» ندارند، و نمی‌توانند محدودیت‌هایی مثل حساب خطی یا منطق تفاوت را به سادگی بیان کنند- ASP به عنوان بهترین راه‌حل برای مسائل دودویی هستند که به نظریه آزاد توابع تفسیرنشده کاهش یافته‌اند. پیاده‌سازی اعداد صحیح ۳۲ بیتی به عنوان آرایه‌بیتی در ASP از مسائل مشابهی رنج می‌برند که حل کننده‌های اولیه SMTها با آن مواجه بودند: برابری‌های «بدیهی» مثل x+y=y+x به سختی قابل استنتاج هستند.

برنامه‌نویسی منطقی محدودیت از محدودیت‌های حسابی خطی پشتیبانی می‌کنند، اما آن‌ها در چارچوب نظری کاملاً متفاوتی قرار دارند. حل‌کننده‌های SMT برای حل فرمول‌هایی در منطق مرتبه بالاتر گسترش یافته‌اند.

دیدگاه‌های حل‌کننده

تلاش‌های اولیه برای حل نمونه‌های مسئله SMT شامل ترجمه آن‌ها به نمونه مسائل SAT دودویی بود (مثلاً یک متغیر صحیح ۳۲ بیتی توسط ۳۲ عدد متغیر تک بیتی با وزن‌های مناسب و عملیات سطح کلمه مثل «جمع» با عملیات منطقی سطح پایینی روی بیت‌ها جایگزین می‌شدند) سپس این فرمول به حل‌کننده SAT دودویی تحویل می‌شد. به این دیدگاه، دیدگاه حریصانه هم می‌گویند، و دارای مزیت‌هایی هم هست: با پیش‌پردازش یک فرمول SMT به یک فرمول SAT دودویی معادل، حل‌کننده‌های SAT دودویی موجود را می‌توان به صورتی که هست استفاده کرد، در این روش، مزیت‌هایش از نظر کارایی و ظرفیت در طی زمان بیشتر می‌شود. از جهت دیگر، فقدان وجود معناشناسی سطح بالا برای نظریه‌های بنیادین، یعنی حل‌کننده دودویی SAT باید خیلی بیشتر از آنچه برای برای کشف واقعیت‌های «بدیهی» لازم است، کار کند (مثلاً $x+y=y+x$ برای جمع اعداد صحیح). این مشاهده منجر به ایجاد تعدادی از حل کننده‌های SMT شد که به شدت «استنتاج دودویی یک جستجوی با سبک DPLL» را به «حل‌کننده‌های خاص نظریه (T-solvers) که به عطف‌های(ANDs) از گزاره‌ها از یک نظریه معین رسیدگی می‌کند»، یکپارچه‌سازی می‌کرد. به این دیدگاه، «دیدگاه کندرو» هم گفته می‌شود.

DPLL(T) دوبل (دوتایی) که این معماری یک «مسئولیت استنتاج بولی» به «حل‌کننده SAT مبتنی بر DPLL» می داد، که به نوبه خود با یک حل‌کننده برای نظریه T از طریق یک واسط خوش‌تعریف تعامل دارد. حل‌کننده نظریه فقط باید در مورد بررسی امکان عطف‌دهی به گزاره‌های نظریه ارسال‌شده به آن، از حل‌کننده SAT و در هنگام کاوش فضای جستجوی دودویی فرمول نگران باشد. برای آنکه این یکپارچه‌سازی به خوبی کار کند، حل‌کننده نظریه باید بتواند در تحلیل انتشار و تضاد مشارکت کند، یعنی باید بتواند واقعیت‌های جدیدی را از واقعیت‌های پیش از این بناشده، استنتاج کند، همچنین از «توضیحات مختصری از غیرممکن بودن» در موقع بروز تعارض‌های نظری پشتیبانی کند. به زبان دیگر، حل‌کننده نظریه باید افزایشی و پس‌گردی باشد.

مسئله SMT برای نظریات تصمیم‌ناپذیر

بیشتر دیدگاه‌های SMT معمول از نظریات تصمیم‌پذیر پشتیبانی می‌کنند. با این حال بیشتر سامانه‌های جهان واقعی را فقط با کمک حساب غیرخطی روی اعداد حقیقی می‌توان مدل‌سازی کرد، که ممکن است توابع متعالی را هم درگیر کند، مثل یک هواپیما و رفتار آن. این واقعیت منجر به ایجاد انگیزه‌ای برای یک گسترش برای مسئله SMT به نظریه‌های غیرخطی شد، مثلاً تعیین آنکه آیا

$\begin{array}{cc}& (\sin (x{)}^3=\cos (\log (y)\cdot x)\vee b\vee -x^2\ge 2.3y)\wedge (\mathrm{\neg }b\vee y<-34.4\vee \exp (x)>\frac{y}{x})\end{array}$

که در آن:

$b\in 𝔹,x,y\in ℝ$

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

مثال‌هایی از حل کننده‌های SMT که می‌خواهند ترکیبات دودویی «اتم نظریه» از نظریات حسابی تصمیم‌ناپذیر روی اعداد حقیقی رسیدگی کنند، ABsolver نام دارند، که از یک معماری کلاسیک DPLL(T) با یک بسته بهینه‌سازی غیرخطی به عنوان حل‌کننده نظریه فرعی (به صورت لازم غیرکامل) استفاده می‌کنند، و iSAT الگو:Webarchive که روی یک اتحاد حل‌کننده DPLL SAT و انتشار محدودیت بازه‌ای ساخته شده‌اند، که الگوریتم iSAT نامیده می‌شود.

حل‌کننده‌ها

جدول زیر بعضی از ویژگی‌های چند تا از حل کننده‌های SMT موجود را خلاصه‌بندی نموده‌است. ستون «SMT-LIB» نشان‌دهنده سازگاری با زبان SMT-LIB است؛ بیشتر سامانه‌هایی را که با 'yes' نشان‌گذاری کرده‌ایم، فقط از نسخه‌های قدیمی SMT-LIB پشتیبانی می‌کنند، یا اینکه فقط پشتیبانی جزئی از زبان دارند. ستون «CVC» نشان‌دهنده پشتیبانی از زبان CVC است. ستون «DIMACS» نشان‌دهنده پشتیبانی از قالب DIMACS است.

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

بن‌سازه			ویژگی‌ها						یادداشت‌ها
Name	OS	License	SMT-LIB	CVC	DIMACS	Built-in theories	API	SMT-COMP [۱]
ABsolver	Linux	CPL	الگو:Yes	الگو:No	الگو:Yes	linear arithmetic, non-linear arithmetic	C++	no	DPLL-based
Alt-Ergo	Linux, Mac OS , Windows	CeCILL-C (roughly equivalent to LGPL)	الگو:Yes	الگو:No	الگو:No	empty theory, linear integer and rational arithmetic, non-linear arithmetic, polymorphic arrays, enumerated datatypes, AC symbols, bitvectors, record datatypes, quantifiers	OCaml	۲۰۰۸	Polymorphic first-order input language à la ML, SAT-solver based, combines Shostak-like and Nelson-Oppen like approaches for reasoning modulo theories
Barcelogic	Linux	Proprietary	الگو:Yes			empty theory, difference logic	C++	۲۰۰۹	DPLL-based, congruence closure
Beaver	Linux, Windows	BSD	الگو:Yes	الگو:No	الگو:No	bitvectors	OCaml	۲۰۰۹	SAT-solver based
Boolector	Linux	MIT	الگو:Yes	الگو:No	الگو:No	bitvectors, arrays	C	۲۰۰۹	SAT-solver based
CVC3	Linux	BSD	الگو:Yes	الگو:Yes		empty theory, linear arithmetic, arrays, tuples, types, records, bitvectors, quantifiers	C/C++	۲۰۱۰	proof output to HOL
CVC4	Linux, Mac OS , Windows, FreeBSD	BSD	الگو:Yes	الگو:Yes		rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bitvectors, strings, and equality over uninterpreted function symbols	C++	۲۰۱۰	version 1.5 released July 2017
Decision Procedure Toolkit (DPT)	Linux	Apache	الگو:No				OCaml	no	DPLL-based
iSAT	Linux	Proprietary	الگو:No			non-linear arithmetic		no	DPLL-based
MathSAT	Linux, Mac OS , Windows	Proprietary	الگو:Yes		الگو:Yes	empty theory, linear arithmetic, nonlinear arithmetic, bitvectors, arrays	C/C++, Python, Java	۲۰۱۰	DPLL-based
MiniSmt	Linux	LGPL	الگو:Yes			non-linear arithmetic		۲۰۱۰	SAT-solver based, Yices-based
Norn									SMT solver for string constraints
OpenCog	Linux	AGPL	الگو:No	الگو:No	الگو:No	probabilistic logic, arithmetic. relational models	C++, Scheme, Python	no	subgraph isomorphism
OpenSMT	Linux, Mac OS , Windows	GPLv3	الگو:Yes		الگو:Yes	empty theory, differences, linear arithmetic, bitvectors	C++	۲۰۱۱	lazy SMT Solver
raSAT	Linux	GPLv3	v2.0			real and integer nonlinear arithmetic		۲۰۱۴، ۲۰۱۵	extension of the Interval Constraint Propagation with Testing and the Intermediate Value Theorem
SatEEn	?	Proprietary	الگو:Yes			linear arithmetic, difference logic	none	۲۰۰۹
SMTInterpol	Linux, Mac OS , Windows	LGPLv3	الگو:Yes			uninterpreted functions, linear real arithmetic, and linear integer arithmetic	Java	۲۰۱۲	Focuses on generating high quality, compact interpolants.
SMCHR	Linux, Mac OS , Windows	GPLv3	الگو:No	الگو:No	الگو:No	linear arithmetic, nonlinear arithmetic, heaps	C	no	Can implement new theories using Constraint Handling Rules.
SMT-RAT	Linux, Mac OS	MIT	الگو:Yes	الگو:No	الگو:No	linear arithmetic, nonlinear arithmetic	C++	۲۰۱۵	Toolbox for strategic and parallel SMT solving consisting of a collection of SMT compliant implementations.
SONOLAR	Linux, Windows	Proprietary	الگو:Yes			bitvectors	C	۲۰۱۰	SAT-solver based
Spear	Linux, Mac OS , Windows	Proprietary	الگو:Yes			bitvectors		۲۰۰۸
STP	Linux, OpenBSD, Windows, Mac OS	MIT	الگو:Yes	الگو:Yes	الگو:No	bitvectors, arrays	C, C++, Python, OCaml, Java	۲۰۱۱	SAT-solver based
SWORD	Linux	Proprietary	الگو:Yes			bitvectors		۲۰۰۹
UCLID	Linux	BSD	الگو:No	الگو:No	الگو:No	empty theory, linear arithmetic, bitvectors, and constrained lambda (arrays, memories, cache, etc.)		no	SAT-solver based, written in Moscow ML . Input language is SMV model checker. Well-documented!
veriT	Linux, OS X	BSD	الگو:Yes			empty theory, rational and integer linear arithmetics, quantifiers, and equality over uninterpreted function symbols	C/C++	۲۰۱۰	SAT-solver based
الگو:Visible anchor	Linux, Mac OS , Windows, FreeBSD	GPLv3	الگو:Yes	الگو:No	الگو:Yes	rational and integer linear arithmetic, bitvectors, arrays, and equality over uninterpreted function symbols	C	۲۰۱۴	Source code is available online
Z3 Theorem Prover	Linux, Mac OS , Windows, FreeBSD	MIT	الگو:Yes		الگو:Yes	empty theory, linear arithmetic, nonlinear arithmetic, bitvectors, arrays, datatypes, quantifiers, strings	C/C++, .NET, OCaml, Python, Java, Haskell	۲۰۱۱	Source code is available online

استانداردسازی و مسابقه حل‌کننده SMT-COMP

تلاش‌های زیادی برای توصیف یک واسط استاندارد شده برای حل کننده SMT (و اثبات‌گر قضیه خودکار، که یک اصطلاح هم‌معنی است) وجود دارد. برجسته‌ترین آن‌ها استاندارد SMT-LIB است که یک زبان بر اساس عبارات S تهیه دیده‌است. دیگر قالب‌های استاندارد شده که معمولاً پشتیبانی می‌شوند شامل قالب DIMACS است که توسط خیلی از حل‌کننده‌های SAT بولی پشتیبانی می‌شود، و قالب CVC که توسط اثبات‌گر قضیه خودکار CVC استفاده می‌شود.

قالب SMT-LIB همراه با تعدادی از محک‌زنی (benchmark) استاندارد آمده‌است، و این موضوع یک مسابقه سالانه بین حل‌کننده‌های SMT را امکان‌پذیر نموده‌است که به آن SMT-COMP گفته می‌شود. در ابتدا، مسابقه در همایش درستی‌سنجی به کمک رایانه (CAV) قرار داشت، اما از سال ۲۰۲۰ مسابقه به عنوان بخشی از کارگاه SMT قرار گرفت، که به همایش ترکیبی بین‌المللی روی استنتاج خودکار (IJCAR) وابسته بود.

کاربردها

حل‌کننده‌های SMT هم برای صحت، اثبات درستی برنامه‌ها، آزمون نرم‌افزار براساس اجرای نمادین، و نیز برای ترکیب، تولید قطعه‌های برنامه با جستجو روی فضای برنامه‌های ممکن مفید است. در خارج از حیطه درستی‌سنجی نرم‌افزار، از حل‌کننده SMT برای استنتاج نوع، و نیز برای مدل‌سازی سناریوهای نظری، که شامل مدل‌سازی اعتقادات کنشگر در کنترل نیروی هسته‌ای است، استفاده شده‌است.

درستی‌سنجی

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

درستی‌سنج‌های زیادی روی حل‌کننده Z3 SMT ساخته شده‌است. Boogie یک زبان درستی‌سنجی سطح میانی است که از Z3 استفاده می‌کند تا به صورت خودکار برنامه‌های دستوری ساده را بررسی کند. درستی‌سنج VCC برای C همزمان از Boogie، و نیز از Dafny برای برنامه‌های مبتنی بر شیء دستوری استفاده می‌کند و از Chalice برای برنامه‌های همزمان استفاده می‌کند، و از Spec# برای C# استفاده می‌کند. زبان F* یک زبان نوع دار وابسته است که از Z3 برای یافتن اثبات استفاده می‌کند؛ کامپایلر این اثبات‌ها را حمل می‌کند تا بایت‌کد حامل اثبات را تولید کند. زیرساخت درستی‌سنجی Viper شرایط درستی‌سنجی را به Z3 کدبندی می‌کند. کتابخانه sbv درستی‌سنجی مبتنی بر SMT را برای برنامه‌های زبان Haskell تهیه می‌بیند، و به کاربر کمک می‌کند تا از بین تعدادی از حل‌کننده‌ها مثل Z3، ABC, Boolector, CVC4، MathSat، و Yices انتخاب انجام دهد.

درستی‌سنج‌های زیادی روی یک حل‌کننده SMT با نام Alt-Ergo ساخته شده‌اند. در ادامه فهرستی از کاربردهای به بلوغ رسیده آمده‌است:

• Why3: یک بن‌سازه برای درستی‌سنجی برنامه به صورت استقرایی، که از Alt-Ergo به عنوان اثبات‌کننده اصلی استفاده می‌کند.
• CAVEAT، یک درستی‌سنج C که توسط CEA توسعه یافته‌است، و توسط شرکت Airbus استفاده می‌شود؛ Alt-Ergo در یکی از صلاحیت سنجی DO-178C از یکی از هواپیماهای جدیدش قرار گرفته‌است.
• Frama-C، یک چارچوب برای تحلیل کد C است، از Alt-Ergo در افزونه‌های Jessie و WP استفاده می‌کند (که اختصاص به «درستی‌سنجی برنامه استقرایی» دارد)؛
• SPARK، از CVC4 و Alt-Ergo (که پشت GNATprove قرار دارد) استفاده می‌کند تا درستی‌سنجی بعضی از ادعاها را در SPARK 2014 خودکارسازی کند؛
• Atelier-B می‌تواند از Alt-Ergo به جای اثبات‌گر اصلی اش استفاده کند (این کار موجب افزایش موفقیت از ۸۴٪ به ۹۸٪ در محک‌زنی‌های پروژه ANR Bware می‌شود)؛
• Rodin، یک چارچوب روش-B است که توسط Systertel توسعه یافته‌است و می‌تواند از Alt-Ergo به عنوان یک back-end استفاده کند.
• Cubicle یک بررسی‌کننده مدل متن‌باز است که از آن برای درستی‌سنجی ویژگی‌های امنیتی برای سامانه‌های تبدیل مبتنی بر آرایه استفاده می‌شود.
• EasyCrypt، یک جعبه ابزار برای استنتاج دربارهٔ ویژگی‌های رابطه‌ای در محاسبات احتمالی است، که کد خصومتی دارد.

بسیاری از حل‌کننده‌های SMT یک قالب واسط معمول که SMTLIB2 نامیده می‌شود را پیاده‌سازی می‌کنند (این فایل‌ها معمولاً پسوند ".smt2" دارند). ابزار LiquidHaskell یک درستی‌سنج مبتنی بر نوع اصلاحی برای Haskell را پیاده‌سازی می‌کند، که می‌تواند از هر حل‌کننده سازگار با SMTLIB2 (مثل CVC4، MathSat یا Z3) استفاده کند.

تحلیل و آزمون مبتنی بر اجرای نمادین

یک کاربرد مهم برای حل‌کننده SMT، اجرای نمادین برای تحلیل و آزمون برنامه‌ها است (مثل تست کلونیک)، که مخصوصا در پیدا کردن آسیب‌پذیری‌های امنیتی کمک کننده است. ابزارهای مهمی که به صورت فعال نگهداری می‌شوند در این زمینه شامل SAGE، از مؤسسه تحقیقاتی مایکروسافت، KLEE, S2E و Triton است. حل‌کننده‌های SMT که مخصوصا در کاربردهای اجرای نمادین مفید است شامل Z3، STP, Z3str2، و Boolector است.