Z3 会支持 AUFBV 吗？
对于以下脚本：
(set-logic AUFBV)
(declare-fun x () (_ BitVec 16))
(declare-const t (Array (_ BitVec 16) (_ BitVec 16)))
(assert (= (select t #x0000) #x0000))
在线 Z3 演示似乎对通话感到满意set-logic，但随后它抱怨各种BitVec和Array. （顺便说一句，无论逻辑名称如何，在线演示似乎都对调用感到满意set-logic，即使是假名，例如(set-logic blarg)。）
SMT-Lib 网站既没有提到 UFBV 也没有提到 AUFBV，但是考虑到它们的无量词对应物（QF_UFBV 和 QF_AUFBV），我希望 Z3 也能支持 AUFBV。
不用说，数组在实践中起着非常重要的作用。鉴于有限性论点，我认为 AUFBV 逻辑应该保持可判定性。很高兴看到 Z3 支持它。
谢谢！
Z3 使用该set-logic命令配置自身。如果 SMT 脚本不包含，set-logic则启用所有理论求解器。如果您set-logic从脚本中删除该命令，那么 Z3 将按预期工作。
正如你所说，AUBFV 逻辑是可判定的。但是，复杂性确实很高（NEXPTIME-complete）。理论上，基于模型的量词实例化 (MBQI) 模块保证 Z3 是此逻辑的决策过程，但由于复杂性高，Z3 在许多脚本中会失败（在没有内存和/或时间的情况下运行）。
逻辑 AUFBV 不在官方支持的逻辑列表中。Z3没有认出来，也没有安装任何理论求解器。因此，要在 Z3 3.1 中使用此逻辑，您不应使用该set-logic命令。
顺便说一句，你真的不需要数组。它们可以使用量词在 UFBV 中编码。在许多情况下，如果使用量词，最好避免使用数组理论。Z3 中的数组理论求解器针对无量词问题进行了优化。
关于诸如 之类的虚假命令(set-logic blarg)，我添加了用于显示警告消息的代码，说明逻辑未被识别，Z3 将使用所有可用的理论。修改将在 Z3 3.2 中可用。我还在官方支持的逻辑列表中包含了 AUFBV。