How to build a custom user propagator?

[acritten]

Hello,

I am investigating how to write and implement a custom graph theory for Z3. I am fairly new to using Z3 and have been doing a bit of reading about the user propagator functionality, but I am unsure what components I would need to write in order to allow Z3 to reason about graphs. (There's a Python library called NetworkX that contains data structures for graphs, so perhaps I could use that with Z3's Python wrapper?)

Does anyone have any guidance on what the user-propagator in my case would need, or on how to build one in the abstract? I am not sure I understand how to relate the given example in the GitHub documentation to my case.