Microsoft Z3 naming assertions

问题:

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

I can do this manually like this:

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

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

any help?

回答1:

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);

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.