【发布时间】：2016-01-14 12:43:48
【问题描述】：
我注意到Z3 C++（和C）API 允许您提供要使用的逻辑。
我有两个问题无法通过在线查看来回答：
- 这些应该是标准SMT-LIB logics 即
QF_LRA - 这些信息何时值得提供，即 Z3 何时真正使用这些信息
我的上下文主要是 QF 没有 BV，但其他一切都是可能的，我正在逐步使用 SMT 求解器，并且我总能弄清楚我一开始会采用什么逻辑。
【问题讨论】：
【发布时间】：2016-01-14 12:43:48
【问题描述】：
Z3 还将尝试找出逻辑是什么（使用默认选项运行时），但它没有针对所有理论组合的自定义策略（参见 default_tactic.cpp 和 smt_strategic_solver.cpp）。当您不确定 Z3 将决定做什么时，最好提前设置策略，这样如果您尝试使用不符合该逻辑的东西就会出错。它还将使用该信息来设置 smt 内核，例如，启用各种预处理器、各种求解器功能和选择启发式方法（例如，参见 smt_setup.cpp）。
【讨论】：
试试看！
通常它确实会产生很大的不同。设置逻辑意味着求解器将使用专门的策略来求解公式，而不是通过通用循环。 Z3 也会尝试猜测逻辑，但通常最好提前提供。
【讨论】：