调整Z3量化器实例的指南（带SMT-LIB接口）。

Question

我正试图在机器产生的问题上调整z3，这些问题是什么？

• 是不满意的。
• 含有与证明无关的论断。
• 不相干的断言中包含了量化的内容。
• 其中z3因为这些不相关的断言而无法找到不满足性证明（手动删除这些断言就可以看出这一点）。

有没有什么通用的准则来处理这种情况？

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

mbqi.id (string) 只对id以string开头的量化器使用基于模型的实例化 (默认： )

但是我没有看到如何使用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 在上面的例子中。