显示量化公式

Question

我如何显示量词消除的结果?
Z3似乎对以下输入

很满意

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

，但它返回与输出相同的内容。

谢谢

Answer 1

Z3x为SMT-LIB 2.0输入格式提供了一个新的前端。在新的前端中，命令simplify不是Z3中可用的所有简化和预处理步骤的"保护伞"。在z32中使用的"做所有的"方法。X有几个问题。在z33中。X，我们开始使用细粒度方法，用户可以指定解决和/或简化公式的策略/策略。例如，可以这样写:

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

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

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