Z3(Py) does not “intersect” Skolem functions as I expected.
I will try to explain my doubt using an imaginary problem which is the one that I have been testing on.
Consider a system that has two processes A and B, and an environment chooses between A or B. When process A is “activated”, then the system must solve P1: Exists y. Forall x. (x>=2) --> (y>1) /\ (y<=x). When the process B is “activated” then the system must solve P2: Exists y. Forall x. (x<2) --> (y>1) /\ (y>x). We can see, in Z3-PY, models of both the P1 and the P2 formulae:
#P1
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())
#P2
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())
Note that the model of P1 is unique: y=2; whereas a model of P2 is y=2, but also y=3, y=4, y=5, ... ad infinitum.
Then, I consider that the "intersection" of both P1 and P2 is the model y=2. In other words, whenever the environment chooses A or B, i.e., whenever the environment forces the system to solve P1 or P2, the system can just respond y=2 and will satisfy the formula, no matter what the environment chose.
I obtained this (unique) “intersection” y=2 by performing the (unique) model of the conjunction of both formulae:
#P1 and P2 intersection
#Note that, this time, I distinguish between ct_k and ctk because I executed them in the same script, no other reason involved.
x,y = Ints('x y')
ct_0 = (x >= 2)
ct_1 = (y > 1)
ct_2 = (y <= x)
phi0 = ForAll([x], Implies(ct_0, And(ct_1,ct_2)))
ct0 = (x < 2)
ct1 = (y > 1)
ct2 = (y > x)
phi1 = ForAll([x], Implies(ct0, And(ct1,ct2)))
phiT = And(phi0,phi1)
s = Solver()
s.add(phiT)
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 outputs [y = 2] as expected.
Now, consider I have a problem: P1 and P2 are no longer Exists-Forall formulae, but Forall-Exists formulae: this means that we will not have models of y, but Skolem functions (as solved in this question What does a model mean in a universally quantified formula? Is it a function?). I implement that as follows:
#P1 Skolem
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())
#P2 Skolem
x = Real('x')
skolem = Function('skolem', RealSort(), RealSort())
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)
As we can see, both of them return [skolem = [else -> 2]] as the first option, and then they offer other (different) options, such as [x = 0, skolem = [else -> If(1 <= Var(0), 5, 2)]] for P2.
My question is: how can I perform the “intersection” of these two formulae? In general, how can I perform intersection of n skolem functions (in Z3)? I tried as follows (using the same idea as before when seeking y=2:
#P1 and P2 Skolem intersection
#Once again, I distinguish ct_k and ctk for execution reasons.
x,y = Ints('x y')
ct_0 = (x >= 2)
ct_1 = (skolem(x) > 1)
ct_2 = (skolem(x) <= x)
phi0 = ForAll([x], Implies(ct_0, And(ct_1,ct_2)))
ct0 = (x < 2)
ct1 = (skolem(x) > 1)
ct2 = (skolem(x) > x)
phi1 = ForAll([x], Implies(ct0, And(ct1,ct2)))
phiT = And(phi0,phi1)
s = Solver()
s.add(phiT)
print(s.check())
print(s.model())
for i in range(0, 5):
if s.check() == sat:
m = s.model()
print(m)
s.add(skolem(x) != i)
And results were as follows:
[skolem = [else -> 3/2]]
[skolem = [else -> 3/2]]
[x = 0, skolem = [else -> 2]]
[x = 0, skolem = [else -> 2]]
[x = 0, skolem = [else -> 3/2]]
[x = 0, skolem = [else -> 3/2]]
What does this mean? Why does it not output just [skolem = [else -> 2]]? In mean, in the same way that y=2 was the model with the other quantifier alternation.
Also, how does it offer 3/2 if we are in the domain of integers?
PS: In the Forall-Exists version of P1, if we print several Skolem functions, then the result is as follows:
[skolem = [else -> 2]]
[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)]]
How is this so?
In one of your programs, you have the declaration:
skolem = Function('skolem', RealSort(), RealSort())
I think you confused yourself by somehow leaving this in? It's hard to tell when you don't post code segments that are fully loadable by themselves. In any case, the following:
from z3 import *
skolem = Function('skolem', IntSort(), IntSort())
#P1 and P2 Skolem intersection
#Once again, I distinguish ct_k and ctk for execution reasons.
x,y = Ints('x y')
ct_0 = (x >= 2)
ct_1 = (skolem(x) > 1)
ct_2 = (skolem(x) <= x)
phi0 = ForAll([x], Implies(ct_0, And(ct_1,ct_2)))
ct0 = (x < 2)
ct1 = (skolem(x) > 1)
ct2 = (skolem(x) > x)
phi1 = ForAll([x], Implies(ct0, And(ct1,ct2)))
phiT = And(phi0,phi1)
s = Solver()
s.add(phiT)
for i in range(0, 5):
if s.check() == sat:
m = s.model()
print(m)
s.add(skolem(x) != i)
Prints:
[skolem = [else -> 2]]
[x = 0,
skolem = [else ->
If(And(1 <= Var(0), 2 <= Var(0)),
2,
If(1 <= Var(0), 4, 2))]]
[x = 0,
skolem = [else ->
If(And(1 <= Var(0), 2 <= Var(0)),
2,
If(1 <= Var(0), 4, 2))]]
[x = 0,
skolem = [else ->
If(And(1 <= Var(0), 2 <= Var(0)),
2,
If(1 <= Var(0), 5, 3))]]
[x = 0,
skolem = [else ->
If(And(1 <= Var(0), 2 <= Var(0)),
2,
If(1 <= Var(0), 6, 4))]]
which looks fine to me. Does this help resolve your issue?