显示量化公式

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