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

Question

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

Z3 曾经有 QUANT_ARITH 配置，表示使用 Cooper 方法或 Omega 测试来消除 LIA 量词。但该选项在 Z3 2.6 中被 ELIM_QUANTIFIERS 取代(参见 Z3 release notes )。

我想问问内部Z3 3.2是怎么知道用什么方法去量词的？用户能否像之前的QUANT_ARITH那样影响方法的选择？

此外，随着 strategy specification language 的引入, Z3 是否允许我们通过扩展或组合这些方法来自定义量词消除？

Answer 1

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

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