z3 支持哪些逻辑? [英] Which logics are supported by z3?

问题描述

是否有 z3 支持的所有理论/逻辑的完整列表?我已经咨询了这个 SMTLIB 教程，它提供了许多逻辑，但我没有相信这份清单是详尽无遗的.z3 文档本身似乎没有指定支持哪些逻辑.

Is there a complete listing of all theories/logics that z3 supports? I have consulted this SMTLIB Tutorial which provides a number of logics, but I do not believe that the list is exhaustive. The z3 documentation itself doesn't seem to specify which logics are supported.

我问是因为我有一个 smt 文件，它无法在 SMTLIB 教程(当用'set-logic'指定时)，但在没有指定逻辑时可以解决.

I ask because I have an smt file which cannot be solved under any of the logics in the SMTLIB Tutorial (when specified with 'set-logic'), but can be solved when no logic is specified.

推荐答案

对于 Z3，我还没有在文档中看到这样的列表，但如果你真的想知道，你可以在源代码中找到它.该列表从 check_logic.cpp 的第 65 行开始.我使用可怕的 awk one-liner 为您解析了列表，并在 2016 年 5 月 20 日(在 Z3 4.4.1 和 4.4.2 之间)找到了这个:

For Z3, I have not seen such a list in the documentation, but you can find it in the source code if you really want to know. The list starts around line 65 of check_logic.cpp. I parsed out the list for you using a scary awk one-liner, and found this as of May 20, 2016 (between Z3 4.4.1 and 4.4.2):

"AUFLIA", "AUFLIRA", "AUFLIRA", "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"、UFBUVIA"、UFBUVIA"", "QF_S"

您可以将其与 SMT-LIB 2 逻辑的官方列表进行比较.

You can compare this to the official list of 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 尚不支持此功能.

Probably more importantly for you is what the "best logic" is for your application. It sounds like you have a large and varying set of problems that you want Z3 to apply whatever tactics it can to. In that case, for now, it's best to leave the logic unspecified. The problem is that in SMT-LIB v2.0 there was no all-encompassing logic -- the largest logic by some standards was AUFNIRA, but this does not include, for example, bit vectors. As a result, CVC4 introduced a non-standard ALL_SUPPORTED logic, and Z3 performs best for some classes of problems when no logic is specified. This shortcoming of the SMT-LIB 2.0 standard is addressed in SMT-LIB 2.5, with a new logic called "ALL". However, this is not yet supported by either Z3 or CVC4.

这篇关于z3 支持哪些逻辑?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！