Почему результат запроса меняется, если прокомментировать промежуточный вызов `(check-sat)`?

При отладке запроса UNSAT я заметил интересную разницу в статусе запроса. Структура запроса:

assert(...)
(push)      ; commenting any of these two calls
(check-sat) ; makes the whole query UNSAT, otherwise it is SAT

assert(...)
(check-sat) ; SAT or UNSAT depending on existence of previous call
(exit)

В запросе нет вызовов pop. Запрос, вызывающий такое поведение, находится здесь.

Идеи почему?

Примечание. На самом деле мне не нужна инкрементальность, она предназначена только для целей отладки. Z3 версия 3.2.


z3 smt
person Ayrat    schedule 30.04.2012    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Это ошибка в одном из механизмов рассуждения квантификаторов. Эта ошибка будет исправлена. А пока вы можете избежать этой ошибки, используя типы данных вместо неинтерпретируемых сортировок и ограничений количества элементов. То есть вы объявляете Q и T как:

(объявить типы данных () ((Q q_accept_S13 q_T0_init q_accept_S7 q_accept_S6 q_accept_S5 q_accept_S4 q_T0_S3 q_accept_S12 q_accept_S10 q_accept_S9 q_accept_all)))

(объявить типы данных () ((T t_0 t_1 t_2 t_3 t_4 t_5 t_6 t_7)))

Приведенные выше объявления по существу определяют два типа «перечисления». С этими объявлениями вы получите непротиворечивый ответ на второй запрос.

person Leonardo de Moura    schedule 30.04.2012