c++ - 在哪里可以了解用于 c++ 的 z3 定理证明器 API？

Question

我想学习用于 c++ 的 z3 API 以及如何在 c++ 程序中使用它们。我试图找到一个教程，但找不到。我可以从哪里学到这一点？有教程之类的吗？谢谢。

Answer 1

Z3 发行版包含 Z3 C++ API 的示例。该示例位于examples/c++/example.cpp。您也可以在这里在线找到它。Z3 C++ API 只是 Z3 C API 之上的一个薄层。它基本上提供了用于管理 Z3 对象的智能指针，并重载了运算符以简化表达式的创建方式。您可以在此处找到这些 API 的文档。

备注：使用 Python 学习 Z3 API 要容易得多。此处提供了基于 Python 的 Z3 教程。