为什么z3不能解决这个看似简单的未解释函数问题呢？

Question

为什么 z3 无法 sat 检查以下内容？

(declare-fun f (Int) Int)
(assert (forall ((a Int) (b Int)) (= (+ (f a) (f b) ) (f (+ a b)))))
(assert (= (f 1) 1))
(check-sat)
(get-model)

我希望得到类似于 f(x) = x 的结果，但是 z3 似乎消耗了越来越多的 ram，并且永远找不到解决方案。这是一些未解释的函数不适合吗？

我试过使用实数并添加一个我认为与 f 相同的附加函数，如下所示：

(declare-fun f (Real) Real)
(declare-fun g (Real) Real)
(assert (forall ((a Real)) (= (g a) a)))
(assert (forall ((a Real) (b Real)) (= (+ (f a) (f b) ) (f (+ a b)))))
(assert (= (f 1) 1))


(check-sat)
(get-model)

Answer 1

嗯，一点都不简单。量词很难，正如您怀疑的那样，SMT 求解器不是用它们进行推理的好选择。在您的特定情况下，模型查找器必须找到一种非常特殊的函数，它具有属性，这远远超出了当前 SMT 求解技术的能力；老实说重点。

话虽如此，你可以研究量词模式：你可以在某些情况下帮助电子匹配引擎解决此类问题，但这绝对不是正确的技术。看这里：https://rise4fun.com/z3/tutorialcontent/guide#h28

为什么z3不能解决这个看似简单的未解释函数问题呢？

Why can't z3 solve this seemingly simple uninterpreted function problem?

smt

z3