Guidance and / or minimal working examples for developing new theories for Z3
From many of the questions asked earlier on StackExchange, I understand that plugin theory is now deprecated in Z3 4.x and is now expected to write its own theory solver and compile Z3 from scratch.
However, I cannot find any guidelines and / or simple working examples on how to implement such new theory solvers. Is there somewhere that I already missed? If not, has anyone written a new theory solver so they can share code?
source to share
There are no official examples or documentation for new theories yet. First, you have to decide if you need a real theory integrated with all the other theories in the smt core, or if your goal can be achieved in tactics (which may require much less coding effort).
I am currently working on a theory plugin for floating point numbers, which is an especially simple theory because it only converts floating point constraints to bit vectors (and then Booleans). This part is not on master yet, but you can see it in the branch fpa-api
at src / smt / theory_fpa.cpp / .h (make sure the correct branch is selected on the web page, otherwise you will only see incomplete stubs.)
source to share