1

私は、満足できるz3に与える特定の一連のアサーションを持っています。を呼び出すと(check-sat)、z3 は を返しますsat。次に を呼び出し(get-model)、特定の変数 の定義を確認します%%P2_*_143。次のようになります。

(define-fun %%P2_*_143 () JS (NUM 2.0))

この定義を取ると、それをアサーションに変えます

(assert (= %%P2_*_143 (NUM 2.0)))

再度呼び出す(check-sat)と、z3 は を返しますunsat。さらに、その後 を呼び出すと(get-unsat-core)、z3 は を返します()。

私の理解では、z3 によって作成されたモデルはすべての変数に満足のいく割り当てを与えるため、その割り当ても満足できるはずであると主張します。これは間違っていますか、それとも他の場所にバグがありますか?

アサーションのセット全体は、https ://gist.github.com/2966738 の要点にあります。追加されたアサーションは一番下にあります。

Mac OS X 10.7.4 で Z3 バージョン 3.2 を使用しています。http://rise4fun.com/z3のオンライン インターフェイスを使用して、この動作を再現することもできました。

4

1 に答える 1

1

同様のバグが数日前に報告されています。線形実数演算パッケージのモデル構築にバグがあります。バグが修正されました。Z3は、無限小を使用して厳密な不等式を処理します。詳細については、次の論文で説明しています。http: //research.microsoft.com/en-us/um/people/leonardo/cav06.pdf

バグはソルバーの健全性に影響を与えないことに注意してください。つまり、sat/unsatの答えは正しいです。ただし、モデルはそうではありません。モデルが正しくないため、例の2番目のクエリは不飽和です。必要に応じて、この問題を修正する新しいバイナリを利用できるようにすることができます。それまでの間、スクリプトに次のコマンドを追加することで、バグを回避できます。

(declare-fun delta () Real)
(assert (< 0.0000001 delta))
(assert (< delta 0.0000002))
于 2012-06-21T18:23:23.993 に答える