z3中的量词消除

Question

我试图让 z3 将公式 ∃u.(u=x)∧(u=y) 简化为 (x=y)。 我试过了：

(declare-sort A)
(declare-const x A)
(declare-const y A)
(assert (exists ((u A)) (and (= u x) (= u y))))
(apply (then ctx-solver-simplify qe))

但这并没有简化公式。为什么？我应该如何简化这个公式？

Answer 1

Z3 无法进行这样的量词消除。使用Redlog的Redlog我们得到：