定量化された式を表示する

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で使用された「do-all」アプローチにはいくつかの問題がありました。 したがって、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フロントエンドを使用して数量限定子を削除することができます。 Z3に古いフロントエンドを使用させるには、コマンドラインオプション-smtcを指定する必要があります。 また、古いフロントエンドはSMT-LIB 2.0に完全に準拠していません。だから、あなたは書く必要があります：