问在Z3中自定义LIA量词消除
EN

Stack Overflow用户

提问于 2011-10-15 05:47:57

回答 1查看 430关注 0票数 2

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

Z3过去有QUANT_ARITH配置，指示使用库珀方法或欧米茄检验来消除LIA量词。但在Z3 2.6中，该选项被ELIM_QUANTIFIERS所取代(参见Z3 release notes)。

我想在内部问一下，Z3 3.2是如何知道使用哪种方法来消除量词的？用户会像以前的QUANT_ARITH一样影响方法的选择吗？

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

回答已采纳

发布于 2011-10-19 04:09:15

对量词消除模块进行了重新实现。新的实现应该更快、更正确。最新的Z3没有库珀方法或欧米茄测试的实现。有关Z3中使用的实际量词消除过程的更多详细信息，请访问：“作为抽象决策过程的线性量词消除，Nikolaj Bjørner，IJCAR2010”。

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

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/7773930

复制

相似问题

问在Z3中自定义LIA量词消除EN