I am playing with Skolem functions in Z3-Py. In the following lines, I describe the Skolem function that satisfies the formula Forall x. Exists y. (x>=2) --> (y>1) /\ (y<=x) interpreted over integers:
x = Int('x')
skolem = Function('skolem', IntSort(), IntSort())
ct_0 = (x >= 2)
ct_1 = (skolem(x) > 1)
ct_2 = (skolem(x) <= x)
phi = ForAll([x], Implies(ct_0, And(ct_1,ct_2)))
s = Solver()
s.add(phi)
print(s.check())
print(s.model())
Which I understand that it outputs the unique 'model' possible: y=2 (i.e., f(x)=2). It is printed as follows:
sat
[skolem = [else -> 2]]
I have a preliminary question: why does the function use an else? I guess it comes from the fact that "it is only activated" if the antecedent (x>=2) holds. But which is the co-domain of the function if it is not the else branch (output 2) the one activated, but the if branch?
But now it comes my actual question. I solved the same formula, but interpreted over reals:
x = Real('x')
skolem = Function('skolem', RealSort(), RealSort())
ct_0 = (x >= 2.0)
ct_1 = (skolem(x) > 1.0)
ct_2 = (skolem(x) <= x)
phi = ForAll([x], Implies(ct_0, And(ct_1,ct_2)))
s = Solver()
s.add(phi)
print(s.check())
print(s.model())
And this outputs... the same Skolem function! Is this right?
In case it is, it is still curious, since it could have chosen many others; e.g., y=1.5. Then, I would like to ask for another Skolem function to Z3, so I proceed as if I was asking for 5 new models:
phi = ForAll([x], Implies(ct_0, And(ct_1,ct_2)))
s = Solver()
s.add(phi)
for i in range(0,5):
if s.check() == sat:
m = s.model()
print(m)
s.add(Not(m))
But I get the following error: Z3Exception: True, False or Z3 Boolean expression expected. Received [skolem = [else -> 2]] of type <class 'z3.z3.ModelRef'>. I mean, I see Z3 expects Boolean for the negation (which is obvious hehe), so how can I encode the fact that "I add the negation of this Skolem function into the formula", i.e., that I want to find another Skolem function?
In your loop, you're trying to add the negation of your model m; but that's not what Not(m) means. In fact, Not(m) is meaningless: Not operates on booleans, not models; which is the bizarre error you're getting.
To do what you're trying to achieve; simply assert that you want a different skolem function:
from z3 import *
x = Real('x')
skolem = Function('skolem', RealSort(), RealSort())
ct_0 = (x >= 2)
ct_1 = (skolem(x) > 1)
ct_2 = (skolem(x) <= 2)
phi = ForAll([x], Implies(ct_0, And(ct_1,ct_2)))
s = Solver()
s.add(phi)
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/2)]]
[x = 0, skolem = [else -> If(2 <= Var(0), 2, 1/2)]]
[x = 0, skolem = [else -> If(2 <= Var(0), 3/2, 1/2)]]
[x = 0, skolem = [else -> If(2 <= Var(0), 3/2, 1/2)]]
Now this is a little hard to read, but I think you can figure it out. A function model is simply a finite-mapping with an else clause, which is what a finite function is. The Var call refers to its argument. I haven't looked at the definitions z3 provides in detail to make sure they're good, but I have no reason to suspect why not. See if you can work this out for yourself; it's a valuable exercise! Feel free to ask further questions if anything isn't clear.