CODEWITHSUNDEEP
z3
dirtyfilthy
dirtyfilthy

Reputation: 53

Workaround for z3 not supporting injectivity

I want to represent a hash function in z3, something like SHA(x). After doing some research, it appears z3 doesn't support injectivity very well, so I can't have a constraint like (and while I realise this isn't strictly speaking true because of collisions, as a heuristic it would be useful for my project)

forall([x, y],Implies(SHA(x)==SHA(y), x==y))

and expect the solver to terminate.

My question is, are there any known best practice workarounds for this problem? For instance, if I added a Implies(SHA(x)==SHA(y), x==y) constraint for every pair of x and y without using a quantifier, would this solve the problem?

Upvotes: 4

Views: 209

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

For uninterpreted functions we use encodings of the form:

Forall([x], inverse_f(f(x)) = x)

so when f is injective, we can introduce a function that realizes the partial inverse on the range of f. The quantified axiom with pairs of equalities is so common that Z3 looks for them and adds the above axiom instead. It gets instantiated for every occurrence of f. Of course, for SHA, which is typically encoded using bit-vectors, introducing an uninterpreted function means that Z3 doesn't use the pure SAT solver. It would in the best case revert to Ackerman encoding, that just re-introduces the original pair-wise encoding.

Upvotes: 4

Related Questions