function with quantifier in Z3

Question

I have a problem with quantifier.

Let a(0) = 0, and a(n+1) would be either a(n)+1 or a(n)+2 based on the value of x(n). We may expect that for any kind of x(.) and for all n, a(n) <= n*2.

Here is the code for Z3:

(declare-fun a (Int) Int)
(declare-fun x (Int) Int)
(declare-fun N () Int)
(assert (forall 
    ((n Int))
    (=> (>= n 0)
        (= (a (+ n 1))
            (ite (> (x n) 0)
            (+ (a n) 1)
            (+ (a n) 2)
            )
        )
    )
))
(assert (= (a 0) 0))
(assert (> (a N) (+ N N)))

(check-sat)
(get-model)

I hope Z3 could return "unsat", while it always "timeout". I wonder if Z3 could handle this kind of quantifier, and if somebody could give some advice.

Thanks.

Answer 1

Thanks, Malte and Nikolaj. The variable N should be bounded:

(assert (> N 0))
(assert (< N 10000))

I replace

(assert (> (a N) (+ N N)))

with

(assert (and
 (not (> (a N) (+ N N)))
 (> (a (+ N 1)) (+ (+ N 1) (+ N 1)))
))

and it works for both definition of a(n). Does this a kind of inductive proof as you mentioned?

Here are the two blocks of code, and both of them return "unsat":

(declare-fun a (Int) Int)
(declare-fun x (Int) Int)
(declare-fun N () Int)
(assert (forall 
  ((n Int))
    (=> (>= n 0)
        (= (a (+ n 1))
        (ite (> (x n) 0)
        (+ (a n) 1)
        (+ (a n) 2)
        )
    ))
))
(assert (= (a 0) 0))

(assert (> N 0))
(assert (< N 10000))
;(assert (> (a N) (+ N N)))
(assert (and
  (not (> (a N) (+ N N)))
  (> (a (+ N 1)) (+ (+ N 1) (+ N 1)))
))
(check-sat)
;(get-model)

and

(declare-fun x (Int) Int)
(declare-fun y (Int) Int)
(declare-fun N () Int)

(define-fun-rec a ((n Int)) Int
  (if (> n 0) 
  (if (> (x (- n 1)) 0) (+ (a (- n 1)) 1) (+ (a (- n 1)) 2)) (y n)))
(assert (= (a 0) 0))

(assert (> N 0))
(assert (< N 10000))
;(assert (> (a N) (+ N N)))
(assert (and
  (not (> (a N) (+ N N)))
  (> (a (+ N 1)) (+ (+ N 1) (+ N 1)))
))
(check-sat)
;(get-model)