在 C# API 中创建枚举 Z3 常量问题答案

【问题标题】：Create enum Z3 constant issue in C# API在 C# API 中创建枚举 Z3 常量问题
【发布时间】：2018-07-01 04:14:57
【问题描述】：

我在 C# 中有一个枚举：

public enum CustomerType
{
    Premium,
    Gold,
    Regular
}

我创建了一个这样的枚举排序：

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

例如，如何创建与CustomerType.Premium 对应的Z3 常量？

尝试context.MkConst("Premium", enumSort); 会生成一个可以采用任何 CustomerType 值的枚举排序。

【问题讨论】：

标签： c# z3

【解决方案1】：

我不是 Z3 C# 绑定方面的专家，但这里有一个可能会有所帮助的示例：https://github.com/Z3Prover/z3/blob/master/examples/dotnet/Program.cs#L1466-L1501

【讨论】：

【解决方案2】：

我已经做到了这一点：

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

【讨论】：

这对我来说听起来不对，因为符号变量不会附加字符串组件。真的有用吗？
是的，它在我的情况下有效。我想检查断言：“type == CustomerType.Premium AND type == CustomerType.Gold”是否无法满足并且有效。