在 Z3 中设置求解器的逻辑（API）

Question

我注意到Z3 C++（和 C）API 允许您提供要使用的逻辑。

我有两个问题在网上查不到答案：

1. 这些应该是标准SMT-LIB 逻辑吗？QF_LRA
2. 这些何时值得提供，即 Z3 何时实际使用此信息

我的上下文主要是 QF，没有 BV，但其他一切都可能，我正在逐步使用 SMT 求解器，并且我始终可以计算出我将在开始时使用的逻辑。

Answer 1

Z3 还将尝试找出逻辑是什么（当使用默认选项运行时），但它没有针对所有理论组合的自定义策略（请参阅default_tropic.cpp和smt_strategic_solver.cpp）。当你不确定 Z3 将决定做什么时，最好预先设定策略，这样如果你尝试使用不符合该逻辑的东西，你就会出错。它还将使用该信息来设置 smt 内核，例如，启用各种预处理器、各种求解器功能以及选择启发式方法（例如，参见smt_setup.cpp）。