从之前在 StackExchange 上提出的许多问题中，我了解到理论插件现已在 Z3 4.x 中弃用，现在人们希望编写自己的理论求解器并从头开始编译 Z3。
但是，我找不到任何关于如何实现此类新理论求解器的指南和/或简单的工作示例。有没有我错过的地方已经可用了？如果没有，是否有人编写了一个新的理论求解器可以共享代码？
目前还没有新理论的官方示例或文档。首先，您应该决定是否需要一个与 smt 内核中所有其他理论相结合的实际理论，或者您的目标是否可以通过某种策略实现（这可能需要更少的编码工作）。
我目前正在研究浮点数的理论插件，这是一个特别简单的理论，因为它仅将浮点约束转换为位向量（然后是布尔值）。这部分还没有在 master 分支中，但是你可以在
src/smt/theory_fpa.cpp/.h的
fpa-api 分支中看到它（确保在网页上选择了正确的分支，否则你'你只会看到尚未实现的存根。）