z3:超时的原因可能是什么(rise4fun)

Question

问题是:在rise4fun中尝试时超时：

我已经试着不使用"forall"，但它也不起作用。

(declare-const x Real)
(declare-const y Real)
(declare-const t Real)
(declare-const u Real)
(declare-const v Real)
(declare-const w Real)
(declare-fun f (Real) Real)
(assert (forall ((x Real) (y Real)) (<= (+ (f x) (f y)) (* 2 (f (/ (+ x y) 2))))))

(assert (<= (+ 2 (f (* 2 (+ t u))) (f (* 2 (+ v w))) (f (+ t u v w))) (+ 2 (* 3 (f (+ t u v w))))))

(check-sat)
(get-model)

有人能帮上忙吗？

Answer 1

该示例同时使用了非线性算术、函数和量词。Z3不会以任何特定的方式处理这种组合。最新版本的Z3确实在没有量词的默认模式下快速终止，但主要是因为幸运，而不是在本例中使用决策过程。然而，有了量词，tZ3就进入了一个搜索空间，在那里它无法求解函数f。