英文:
z3 enumsort exception after version 4.12.0
问题
升级到版本4.12.0后，在函数中再次声明EnumSort时出现了异常。
这是正常现象还是一个缺陷？
英文:
After I upgrade z3 to version 4.12.0, exception happened when declarating an EnumSort again in a function.
Is it normal or a defect?
from z3 import *
def enum_decl():
Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
enum_decl()
# invoke again, raise exception of "enumeration sort name is already declared"
enum_decl()
答案1
得分: 1
是的，这是一个故意的更改，于2022年11月19日添加：https://github.com/Z3Prover/z3/blame/e8a38c548235d21c9f075cc9cdbe473fc68ef8bd/src/api/api_datatype.cpp#L108
而且这是可取的。作为更糟糕的例子，考虑以下情况：
from z3 import *
Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
# 使用red/green/blue作为Color的代码
# 稍后再次声明：
Color, (purple, white) = EnumSort('Color', ['purple', 'white'])
# 使用purple/white作为Color的代码
如果允许这样的重复声明，将会导致不一致的状态。在任何z3上下文中，排序名称只有一个命名空间，因此您不能重新定义。而且这样的重新声明很可能是编程错误，所以他们添加了检查以避免错误使用它。
您是否有能够重新声明枚举排序的实际用例？这些声明通常要么在顶层（即一次性）完成，要么在某个类初始化程序中完成；以避免这种冲突。
英文:
Yes, this is a deliberate change, put in on November 19, 2022: https://github.com/Z3Prover/z3/blame/e8a38c548235d21c9f075cc9cdbe473fc68ef8bd/src/api/api_datatype.cpp#L108
And indeed this is desirable. As a worse example, consider:
from z3 import *
Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
# Code using red/green/blue as Color
# Later, declare again:
Color, (purple, white) = EnumSort('Color', ['purple', 'white'])
# Code using purple/white as Color
If you were to allow repetitions like this, you'd have an inconsistent state of affairs. In any z3 context, there's only one namespace for sort names, so you cannot have a redefinition. (At least not without doing a whole lot of internal rewriting.) And such a redeclaration is most likely a programming error anyhow, so they put in a check to avoid mistaken uses of it.
Do you have an actual use case for being able to redeclare an enum-sort? Such declarations are usually either done at the top-level (i.e., once), or in some class-initializer anyhow; to avoid such clashes.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论