STP(1) User Commands STP(1) نام (NAME) stp - حل‌کنندهٔ SMT و اثبات‌کنندهٔ سادهٔ قضیه توضیحات (DESCRIPTION) کاربرد: stp [گزینه‌ها] که در آن ورودی بسته به گزینه‌ها و پسوند فایل، 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 باید دسترسی شما را به راهنمای کامل فراهم کند. stp 2.3.3 August 2026 STP(1)