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

【问题标题】：Why can't z3 solve this seemingly simple uninterpreted function problem?为什么z3不能解决这个看似简单的未解释函数问题呢？
【发布时间】：2019-08-19 06:28:24
【问题描述】：

为什么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 似乎消耗了越来越多的内存，并且从未找到解决方案。这是未解释的函数不适合的东西吗？

我尝试使用 reals 并添加一个我期望与 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)

【问题讨论】：

标签： z3 smt

【解决方案1】：

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

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

【讨论】：