Trivial Hash Collision between 0. and 0.F

[zwimer]

The following ASTs have the following hashes.
(_ +zero 8 24) has a hash of 1098364533
(_ +zero 11 53) has a hash of 1098364533

The same collision happens for -0. and -0.F.

Is this just two 1/(2^32) hash collisions? Or do the hashes not consider the sort? Or is this a bug?

[zwimer]

I reported this as an issue since it feels like a bug as Z3_get_ast_hash reports:

Return a hash code for the given AST. The hash code is structural. You can use Z3_get_ast_id interchangeably with this function.

Likewise, the identical function Z3_get_ast_id reports:

Return a unique identifier for t. The identifier is unique up to structural equality. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.

Docs linked here.

[nunoplopes]

Of course hashes are not unique, and there are collisions. Identifiers are unique (just a bumped counter).
The question is: do you observe a performance issue because of this collision in practice? If so, can you produce a repro?

Of course the hashing function can always be improved. But there's a tradeoff between speed and quality. Changing the hashing function is not something to be done lightly.
Please reopen if you have data that backs up a change.

[wintersteiger]

I think function type parameters (to _) are not hashed. Like Nuno said, that's not a problem in practice, but the documentation promises those IDs to be unique, for which we would have to take parameters into account, or clean up the docs.

[NikolajBjorner]

(_ +zero 8 24)
(_ +zero 11 53)
Have different sorts, the same function symbol. The sorts are not used when computing hashes.

[NikolajBjorner]

I assume you can use the id instead of the hash.

[zwimer]

@NikolajBjorner What ID are you referring to? According to the docs Z3_get_ast_id are the same thing Z3_get_ast_hash:

Return a hash code for the given AST. The hash code is structural. You can use Z3_get_ast_id interchangeably with this function.

Also, would you like me to make a PR noting that sorts are not considered 'structural', at least by the hash docs' definition of structural?

[NikolajBjorner]

I assume you can use Z3_get_ast_id instead of Z3_get_ast_hash.

[NikolajBjorner]

I changed the hash function to use the sort as well so now you get two different hash values for your example.
Hashes are still not unique. If you have 65K nodes you should be very likely to get a hash collision but there are never collisions on the value of get_ast_id.

[zwimer]

Ah, thanks!