0
我對許多X86指令的行爲進行了精確且有效的描述，它們適用於QF_ABV中的編碼，並直接使用標準求解器（不使用特殊求解策略）求解。我寫了一個SMT-LIB腳本，其界面我的最終目標完全吻合：Z3：是否適合我的應用程序的自定義理論擴展？
X86State，記錄排序描述的x86機器狀態（寄存器和標誌爲bitvectors和內存數組）。X86Instr，排序描述（作爲描述寄存器的ML-像識別聯合，存儲器表達，等等列舉助記符，操作數）- 函數
x86-translate服用x86指令的記錄的X86State和X86Instr，並返回一個新X86State。它對X86Instr進行解碼，並根據給定的X86Instr對輸入X86State的符號效應產生新的X86State。
原型設計很棒：用戶可以輕鬆直接編寫x86。在簡化了使用庫構建的公式之後，所有函數和無關數據類型都將被刪除，並保留QF_ABV表達式。我希望用戶可以簡單地使用(set-logic QF_ABV)和#include我的腳本（唉，既不是SMT-LIB標準也不支持#include）。
不幸的是，通過定義函數和類型，腳本需要諸如未解釋的函數等理論，因此需要除QF_ABV（或甚至由於類型導致的QF_AUFBV）以外的邏輯。我對SMT解決方案的經驗表明，應該爲最佳解決時間指定最低可接受的邏輯。另外，我還不清楚我是否可以按照自己的願望在程序化環境中重用我的SMT-LIB腳本（例如OCaml，Python，C）。最後，由於缺乏高階函數，因此腳本有點冗長，並且我無法訪問導致代碼重複的par。
因此，儘管完成了我的技術目標，但我認爲SMT-LIB可能是錯誤的方法。是否有與Z3交互的更自然的途徑來實現我的x86指令描述/ QF_ABV翻譯方案？在這些途徑中，SMT-LIB腳本是否可以重複使用？例如，您可以構建「自定義OCaml頂層」，即帶有「刻錄到其中」腳本的解釋器。類似的東西可能會很好。或者是否必須在通過理論擴展（C DLL）與Z3交互的程序中以其他語言重新實現該功能？這裏最好的選擇是什麼？