早在旧天（即最后一年），我们曾经可以使用插件理论作为一个黑客来实现简单化者定制。 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的）提供所需的。 如果一些外部开发者的兴趣在实施和维护这个功能将是巨大的。 我敢肯定，这将有利于很多用户。
文章来源: Custom simplifiers
