Cannot define recursive type with Array in Z3

Question

I can define the following recursive datatype in Z3:

(declare-datatypes ()
   ((Tree
      (leaf (content Int))
      (node (left Tree) (right Tree)))))

But I cannot define the following. Do I need to declare something first? Or if that's not allow, how do I obtain an equivalent definition (where one constructor has arbitrary fields of the same type, indexed by integers)?

(declare-datatypes ()
   ((Tree
      (leaf (content Int))
      (node (children (Array Int Tree))))))

Answer 1

This (four year old) question is very closely related to yours: "a datatype contains a set in Z3". In the answers to that question, Leonardo de Moura says that this is not possible, and Nikolaj Bjørner gives a very detailed explanation about how one might work around the limitation. Probably you know they wrote the original paper presenting Z3 in 2008, see Z3: An Efficient SMT Solver. If we are lucky, maybe one of them will verify that recursively mixing arrays and datatypes is still not supported in Z3.

Also, what you are asking for is very similar to the tree example provided under the heading "Mutually recursive datatypes" in the rise4fun Z3 tutorial, except your question uses an array, while the the example on rise4fun uses a list. I wonder if the list-backed example on rise4fun might be modified to add an index to each list node. Something like this:

(declare-datatypes () ((Tree leaf (node (value Int) (children TreeList)))
                        (TreeList nil (cons (car Tree) (cdr TreeList) (index Int)))))
(assert
    (forall ((treeList TreeList))
        (implies
            (and
                (distinct treeList nil)
                (distinct (cdr treeList) nil)
            )
            (=
                (index (cdr treeList))
                (+ 1 (index treeList))
            )
        )
    )
)
(check-sat)

Unfortunately, Z3 gives unsat for this example, so evidently something is wrong here.