Guideline and/or Minimal Working Examples for Developing New Theory Solvers for Z3

Question

From the many questions previously asked on StackExchange, I understand that the theory plugin is now deprecated in Z3 4.x and one is now expected to write their 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 have missed already available? If not, has anyone written a new theory solver that they can share the code?

Answer 1

There are no official examples or documentation for new theories yet. First, you should decide whether you need an actual theory that is integrated with all the other theories in the smt kernel, or whether your goal can be achieved within a tactic (which might require much less coding effort).

I'm currently working on a theory plugin for floating-point numbers, which is a particularly simple theory because it only translates floating-point constraints to bit-vectors (and then Booleans). This part is not yet in the master branch, but you can see it in the fpa-api branch at src/smt/theory_fpa.cpp/.h (make sure that the right branch is selected on the webpage, otherwise you'll just see stubs that are not implemented yet.)