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

The formula is SAT, for N < 0, the graph of a is underspecified. But the default quantifier instantiation engine can't determine this. You can take advantage of that you are defining a recursive function to enforce a different engine.

;(declare-fun a (Int) Int)
 (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 (> (a N) (+ N N)))

(check-sat)
(get-model)

As Malte writes, there is no support for induction on such formulas so don't expect Z3 to produce induction proofs. It does find inductive invariants on a class of Horn clause formulas, but it requires a transformation to cast arbitrary formulas into this format.