从Z3最新版本Z3-4.4.1的RELEASE_NOTES开始，已经支持浮点理论。我已经成功地以离线方式对其进行了测试。但是，在我目前的项目中，需要在C++ API中使用Z3，阅读相关文档和源代码后，我没有找到任何浮点理论的API函数。 C++ API是否支持Z3的浮点理论？
尽管如此，也许我可以将我的约束集写入一个 smt 格式的文件，然后使用 Z3 API 来解析这个文件。但是，这是我最后的选择。
最佳答案
C++ API 本质上是 C API 的包装器，用于常见的习语，例如，自动化引用计数。两者可以而且应该一起使用。例如，C-API example显示如何通过调用 C 函数 Z3_mk_bvsrem 创建带符号的位 vector 余数项(没有 C++ 函数)。同样的技巧适用于所有浮点项；只需通过各自的 C 函数创建它们，然后将它们保存在 (C++) z3::expr 对象中。
关于c++ - 在 C++ API 中支持 Z3 的浮点理论，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/33302554/