哪里可以学习有关C++的z3定理证明API？

Question

我想学习C++的z3 API以及如何在C++程序中使用它们。我试图找到一个教程，但不能。 我从哪里可以知道？任何教程或什么？ 谢谢。

Answer 1

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

备注：使用Python学习Z3 API要容易得多。基于Python的Z3教程可用here。