Показать, какие шаблоны Z3 выводит для квантификаторов

Question

Я хотел бы посмотреть, какие шаблоны Z3 использует для некоторых квантификаторов в моих формулах.

Этот комментарий предполагает, что это возможно, но я не смог найти больше деталей.

Как мне заставить Z3 распечатать эту информацию?

Answer 1

Основываясь на полезном комментарии Кристофа, я обнаружил, что сборка Z3 в режиме отладки (проход -d в mk_make.py во время процесса сборки), а затем прохождения -v:10 В командной строке на полученном Z3 выводятся выведенные шаблоны.