Z3的最新版本将 Z3_context 和 Z3_solver 的概念分离 . API主要反映了这些变化;例如 push 在上下文中被弃用，并被重新指定为将求解器作为额外参数 .
Z3_context
Z3_solver
push
然而，理论界面尚未更新 . 理论仍然是从上下文创建的，据我所知，从未明确地附加到求解器上 .
人们可能会认为从上下文创建的理论将始终附加到从上下文创建的所有求解器，但从我们的经验来看，似乎并非如此 . 相反，用户定义的理论似乎完全被忽略了 .
Z3_solver 与 Z3_theory 的组合的确切状态是什么？
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 上工作了 . 我们基本上只是维护它并修复错误 .
src/smt
smt::context
在我们发布Z3源代码之后，我想象理论插件支持不再是必需的，因为用户可以在Z3代码库中添加他们的扩展 . 但是，这种观点过于简单，因为它阻止用户使用不同的编程语言编写扩展 . 因此，目前的计划是最终为新解算器提供理论插件，最终将在Z3中提供 . 目标是拥有一个API，例如：
Z3_solver Z3_mk_mcsat_solver(Z3_context ctx, Z3_mcsat_ext ext);
此API将使用给定的扩展名 ext 创建新的求解器对象 .
ext
与此同时，我们还可以使用以下函数扩展API：
Z3_solver Z3_mk_smt_solver(Z3_context ctx, Z3_theory t);
这将使用给定的理论插件基于 smt::context 创建一个新的求解器对象 . 这个解决方案在概念上很简单，但实现它需要很多"plumbing" . 我们必须调整 Z3_theory 对象，修复一些限制，以防止理论插件与创建 smt::context （例如 MBQI ）等副本的功能一起使用 . 如果有人对此界面非常感兴趣，我会在其上投入周期（注释） ：我们只有少数用户使用理论插件） . 我对此并不十分兴奋，因为该计划最终将取代 smt::context .
MBQI
1 回答
理论插件很久以前就引入了（版本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代码库中添加他们的扩展 . 但是，这种观点过于简单，因为它阻止用户使用不同的编程语言编写扩展 . 因此，目前的计划是最终为新解算器提供理论插件，最终将在Z3中提供 . 目标是拥有一个API，例如：
此API将使用给定的扩展名
ext创建新的求解器对象 .与此同时，我们还可以使用以下函数扩展API：
这将使用给定的理论插件基于
smt::context创建一个新的求解器对象 . 这个解决方案在概念上很简单，但实现它需要很多"plumbing" . 我们必须调整Z3_theory对象，修复一些限制，以防止理论插件与创建smt::context（例如MBQI）等副本的功能一起使用 . 如果有人对此界面非常感兴趣，我会在其上投入周期（注释） ：我们只有少数用户使用理论插件） . 我对此并不十分兴奋，因为该计划最终将取代smt::context.