Nesting Arrays in Datatypes

[philzook58]

How do I make a datatype that nests the datatypes into the result of an array in the python bindings? https://microsoft.github.io/z3guide/docs/theories/Datatypes/#nested-datatypes-with-arrays-and-sequences

The following does not work. ArraySort gets mad because it is expected a SortRef not a Datatype

MyType = Datatype('MyType')
MyType.declare('mk_mytype', ('children', ArraySort(IntSort(), MyType)))
MyType = MyType.create()

---------------------------------------------------------------------------
Z3Exception                               Traceback (most recent call last)
/tmp/ipykernel_2765546/2481600882.py in ?()
      1 MyType = Datatype('MyType')
----> 2 MyType.declare('mk_mytype', ('children', ArraySort(IntSort(), MyType)))
      3 MyType = MyType.create()

~/.local/lib/python3.10/site-packages/z3/z3.py in ?(*sig)
   4764     r = sig[arity]
   4765     d = sig[0]
   4766     if z3_debug():
   4767         for s in sig:
-> 4768             _z3_assert(is_sort(s), "Z3 sort expected")
   4769             _z3_assert(s.ctx == r.ctx, "Context mismatch")
   4770     ctx = d.ctx
   4771     if len(sig) == 2:

~/.local/lib/python3.10/site-packages/z3/z3.py in ?(cond, msg)
    105 def _z3_assert(cond, msg):
    106     if not cond:
--> 107         raise Z3Exception(msg)

Z3Exception: Z3 sort expected

[LeventErkok]

Quoting from Section 10.4 of https://www.cs.colostate.edu/~cs440/spring19/slides/z3-tutorial.pdf:

You cannot nest recursive data-type definitions inside other types, such as arrays. So the following declaration is not accepted by Z3:
(declare-datatypes ((Unsupported (mk-rec-array (hd (Array Int Unsupported))))))

The reason for this has to do with well-formedness. You can think of arrays as functions, and the cardinality of the resulting type cannot be modeled in ordinary set-theory based semantics. (It can be modeled using CPOs/domain-theory, but that's not what SMTLib is based on.)

[philzook58]

The restriction is usually to negative occurrences of the datatype inside nested arrays / functions, which I what I thought was being referenced in the z3 tutorial line "Similarly, it may be convenient to use a nesting of algebraic data-types and arrays. Z3 supports nesting ADTs over sequences and over ranges of arrays.". As an example (Array Bool T) is unproblematic as it is the same as Pair T T. (Array Int T) can't be simply expressed in another form but I don't think it is all that problematic in a typical semantics (besides the fact it is encoding an infinitely branched node in a sense).

Experimenting with the smtlib prompt it appears this definition is accepted, but I do not know how to replicate in the z3 python or C api

%%file /tmp/test.smt2
(declare-datatypes ((MyT 0)) (((Nil) 
                               (MyConstr (hd (Array Int MyT))))))
(declare-const x MyT)
(assert (distinct x Nil))
(check-sat)
(get-model)

sat
(
  (define-fun x () MyT
    (MyConstr ((as const (Array Int MyT)) Nil)))
)

For context on my application, I was trying to create a universal "Any" datatype for which I could encode many of the possible sorts. A poor man's generic/dynamic typing. Using an uninterpreted Name sort, this could perhaps encode some variation of PHOAS, and also similar types show up in interaction trees / iteratees (although I think these are usually coinductive).

[LeventErkok]

This is confusing indeed. Perhaps the trick is to "stage" the creation?

from z3 import *

MyType = Datatype('MyType')
MyType.declare('mk_nil')
MyTypeSort = MyType.create()
MyType.declare('mk_mytype', ('children', ArraySort(IntSort(), MyTypeSort)))

print(MyType.constructors)

This prints:

[('mk_nil', 'is-mk_nil', ()), ('mk_mytype', 'is-mk_mytype', (('children', Array(Int, MyType)),))]

which doesn't look wrong. But it feels hacky, and I haven't played around with it to see if it actually works. Would be good to experiment. Would love to hear if you try this out and see if it actually works.

[LeventErkok]

Playing it a bit:

from z3 import *

MyType = Datatype('MyType')
MyType.declare('mk_nil')
MyTypeSort = MyType.create()
MyType.declare('mk_mytype', ('children', ArraySort(IntSort(), MyTypeSort)))
MyType = MyType.create()

x = Const("x", MyType)
s = Solver()
s.add(x != MyType.mk_nil)
print(s.check())
print(s.model())

prints:

sat
[x = mk_mytype(K(Int, mk_nil))]

which seems reasonable. But if I try:

print(s.sexpr())

before the call to check, I get a segmentation-fault and my python process crashes. This doesn't give me much confidence.