z3 - 在 Z3 中自定义 LIA 量词消除

Question

我正在使用 F# 和 Z3 3.2 API 对 LIA 进行量词消除。

Z3 过去的QUANT_ARITH配置表明使用 Cooper 方法或用于 LIA 量词消除的 Omega 测试。但该选项在 Z3 2.6 中被替换为ELIM_QUANTIFIERS（参见Z3 发行说明）。

想问内部Z3 3.2怎么知道量词消除用什么方法？QUANT_ARITH用户可以像以前一样影响方法的选择吗？

此外，随着策略规范语言的引入，Z3 是否允许我们通过扩展或组合这些方法来自定义量词消除？

Answer 1

量词消除模块被重新实现。新的实现应该更快更正确。最新的 Z3 没有实现 Cooper 的方法或 Omega 测试。您可以在以下位置找到有关 Z3 中使用的实际量词消除过程的更多详细信息：“作为抽象决策过程的线性量词消除，Nikolaj Bjørner，IJCAR 2010”。

关于策略规范语言，我们最终将公开执行量词消除的策略。我们目前正在研究这个基础设施，更多消息即将发布。