问题描述
Z3 支持 SMT-lib set-logic 语句来限制特定片段。例如，在使用 (set-logic QF_LRA) 的程序中，启用了无量词的线性实数算法。如果启用了多种理论，我认为需要 SAT 是有道理的。但是，我不清楚是否有可能启用单一理论并保证 SAT 永远不会运行，从而将 Z3 完全简化为仅针对该单一理论的求解器。例如，这对于声称某个工具遵守求解器针对给定理论的特定性能界限很有用。
有没有办法在 SMT-lib 中或直接在 Z3 中做到这一点？或者保证禁用 SAT 求解器是不可能的？
解决方法
许多 SMT 求解器基本上实现的 Nelson-Oppen 理论组合算法关键依赖于 SAT 求解器：从某种意义上说，SAT 求解器是解决您的 SMT 查询的引擎，咨询理论求解器以确保它找到的冲突根据理论规则传播/解决。因此，在没有底层 SAT 引擎的情况下谈论 SMT 求解器是不可能的，而且 SMTLib 或我所知道的任何其他工具都不允许您“关闭”SAT。它是整个系统的一个组成部分，不能随意打开/关闭。这是 Nelson-Oppen 的一组不错的幻灯片：https://web.stanford.edu/class/cs357/lecture11.pdf
我想可以构建一个不使用这种架构的 SMT 求解器；但是每个理论求解器本质上都需要嵌入一个 SAT 求解器。因此，即使在那种情况下，也确实不可能提取出“SAT”位。
如果您想精确测量求解器的哪个部分花费了多少时间，最好的办法是对求解器进行检测以收集有关其花费时间的统计信息。即便如此，准确地调用哪些部分属于 SAT 求解器，哪些部分属于理论求解器，哪些部分属于它们的组合也会很棘手。