Unexpected behaviour relating to the PartialOrder function

[wijnanduu]

It seems that the partial order produced by the PartialOrder function does not necessarily satisfy reflexivity. For instance, running the following code returns sat:

from z3 import *
s = Solver()
R = PartialOrder(IntSort(), 0)
x = Int('x')
s.add(Not(R(x, x)))
s.check()

I have looked at the model for this solver but I do not understand it:

[x = 2,
 next = [else ->
         If(And(member(Var(0), Var(2)),
                Not(member(Var(1), Var(3)))),
            pair(cons(Var(1), fst(Var(4))),
                 cons(Var(1), snd(Var(4)))),
            Var(4))],
 partial-order = [else ->
                  Or(connected(cons(Var(0), nil),
                               Var(1),
                               cons(Var(0), nil)),
                     Var(0) == Var(1))],
 member = [else ->
           If(is(nil, Var(1)),
              False,
              If(head(Var(1)) == Var(0),
                 True,
                 member(Var(0), tail(Var(1)))))],
 connected = [else ->
              If(fst(pair(nil, Var(2))) == nil,
                 False,
                 If(member(Var(1), fst(pair(nil, Var(2)))),
                    True,
                    connected(fst(pair(nil, Var(2))),
                              Var(1),
                              snd(pair(nil, Var(2))))))]]

I also checked the other properties (transitivity and antisymmetry) and those do seem to work, consider for example the following code verifying transitivity that does produce unsat:

from z3 import *
s = Solver()
R = PartialOrder(IntSort(), 0)
x, y, z = Ints('x y z')
s.add(R(x, y))
s.add(R(y, z))
s.add(Not(R(x, z)))
s.check()

However -- and I don't know whether these issues are related, or that I am just misunderstanding something -- when I add a call to s.push() before adding the conditions in the snippet above, the answer changes from unsat to sat:

from z3 import *
s = Solver()
R = PartialOrder(IntSort(), 0)
x, y, z = Ints('x y z')
s.push()
s.add(R(x, y))
s.add(R(y, z))
s.add(Not(R(x, z)))
s.check()

From my understanding of push and pop the two pieces of code above should result in identical outputs? The same happens for the antisymmetry condition, i.e., the following produces unsat:

from z3 import *
s = Solver()
R = PartialOrder(IntSort(), 0)
x, y = Ints('x y')
s.add(R(x, y))
s.add(R(y, x))
s.add(Not(x == y))
s.check()

And the following produces sat:

from z3 import *
s = Solver()
R = PartialOrder(IntSort(), 0)
s.push()
x, y = Ints('x y')
s.add(R(x, y))
s.add(R(y, x))
s.add(Not(x == y))
s.check()

I am on version 4.11.2.0 of the z3 python package.

[wijnanduu]

Btw, if I use LinearOrder instead of PartialOrder the reflexivity issue goes away, but adding a call to s.push() as in the other examples again changes the answer to sat:

from z3 import *
s = Solver()
R = LinearOrder(IntSort(), 0)
x = Int('x')
s.push()
s.add(Not(R(x, x)))
s.check()
s.model()

This produces the model: [x = 2, linear-order = [else -> False]].

[NikolajBjorner]

• partial /linear /etc order solver wasn't loaded when there was a push before the first declaration.
• partial order solver had incomplete check for negated relations