pull_nested_quantifiers選項在Z3中簡化了嗎？

Question

我想將公式中的所有嵌套量詞都拉到最外層。我希望下面的命令在Z3的工作，但他們不這樣做：

(set-option :pull-nested-quantifiers true) 
(simplify (exists ((x Int)) (and (>= x 0) 
          (forall ((y Int)) (and (>= y 1) (> x y)))))) 

什麼是:pull-nested-quantifiers的目的是什麼？我怎樣才能使用SMT-LIB或Z3 API來提取嵌套量詞？

Answer 1

在Z3 3.x中，simplify命令僅應用通用本地簡化步驟。 「Pull-nested-quantifiers」是一個預處理步驟。它將作爲未來版本中的策略/策略。 Z3 3.2在SMT 2.0前端已經有了許多內置策略/策略。下一個版本將會有更多的策略。它們也將在API中提供。如果您需要某個項目的此功能，只需發送一封電子郵件，我將爲您製作非官方（測試版）版本。因爲如果通用量詞不具有嵌套（通用）量詞，基於模型的量詞實例MBQI模塊工作得更好，所以我們有了這個預處理步驟。你的例子沒問題，因爲Z3將消除存在並用新常數代替x。