I just want to print the CNF (DIMACS) formula for a hashing algorithm (I don't need Z3 to actually solve it). I am aware that I can use the tactics framework to print the CNF formula instead of running the solver, but ss there an easy way to describe the hash, like solver.add(SHA256), or do I need to manually encode every step of the hash algorithm?
None of the Z3 docs mentioned hash algorithms and I couldn't find anything a web search.
You have to code the hashing algorithm in z3 yourself, so it can work on symbolic inputs.
Z3 understands smtlib, which is rather a low level language. I’d advise using an interface from a high-level language. If you’re familiar with Haskell, here’s a symbolic implementation of various SHA algorithms that can serve as a starting point for you: https://hackage.haskell.org/package/sbv-10.7/docs/Documentation-SBV-Examples-Crypto-SHA.html