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