Build in Z3 python a list of tuples

I am attempting to use Z3 solver in python to create a predicate path(list) which returns true if the list is a valid path on a given graph G

I would like to construct a list of tuples using Z3 to represent all edges present in the graph, here is my first attempt:

from z3 import *

IntPair = TupleSort("IntPair", [IntSort(), IntSort()])

List = Datatype('List')
List.declare('list', ('head', IntPair), ('tail', List))
List.declare('empty')
List = List.create()

However I am getting an error:

Z3Exception: Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)

From this line:

List.declare('list', ('head', IntPair), ('tail', List))

I am not sure which accessor is violating and causing this error. If we consider a list of integers:

List.declare('list', ('head', IntSort()), ('tail', List))

The above will run without errors.

Thank you.

Answer

When you call TupleSort it returns a triple. The sort, a constructor, and the accessors. You need to pattern-match and give each a separate name. That is, replace your line:

IntPair = TupleSort("IntPair", [IntSort(), IntSort()])

with:

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

Now IntPair is the name of the sort you wanted; and the rest of your program will go without any errors.

As you develop your program further, you’ll need to use mkIntPair, first and second as you access and construct those pairs inside your list.