3

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

但是，理论界面尚未更新。理论仍然是从上下文中创建的，据我所知，从来没有明确地附加到求解器上。

人们可能认为从上下文创建的理论将始终附加到从上下文创建的所有求解器，但根据我们的经验，情况似乎并非如此。相反，用户定义的理论似乎被完全忽略了。

Z3_solvers 与s组合的确切状态是Z3_theory什么？

4

1 回答 1

3

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

在当前的 Z3 中，我们有许多不同的求解器。最旧的（在文件夹中实现src/smt）称为smt::context. 理论插件实际上是这个旧求解器的扩展。我们说它smt::context是一个通用求解器，因为它支持许多理论和量词。实际上，在 Z3 4.3.1 中，它是唯一可用的通用求解器。但是，我相信它基于一个过时的架构，不足以满足我们为 Z3 计划的新功能。我的计划是将来用基于此处描述的架构的求解器来替换它。此外，我们不再真正工作smt::context了。我们基本上只是在维护它并修复错误。

在我们发布 Z3 源代码后，我想不再需要理论插件支持，因为用户可以在 Z3 代码库中添加他们的扩展。然而，这种观点过于简单，因为它阻止了用户使用不同的编程语言编写扩展。因此，目前的计划是最终为新求解器提供理论插件，最终将在 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）副本的功能一起使用等。如果有人对这个接口非常感兴趣，我会在它上面投资周期（备注：我们有只有少数用户使用理论插件）。我对此并不感到非常兴奋，因为计划最终将替换smt::context.

于 2012-11-29T07:36:39.713 回答