调整 Z3 量词实例化的指南（使用 SMT-LIB 接口）

Question

我正在尝试调整 z3 以解决机器生成的问题

• 无法满足，
• 包含与证明无关的断言
• 不相关的断言包含量词
• 由于这些不相关的断言，z3 无法找到不可满足性证明（手动删除它们会显示这一点）。

是否有任何一般准则来处理这种情况？

通过命令行选项，我想我可以尝试：

mbqi.id (string) 仅对 id 以字符串开头的量词使用基于模型的实例化（默认值：）

但我不知道如何使用 SMT-LIB 语法将 id 附加到量词。有知道的朋友可以分享一下吗？

Answer 1

这里所说的id只是量化变量的名称。如果你有：

(declare-sort S 0)
(declare-fun gt (S S) bool)

(assert (forall ((inst_a S) (inst_b S))
          (or (gt inst_a inst_b) (gt inst_b inst_a))))

(check-sat)

那么你可以说：

z3 smt.mbqi=true smt.mbqi.id=inst a.smt2

不要忘记使用smt.mbqi=true 来开启 MBQI。如果你使用这个调用，那么 z3 只会在上例中量化变量以inst 开头时实例化一个模式。