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。