为什么 Z3 不能在不进行看似微不足道的修改的情况下解决这个实例？

Question

原题为：

(declare-const a Real)
(declare-const b Bool)
(declare-const c Int)

(assert (distinct a 0.))

(assert (= b (distinct (* a a) 0.)))

(assert (= c (ite b 1 0)))

(assert (not (distinct c 0)))

(check-sat)

结果未知。

但最后两个约束合起来等同于(assert (= b false))，并且在手动执行此重写后

(declare-const a Real)
(declare-const b Bool)
(declare-const c Int)

(assert (distinct a 0.))

(assert (= b (distinct (* a a) 0.)))

(assert (= b false))

;(assert (= c (ite b 1 0)))

;(assert (not (distinct c 0)))

(check-sat)

Z3 现在可以解决这个实例（不满意）。

为什么Z3可以解决第二个问题，但不能解决第一个问题，即使第一个问题可以简化为第二个问题？

编辑：

在定位问题的过程中发现了一个很奇怪的地方

Z3 解决了以下实例和 returns "unsat":

(declare-fun a() Real)
(declare-fun b() Bool)
(declare-fun c() Int)

(assert (distinct a 0.0))

(assert (= b (distinct (* a a) 0.0)))

(assert (= b false))

;(assert (= c 0))

(check-sat)

但是如果我取消注释 (assert (= c 0))，求解器 returns "unknown"，即使 c=0 与上述断言无关。

Answer 1

这里的问题是像 (* a a) 这样的表达式是非线性的，Z3 的非线性问题默认求解器会放弃，因为它认为它太难了。 Z3 确实有另一个求解器，但那个求解器的理论组合非常有限，也就是说，你不能将它用于混合布尔、位向量、数组等问题，而只能用于算术问题。将 (check-sat) 命令替换为 (check-sat-using qfnra-nlsat).

即可轻松测试