z3 - Z3 中求解器的设置逻辑(API)

Question

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

我有两个关于这个的问题，我无法通过在线查看来回答:

1. 这些应该是标准的吗 SMT-LIB logics即 QF_LRA
2. 这些什么时候值得提供，即 Z3 什么时候会实际使用这些信息

我的上下文主要是 QF，没有 BV，但其他一切都可能，我正在逐步使用 SMT 求解器，我总能在一开始就弄清楚我将采用什么逻辑。

Answer 1

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