我想知道如何用Z3有效地证明一个有点简单的函数，即 f : u32 -> u32 是双宾函数。
def f(n):
for i in range(10):
n *= 3
n &= 0xFFFFFFFF # Let's treat this like a 4 byte unsigned number
n ^= 0xDEADBEEF
return n
我已经知道它是双射的 因为它是由双射函数组成的 所以这更多的是一个计算问题。
现在，知道域和codomain是有限的，而且大小相同，我想先通过要求Z3找到它是注入式的反例来实现。
N = BitVec('N', 32)
M = BitVec('M', 32)
solve(N != M, f(N) == f(M))
然而这需要相当长的时间(> 10分钟，但之后就关闭了)，而且是合理的，因为搜索空间几乎是64位的，而且函数可能是相当复杂的推理，因为它混合了大量的乘法和二进制算术，所以我想是否有可能改用surjection来证明它，也许结果会更快。
其实这样是否更快，或者说是否还有办法高效地解决这个问题，可能是另一个问题，然而我陷入了思考，如何用surjection来证明它，即要求Z3找到一个 M 以致于 f(N) != M forall N.
这和证明注入性有什么不同吗？
在Z3的python绑定中如何陈述？
是否有可能将存在性限定符从超射声明中移除？
有没有更有效的方法来证明一个函数是双射性的？因为对于这样的事情，用蛮力搜索可能更有效率，因为对于32位向量来说，需要的内存应该不是很多，但是对于64位的输入输出来说，这种方法肯定是不行的。
你会把附加性写成如下。
N = BitVec('N', 32)
M = BitVec('M', 32)
s = Solver()
s.add(ForAll([N], f(N) != M))
r = s.check()
if r == sat:
print(s.model())
else:
print(r)
不幸的是，在位向量中添加量化符会使逻辑无法确定，在我的机器上，z3在10秒后就放弃了。
unknown
一般来说，添加量化符会让z3（或其他SMT解算器）很难解决这个问题。你最初的编码:
solve(N!=M, f(N) == f(M))
可能是这个问题的最佳编码方式。事实上，如果你把范围从 10 改为更小的范围（我试过最多到 3），z3 的答案是 unsat 比较快。但是很明显，随着你的函数的迭代次数的增加，求解时间会以指数级的方式进行 f 增加。
SMT求解器可能不是证明这种性质的最佳工具。你当然可以表达这样的约束条件，但你最多只能得到 unknown 作为一个答案，最坏的情况是它会永远循环下去。一个合适的定理证明器（如Isabelle、HOL、Coq、ACL2等）会提供一个更好的（代价是自动化程度较低）平台来做这些证明。
使用数学分析证明很简单。 程序化的时候 Domain 或 Coo-domain 是 interval [或 not finite] 不能用蛮力来完成（不能检查无限值）。即使用 finite D/C 蛮力的话，需要一段时间，这取决于D的大小(无用的解决方案)
解决的方法是计算首因式，看一看 monotony (对于多项式来说相当简单，如果限制在1-2度甚至更简单)。如果在定义的区间上是单调的，则 injective 是实现。对于 surjective 需要 C=f(D) (去只是单调)，并检查出。C=[f(a),f(b)] 其中a,b的界限 D [a,b] , f:[a,b] -> C =f(D) (基本上是[f(a),f(b)]或[f(b),f(a)])
另一种选择是使用启发式算法，只检查一些随机值，但这更像是一种暗示，并不能证明函数是射式或超射式。(也许有更好的启发式解决方案，但在这里也许可以问google-master)
可能行得通的解法（启发式） 说f:[a,b]->[c,d] 1. 将[a,b]分成1000点[或由你决定]，p1 < p2 < p3 ... < p1000 2.计算f(point_1) ... f(point_n)，并存储结果 3. 单调有f(point_1) < f(point_2) < ... < f(point_1000) [或>].如果是注入式 4. 计算f(a),f(b),应该有[c,d]=[f(a),f(b)]->如果3实现了就可以了.如果是，则顺理成章和加射式=>双射式。