understanding the z3 model

问题:

Z3Py snippet:

x = Int('x')
fun = Function('fun', IntSort(), IntSort(), IntSort())
phi = ForAll(x, (fun(x, x) != x)) 
print phi
solve(phi)

Permalink: http://rise4fun.com/Z3Py/KZbR

Output:

∀x : fun(x, x) ≠ x
[elem!0 = 0,
 fun!6 = [(1, 1) → 2, else → 1],
 fun = [else → fun!6(ζ5(ν0), ζ5(ν1))],
 ζ5 = [1 → 1, else → 0]]

Question: I am trying to understand the model generated by Z3. I have following doubts.

1. In the model generated by z3, fun has only the else part. So on first glance, it looks like there is a single value irrespective of the arguments. But on closer look, it seems like v0 and v1 are the formal parameters of fun. Is there some convention for this?
2. Which variable does elem!0 refer to?

Thanks.

回答1:

The models produced by Z3 should be viewed as pure functional programs. This becomes clear when we ask Z3 to display the model in SMT 2.0 format. We can accomplish that by using the method sexpr(). Here is your example using this method (http://rise4fun.com/Z3Py/4Pw):

x = Int('x')
fun = Function('fun', IntSort(), IntSort(), IntSort())
phi = ForAll(x, (fun(x, x) != x)) 
print phi
s = Solver()
s.add(phi)
print s.check()
print s.model().sexpr()

The interpretation of fun contains free variables. You should read it as: fun(v0, v1) = fun!6(k5(v0), k5(v1)). This is explicit when the model is displayed in SMT 2.0 format. When I wrote the Python pretty printer, I tried to focus on quantifier-free problems. The "models as functional programs" idea is not relevant for quantifier-free problems. I will try to improve the Python model pretty printer in the future. The constant elem!0 is an auxiliary constant created by Z3 during the solving process. It is not really needed in the end (after the model is simplified). I will improve the model "dead code" elimination procedure to get rid of this unnecessary information. However, the model is correct. It does satisfy the quantifier. You can find more details regarding the encoding used by Z3 at http://rise4fun.com/Z3/tutorial/guide, and the auxiliary function k!5 is a "projection" function described in this article.