【发布时间】：2014-01-27 04:14:03
【问题描述】：
我对许多 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）。
不幸的是，通过定义函数和类型，脚本需要诸如未解释函数之类的理论，因此需要QF_ABV以外的逻辑（甚至QF_AUFBV由于类型）。我对 SMT 求解器的经验表明，应指定可接受的最低逻辑以获得最佳求解时间。此外，尚不清楚我是否可以按照我的意愿在编程上下文（例如 OCaml、Python、C）中重用我的 SMT-LIB 脚本。最后，由于缺少高阶函数，以及我无法访问par 导致代码重复，该脚本有点冗长。
因此，尽管已经实现了我的技术目标，但我认为 SMT-LIB 可能是错误的方法。是否有更自然的途径与 Z3 交互来实现我的 x86 指令描述/QF_ABV 翻译方案？ SMT-LIB 脚本是否可以在这些途径中重复使用？例如，您可以构建“自定义 OCaml 顶级”，即带有“刻录到其中”的脚本的解释器。像这样的东西可能很好。或者我是否必须在通过理论扩展（C DLL）与 Z3 交互的程序中用另一种语言重新实现功能？这里最好的选择是什么？
【问题讨论】：
标签： z3