z3 - 用单向函数扩展“z3”

Question

z3我希望在Python 程序中使用单向函数。我希望 z3 尊重以下属性/策略：

• 如果x = y, 那么f(x) = f(y)
• f是一个可计算的 Python 函数，我可以在x已知时提供
• 如果f(x) = y，尝试通过匹配先前分配的f(*y) = f(x)暗示来解决x = *y（永远不要试图猜测x计算为y）

是否有支持此构造的内置功能或任何其他可能有助于引入它的功能？

标签： z3smtz3py