How does one extend Z3 with new solvers / theories?

[bollu]

Hello,

I was interested in understanding what the process is to extend Z3's theory, and add additional solvers for existing theories. Googling led me to StackOverflow answers which states that the plugin based architecture is deprecated.

I can't seem to find any up-to-date information about how to extend Z3.

For some context, I'm interested in plugging in isl (integer set library) into Z3 as a new solver for linear / affine constraints, and also expose some of the "extra" functionality that ISL provides, but I have no idea how to start.

Thanks!

[NikolajBjorner]

For isl I would suggest cloning smt/theory_lra.cpp and smt/theory_lra.h.
Remove the code inside and stub it with your own code.
Adding solvers is a significant task, though. Not because of lack of documentation and background material, but mainly as it requires to understand well the invariants the code should maintain.
Primarily everthing is stack-based. The terms that are internalized within a scope level are only valid as long as the scope does not disappear. Theory solvers typically also maintain their own state that has to be properly scoped.
The comments in smt_theory.h provide some guidance about how the solver API is used.

[i-walker]

May I ask @NikolajBjorner , whether that has changed or if a plugin architecture is now available to extend Z3 with new Logics and Theories?

[NikolajBjorner]

Plugins are inside of z3 source code. There is no external way to add theories.

[i-walker]

Thanks :) Are there any plans to change that or a roadmap?