Неудовлетворительные ядра в Z3 Python

Я работаю с Python API Z3, пытаясь включить его поддержку в инструмент исследования, который я пишу. У меня вопрос по извлечению неудовлетворительного ядра с помощью интерфейса Python.

У меня такой простой запрос:

(set-option :produce-unsat-cores true)
(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(check-sat)
(get-unsat-core)
(exit)

Запустив этот запрос через исполняемый файл z3 (для Z3 4.1), я получаю ожидаемый результат:

unsat
(__constraint0)

Для Z3 4.3 я получаю ошибку сегментации:

unsat
Segmentation fault

Это не главный вопрос, хотя наблюдение было интригующим. Затем я изменил запрос (внутри файла) как

(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(exit)

Используя обработчик файлов, я передал содержимое этого файла (в переменной queryStr) в следующий код Python:

import z3
...
solver = z3.Solver()
solver.reset()
solver.add(z3.parse_smt2_string(queryStr))
querySatResult = solver.check()
if querySatResult == z3.sat:
    ...
elif querySatResult == z3.unsat:
    print solver.unsat_core()

Я получаю пустой список от функции `unsat_core ': []. Я неправильно использую эту функцию? Строка документации для функции предполагает, что вместо этого я должен сделать что-то похожее на

solver.add(z3.Implies(p1, z3.Not(0 == 0)))

Однако мне было интересно, можно ли по-прежнему использовать запрос как есть, поскольку он соответствует стандартам SMT-LIB v2.0 (я полагаю), и упустил ли я что-то очевидное.


z3 z3py
person Jon Kotker    schedule 28.01.2013    source источник

Ответы (1)


arrow_upward
8
arrow_downward

Наблюдаемый вами сбой был исправлен, и исправление будет доступно в следующем выпуске. Если вы попробуете «нестабильную» (незавершенную) ветку, вы должны получить ожидаемое поведение. Вы можете получить нестабильную ветку, используя

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

API parse_smt2_string предоставляет только базовую поддержку для синтаксического анализа формул в формате SMT 2.0. Аннотации :named не сохраняются. Мы устраним это и другие ограничения в будущих версиях. А пока мы должны использовать «литералы ответов», такие как p1, и утверждения в форме:

solver.add(z3.Implies(p1, z3.Not(0 == 0)))

В «нестабильной» ветке мы также поддерживаем следующий новый API. Он «имитирует» :named утверждения, используемые в стандарте SMT 2.0.

def assert_and_track(self, a, p):
    """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.

    If `p` is a string, it will be automatically converted into a Boolean constant.

    >>> x = Int('x')
    >>> p3 = Bool('p3')
    >>> s = Solver()
    >>> s.set(unsat_core=True)
    >>> s.assert_and_track(x > 0,  'p1')
    >>> s.assert_and_track(x != 1, 'p2')
    >>> s.assert_and_track(x < 0,  p3)
    >>> print(s.check())
    unsat
    >>> c = s.unsat_core()
    >>> len(c)
    2
    >>> Bool('p1') in c
    True
    >>> Bool('p2') in c
    False
    >>> p3 in c
    True
    """
    ...
person Leonardo de Moura    schedule 28.01.2013
comment
Большое спасибо за невероятно быстрый и подробный ответ, Леонардо. На данный момент я буду использовать первый предложенный подход (с `литералами ответа '). - person Jon Kotker; 29.01.2013