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

По сути у меня та же проблема, что и описаннаяВот, Я хочу использовать 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» объекты в будущем, которые будут иметь поддержку для извлечения decls, формул и т. д. (см.Z3 4.0: получить полную модель). Есть ли здесь что-то новое, что я еще не обнаружил в документации?

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

Элизабет