z3py: How to prevent accessor call on custom data type when a differen constructor is used?

Question

I created a custom List-Datatype similar to the tutorial on https://ericpony.github.io/z3py-tutorial/advanced-examples.htm:

def ListSort(sort):
    # Declare a List of sort elements
    listType = Datatype('List(%s)' % str(sort))
    listType.declare('cons', ('head', sort), ('tail', listType))
    listType.declare('empty')
    return listType.create()

IntListSort = ListSort(IntSort())

I now want to use this type, but when solving the following formula, I get a weird result:

solve(Int("x") == 1 + IntListSort.head(IntListSort.empty))

Output

[x = 1 + head(empty)]

While this sounds like a perfectly reasonable result when just looking at the code, this was definitely not my intention. head(empty) shouldn't really return an element of sort IntSort(). head(List) shouldn't even be available for empty lists, only for lists created using cons.

This might not be an issue for programs where I manually craft the equations to be solved, but I need to use this in a more complex context, and my program just gave me such an "integer" when looking for a counter example, but such a result is not really helpful.

Is there a way to restrict head such that it can only be applied to lists constructed using cons?

One idea I thought about was to create a separate type called EmptyListSort, but I would still need to allow ListSorts to be empty as well, so this would lead back to the same issue...

Answer 1

SMTLib is a logic of total-functions. When you define an algebraic data-type, then all the functions that get defined along with that data-type (i.e., head, tail in your example) are always total. That is, they can be applied to any list value, regardless of how that value is constructed.

There's nothing in the type-system that'd allow you to prohibit this. (Doing so would require a notion of dependent types, and SMTLib's type system is nowhere near that sophisticated.)

Then, you might ask, what happens if you apply head to empty: The logic leaves it underspecified: That is, the solver can pick any value it wants for the result of head(empty). It can even pick different values if you use this expression twice in different contexts.

So, how does one avoid the problem you're having? Well, you have to add your own constraints when you apply head. That is, you have to program such that if head is called on empty, you force the solver to be in an unsat state. To do so, I'd define a custom version of head, that asserts the required condition:

def customHead(s, lst):
    s.add(IntListSort.is_cons(lst))
    return IntListSort.head(lst)

This definition of customHead is equivalent to head, except it forces all the arguments it receives to be cons nodes. Now you can use it like this:

s = Solver()
x = Int('x')
s.add(x == 1 + customHead(s, IntListSort.empty))
print(s.check())

And this prints:

unsat

That is, it "catches" the bad case you wanted to avoid, by forcing the solver to return unsat. This may or may not be suitable for your eventual goal; but this is the only way to model such behavior.

And here is what happens if we pass a cons list:

s = Solver()
x = Int('x')
s.add(x == 1 + customHead(s, IntListSort.cons(10, IntListSort.empty)))
print(s.check())
print(s.model())

This prints:

sat
[x = 11]

as you'd expect.