从之前在 StackExchange 上提出的许多问题中，我了解到该理论 插件现在在 Z3 4.x 中已被弃用，现在期望编写自己的理论求解器并从头开始编译 Z3。
但是，我找不到关于如何实现此类新理论求解器的任何指南和/或简单的工作示例。有没有我错过的地方已经可用？如果没有，是否有人编写了可以共享代码的新理论求解器？
最佳答案
尚无新理论的官方示例或文档。首先，您应该决定您是否需要一个与 smt 内核中所有其他理论集成的实际理论，或者您的目标是否可以在一种策略中实现(这可能需要更少的编码工作)。
我目前正在研究 float 的理论插件，这是一个特别简单的理论，因为它只将浮点约束转换为位向量(然后是 bool 值)。这部分还没有在master分支中，但是你可以在src/smt/theory_fpa.cpp/.h的fpa-api分支中看到它(确保在网页上选择了正确的分支，否则你只会看到尚未实现的 stub 。)
关于z3 - 为 Z3 开发新理论求解器的指南和/或最小工作示例，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/26560978/