最新版本Z3 http://z3.codeplex.com解耦了以下概念Z3_context and Z3_solver. The API http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html主要反映了这些变化；例如push在上下文中已弃用，并重新指定为将求解器作为额外参数。
然而，理论界面尚未更新。理论仍然是根据上下文创建的，据我所知，理论从未明确附加到求解器。
人们可能会认为从上下文创建的理论将始终附加到从上下文创建的所有求解器，但根据我们的经验，情况似乎并非如此。相反，用户定义的理论似乎完全被忽略了。
组合的具体状态如何Z3_solvers with Z3_theorys ?
理论插件很久以前就被引入了（2.8版本），从那时起Z3已经发生了很大的变化。
它们在 Z3 4.x 中被视为已弃用。它们仍然可以与旧 API 一起使用，但不能与新功能一起使用，特别是与 Z3 解算器对象一起使用（Z3_solver).
在当前的 Z3 中，我们有许多不同的求解器。最旧的一个（在文件夹中实现src/smt） 叫做smt::context。理论插件实际上是这个旧求解器的扩展。
我们说smt::context是一个通用求解器，因为它支持许多理论和量词。
实际上，在 Z3 4.3.1 中，它是唯一可用的通用求解器。
然而，我认为它基于过时的架构，不足以满足我们为 Z3 规划的新功能。我的计划是将来用基于所描述的架构的求解器替换它here http://research.microsoft.com/en-us/um/people/leonardo/files/mcsat.pdf。
此外，我们并没有真正致力于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 (e.g., MBQI）等。如果有人对这个界面非常感兴趣，我会在上面投入周期（注：我们的理论插件只有少数用户）。我对此并不是很兴奋，因为计划最终会取代smt::context.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
