I was wondering if it is safe to use membership testing with python built-in set type and z3 constants.
Suppose to have the following example:
a = Int('a')
a2 = Int('a')
s = set()
s.add(a)
print(a2 in s)
The last line return True, which is my desired behaviour (when name is the same). However, the __eq__() operator in ExpRef is redefined to return the constraint 'self == other' and so I don't understand where this True come from. Could it happen that the in operator might return True when having two constants with a different name?
__eq__ indeed just returns a constraint, but __bool__ on that constraint returns a boolean that compares whether the two arguments are syntactically equal. So basically __eq__ is overloaded in such a way that a == a2 by itself just creates an equality constraint, but using it in a boolean context actually makes it compare whether a and a2 are syntactically the same. So two constants with the same name will compare equal, but constants with different names would not.
__hash__ is also defined using that same notion of equality. So it's safe to use in sets (or as keys in dicts).