.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.49.3.
.TH STP "1" "August 2026" "stp 2.3.3" "User Commands"
.SH "نام (NAME)"
stp \- حل‌کنندهٔ SMT و اثبات‌کنندهٔ سادهٔ قضیه
.SH "توضیحات (DESCRIPTION)"
کاربرد: stp [گزینه‌ها] <input\-file>
.IP
که در آن ورودی بسته به گزینه‌ها و پسوند فایل، SMTLIB1/2 یا CVC است
.SS "مهم‌ترین گزینه‌ها:"
.TP
\fB\-h\fR [ \fB\-\-help\fR ]
نمایش این راهنما
.TP
\fB\-\-version\fR
نمایش شماره نسخه
.SS "ساده‌سازی‌ها:"
.TP
\fB\-\-disable\-simplifications\fR
غیرفعال کردن همهٔ ساده‌سازی‌ها
.TP
\fB\-w\fR [ \fB\-\-switch\-word\fR ]
خاموش کردن حل‌کننده در سطح کلمه (wordlevel solver)
.TP
\fB\-a\fR [ \fB\-\-disable\-opt\-inc\fR ]
غیرفعال کردن ساده‌ساز بازنویسی
.TP
\fB\-\-disable\-cbitp\fR
غیرفعال کردن انتشار بیت ثابت (constant bit propagation)
.TP
\fB\-\-disable\-equality\fR
غیرفعال کردن انتشار برابری (equality propagation)
.TP
\fB\-\-size\-reducing\-only\fR
تنها ساده‌سازی‌های کاهش‌دهنده اندازه
.TP
\fB\-\-unconstrained\-variable\-elimination\fR arg (=1)
متغیرهای مقیدنَشده حذف می‌شوند.
.TP
\fB\-\-aig\-rewrite\-passes\fR arg (=0)
تعداد دورهای بازنویسی AIG برای اجرا
.TP
\fB\-\-flattening\fR arg (=0)
فعال‌سازی هموارسازی آگاه از اشتراک‌گذاری برای گره‌های با چندگانگی (arity) بیشتر از ۲
.TP
\fB\-\-rewriting\fR arg (=1)
فعال‌سازی بازنویسی آگاه از اشتراک‌گذاری
.TP
\fB\-\-split\-extracts\fR arg (=1)
ایجاد متغیرهای جدید برای برخی استخراج‌ها (extracts)
.TP
\fB\-\-ite\-context\-simplifications\fR arg (=0)
استفاده از آنچه در یک گره if\-then\-else درست دانسته می‌شود برای ساده‌سازی شاخه‌های درست (true) یا نادرست (false)
.TP
\fB\-\-aig\-core\-simplification\fR arg (=0)
ساده‌سازی هسته گزاره‌ای با AIGها
.TP
\fB\-\-use\-intervals\fR arg (=1)
ساده‌سازی با تحلیل بازه‌ای
.TP
\fB\-\-pure\-literals\fR arg (=1)
لفظ‌های محض (pure literals) جایگزین می‌شوند.
.TP
\fB\-\-always\-true\fR arg (=0)
گره‌هایی که همواره درست هستند (مثلاً تصدیق‌شده‌ها) در سراسر مسئله با true جایگزین می‌شوند
.TP
\fB\-\-merge\-same\fR arg (=0)
استفاده از قواعد ساده جبر بولی برای ترکیب عطف‌ها در بالاترین سطح
.TP
\fB\-\-bit\-blast\-simplification\fR arg (=0)
در میانهٔ ساده‌سازی، تبدیل به AIGها و جستجو برای بیت‌هایی که AIGها تشخیص می‌دهند درست/نادرست یا مشابه گره دیگری هستند، در صورتی که سختی کمتر از این مقدار باشد. مقدار \fB\-1\fR به معنای همیشه است.
.TP
\fB\-\-size\-reducing\-fixed\-point\-limit\fR arg (=0)
اگر تعداد گره‌های غیربرگ کمتر از این مقدار باشد، ساده‌سازی‌های کاهش‌دهنده اندازه را تا رسیدن به نقطه ثابت اجرا کن. مقدار \fB\-1\fR به معنای همیشه است.
.TP
\fB\-\-simplify\-to\-constants\-only\fR arg (=0)
تنها استفاده از ساده‌سازی‌هایی از مجموعهٔ با احتمال افزایش اندازه که گره‌ها را به مقادیر ثابت تبدیل می‌کنند
.TP
\fB\-\-difficulty\-reversion\fR arg (=1)
واگردانی ساده‌سازی‌های افزاینده اندازه در صورتی که مسئله را ساده‌تر نکرده باشند
.SS "گزینه‌های حل‌کننده SAT:"
.TP
\fB\-\-cryptominisat\fR
استفاده از cryptominisat به عنوان حل‌کننده. فقط استفاده از CryptoMiniSat نسخه 5.0 یا بالاتر (پیش‌فرض).
.TP
\fB\-\-threads\fR arg (=1)
تعداد رشته‌ها (threads) برای cryptominisat
.TP
\fB\-\-simplifying\-minisat\fR
استفاده از نسخه simplifying minisat نصب‌شده به عنوان حل‌کننده
.TP
\fB\-\-minisat\fR
استفاده از نسخه minisat نصب‌شده به عنوان حل‌کننده
.SS "گزینه‌های پالایش:"
.TP
\fB\-r\fR [ \fB\-\-ackermanize\fR ]
کدگذاری مشتاقانه اصول بدیهی خواندن آرایه (آکرمن‌سازی)
.SS "گزینه‌های Bit-blasting:"
.TP
\fB\-\-bb\fR.div\-v1 arg (=1)
گونهٔ ۱ کدگذاری تقسیم بدون علامت
.TP
\fB\-\-bb\fR.div\-v2 arg (=1)
گونهٔ ۲ کدگذاری تقسیم بدون علامت
.TP
\fB\-\-bb\fR.div\-v3 arg (=0)
گونهٔ ۳ کدگذاری تقسیم بدون علامت
.TP
\fB\-\-bb\fR.add\-v1 arg (=1)
گونهٔ ۱ کدگذاری جمع
.TP
\fB\-\-bb\fR.add\-v2 arg (=1)
گونهٔ ۲ کدگذاری جمع
.TP
\fB\-\-bb\fR.vle\-v1 arg (=1)
گونهٔ ۱ کدگذاری مقایسه
.TP
\fB\-\-bb\fR.mult\-variant arg (=1)
گونهٔ کدگذاری ضرب بدون علامت
.TP
\fB\-\-bb\fR.mult\-v2 arg (=0)
گونهٔ ۲ کدگذاری ضرب بدون علامت
.TP
\fB\-\-bb\fR.conjoin\-constant arg (=0)
هنگامی که انتشار بیت ثابت در حین ساخت AIG یک بیت ثابت را تشخیص می‌دهد، گره AIG را تصدیق (assert) کرده و در AIG آن را با بیت ثابت جایگزین می‌کند
.SS "گزینه‌های چاپ:"
.TP
\fB\-b\fR [ \fB\-\-print\-stpinput\fR ]
چاپ مجدد ورودی STP در cout
.TP
\fB\-\-print\-back\-CVC\fR
چاپ ورودی در قالب CVC و سپس خروج
.TP
\fB\-\-print\-back\-SMTLIB2\fR
چاپ ورودی در قالب SMT\-LIB2 و سپس خروج
.TP
\fB\-\-print\-back\-SMTLIB1\fR
چاپ ورودی در قالب SMT\-LIB1 و سپس خروج
.TP
\fB\-\-print\-back\-GDL\fR
چاپ قالب گراف AiSee و سپس خروج
.TP
\fB\-\-print\-back\-dot\fR
چاپ قالب گراف dotty/neato و سپس خروج
.TP
\fB\-p\fR [ \fB\-\-print\-counterex\fR ]
چاپ مثال نقض
.TP
\fB\-y\fR [ \fB\-\-print\-counterexbin\fR ]
چاپ مثال نقض به صورت دودویی
.TP
\fB\-q\fR [ \fB\-\-print\-arrayval\fR ]
چاپ arrayval به ترتیب تعریف‌شده
.TP
\fB\-s\fR [ \fB\-\-print\-functionstat\fR ]
چاپ آمار توابع
.TP
\fB\-t\fR [ \fB\-\-print\-quickstat\fR ]
چاپ آمار سریع
.TP
\fB\-v\fR [ \fB\-\-print\-nodes\fR ]
چاپ گره‌ها
.TP
\fB\-n\fR [ \fB\-\-print\-output\fR ]
چاپ خروجی
.SS "گزینه‌های ورودی:"
.TP
\fB\-m\fR [ \fB\-\-SMTLIB1\fR ]
استفاده از تجزیه‌کننده قالب SMT\-LIB1
.TP
\fB\-\-SMTLIB2\fR
استفاده از تجزیه‌کننده قالب SMT\-LIB2
.TP
\fB\-\-CVC\fR
استفاده از تجزیه‌کننده قالب CVC
.SS "گزینه‌های خروجی:"
.TP
\fB\-\-output\-CNF\fR
ذخیره CNF در output_[0..n].cnf.
توجه: متغیرها نمی‌توانند به عقب نگاشت شوند، و مسائلی که فقط با ساده‌ساز پیش‌پردازش حل می‌شوند هیچ CNF تولید نخواهند کرد زیرا حل‌کننده SAT هرگز فراخوانی نمی‌شود
.TP
\fB\-\-output\-bench\fR
ذخیره در قالب bench متعلق به ABC در output.bench
.SS "گزینه‌های خروجی:"
.TP
\fB\-\-exit\-after\-CNF\fR
خروج پس از تولید CNF
.TP
\fB\-g\fR [ \fB\-\-max\-num\-confl\fR ] arg (=\-1)
تعداد تعارض‌هایی که پس از آن حل‌کننده SAT متوقف می‌شود. مقدار \fB\-1\fR به معنای هرگز است.
.TP
\fB\-k\fR [ \fB\-\-max\-time\fR ] arg (=\-1)
تعداد ثانیه‌هایی که پس از آن حل‌کننده SAT متوقف می‌شود. مقدار \fB\-1\fR به معنای هرگز است.
.TP
\fB\-d\fR [ \fB\-\-check\-sanity\fR ]
ساخت مثال نقض و بررسی سلامت آن
.SS "گزینه‌های پنهان:"
.TP
\fB\-\-file\fR arg
فایل ورودی
.SH "همچنین ببینید (SEE ALSO)"
مستندات کامل برای
.B stp
به صورت یک کتابچه راهنمای Texinfo نگهداری می‌شود. اگر برنامه‌های
.B info
و
.B stp
به‌درستی روی سیستم شما نصب شده باشند، دستور
.IP
.B info stp
.PP
باید دسترسی شما را به راهنمای کامل فراهم کند.