z3 - 显示量化的公式

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

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

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

谢谢

最佳答案

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)))

关于z3 - 显示量化的公式，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/8138045/