z3 - 显示量化出的公式

Question

如何显示量词消除的结果？
z3 似乎对以下输入感到满意

(set-option :elim-quantifiers true)
(declare-fun y () Real)
(simplify (exists ((x Real)) (>= x y)))

但它返回的结果与输出相同。

谢谢

Answer 1

Z3 3.x 具有用于 SMT-LIB 2.0 输入格式的新前端。在新的前端中，该命令simplify并不是 Z3 中所有简化和预处理步骤的“保护伞”。Z3 2.x 中使用的“全能”方法存在几个问题。因此，在 Z3 3.x 中，我们开始使用细粒度方法，用户可以指定策略/策略来解决和/或简化公式。例如，可以写：

(declare-const x Int)
(assert (not (or (<= x 0) (<= x 2))))
(apply (and-then simplify propagate-bounds))

这个新的基础设施正在建设中。例如，Z3 3.2 没有用于在新前端中消除量词的命令/策略。量词消除的命令/策略将在 Z3 3.3 中提供。同时，您可以使用旧的 SMT-LIB 前端来消除量词。您必须提供命令行选项-smtc来强制 Z3 使用旧的前端。此外，旧的前端并不完全兼容 SMT-LIB 2.0。所以，你必须写：

(set-option ELIM_QUANTIFIERS true)
(declare-fun y () Real)
(simplify (exists ((x Real)) (>= x y)))