z3的自定义理论[关闭]

Question

我正在尝试构建一个弦理论求解器，其中一个想法是在 z3 证明器中编写代码，但这需要了解整个 z3 代码，我想知道是否有关于如何做的教程那？我已经彻底检查了，但我似乎没有找到任何东西。

Answer 1

如果不或多或少地熟悉内部结构，就无法真正将自定义理论与 z3 集成，不幸的是，这个过程并没有得到很好的记录。这不足为奇：Z3 是一个大型的研究 (-y) 项目，其中有许多活动部分。

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

此资源是一篇关于如何理解理论求解器架构的精彩文章：http://theory.stanford.edu/~nikolaj/z3navigate.html

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

祝你好运！