A Skolem model in Z3 should be unique, but is printing several (and repeated)

Question

I am testing how similar are "assignment"-like models and "Skolem-function"-like models in Z3.

Thus, I proposed an experiment: I will create a formula for which the unique model is y=2; and try to "imitate" this formula so that the (unique) model is a Skolem function f(x)=2. I did this by using ExistsForall quantification for the y=2 case and ForallExists quantification for the f(x)=2 case.

Thus, I first performed the following (note that the y is existentially quantified from the top-level declaration):

from z3 import *

x,y = Ints('x y')

ct_0 = (x >= 2)
ct_1 = (y > 1)
ct_2 = (y <= x)

phi = ForAll([x], Implies(ct_0, And(ct_1,ct_2)))

s = Solver()
s.add(phi)
print(s.check())
print(s.model())

for i in range(0, 5):
  if s.check() == sat:
    m = s.model()[y]
    print(m)
    s.add(And(y != m))

This code successfully prints out y=2 as a unique model (no matter we asked for 5 more). Now, I tried the same for f(x)=2 (note that there is no y):

skolem = Function('skolem', IntSort(), IntSort())

x = Int('x')

ct0 = (x >= 2)
ct1 = (skolem(x) > 1)
ct2 = (skolem(x) <= x)

phi1 = ForAll([x], Implies(ct0, And(ct1,ct2)))

s = Solver()
s.add(phi1)

for i in range(0, 5):
  if s.check() == sat:
    m = s.model()
    print(m)
    s.add(skolem(x) != i)

This prints:

[skolem = [else -> 2]]
[x = 0, skolem = [else -> If(2 <= Var(0), 2, 1)]]
[x = 0, skolem = [else -> If(2 <= Var(0), 2, -1)]]
[x = 0, skolem = [else -> If(2 <= Var(0), 2, -1)]]
[x = 0, skolem = [else -> If(2 <= Var(0), 2, -1)]]

My question is: why is the y=2 unique, whereas we get several Skolem functions? In Skolem functions, we get (and repeatedly) some functions in which the antecedent of phi1 (i.e., (x >= 2)) is negated (e.g., x=0); but in models, we do not get stuff like x=0 implies y=1, we only get y=2 because that is the unique model that does not depend on x. In the same way, [skolem = [else -> 2]] should be the unique "Skolem model" that does not depend on x.

Answer 1

There's a fundamental difference between these two queries. In the first one, you're looking for a single y that acts as the value that satisfies the property. And indeed y == 2 is the only choice.

But when you have a skolem function, you have an infinite number of witnesses. The very first one is:

skolem(x) = 2

i.e., the function that maps everything to 2. (You're internally equating this to the model y=2 in the first problem, but that's misleading.)

But there are other functions too. Here's the second one:

skolem(x) = if 2 <= x then 2 else 1

You can convince yourself this is perfectly fine, since it does give you the skolem function that provides a valid value for y (i.e., 2), when the consequent matters. What it returns in the else case is immaterial. (i.e., when x < 2). And similarly, you can simply do different things when x < 2, giving you an infinite number of skolem functions that work. (Of course, the difference is not interesting, but different nonetheless.)

What you really are trying to say, I guess, is there's nothing "else" that's interesting. Unfortunately that's harder to automate, since it's hard to get a Python function back from a z3 model. But you can do it manually:

from z3 import *

skolem = Function('skolem', IntSort(), IntSort())

x = Int('x')

ct0 = (x >= 2)
ct1 = (skolem(x) > 1)
ct2 = (skolem(x) <= x)

phi1 = ForAll([x], Implies(ct0, And(ct1,ct2)))

s = Solver()
s.add(phi1)

print(s.check())
print(s.model())

# The above gives you the model [else -> 2], i.e., the function that maps everything to 2.
# Let's add a constraint that says we want something "different" in the interesting case of "x >= 2":
s.add(ForAll([x], Implies(x >= 2, skolem(x) != 2)))
print(s.check())

This prints:

sat
[skolem = [else -> 2]]
unsat

which attests to the uniqueness of the skolem-function in the "interesting" case.