Using theory plugins with solvers

Recent versions of Z3 have decoupled the notions of Z3_context and Z3_solver. The API mostly reflects these changes; for instance push is deprecated on contexts and respecified as taking a solver as an extra argument.

The interface for theories has not been updated, however. Theories are still created from contexts, and as far as I can tell, never explicitly attached to solvers.

One could think that a theory created from a context will always be attached to all solvers created from the context, but it seems from our experience that this is not the case. Instead, user-defined theories seem to be ignored entirely.

What is the exact status of the combination of Z3_solvers with Z3_theorys ?

The theory plugins were introduced a long time ago (version 2.8), since then Z3 has changed a lot. They are considered deprecated in Z3 4.x. They can still be used with the old API, but can't be used with new features and in particular with Z3 solver objects (Z3_solver).

In the current Z3, we have many different solvers. The oldest one (implemented in the folder src/smt) is called smt::context. The theory plugins are actually extensions for this old solver. We say smt::context is a general purpose solver as it supports many theories and quantifiers. Actually, in Z3 4.3.1, it is the only general purpose solver available. However, I believe it is based on an obsolete architecture that is not adequate for the new features we are planning for Z3. My plan is to replace it in the future with a solver based on the architecture described here. Moreover, we don't really work on smt::context anymore. We are essentially just maintaining it and fixing bugs.

After we released the Z3 source code, I imagined the theory plugin support was not necessary anymore since users would be able to add their extensions inside the Z3 code base. However, this view is too simplistic since it prevents users from writing extensions in different programming languages. So, the current plan is to eventually have theory plugins for the new solver that will be eventually available in Z3. The goal is to have an API such as:

  Z3_solver Z3_mk_mcsat_solver(Z3_context ctx, Z3_mcsat_ext ext);

This API would create a new solver object using the given extension ext.

In the meantime, we could also extend the API with a function such as:

  Z3_solver Z3_mk_smt_solver(Z3_context ctx, Z3_theory t);

That would create a new solver object based on smt::context using the given theory plugin. This solution is conceptually simple, but there is a lot of "plumbing" needed to make it happen. We have to adjust the Z3_theory object, fix some limitations that prevent theory plugins to be used with features that create copies of smt::context (e.g., MBQI), etc. If someone is very interested in this interface, I would invest cycles on it (remark: we had only a handful of users for the theory plugins). I'm not super excited about it because the plan is to eventually replace smt::context.