z3 - z3 支持哪些逻辑？

Question

是否有 z3 支持的所有理论/逻辑的完整列表？我咨询过这个SMTLIB Tutorial它提供了许多逻辑，但我认为该列表并不详尽。 z3 文档本身似乎没有指定支持哪些逻辑。

我问是因为我有一个smt文件，在SMTLIB Tutorial中的任何逻辑下都无法解决。 (当用 'set-logic' 指定时)，但可以在未指定逻辑时解决。

Answer 1

对于Z3，我还没有在文档中看到这样的列表，但如果你真的想知道，你可以在源代码中找到它。该列表从 check_logic.cpp 的第 65 行开始.我使用可怕的 awk one-liner 为您解析了列表，并在 2016 年 5 月 20 日(在 Z3 4.4.1 和 4.4.2 之间)发现了这个列表:
"AUFLIA", "AUFLIRA", "AUFNIRA", "LRA", "QF_ABV", "QF_AUFBV", "QF_UFBV", "QF_AUFLIA", "QF_AX", "QF_BV", "QF_IDL", "QF_RDL", "QF_LIA", "QF_LRA", "QF_NIA", "QF_NRA", "QF_UF", "QF_UFIDL", "QF_UFLIA", "QF_UFLRA", "QF_UFNRA", "UFLRA", "UFNIA", "UFBV", "QF_S"
您可以将其与SMT-LIB 2 logics 的官方列表进行比较。 .

对您而言，可能更重要的是您的应用程序的“最佳逻辑”是什么。听起来您有大量不同的问题，您希望 Z3 应用它可以应用的任何策略。在这种情况下，目前最好不要指定逻辑。问题是在 SMT-LIB v2.0 中没有包罗万象的逻辑——某些标准最大的逻辑是 AUFNIRA，但这不包括，例如，位向量。因此，CVC4 引入了非标准的 ALL_SUPPORTED 逻辑，当没有指定逻辑时，Z3 对某些类别的问题表现最佳。 SMT-LIB 2.0 标准的这个缺点在 SMT-LIB 2.5 中得到解决，新逻辑称为“ALL”。但是，Z3 或 CVC4 尚不支持此功能。