Создать постоянную проблему enum Z3 в C # API

Question

У меня есть перечисление в C #:

public enum CustomerType
{
    Premium,
    Gold,
    Regular
}

Я создал сортировку enum, как это:

var enumSort = context.MkEnumSort("CustomerType", "Premium", "Gold", "Regular");

Как создать, например, константу Z3, соответствующую CustomerType.Premium?

Попытка context.MkConst("Premium", enumSort); производит сортировку по перечислению, которая может принимать любое значение CustomerType.

Answer 1

Я не эксперт по привязкам Z3 C #, но вот пример, который может помочь: https://github.com/Z3Prover/z3/blob/master/examples/dotnet/Program.cs#L1466-L1501

Answer 2

Я достиг этого используя:

sort.As<EnumSort>().Consts.First(x => x.FuncDecl.Name.ToString() == "Premium").