1

print solver.model()次のプログラムは、マスター git ブランチ (commit 89c1785b) の最新バージョンの Z3 を使用して、印刷できない (つまり、例外をスローする) Z3 モデルを生成します。

x = Int('x')
a = Array('a', IntSort(), BoolSort())
b = Array('b', IntSort(), BoolSort())
c = Array('c', BoolSort(), BoolSort())

e = ForAll(x, Or(Not(a[x]), c[b[x]]))
print e

solver = Solver()
solver.add(e)
c = solver.check()
print c
if c == sat:
    print solver.model()

生成:

ForAll(x, Or(Not(a[x]), c[b[x]]))
sat
Traceback (most recent call last):
  File "z3bug.py", line 16, in <module>
    print solver.model()
  File "src/api/python/z3.py", line 5177, in __repr__
  File "src/api/python/z3printer.py", line 939, in obj_to_string
  File "src/api/python/z3printer.py", line 841, in __call__
  File "src/api/python/z3printer.py", line 831, in main
  File "src/api/python/z3printer.py", line 760, in pp_model
  File "src/api/python/z3printer.py", line 794, in pp_func_interp
  File "src/api/python/z3.py", line 5088, in else_value
  File "src/api/python/z3.py", line 818, in _to_expr_ref
  File "src/api/python/z3core.py", line 2307, in Z3_get_ast_kind
z3types.Z3Exception: 'invalid argument'

http://rise4fun.com/Z3Py/lfQGのオンライン z3py インターフェイスでも同じ動作を再現できます。もう少しデバッグすると、モデルの割り当てcが、z3.FuncInterp呼び出し時に「無効な引数」例外をスローするものであることが示唆else_value()されます。

これは Z3 のバグですか、それとも私の予想が正しくないのでしょうか? 私の期待は、それ以外の場合は完全な関数ではないため、else_value()a のを常に取得できるはずですが、おそらくこれは常に正しいとは限りませんか?FuncInterp

4

1 に答える 1

3

これは、Z3 Python プリンターのバグです。私はバグを修正しました。修正は既に codeplex で入手できます。

http://z3.codeplex.com/SourceControl/changeset/f8014f54c18a

修正を (今) 入手するには、「作業中」( unstable) ブランチを取得する必要があります。修正はmaster、次の公式リリースのブランチで利用できるようになります。unstableブランチを取得するには、次を使用する必要があります。

git clone https://git01.codeplex.com/z3 -b unstable

別のオプションは、を使用することprint solver.model().sexpr()です。Python ベースのプリンターではなく、Z3 内部プリンターを使用します。

についてelse_value()は、Z3 で指定できない場合があります。意味は「ドントケア」です。つまり、任意の解釈を使用して式を満たすことができます。また、Z3 Python API が指定されNoneていない場合に返されるように修正しましたelse_value。

于 2012-12-17T23:23:27.203 に答える