Strange behavior while accessing elements of empty sequences in z3

I've found strange effect while solving some constraints with z3py. Here's the code:

from z3 import *

# Custom tuple
IntPair, mkIntPair, (first, second) = TupleSort("IntPair", [IntSort(), IntSort()])

s = Solver()

iseq = Const('iseq', SeqSort(IntPair))
p = mkIntPair(Int('a'), Int('b'))

# Some constraints
s.add(And(first(p) > 0, second(p) > 0))
s.add(Length(iseq) == 0)
s.add(first(iseq[0]) >= first(p))

if s.check() == sat:
    print(s.model())

The output is:

[b = 1,
 iseq = Empty(Seq(IntPair)),
 a = 1,
 seq.nth_u = [else -> IntPair(1, 2)]]

As you can see, iseq is empty in the z3 model because of Length(iseq) == 0 constraint. But how constraint first(iseq[0]) >= first(p) can be satisfiable here? How we can access 0th element in an empty sequence? And how to modify this code to make it unsatisfiable because of something like sequence-out-of-range reason?

Thanks!

Solution

This is by design.

Note that sequence logic isn't yet formalized by SMTLib, and the implementation in z3 is based on https://smt2012.loria.fr/paper11.pdf

In Section 2.2.1 of that paper, it states:

Observe that the value of (seq-head seq-empty) is undetermined. Similarly for seq-tail, seq-first and seq-last. Their meaning is under-specified. Thus, the theory Seq admits all interpretations that satisfy the free monoid properties and the axioms above.

That is, z3 is free to assign any value it wants when you take the head of an empty sequence, or the ith element of a sequence whose length is at most i, for any i.

You might ask why this is the case. The short answer is that SMTLib is essentially a logic of total functions, i.e., all terms are either values or they can be reduced to a value. It does not support what's known as "partial functions," i.e., functions that are not defined over their whole domain according to the types. Sequence access happens to be one of those functions. Another typical example is division by 0: Over reals, division by 0 is underspecified, i.e., the solver is free to assign any value it wants. (See https://smtlib.cs.uiowa.edu/theories-Reals.shtml, under the section "notes.")

If you inspect the model z3 is giving you, you can see the evidence of this:

seq.nth_u = [else -> IntPair(1, 2)]]

The above means that z3 will assign the pair (1,2) whenever you access any element that's out-of-bounds. For a different problem z3 can choose a different interpretation of course, to make sure all the other constraints are satisfied.

If you want your query to be unsat, then you have to be careful in your modeling. That is, if you are accessing the ith element of any sequence, you have to also assert the sequence has at least i+1 elements. That is, if you add the constraint:

s.add(first(iseq[0]) >= first(p))

then you're morally required to also add:

s.add(Length(iseq) > 0)

You can do this manually, or your programming environment can do it for you behind the scenes. The Python bindings leave this part to the programmer: While this is a reasonable choice in designing the API, it's not necessarily the only one. Long story short, if you add the second constraint above, z3 will to tell you unsat for obvious reasons, and as you wanted.

Note that it's not a terribly difficult exercise to add your own indexing operator that did this automatically for you. You can define:

def access(solver, seq, idx):
    solver.add(Length(seq) > idx)
    return seq[idx]

And then:

s.add(first(access(s, iseq, 0)) >= first(p))

which will also produce unsat, taking care of the cardinality requirements for you behind the scenes without you having to worry about it every single time.