Microsoft Z3命名断言 [英] Microsoft Z3 naming assertions

问题描述

我需要在我的z3模型中命名一些断言，以便它能够生成非饱和核.

I need to name some assertions im my z3 model so that it is able to generate unsat cores.

我可以这样手动进行:

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

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

I just need to do it using the .NET API directly.

有什么帮助吗?

推荐答案

Z3不直接通过.NET API支持此功能.相反，应该创建一个布尔常量(名称，例如x)，然后可以使用该常数来声明条件约束，例如

Z3 does not support this directly through the .NET API. Instead, a Boolean constant should be created (the name, e.g., x), which can then be used to assert conditional constraints, e.g.,

solver.AssertAndTrack(constraint, x);

然后将约束命名为x，并且该常数用于在unsat内核中引用它. 有关Python中的示例，另请参见其他问题； .NET API中的策略相同，只是函数名称略有不同.

The constraint is then named x and this constant is used to refer to it in the unsat cores. For an example in Python, see also this other question; the strategy is the same in the .NET API, only the function names differ slightly.

这篇关于Microsoft Z3命名断言的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！