Z3理论插件拆分成子问题

Question

有时(或多次)发生的情况是，问题太大，以至于Z3求解器有很多超时。在这种情况下，我认为将问题分成更小的子问题将是有益的。

我想特别问一下Z3中的Theory Plugins。

假设我有3个变量A,B and C。并且我正在为它们每一个赋值。假设由于我指定的一些约束，分配的值是A=0和B=1。现在，根据A and B的这些值，使用另一组方程计算C，这些方程可能没有编码为约束。在这种情况下，有没有可能编写一个理论插件，当A and B被分配了某些值时，然后回调一些函数来返回C的值。

我在examples目录中看到了一个理论示例，但是它对我来说并不是很清楚。我还试着阅读了文档。

Answer 1

理论插件并不是将问题分解为子问题的理想技术。当我们想要扩展Z3支持的理论集时，通常会定义一个理论插件。例如，假设我们想要包含一个可以对字符串进行推理的模块。此模块将提供新的解释符号，如：substring、contains等。This article描述了集合+基数约束的决策过程。这个过程是作为Z3的一个理论插件实现的。

话虽如此，理论插件目前已被弃用。它们在Z3中仍然受支持，但与新的Solver API不兼容。要使用插件，我们必须使用旧的(不推荐使用的) API。

下面是一些相关的文章，描述了Z3中理论插件API的当前状态：

• Using theory plugins with solvers
• What happened to the custom theory solver methods in the Z3 API?