1

以下程序使用 master git 分支 (commit 89c1785b) 中的最新版本 Z3 生成无法打印的 Z3 模型（即print solver.model()抛出异常）：

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

为了得到修复（现在），我们必须检索“work-in-progress”（unstable）分支。该修复程序将master在下一个正式版本的分支中提供。要检索unstable分支，我们应该使用：

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

另一种选择是使用print solver.model().sexpr(). 它将使用 Z3 内部打印机而不是基于 Python 的打印机。

关于else_value()，其值可能未由 Z3 指定。它的意思是：它是一个“不在乎”。也就是说，可以使用任何解释来满足该公式。我还修复了 Z3 Python API在未指定None时返回。else_value

于 2012-12-17T23:23:27.203 回答