使用 C++ API 简化 z3 表达式答案

【问题标题】：Simplifying z3 expression using C++ API使用 C++ API 简化 z3 表达式
【发布时间】：2014-03-26 15:14:49
【问题描述】：

我有这样的表情

  z3::expr expr = (exists ((flag Bool))
               (exists ((w Int))
                 (exists ((i Int))
                  (exists ((counter Int))
                      (and (= i (+ x y z))
                           flag
                           (not (= i 0))
                           (= i counter)
                           (not (= w counter))
                           (>= i 1)
                           (= w 0)))))))

我使用 C++ API 进行量词消除和简化。

z3::goal g(ctx);
g.add(expr);
z3::apply_result  result = (qe & simplify & propagate_ineqs)(g);

我已经定义了策略。

我想得到这样的结果：

(or (>= (+ x y z) 1 )
     (<= (+ x y z) -1 ))

但我得到了适合我的应用程序的输出：

 (let ((a!1 (or (<= (+ (* (- 1) x)
                          (* (- 1) y)
                          (* (- 1) z))
                       (- 1))
                   (<= (+ x y z) (- 1)))))
      (and (or (<= (+ x y z) (- 1))
               (>= (+ x y z) 1))
           a!1
           (>= (+ x y z) 1)))

我应该使用什么策略让它按我的意愿工作？

【问题讨论】：

标签： z3

【解决方案1】：

在定义目标之前，我通过在上下文中设置这些选项解决了这个问题：

ctx.set(":pp-min-alias-size", 1000000);
ctx.set(":pp-max-depth", 1000000);

它并没有像我想要的那样简化，而是去掉了“let”，这总比没有好！

【讨论】：