z3 - 自定义简化器

Question

回到过去（即去年），我们曾经能够使用理论插件作为实现自定义简化器的黑客手段。Z3 文档甚至包含“程序附件”的示例。

我的问题很简单；有什么方法可以用 Z3 4.x 实现相同的目标？

特别是，我对一种为 Z3 提供外部计算的基本术语评估的方法感兴趣。

Answer 1

理论插件目前在 Z3 4.x 中被标记为已弃用。因此，尽管它们仍可用于实现自定义简化器，但用户将被迫使用已弃用的 API。

在 Z3 4.x 中，自定义简化器应作为战术实现。新的构建系统使扩展可用策略集变得相当容易。我将尝试写一篇关于如何在 Z3 代码库中编写战术的教程。当然，在这种方法中，我们必须编写 C++ 代码。主要优点是该策略将适用于所有前端（C、C++、.Net、Java、Python、OCaml、SMT2）。此外，外部开发人员可以将他们的策略贡献给 Z3 代码库，并且它们将可供所有 Z3 用户使用。

我们还计划支持一个 API，用于根据用户提供的回调创建简化策略。这个 API 将允许用户用他们最喜欢的编程语言编写“自定义简化器”。这个新的 API 在概念上很简单，但需要进行大量“黑客攻击”才能使其在每个前端（C++、.Net、Java、Python、OCaml）中可用。如果某些外部开发人员有兴趣实现和维护此功能，那就太好了。我相信这将使许多用户受益。