Mutually recursive datatypes in z3 and their interaction with built-in types

Question

I am currently trying to use Z3 to encode a simple program logic for an untyped language with polymorphic lists.

As far as I understand, from the Z3 tutorial by Moura and Bjorner, it is not possible to "nest recursive data-type definitions inside other types, such as arrays".

So, suppose I have the following OCaml type:

type value =
    | Num of float
    | String of string
    | List of value list

Ideally, I would like to encode this type in Z3 using the built-in Z3List type, but I think this is not possible, because Z3 does not support mutual recursion between recursive data-types and the other types. Can someone confirm that this is the case?

If it is so, I guess the only possible way is for me to define my own type for a list of values, say my_list, and for the types my_list and value to be mutually recursive. In OCaml:

type value =
    | Num    of float
    | String of string
    | List   of my_list
and my_list =
    | Cons   of value * my_list
    | nil

But this means that I will not be able to leverage the built-in reasoning infrastructure that Z3 supports for Z3Lists. Is there a better way to do this?

Answer 1

It is correct that you would have to use the flattened version with my_list. The good news is that the built-in reasoning on lists in Z3 uses just the same mechanism as other data-types so you would get the same reasoning support with the flat data-type declaration.