z3 - z3 的定制理论

Question

关闭。这个问题不满足Stack Overflow guidelines .它目前不接受答案。












想改善这个问题吗？更新问题，使其成为 on-topic对于堆栈溢出。

6 个月前关闭。




Improve this question




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

Answer 1

如果不或多或少地熟悉内部结构，您就无法真正将自定义理论与 z3 集成，不幸的是，此过程并没有得到很好的记录。这并不奇怪:Z3 是一个庞大的研究(-y)项目，并且有许多事件部件。
话虽如此，请参阅来自 Nikolaj 的先前建议的堆栈溢出问题，他是 z3 的主要作者:SMT solver with custom theories?
这个资源是关于如何理解理论求解器的架构的一篇很好的文章:http://theory.stanford.edu/~nikolaj/z3navigate.html
不管你走哪条路，你都会有很多问题。最好的提问地点是 z3 GitHub 站点的“讨论”论坛:https://github.com/Z3Prover/z3/discussions
祝你好运!