Proving inductive facts in Z3

Question

I am trying to prove an inductive fact in Z3, an SMT solver by Microsoft. I know that Z3 does not provide this functionality in general, as explained in the Z3 guide (section 8: Datatypes), but it looks like this is possible when we constrain the domain over which we want to prove the fact. Consider the following example:

(declare-fun p (Int) Bool)
(assert (p 0))

(assert (forall ((x Int)) 
    (=> 
    (and (> x 0) (<= x 20))
    (= (p (- x 1)) (p x) ))))
(assert (not (p 20)))

(check-sat)

The solver responds correctly with unsat, which means that (p 20) is valid. The problem is that when we relax this constraint any further (we replace 20 in the previous example by any integer greater than 20), the solver responds with unknown.

I find this strange because it does not take Z3 long to solve the original problem, but when we increase the upper limit by one it becomes suddenly impossible. I have tried to add a pattern to the quantifier as follows:

(declare-fun p (Int) Bool)
(assert (p 0))

(assert (forall ((x Int)) 
    (! (=> 
    (and (> x 0) (<= x 40))
    (= (p (- x 1)) (p x) )) :pattern ((<= x 40)))))
(assert (not (p 40)))

(check-sat)

Which seems to work better, but now the upper limit is 40. Does this mean that I can better not use Z3 to prove such facts, or am I formulating my problem incorrectly?

Answer 1

Z3 uses many heuristics to control quantifier instantiation. One one them is based on the "instantiation depth". Z3 tags every expression with a "depth" attribute. All user supplied assertions are tagged with depth 0. When a quantifier is instantiated, the depth of the new expressions is bumped. Z3 will not instantiate quantifiers using expressions tagged with a depth greater than a pre-defined threshold. In your problem, the threshold is reached: (p 40) is depth 0, (p 39) is depth 1, (p 38) is depth 2, etc.

To increase the threshold, you should use the option:

(set-option :qi-eager-threshold 100)

Here is the example with this option: http://rise4fun.com/Z3/ZdxO.

Of course, using this setting, Z3 will timeout, for example, for (p 110).

In the future, Z3 will have better support for "bounded quantification". In most cases, the best approach for handling this kind of quantifier is to expand it. With the programmatic API, we can easily "instantiate" expressions before we send them to Z3. Here is an example in Python (http://rise4fun.com/Z3Py/44lE):

p = Function('p', IntSort(), BoolSort())

s = Solver()

s.add(p(0))
s.add([ p(x+1) == p(x) for x in range(40)])
s.add(Not(p(40)))

print s.check()

Finally, in Z3, patterns containing arithmetic symbols are not very effective. The problem is that Z3 preprocess the formula before solving. Then, most patterns containing arithmetic symbols will never match. For more information on how to use patterns/triggers effectively, see this article. The author also provides a slide deck.