CODEWITHSUNDEEP
c++logicz3verificationtheorem-proving
user2347029
user2347029

Reputation: 21

Where to learn about z3 theorem prover APIs for c++?

I want to learn z3 APIs for c++ and how to use them in a c++ program. I tried to find a tutorial but couldn't. Where can I learn that from? Any tutorial or something? Thanks.

Upvotes: 1

Views: 2454

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

The Z3 distribution contains an example for the Z3 C++ API. The example is located at examples/c++/example.cpp. You can also find it online here. The Z3 C++ API is just a thin layer on top of the Z3 C API. It basically provides smart pointers for managing Z3 objects, and overloads operators to simplify how expressions are created. You can find documentation for these APIs here.

Remark: it is much easier to learn the Z3 API using Python. A Z3 tutorial based on Python is available here.

Upvotes: 4

Related Questions