Как отобразить конкретное ограничение unsat, а не все ядро ​​(Z3, Python)

Как я могу перечислить только конкретные результаты ограничений из моего ненасыщенного ядра? У меня много условий, и печать всего ядра не печатает все. Я читал, что это можно сделать с помощью команд assert_and_track и unsat_core. Я нашел несколько примеров, но они не работают. Есть ли опыт в этом?

s.assert_and_track(A > B, 'p1')
s.assert_and_track(B > C, 'p2')
if s.check() == sat:
  print('ok')
else:
  c = s.unsat_core
  print(c) <- this print all core

Итак, как напечатать только p1 или p2 (только результат true/false)? например p2 = false, или может отображаться так, как отображается в режиме print(c), но только для p1.


z3 smt z3py
person z3_test    schedule 22.10.2015    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Самый простой способ добиться этого — просто сохранить карту меток в ограничениях, для этого примера мы можем сделать

M = {}
M['p1'] = (A > B)
M['p2'] = (B > C)
M['p3'] = (C > A)

так что позже мы можем напечатать ядро ​​с точки зрения этих ограничений, например, следующим образом

core = s.unsat_core()
for e in core:
    print(M[str(e)])

Конечно, это также сработает, если вы хотите распечатать только некоторые записи вместо всех.

person Christoph Wintersteiger    schedule 23.10.2015
comment
Это не работает. Сначала я должен из-за синтаксической ошибки исправить print M[str(e)] на print (M[str(e)]), а затем я получаю TypeError: 'method' object is not iterable в строке for e in core:. Также попробуйте отобразить его напрямую с помощью print (M['p1']), но это отображение A > B. Поэтому я пытаюсь преобразовать его в логическое значение print (bool(M['p1'])), но этот вывод всегда соответствует истине, независимо от того, какие условия (‹ › ==) я устанавливаю. - person z3_test; 25.10.2015
comment
Похоже, вы используете Python 3.x, а я использую 2.x; Мне придется обновить пример, чтобы он работал с 3.x. - person Christoph Wintersteiger; 25.10.2015
comment
Я обновил пример и исправил другую проблему Python 3.x API Z3. Пример отлично работает с моим Python 3.4.3 в Windows. Вы используете старую версию Z3 или Python? - person Christoph Wintersteiger; 26.10.2015
comment
Python v3.5, Z3 v4.4.1 — оба x64. У меня есть в моем тесте небольшая опечатка unsat_core должна быть unsat_core() теперь это без ошибок, но все еще нет вывода. Если я использую объект прямой печати print (M['p1']), я получаю на выходе A > B - person z3_test; 26.10.2015