Question about integer index of PartialOrder (and similar functions)

[wijnanduu]

Z3 provides a specific, more efficient implementation of some special relations such as partial orders, see https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-special-relations. The function PartialOrder for creating these relations has a second argument which specifies a kind of identifier for the relation, and relations with the same identifier are equal: "The second argument is an unsigned integer used to distinguish the partial order R from other partial order relations over the same signature." Other datatypes also have such an identifier, but they use strings instead of integers. For instance, to define two distinct integers x and y we would write x = Int('x') and y = Int('y'), instead of x = Int(0) and y = Int(1).

I'm wondering why the special relations use integers instead of strings? Using strings would strike me as more convenient and more consistent with the rest of Z3. It would also help differentiate the relations when looking at the solver. Consider for instance the following code:

s = Solver()
R = PartialOrder(IntSort(), 0)
S = PartialOrder(IntSort(), 1)
s.add(R(1, 2))
s.add(S(3, 4))
print(s)

This prints [partial-order(1, 2), partial-order(3, 4)]. It would make more sense to me to write R = PartialOrder('R', IntSort()) and S = PartialOrder('S', IntSort()) and then have the solver look like [R(1, 2), S(3, 4)].

Edit: looking a bit further into this, I can't really understand the model output the partial orders R and S defined above. Consider the following code:

s = Solver()
R = PartialOrder(IntSort(), 0)
S = PartialOrder(IntSort(), 1)
s.add(R(1, 2))
s.add(Not(S(1, 2))
print(s.check())

This produces sat, so this set of sentences has a model. We would expect this model to differentiate R and S since they disagree on (1, 2), but this does not seem to be the case. The code

m = s.model()
print(m[R])
print(m[S])

produces twice the following output:

[else ->
 Or(connected(cons(Var(0), nil), Var(1), cons(Var(0), nil)),
    Var(0) == Var(1))]