Z3理论插件分裂到子问题
问题描述：
有时（或多次）它发生的问题是如此之大，以至于Z3解算器有很多超时问题。在这种情况下，我认为将问题分解为较小的子问题将会有所帮助。Z3理论插件分裂到子问题
我想在Z3中具体询问Theory Plugins。
假设我有3个变量A,B and C。我正在为他们每个人分配价值。 假设由于我指定的一些限制，分配的值是A=0和B=1。现在，取决于这些A and B的值，C是用另一组方程计算的，可能不是作为约束编码的。在这种情况下，是否可以写一个理论插件，它会说当A and B分配了某些值，然后回调一些函数返回值C。
我在示例目录中看到了一个理论示例，但它对我来说不是很清楚。另外我试图阅读文档。
答
理论插件并不是将问题分解为子问题的理想技术。当我们想要扩展Z3支持的一套理论时，通常会定义一个理论插件。例如，假设我们想要包含一个可以推理字符串的模块。该模块将提供新的解释符号，例如：substring,contains等。 This article描述了用于集合+基数约束的决策过程。这个程序是作为Z3的理论插件实现的。
这就是说，理论插件目前已被弃用。它们在Z3中仍受支持，但它们与新的Solver API不兼容。要使用插件，我们必须使用旧的（不赞成使用的）API。
这里有一些相关的职位描述理论插件API的当前状态Z3：