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

Question

量化記号消去法の結果を表示するにはどうすればよいですか？
z3は次の入力に満足しているようです

(set-option :elim-quantifiers true)
(declare-fun y () Real)
(simplify (exists ((x Real)) (>= x y)))

ただし、出力と同じように返されます。

ありがとう

Answer 1

Z3 3.xには、SMT-LIB2.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には、新しいフロントエンドで数量詞を削除するためのコマンド/戦術がありません。量化記号消去法のコマンド/戦術は、Z33.3で使用できるようになります。それまでの間、数量詞を削除するために古いSMT-LIBフロントエンドを使用できます。-smtcZ3に古いフロントエンドを使用させるには、コマンドラインオプションを指定する必要があります。さらに、古いフロントエンドはSMT-LIB2.0に完全には準拠していません。したがって、次のように記述する必要があります。

(set-option ELIM_QUANTIFIERS true)
(declare-fun y () Real)
(simplify (exists ((x Real)) (>= x y)))