pySMT SMT-LIB格式詳解如何解析、打印并擴(kuò)展smt2文件parser與script實(shí)戰(zhàn)【免費(fèi)下載鏈接】pysmtpySMT: A library for SMT formulae manipulation and solving項(xiàng)目地址: https://gitcode.com/gh_mirrors/py/pysmtpySMT 是一個(gè)用于 SMT 公式操作與求解的 Python 庫而SMT-LIB 格式即 smt2 文件正是它與各類求解器之間的通用語言。本文帶你從零看懂 SMT-LIB 語法并實(shí)戰(zhàn)演示如何用 pySMT 的smtlib模塊解析、打印、擴(kuò)展smt2 文件——即使你是第一次接觸 SMT也能快速上手。 什么是 SMT-LIB 格式SMT-LIB 2.6 是一套基于LISP 風(fēng)格 S 表達(dá)式的文本標(biāo)準(zhǔn)幾乎所有 SMT 求解器Z3、CVC5、MathSAT、Yices 等都支持它。一個(gè)典型的 smt2 文件由若干命令組成pySMT 自帶的示例見 examples/smtlib.py就是一個(gè)很好的入門樣本(set-logic QF_LIA) (declare-fun p () Int) (declare-fun q () Int) (declare-fun x () Bool) (define-fun .def_1 () Bool (! (and x y) :cost 1)) (assert ( x ( p q))) (check-sat) (push) (assert ( y ( q p))) (check-sat) (pop)核心命令速查表命令作用(set-logic ...)聲明邏輯如QF_LIA、QF_BV(declare-fun x () Int)聲明變量 / 函數(shù)(define-fun f (...) ...)定義可復(fù)用的函數(shù)(assert expr)添加斷言約束(check-sat)請(qǐng)求求解返回sat/unsat(get-model)輸出滿足約束的模型(push)/(pop)增量求解的斷言上下文類似棧(! expr :key value)注解為表達(dá)式附加元信息理解這張表后任何 smt2 文件對(duì)你來說都只是一堆帶括號(hào)的命令。? pySMT 解析 smt2 的三層 APIpySMT 把 SMT-LIB 處理封裝在 pysmt/smtlib/ 模塊中按粒度由淺入深分三層你的需求推薦 API所在位置讀文件直接拿到公式read_smtlib(fname)pysmt/shortcuts.py拿到可迭代的命令序列SmtLibParser.get_script()pysmt/smtlib/parser/parser.py逐條處理原始命令流get_command_generator()同上最省事的方式只需一行from pysmt.shortcuts import read_smtlib f read_smtlib(demo.smt2) # 自動(dòng)取腳本中最后一條斷言對(duì)應(yīng)的公式 print(f)注意pySMT 讀取時(shí)還會(huì)透明支持.bz2壓縮文件解析器內(nèi)置了open_幫助函數(shù)這對(duì)處理大量基準(zhǔn)測(cè)試集非常方便。如果追求極致解析速度還可設(shè)置環(huán)境變量PYSMT_CYTHONtrue讓解析器自動(dòng)走 Cython 加速路徑見 pysmt/smtlib/parser/init.py。 從 smt2 到 Python 公式parser 實(shí)戰(zhàn)想更精細(xì)地控制解析過程可以直接使用SmtLibParserfrom pysmt.smtlib.parser import SmtLibParser parser SmtLibParser() script parser.get_script_fname(demo.smt2) # 內(nèi)部走 Tokenizer → 命令表 → SmtLibScript for cmd in script: print(cmd.name) # set-logic / declare-fun / assert ... f script.get_last_formula() # 考慮 push/pop 后的最終公式解析管線可以概括為三步Tokenizer按 LISP 規(guī)則把文本切成 token支持交互模式逐字符讀取見 parser.py 中的Tokenizer類SmtLibParser查內(nèi)部命令表self.commands把每條命令解析成SmtLibCommand對(duì)象表達(dá)式則交給get_expression遞歸構(gòu)造 pySMT 的FNodeSmtLibScript把命令序列收集成腳本對(duì)象見 pysmt/smtlib/script.py并提供實(shí)用工具script.contains_command(check-sat)—— 檢查某命令是否存在script.count_command_occurrences(assert)—— 統(tǒng)計(jì)出現(xiàn)次數(shù)script.filter_by_command_name(declare-fun)—— 篩選某類命令script.get_strict_formula()—— 假設(shè)只有一份公式的嚴(yán)格模式遇到push/pop或多次check-sat會(huì)拋異常script.get_last_formula()—— 常規(guī)模式返回腳本執(zhí)行完后的最終公式。怎么選大多數(shù)基準(zhǔn)文件是一堆斷言 一次check-sat兩個(gè)方法結(jié)果相同增量腳本則必須用get_last_formula()。? 如何把公式打印回 SMT-LIB 格式反序列化同樣簡(jiǎn)單pySMT 的打印器 pysmt/smtlib/printers.py 中的SmtPrinter通過樹遍歷把FNode還原成 SMT-LIB 語法import sys script.serialize(sys.stdout, daggifyTrue) # 輸出 smt2 文本其中daggify參數(shù)控制輸出形態(tài)daggifyTrueDAG 模式把重復(fù)子表達(dá)式提取為.def_0、.def_1… 等define-fun文件更短、求解器更快daggifyFalse樹模式每次展開完整表達(dá)式可讀性更好。單個(gè)公式也可以直接f.serialize()得到 SMT-LIB 字符串。整個(gè)讀入 → 變換 → 輸出閉環(huán)正是 SMT-LIB/parse_and_print.py 基準(zhǔn)腳本在做的事。? 注解annotationssmt2 里的隱藏信息SMT-LIB 標(biāo)準(zhǔn)允許用!給表達(dá)式附加元數(shù)據(jù)例如示例中的(! (and x y) :cost 1)。pySMT 用 pysmt/smtlib/annotations.py 中的Annotations統(tǒng)一管理這些注解ann script.annotations print(ann.all_annotated_formulae(cost)) # 列出所有帶 :cost 的公式這是做模型檢查、加權(quán)約束等自定義格式時(shí)的推薦擴(kuò)展方式——不破壞 SMT-LIB 兼容性的同時(shí)傳遞額外語義。 進(jìn)階擴(kuò)展解析器支持自定義 smt2 命令如果你的輸入文件包含 pySMT 不認(rèn)識(shí)的命令比如模型檢查領(lǐng)域的(init ...)、(trans ...)標(biāo)準(zhǔn)解析器會(huì)拋出UnknownSmtLibCommandError。此時(shí)只需繼承SmtLibParser并注冊(cè)新命令from pysmt.smtlib.parser import SmtLibParser class TSSmtLibParser(SmtLibParser): def __init__(self, envNone, interactiveFalse): SmtLibParser.__init__(self, env, interactive) self.commands[init] self._cmd_init # 注冊(cè)新命令 self.commands[trans] self._cmd_trans del self.commands[check-sat] # 刪除不適用的命令 self.interpreted[next] self._operator_adapter(self._next_var) # 注冊(cè)新算子完整示例含符號(hào)遷移系統(tǒng)的(init)、(trans)、(next)處理在 examples/smtlib.py 中可以完整閱讀對(duì)應(yīng)的回歸測(cè)試是 pysmt/test/smtlib/test_parser_extensibility.py。擴(kuò)展三要點(diǎn)新命令注冊(cè)進(jìn)self.commands處理函數(shù)接收 token 流、調(diào)用self.get_expression(tokens)取表達(dá)式新算子注冊(cè)進(jìn)self.interpreted_operator_adapter幫你處理變參不需要的命令直接del遇到時(shí)會(huì)顯式報(bào)錯(cuò)而不是靜默忽略。 真實(shí)的 smt2 基準(zhǔn)文件在哪里想練手項(xiàng)目倉庫自帶了一個(gè)小型基準(zhǔn)測(cè)試庫按邏輯分類存放了大量.smt2.bz2文件pysmt/test/smtlib/fuzzed/覆蓋QF_BV、QF_LIA、QF_UFLRA等 20 個(gè)邏輯的 fuzzing 測(cè)試集pysmt/test/smtlib/omt/多目標(biāo)優(yōu)化OMT擴(kuò)展格式樣例如clique.smt2、shortpath.smt2pysmt/test/smtlib/small_set/各邏輯的精挑小樣例如QF_LIA/prp-20-46.smt2.bz2。批量處理這些文件可以參考 SMT-LIB/parse_all.py——它用multiprocessing并行解析整個(gè)目錄并輸出耗時(shí)統(tǒng)計(jì)是非常實(shí)用的模板腳本。另外pySMT 還支持HR 格式Human-Readable更接近數(shù)學(xué)書寫習(xí)慣的表達(dá)式由 pysmt/parsing.py 負(fù)責(zé)解析可與 SMT-LIB 格式互補(bǔ)使用。? 快速總結(jié)三步搞定 smt2讀一行read_smtlib()拿公式或SmtLibParser().get_script_fname()拿完整命令流寫script.serialize(stream, daggifyTrue)或formula.serialize()還原成 smt2擴(kuò)繼承SmtLibParser往commands/interpreted表里注冊(cè)你的自定義命令與算子。想親手試一遍克隆倉庫后運(yùn)行示例腳本即可git clone https://gitcode.com/gh_mirrors/py/pysmt cd pysmt pip install -e . python examples/smtlib.py掌握 parser 與 script 這兩個(gè)核心對(duì)象后無論處理求解器輸出、生成基準(zhǔn)測(cè)試還是擴(kuò)展私有格式你都已經(jīng)具備了在 pySMT 生態(tài)里自由操作 SMT-LIB 文件的全部能力?！久赓M(fèi)下載鏈接】pysmtpySMT: A library for SMT formulae manipulation and solving項(xiàng)目地址: https://gitcode.com/gh_mirrors/py/pysmt創(chuàng)作聲明：本文部分內(nèi)容由AI輔助生成（AIGC），僅供參考