哪裏可以學習有關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。