我只想打印哈希算法的 CNF (DIMACS) 公式（我不需要 Z3 来实际解决它）。我知道我可以使用策略框架来打印 CNF 公式而不是运行求解器，但是有一种简单的方法来描述哈希，例如
solver.add(SHA256)Z3 文档都没有提到哈希算法，我在网络搜索中找不到任何内容。
您必须自己在 z3 中编写哈希算法，以便它可以处理符号输入。
Z3 理解 smtlib，这是一种低级语言。我建议使用高级语言的界面。如果您熟悉 Haskell，这里有各种 SHA 算法的符号实现，可以作为您的起点：https://hackage.haskell.org/package/sbv-10.7/docs/Documentation-SBV-Examples -加密-SHA.html