3

http://rise4fun.com/Z3Py/GTYuでPyZ3プログラムを参照してください。の最初の呼び出しはcheck()正常に機能しますが、ソルバーに制約を追加してcheck()再度呼び出すと、一貫性のないモデルが得られます。

sy_i = Bool('sy_i')
s0_v, s1_v, s2_v, sx_v, sy_v = Reals('s0_v s1_v s2_v sx_v sy_v')

c = [s0_v >= 1,
     sx_v >= 1,

     s1_v >= s0_v * sx_v,

     sy_v >= 1,

     Or(Not(sy_i), s1_v == RealVal(0.0)),

     s2_v >= s1_v * sy_v
]

solver = Solver()
solver.add(c)
print solver.check()
print solver.model()

solver.add(True)
solver.check()
print solver.model()

誰かが何が起こっているのか知っていますか？

不安定なZ3バージョンでも同じ結果が得られます。

追加のコンテキスト：

このプログラムは、答えの素晴らしいアドバイスに従って、結合ソルバーnlsatとソルバーを使用するより大きなプログラムを単純化したものです。Z3の実際の算術とデータ型の理論は、それほどうまく統合されていません。bool

この方法は非常にうまく機能しているように見えますが、制約を追加してソルバーを再利用しようとすると、この問題が発生することに注意してください。多分それは解決方法を誤検出しますか？

4

1 に答える 1

2

デフォルトのソルバーオブジェクトSolver()は、基本的にソルバーのポートフォリオです。また、使用パターン（インクリメンタルまたは非インクリメンタル）の検出も試みます。複数check()が実行される場合、ユーザーが「インクリメンタル」モードであると想定し、非線形演算には完全ではない汎用インクリメンタルソルバーを使用します。

Z3に常にを使用させるnlsatには、を使用してソルバーオブジェクトを作成する必要があります。

solver = Tactic('qfnra-nlsat').solver()

そうすれば、、、複数のを使用push()できpop()ますcheck()。ただし、以前の呼び出しnlsatからの作業を「再利用」することはありません。これがスクリプトの新しいバージョンです。check()

于 2013-01-07T17:58:32.890 に答える