在 Z3 中自定义 LIA 量词消除

Posted 2023-03-28

【中文标题】在 Z3 中自定义 LIA 量词消除

【英文标题】：Customize LIA quantifier elimination in Z3

【发布时间】：2011-10-14 21:47:57

【问题描述】：

我正在使用 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 是否允许我们通过扩展或组合这些方法来自定义量词消除？

【参考方案1】：

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

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

【讨论】：

我还是一头雾水。上面的论文提到了几种量词消除的实现，包括 Cooper 算法和 Omega 测试，但我还没有看到 Z3 中公开的这些选项。论文是在重新实现量词消除模块之前写的吗？

新旧实现在短时间内共存。旧的（包含 Cooper 的方法和 Omega 测试）已于 2010 年 11 月正式删除。