数式内のネストされたすべての量指定子を最も外側のレベルに移動したいと考えています。次のコマンドが 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 を使用してネストされた量指定子を取得するにはどうすればよいですか?