0

有时（或多次）会发生问题如此之大，以至于 Z3 求解器有很多超时。在这种情况下，我认为将问题拆分为更小的子问题会很有好处。

我想专门问一下Theory PluginsZ3中的问题。

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

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

4

1 回答 1

1

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

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

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

于 2013-02-21T00:20:41.410 回答