在 Z3 中自定义 LIA 量词消除
我正在使用 F# 和 Z3 3.2 API 对 LIA 进行量词消除。
Z3 曾经有 QUANT_ARITH 配置，表示使用 Cooper 方法或 Omega 测试来消除 LIA 量词。但该选项在 Z3 2.6 中被 ELIM_QUANTIFIERS 取代（请参阅 Z3 发行说明）。
我想问一下内部Z3 3.2如何知道使用哪种方法来消除量词？用户是否可以影响之前像QUANT_ARITH这样的方法的选择？
此外，随着策略规范语言的引入， Z3允许我们通过扩展或组合这些方法来定制量词消除吗？
I'm doing quantifier elimination on LIA using F# and Z3 3.2 API.
Z3 used to have QUANT_ARITH configuration which indicates the use of Cooper's method or the Omega test for LIA quantifier elimination. But that option was replaced by ELIM_QUANTIFIERS in Z3 2.6 (see Z3 release notes).
I want to ask internally how Z3 3.2 knows which method to use for quantifier elimination? Can users affect the choice of method like QUANT_ARITH before?
Furthermore, with the introduction of strategy specification language, will Z3 allow us to customize quantifier elimination by extending or combining these methods?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
重新实现了量词消除模块。新的实施应该更快、更正确。
最新的 Z3 没有实施 Cooper 方法或 Omega 测试。
您可以在以下位置找到有关 Z3 中使用的实际量词消除过程的更多详细信息：
“线性量词消除作为抽象决策程序，Nikolaj Bjørner，IJCAR 2010”。
关于策略规范语言，我们最终将公开执行量词消除的策略。
我们目前正在开发此基础设施，更多消息即将发布。
The quantifier elimination module was re-implemented. The new implementation should be faster and correct.
The latest Z3 does not have a implementation of Cooper’s method or Omega test.
You can find more details about the actual quantifier elimination procedure used in Z3 at:
“Linear Quantifier Elimination as an Abstract Decision Procedure, Nikolaj Bjørner, IJCAR 2010”.
Regarding the strategy specification language, we will eventually expose tactics for performing quantifier elimination.
We are currently working on this infrastructure, more news are coming soon.