Z3 4.3.1 C-API parse_smtlib2_string: откуда получить объявления?

к сожалению, у меня недостаточно репутации, чтобы комментировать ответы на другие вопросы. Поэтому я должен начать новый вопрос.

По сути, у меня такая же проблема, как описано здесь. Я хочу использовать Z3 для инкрементного решения. Для получения ограничений в Z3 я использую строки smtlib2. Все работает отлично для первого набора ограничений, где я могу поместить объявления переменных и т.д. Непосредственно в строку smtlib2. При добавлении дополнительных ограничений постепенно, Z3_parse_smtlib2_string должен получать число предыдущих объявлений (unsigned num_decls), объявления (Z3_func_decl const decls []) и их имена (Z3_symbol const decl_names []). Для строк smtlib интерфейс Parser предлагает функции для извлечения этой информации, например "Z3_get_smtlib_num_decls" и "Z3_get_smtlib_decl". Однако они не работают для строк smtlib2.

Был способ обхода моделей. Для этого решения Z3 должен возвращать модели, включая каждую объявленную переменную ("полные модели"), которая по-видимому не соответствует по умолчанию. Решение этой проблемы описано здесь (для Z3 4.0). К сожалению, это больше не работает для Z3 4.3.

Есть ли у кого-то идея, как я могу получить полные модели от Z3, которые не так сильно зависят от используемой версии? Или еще лучше: есть ли более прямые способы получить декларации в то же время? Около года назад Леонардо де Моура упомянул, что в будущем будут объекты "Parser", которые будут иметь поддержку для извлечения деклараций, формул и т.д. (См. Z3 4.0: получить полную модель). Есть ли что-то новое здесь, которое я еще не обнаружил в документации?

Большое спасибо!

Элизабет

1 ответ

Вы можете использовать подвыражения для сбора вспомогательных объявлений сортировки и функций. Следующий расширенный пример содержит код, который анализирует SMTLIB2, и он должен пересекать возвращаемые выражения для сбора объявлений сортировки и функций. Вы можете просмотреть его здесь

Он использует API C++. Функция collect_decls пересекает выражение и собирает неинтегрированные сортировки и функции (эта функция предполагает, что не существует определяемых пользователем алгебраических типов данных и не пытается их извлечь).

licensed under cc by-sa 3.0 with attribution.