问Z3枚举排序更新
EN

Stack Overflow用户

提问于 2015-11-20 21:56:34

回答 1查看 174关注 0票数 0

是否可以通过向枚举排序添加(或删除)符号来更新枚举排序？我想要做的是添加一个新的值到符号列表中(见下文)，即使在一个变量，比如"X"，从那个排序中创建之后。

EnumSort eSort = con.mkEnumSort(name,symbols);
SetSort eSetSort = con.mkSetSort(eSort);

如果我创建一个新的枚举排序并获得一个值"v“，那么对于X(成员资格)中的表达式v\，我会得到一个错误"domain sort and parameter do not match”。

发布于 2015-11-20 23:34:43

没有一种方法可以改变排序。您可以创建单个枚举排序，并对在枚举排序上创建的集添加各种范围约束。

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/33828492

复制

相似问题

问Z3枚举排序更新EN