z3：超时的原因可能是什么（rise4fun）答案

【问题标题】：z3: What might be the reason for timeout (rise4fun)z3：超时的原因可能是什么（rise4fun）
【发布时间】：2015-05-30 08:27:04
【问题描述】：

问题是：我在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)

有人可以帮忙吗？

【问题讨论】：

标签： z3

【解决方案1】：

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

【讨论】：