Ошибка плагина теории Z3

Я создал собственный плагин теории, который на данный момент ничего не делает. Все обратные вызовы реализованы и зарегистрированы, но они просто возвращаются. Затем я считываю набор из declare-consts, declare-funs и asserts, используя Z3_parse_smtlib2_string, и передаю полученный ast в Z3_assert_cnstr. Последующий вызов Z3_check_and_get_model завершается со следующей ошибкой:

Обратный вызов mk_fresh_ext_data не был установлен для пользовательской теории, вы должны использовать Z3_theory_set_mk_fresh_ext_data_callback

Насколько я могу судить, Z3_theory_set_mk_fresh_ext_data_callback не существует.

Используя ту же строку, но без регистрации теоретического плагина, Z3_check_and_get_model возвращает sat и выдает ожидаемую модель.

Я использую версию 4 и 64-битные библиотеки Linux.

Полный пример находится здесь: http://pastebin.com/hLJ8hFf1.


z3
person zanderso    schedule 25.07.2012    source источник
comment
Упрощенный пример ссылка   -  person zanderso    schedule 25.07.2012
comment
То же самое с утверждениями, созданными с использованием API вместо парсинга вызовов: ссылка. Кроме того, проблема, похоже, связана с использованием forall. Когда утверждение не имеет forall, все работает так, как ожидалось.   -  person zanderso    schedule 25.07.2012

Ответы (1)


arrow_upward
1
arrow_downward

Проблема заключается в модуле создания экземпляров квантификатора на основе модели (MBQI). Этот модуль пытается создать копию основного логического механизма. Чтобы создать копию, Z3 должен скопировать каждый теоретический плагин. Он может сделать это для всех встроенных теорий, но не для внешних теорий.

Исходный API-интерфейс теоретического плагина не имел поддержки копирования, поскольку он был реализован до модуля MBQI. Для этого предназначен API Z3_theory_set_mk_fresh_ext_data_callback. Однако по ряду причин он до сих пор не разоблачен. Основная проблема в том, что в Z3 4.0 появился новый API для решателей. Текущий API подключаемого модуля теории несовместим с новым API решателя. Мы изучаем способы их интеграции. В Z3 4.0 теоретические плагины работают только со старым (устаревшим) API-интерфейсом решателя.

Чтобы избежать описанной вами проблемы, вам просто нужно отключить модуль MBQI. Вы можете сделать это, установив MBQI=false при создании Z3_context. В C вы можете сделать это, используя следующий фрагмент кода.

Z3_config cfg; 
Z3_context ctx;
cfg = Z3_mk_config();
Z3_set_param_value(cfg, "MBQI", "false");
ctx = Z3_mk_context(cfg);

Это также объясняет, почему ваш плагин работает с формулами без квантификаторов. Модуль MBQI не используется для такого рода формул.

person Leonardo de Moura    schedule 25.07.2012
comment
Спасибо! Итак, на данный момент, похоже, я могу использовать теоретические плагины или квантификаторы, но не то и другое одновременно. Это точно? (После установки MBQI в false приведенный выше пример больше не вызывает ошибку, но все, что я пробовал с квантификатором, возвращает неизвестное.) Кроме того, есть ли где-нибудь учебник для нового API решателя/тактики? - person zanderso; 25.07.2012
comment
Вы по-прежнему можете использовать квантификаторы, но они будут обрабатываться с использованием только механизма E-matching. Z3 по-прежнему может отображать многие формулы как unsat, используя только E-сопоставление. Однако механизм E-сопоставления вернет unknown для любой разрешимой проблемы. Так ли это в ваших примерах? - person Leonardo de Moura; 25.07.2012
comment
Вот ссылка на онлайн-учебники по тактике: rise4fun.com/z3/tutorial/strategies, rise4fun.com/z3py/tutorial/strategies - person Leonardo de Moura; 25.07.2012
comment
У нас есть онлайн-учебники, описывающие новый API-интерфейс решателя на основе Python API. rise4fun.com/Z3Py/tutorial/guide (раздел Решатели). - person Leonardo de Moura; 25.07.2012