Z3 называет пусть привязки в API

Question

Я использую Z3 из API и ищу способ отладки моих ограничений. Мой код компилируется, и Z3 работает с моими ограничениями, но что-то не так с моими ограничениями. Я надеюсь взглянуть на ограничения, которые я дал Z3, чтобы определить, что не так или отсутствует, но я не уверен, как это сделать так, чтобы это было очень читабельно. Проблема заключается в том, что использование таких средств, как SMTLIB_DUMP_ASSERTIONS, не дает значимых имен ни в каких переменных, связанных с let. Поскольку у меня много повторений одних и тех же выражений, почти все привязано к сгенерированной переменной.

Есть ли способ выгрузить файл входных ограничений, где переменные let-bound имеют имя, которое я присвоил? Мне не особо важно, какой формат, но SMTLIB 1 или 2 было бы неплохо.

Answer 1

Нет, вы не можете предоставить имена для автоматического создания переменных на принтерах Z3 AST. Одно из возможных решений - написать собственный принтер AST. В дистрибутиве Z3 у нас есть пример приложения examples/c/test_capi.c. Содержит функцию:

void display_ast(Z3_context c, FILE * out, Z3_ast v) 

Показывает, как реализовать простой принтер AST. Этот пример очень прост, но это отправная точка.