如何简化使用z3隐藏变量的结果？
如何简化使用z3隐藏变量的结果？
提问于 2012-09-03 16:53:12
我希望隐藏一些变量，并得到简化的结果。
我希望隐藏c1、c2和d，如下所示：
(declare-const v1 Real)
(declare-const v2 Real)
(elim-quantifiers (exists ((c1 Real) (c2 Real)(d Real))
(and (<= c1 10.0) (>= c2 5.0) (>= d 0.0)
(= v1 (+ c1 d))
(= v2 (+ c2 d)))))但是结果看起来很复杂，实际上结果应该是v2>=5.0 & v1<= v2+5.0，我用过(apply ctx-solver-simplify)的代码是
(declare-const v1 Real)
(declare-const v2 Real)
(assert (elim-quantifiers (exists ((c1 Real) (c2 Real)(d Real))
(and (<= c1 10.0) (>= c2 5.0) (>= d 0.0)
(= v1 (+ c1 d))
(= v2 (+ c2 d))))))
(apply ctx-solver-simplify)但是，当我添加apply ....There is ....There error时，脚本不能工作。有人能帮我修一下吗？
回答 1
Stack Overflow用户
回答已采纳
发布于 2012-09-03 19:08:50
您可以使用then策略将量词消除应用于公式，并将上下文简化应用于生成的所有子目标：
(declare-const v1 Real)
(declare-const v2 Real)
(assert (exists ((c1 Real) (c2 Real)(d Real))
(and (<= c1 10.0) (>= c2 5.0) (>= d 0.0)
(= v1 (+ c1 d))
(= v2 (+ c2 d)))))
(apply (then qe ctx-solver-simplify))结果是v2 >= 5.0 and v1 - v2 <= 5.0，它与您想要的非常接近。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/12244701
复制相关文章
相似问题
腾讯云开发者
