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 求解器，哪些部分属于理论求解器，以及哪些部分属于它们的组合将是棘手的。
【讨论】：