4

我想知道Z3现在能不能给出最小的不能满足的核心。或者是否有人为此开发了良好的支持？有人知道吗？

非常感谢。

4

1 回答 1

4

Z3 产生无法满足的核心，但它们不一定是最小的。

这是一个关于如何提取未饱和核心的示例： http ://rise4fun.com/Z3/smtc_core

您可能还想检查以下问题：

Z3 中的软/硬约束

z3 中 SMT-LIB 2.0 断言上的标签

于 2012-05-11T17:35:34.320 回答