在Z3中，pull_nested_quantifiers选项是否与simplify一起使用？
在Z3中，pull_nested_quantifiers选项是否与simplify一起使用？
提问于 2012-03-07 00:22:01
我希望将公式中的所有嵌套量词拉到最外层。我希望以下命令能在Z3中工作，但它们不能：
(set-option :pull-nested-quantifiers true)
(simplify (exists ((x Int)) (and (>= x 0)
(forall ((y Int)) (and (>= y 1) (> x y)))))):pull-nested-quantifiers的用途是什么？如何使用SMT-LIB或Z3 API拉取嵌套量词？
回答 1
Stack Overflow用户
回答已采纳
发布于 2012-03-08 03:56:29
在Z3 3.x中，simplify命令仅应用通用的本地简化步骤。“拉嵌套量词”是一个预处理步骤。它将在未来的版本中作为一种战术/策略。SMT3.2在Z3 2.0前端已经有许多内置的战略/战术。下一个版本将有更大的一组策略。它们也将在API中提供。如果你需要一些项目的这个功能，只需给我发一封电子邮件，我会为你做一个非官方的(测试版)版本。
最后，我们有这个预处理步骤，因为如果通用量词没有嵌套(通用)量词，则基于模型的量词实例化MBQI模块工作得更好。您的示例是正确的，因为Z3将消除存在词，并用一个新的常量替换x。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/9587683
复制相关文章
相似问题
腾讯云开发者
