z3 smt пример mini_ic3.py

Question

Я скачал z3 и нашел программу mini_ic3.py? Я думаю, что это для ic3 - программы формальной верификации на основе индуктивного инварианта.

Есть ли справочный документ, который можно порекомендовать для понимания mini_ic3.py в каталоге z3

Answer 1

Боюсь, что нет особого описания этой конкретной реализации.Лучше всего прочитать https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-bounded-model-checking

Оригинальные документы IC3 также помогут.Вот отличное введение: http://theory.stanford.edu/~arbrad/papers/Understanding_IC3.pdf