z3 - Z3 API 中的自定义理论求解器方法发生了什么变化？

Question

我一直在阅读 Nikolai 关于 Z3 工程理论的文章，​​了解如何将自定义决策程序与 Z3 接口。其中提到了几种方法，例如 AssertTheoryAxiom、NewAssignment 和 FinalCheck 等。但是，我无法在http://research.microsoft.com/en-us/um/redmond/projects/z3/namespace_microsoft_1_1_z3.html的最新（新？）Z3 API 中找到它们。有人可以告诉我他们或他们的替代者在哪里吗？2. 在相关说明中，我在界面中看到了几个新概念，例如探针和战术。这些是否在任何地方进行了描述或解释？

Answer 1

当前不推荐使用自定义决策过程的界面。它们仍然可以与旧的求解器 API 一起使用。有关其他信息，请参阅以下帖子：

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

• 自定义简化器

这是已弃用 API 的完整列表。关于战术和探测，请参阅这篇文章，以及有关它的 Z3 教程（Python和SMT 2.0）。