Needless Var() returned by Solver.model()

Question

Solver.model() sometimes returns an assignment with a seemingly-needless Var(), whereas I was (perhaps naively) expecting Solver.model() to always return a concrete value for each variable. For example:

#!/usr/bin/python
import z3

x, y = z3.Ints('x y')
a = z3.Array('a', z3.IntSort(), z3.IntSort())
e = z3.Not(z3.Exists([x], z3.And(x != y, a[x] == a[y])))

solver = z3.Solver()
solver.add(e)
print solver.check()
print solver.model()

produces

sat
[k!1 = 0,
 a = [else -> k!5!7(k!6(Var(0)))],
 y = 1,
 k!5 = [else -> k!5!7(k!6(Var(0)))],
 k!5!7 = [1 -> 3, else -> 2],
 k!6 = [1 -> 1, else -> 0]]

What's going on here? Is Var(0) in a's "else" referring to the 0th argument to the a array, meaning a[i] = k!5!7[k!6[i]]? Is it possible to get a concrete satisfying assignment for a out of Z3, such as a = [1 -> 1, else -> 0]?

Answer 1

This is the intended output. The interpretation for functions and arrays should be viewed as function definitions. Keep in mind that the assertion

z3.Not(z3.Exists([x], z3.And(x != y, a[x] == a[y])))

is essentially a universal quantifier. For quantifier free problems, Z3 does generate the "concrete assignments" suggested in your post. However, this kind of representation is not expressive enough. In the end of the message, I attached an example that cannot be encoded using "concrete assignments". The following post has additional information about how models are encoded in Z3.

• understanding the z3 model

You can find more details regarding the encoding used by Z3 at http://rise4fun.com/Z3/tutorial/guide

Here is an example that produces a model that can't be encoded using "concrete" assignments (available online at http://rise4fun.com/Z3Py/eggh):

a = Array('a', IntSort(), IntSort())
i, j = Ints('i j')
solver = Solver()
x, y = Ints('x y')
solver.add(ForAll([x, y], Implies(x <= y, a[x] <= a[y])))
solver.add(a[i] != a[j])
print solver.check()
print solver.model()