我有许多X86指令的行为的精确和有效的描述，适用于 QF_ABV 中的编码并直接用标准求解器解决（不使用特殊的求解策略） . 我写了一个SMT-LIB脚本，其界面完全符合我的最终目标：
-
X86State，描述x86机器状态的记录排序（寄存器和标志为位向量，内存为数组） . -
X86Instr，描述x86指令的记录排序（枚举助记符，操作数为类似ML的区分联合，描述寄存器，内存表达式等） -
一个函数
x86-translate获取X86State和X86Instr，并返回一个新的X86State. 它解码X86Instr并根据给定X86Instr对输入X86State的符号效果产生新的X86State.
它非常适合原型设计：用户可以轻松直接地编写x86 . 在简化使用库构建的公式之后，将消除所有函数和无关数据类型，留下 QF_ABV 表达式 . 我希望用户可以简单地 (set-logic QF_ABV) 和 #include 我的脚本（唉，既不是SMT-LIB标准也不是Z3支持 #include ） .
不幸的是，通过定义函数和类型，脚本需要诸如未解释函数之类的理论，因此需要除_317699之外的逻辑（或者由于类型而需要 QF_AUFBV ） . 我对SMT求解器的经验决定了应该指定最低可接受逻辑以获得最佳求解时间 . 另外，我还不清楚是否可以在程序化上下文（例如OCaml，Python，C）中重用我的SMT-LIB脚本 . 最后，由于缺少高阶函数，脚本有点冗长，而且我无法访问 par 导致代码重复 .
因此，尽管已经完成了我的技术目标，但我认为SMT-LIB可能是错误的方法 . 是否有更自然的途径与Z3交互以实现我的x86指令描述/ QF_ABV 翻译方案？ SMT-LIB脚本在这些途径中是否可以重复使用？例如，您可以构建"custom OCaml top-levels"，即带有脚本"burned into them"的解释器 . 这样的事情可能会很好 . 或者我是否必须在通过理论扩展（C DLL）与Z3交互的程序中重新实现另一种语言的功能？这里最好的选择是什么？
1 回答
好吧，我不认为人们手工编写.smt2文件 . 这些通常由某些程序自动生成 . 我发现Z3 Python界面相当不错，所以我想你可以尝试一下 . 但是你总是可以用任何语言编写一个简单的.smt2转储程序 .
顺便说一句，您是否计划发布您为X86编写的规范？我真的很感兴趣！