Непечатаемый Solver.model()

Следующая программа генерирует модель Z3, которую нельзя распечатать (то есть print solver.model() выдает исключение), используя последнюю версию Z3 из главной ветки git (коммит 89c1785b):

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'

Я также могу воспроизвести такое же поведение в онлайн-интерфейсе z3py по адресу http://rise4fun.com/Z3Py/lfQG. Немного больше отладки предполагает, что назначение модели для c является z3.FuncInterp, которое выдает исключение «недопустимый аргумент», когда вы вызываете для него else_value().

Это баг в Z3, или мои ожидания не совсем оправдались? Я ожидал, что всегда должна быть возможность получить else_value() из FuncInterp, иначе это неполная функция, но, возможно, это не всегда правильно?


z3 z3py
person user1861926    schedule 17.12.2012    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Это ошибка в принтере 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(). Он будет использовать внутренний принтер Z3 вместо принтера на основе Python.

Что касается else_value(), его значение не может быть указано Z3. Смысл его: это "все равно". То есть для удовлетворения формулы можно использовать любую интерпретацию. Я также исправил Z3 Python API, чтобы он возвращал None, когда else_value не указано.

person Leonardo de Moura    schedule 17.12.2012