在 C++ API 中支持 Z3 的浮点理论

Question

从Z3最新版本Z3-4.4.1的RELEASE_NOTES开始支持浮点理论。我已经成功地离线测试了它。但是在我目前的项目中，Z3需要用到C++ API，看了相关文档和源码后，没有找到任何浮点理论的API函数。 C++ API是否支持Z3的浮点理论？

尽管如此，也许我可以将我的约束集写入一个 smt 格式文件，然后使用 Z3 API 来解析这个文件。但是，这是我最后一次尝试的选择。

Answer 1

C++ API 本质上是 C API 的包装，用于常见习语，例如自动化引用计数。两者可以而且应该一起使用。例如，C-API example 展示了如何通过调用 C 函数 Z3_mk_bvsrem 创建位向量有符号余数项（没有 C++ 函数）。同样的技巧适用于所有浮点项；只需通过各自的 C 函数创建它们，然后将它们保存在 (C++) z3::expr 对象中。