z3 smt example mini_ic3.py

Question

我已经下载了z3并找到了一个mini_ic3.py程序？我认为它是针对ic3的 - 一个基于归纳不变的形式验证程序。

是否有一些参考论文可以推荐用于理解 Z3 目录中的mini_ic3.py

Answer 1

恐怕没有太多直接描述该特定实现的内容。最好的选择是通读 https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-bounded-model-checking

原始的IC3论文本身也会有所帮助。以下是很好的介绍： http://theory.stanford.edu/~arbrad/papers/Understanding_IC3.pdf