z3 - 如何简化使用 z3 隐藏变量的结果？

Question

我希望隐藏一些变量并获得简化的结果。

我想隐藏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 ....有错误时，脚本无法工作。有人可以帮我解决吗？

Answer 1

您可以使用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与您想要的非常接近。