Z3能否推理函数相等性？使用量化断言函数相等是否安全？

直接使用(= f g)断言两个未解释函数相等时Z3返回unknown，原因在于Z3默认的求解策略对这种高阶函数等式（将函数本身作为值比较）的处理能力有限——它不会自动将函数相等展开为"对所有输入参数输出一致"的一阶逻辑表述，因此无法识别出f(2)=2和g(2)=3之间的矛盾，只能返回未知。

而用全称量化公式(forall ((x Int)) (= (f x) (g x)))来断言函数相等是完全安全且符合一阶逻辑语义的：

• 从逻辑定义上讲，两个函数相等的本质就是对定义域内的所有输入，它们的输出都严格相等，这个量化公式正好精准表达了这一点。
• 对Z3来说，这种一阶量化语句可以通过其内置的量化实例化机制处理，像你的例子里，Z3会自动实例化x=2的情况，直接发现f(2)和g(2)的取值矛盾，从而正确返回unsat。

如果要断言两个函数不等，对应的写法是(exists ((x Int)) (not (= (f x) (g x))))，这同样是安全的——它对应"存在至少一个输入使得两个函数输出不同"的逻辑定义，Z3也能正确处理这类断言。

内容的提问来源于stack exchange，提问作者Pietro Braione