красивая печать Z3 с C API
Есть ли способ напечатать AST в удобочитаемой форме, как в API Python?
Я хотел бы иметь что-то вроде
(x = 3) ^ (f(3) > 2)
Вместо
(and (= x 3) (> (f 3) 2)
Решение
Нет, API Z3 C / C ++ не имеет этой функции. Красивый принтер в Z3 Python API был реализован на Python. Он не является частью основного API. Принтер Z3 Python реализован в файле src/api/python/z3printer.py (увидеть Вот). Реализовать его в C / C ++ можно с помощью нотации, подобной C / C ++.
Другие решения
Других решений пока нет …