z3 - 将理论插件与求解器一起使用

Z3的最新版本已将Z3_context和Z3_solver的概念解耦。 API主要反映了这些变化；例如push在上下文中已弃用，并重新指定为以求解器作为额外参数。

但是，理论接口(interface)尚未更新。理论仍然是根据上下文创建的，据我所知，它们从未明确附加到求解器上。

可以认为，根据上下文创建的理论将始终附加到根据上下文创建的所有求解器中，但是从我们的经验来看，事实并非如此。相反，用户定义的理论似乎被完全忽略了。
Z3_solver与Z3_theory组合的确切状态是什么？

最佳答案

理论插件是很久以前引入的(2.8版)，此后Z3发生了很大变化。
在Z3 4.x中认为它们已弃用。它们仍然可以与旧的API一起使用，但不能与新功能一起使用，尤其不能与Z3求解器对象(Z3_solver)一起使用。

在当前的Z3中，我们有许多不同的求解器。最旧的(在src/smt文件夹中实现)称为smt::context。理论插件实际上是这个旧求解器的扩展。
我们说smt::context是通用解算器，因为它支持许多理论和量词。
实际上，在Z3 4.3.1中，它是唯一可用的通用求解器。
但是，我认为它基于过时的架构，不足以满足我们为Z3计划的新功能。我的计划是将来使用基于here描述的体系结构的求解器替换它。
而且，我们不再真正使用smt::context了。我们实质上只是维护它并修复错误。

在发布Z3源代码之后，我以为不再需要理论上的插件支持，因为用户可以在Z3代码库中添加其扩展名。但是，此 View 过于简单，因为它阻止用户使用不同的编程语言编写扩展。
因此，当前的计划是最终为新的求解器提供理论插件，并将最终在Z3中提供。目标是拥有一个API，例如:

  Z3_solver Z3_mk_mcsat_solver(Z3_context ctx, Z3_mcsat_ext ext);

该API将使用给定的扩展名ext创建一个新的求解器对象。

同时，我们还可以使用以下功能扩展API:

  Z3_solver Z3_mk_smt_solver(Z3_context ctx, Z3_theory t);

这将使用给定的理论插件基于smt::context创建一个新的求解器对象。
这个解决方案从概念上讲很简单，但是要实现它，需要很多“管道”。
我们必须调整Z3_theory对象，解决一些限制，以防止理论插件与创建smt::context副本(例如MBQI)的功能一起使用，等等。如果有人对此接口(interface)非常感兴趣，我会为此投资一些周期(备注:理论插件的用户很少。我对此并不感到特别兴奋，因为计划最终将替换smt::context。