CODEWITHSUNDEEP
z3
Aigerim Zhuankhan
Aigerim Zhuankhan

Reputation: 11

z3: What might be the reason for timeout (rise4fun)

The problem is: timeout when I try it in rise4fun:
I already tried not to use "forall", but it doesn't work too.

(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)

Can anybody help?

Upvotes: 1

Views: 144

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

The example uses both non-linear arithmetic, functions and quantifiers. Z3 does not handle this combination in any particular way. The latest version of Z3 does terminate quickly in default mode without the quantifier, but mainly by being lucky as opposed to using a decision procedure, in this case. With the quantifier, however, tZ3 enters a search space where it is unable to solve for the function f.

Upvotes: 1

Related Questions