assert - Microsoft Z3 命名断言

Question

我需要在我的 z3 模型中命名一些断言，以便它能够生成 unsat 核心。

我可以像这样手动执行此操作：

(assert (! (assertion) :named x))

我只需要直接使用 .NET API 即可。

有什么帮助吗？

Answer 1

Z3 不直接通过 .NET API 支持这一点。相反，应该创建一个布尔常量（名称，例如，x），然后可以使用它来断言条件约束，例如，

solver.AssertAndTrack(constraint, x);

然后命名约束，x并使用该常量在未饱和核心中引用它。有关 Python 中的示例，另请参见另一个问题；.NET API 中的策略是相同的，只是函数名称略有不同。