Z3 可以推理函数相等吗？

Question

我想在 Z3 中断言两个（未解释的）函数是相等的，但我不完全确定 Z3 能够推理这种相等性。例如，如果 Z3 收到此 smtlib 脚本：

(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (= (f 2) 2))
(assert (= (g 2) 3))
(assert (= f g))
(check-sat)

它回答

unknown

。另一方面，通过将

(assert (= f g))

替换为

(assert (forall ((x Int)) (= (f x) (g x))))

，Z3 可以正确回答

unsat

。使用量化来断言两个函数相等（也可能不相等）是否安全？

Answer 1

严格来说，SMTLib语言不允许函数类型相等：它是多排序的一阶逻辑，即，仅在全是一阶的排序上定义相等。

但是，z3 确实允许这样的等式作为扩展。这并不意味着它总是可以决定这种平等。所以获得

unknown

是意料之中的事。 （一般来说，函数相等没有决策过程，即总会有输入，求解器要么永远循环，要么必须回答

unknown

。但这是一个不同的讨论。）

话虽如此，SMTLib（v3）的下一次迭代将拥有更高阶的核心逻辑。因此，它将成为您可以编写

(= f g)

的语言的一部分，其中

f

和

g

是函数。 （再次强调，这并不意味着求解器能够解决此类问题。）

CVC5已经初步支持此类高阶特征：

$ cat a.smt2
(set-logic HO_ALL)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (= (f 2) 2))
(assert (= (g 2) 3))
(assert (= f g))
(check-sat)
$ cvc5 a.smt2
unsat

注意特殊的

HO_ALL

逻辑名称，它不是标准的一部分，而是 CVC5 扩展。

所以，长话短说，你写的完全没问题。是否能够决定任何有趣的平等函数是一个不同的讨论。