3

z3 を 4.1 から 4.3.1 にアップグレードしたところ、smtlib2 入力が変更されたようです。現在、関数/定数宣言は pop ステートメントによって削除されません。

以下は、z3 4.1 (およびその他の SMT ソルバー...) で正常に動作する SMTlib2 入力ですが、z3 4.3.1 ではエラーが返されます: (エラー "行 19 列 25: 無効な宣言、定数 'bs_2' (with the与えられた署名) すでに宣言されています")

(set-option :produce-models true)
(set-option :produce-unsat-cores true)
(set-option :interactive-mode true)
(set-option :print-success false)
(push 1)
(declare-fun bs_1 () Bool)
(push 1)
(declare-fun bs_2 () Bool)
(assert (and  bs_1 (not bs_2)))
(check-sat)
(pop 1)
(push 1)
(declare-fun bs_2 () Bool)
(assert (and  bs_1 (not bs_2)))
(check-sat)
(pop 1)
(pop 1)
(exit)

最後の bs_2 宣言を削除すると、z3 4.3.1 では正常に機能しますが、z3 4.1 では機能しません。プッシュ/ポップの使い方が間違っていますか?

4

1 に答える 1

4

Z3 4.3.1 では、Z3 をより使いやすくするために、SMT-LIB 2.0 の制限の一部を緩和しようとしました。たとえば、when is(+ x 2)の代わりに書くことができるようになりました。宣言は、Z3 4.1 のようにスコープではなくグローバルです。動機は、ユーザーが問題をより簡潔にエンコードできるようにすることでした。次のオプションを使用して、Z3 4.1 のようにスコープ宣言を有効にすることができます(+ x 2.0)xReal

(set-option :global-decls false)

そうは言っても、この変更は、他の SMT ソルバーに慣れているユーザーや、SMT-LIB 標準を説明するマニュアルを読んでいるユーザーにとって、非常に混乱し、直感に反するものであることを理解しています。したがって、デフォルトを に戻します(set-option :global-decls false)。

于 2012-11-20T15:11:03.213 に答える