问题描述
我需要在我的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命名断言的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！