基于z3的定制理论

Question

我正在尝试构建一个字符串理论求解器，其中一个想法是在z3验证器中编写代码，但这需要理解整个z3代码，我想知道是否有关于如何做到这一点的教程？我已经彻底检查过了，但似乎什么也找不到。

Answer 1

如果不或多或少地熟悉内部结构，您就不可能真正地将自定义理论与z3集成在一起，不幸的是，这个过程并没有被很好地记录下来。这并不令人惊讶: Z3是一个大型的研究项目(-y)，并且有许多移动部件。

话虽如此，请参阅z3：SMT solver with custom theories?的主要作者Nikolaj先前的建议中的堆栈溢出问题。

这个资源是一篇关于如何理解理论解决者架构的很好的文章：http://theory.stanford.edu/~nikolaj/z3navigate.html。

不管你走哪条路，你都会有很多问题。问他们最好的地方是z3 GitHub站点的“讨论”论坛：https://github.com/Z3Prover/z3/discussions。

祝你好运！