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()
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.