How to write user plugin for z3

[d1tto]

Hi, I’m a newbie who just started learning SMT and is interested in SMT solver. I want to start by writing my own plugin. I looked at some early z3str code and they used the api that z3 created in api_user_theory.cpp, but those apis have been removed from z3’s code base. How do I write a standalone plugin in the latest version of z3? Can you give me some advice on how to learn z3 code base? Thanks very much!

[NikolajBjorner]

z3str used a deprecated API.

An updated API for plugins is available.

• https://github.com/Z3Prover/z3/tree/master/examples/userPropagator
• https://microsoft.github.io/z3guide/programming/Example%20Programs/User%20Propagator
• https://link.springer.com/chapter/10.1007/978-3-031-24950-1_5

[d1tto]

Thank you very much! This helped me a lot.