顯示量化公式

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