Can Z3 check the satisfiability of formulas that c

问题:

I'm trying out some of the examples of a Z3 tutorial that involve recursive functions. I've tried out the following example.

1. Fibonacci (Section 8.3)
2. IsNat (Section 8.3)
3. Inductive (Section 10.5)

Z3 times out on all of the above examples. But, the tutorial seems to imply that only Inductive is non-terminating.

Can Z3 check the satisfiability of formulas that contain recursive functions or it cannot handle any inductive facts?

回答1:

These examples from the Z3 tutorial are there to illustrate limitations of the technology behind Z3.

Z3 fails on these examples for two reasons:

1. The models produced by Z3 assign an interpretation for each uninterpreted function symbol. The models can be viewed as functional programs. The current version does not produce recursive definitions. The first example is satisfiable, but Z3 fails to produce an interpretation for fib because it does not support recursive definitions. We have plans to extend Z3 in this direction.

2. Z3 does not support proofs by induction. Examples 2 and 3 are unsatisfiable, but Z3 fails because it does not support proof by induction. We also have plans to add basic support for that.

Although these items are on my TODO list, I will not start working on them this year.