Recursive datatypes with sequences in Python

[hacker-volodya]

In guide there is an example of using recursive datatypes with sequences and arrays:

(declare-sort Expr)
(declare-sort Var)
(declare-datatypes ((Stmt 0)) 
  (((Assignment (lval Var) (rval Expr)) 
    (If (cond Expr) (th Stmt) (el Stmt)) 
    (Seq (stmts (Seq Stmt))))))

(declare-const s Stmt)
(declare-const t Stmt)

(assert ((_ is Seq) t))
(assert ((_ is Seq) s))
(assert (= s (seq.nth (stmts t) 2)))
(assert (>= (seq.len (stmts s)) 5))
(check-sat)
(get-model)
(assert (= s (Seq (seq.unit s))))
(check-sat)

Is it possible to define Stmt using python bindings?

Something like:

SomeType = Datatype('SomeType')
SomeType.declare('nil')
SomeType.declare('some', SeqSort(SomeType))
SomeType = SomeType.create()

However, initializing SeqSort with incomplete Datatype is not possible:

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "C:\Users\user\AppData\Local\Programs\Python\Python310\lib\site-packages\z3\z3.py", line 10746, in SeqSort
    return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx)
AttributeError: 'Datatype' object has no attribute 'ctx_ref'

[NikolajBjorner]

from z3 import *
SomeType = Datatype('SomeType')
SomeTypeS = DatatypeSort('SomeType')
SomeType.declare('nil')
SomeType.declare('some', ('someof', SeqSort(SomeTypeS), ))
SomeType = SomeType.create()
print(SomeType)
print(SomeTypeS)
print(SomeType.eq(SomeTypeS))

Background: the function "Datatype" creates a "builder" object where you can attach the constructors of a data-type.
The function "DatatypeSort" accesses the sort object of name 'SomeType'. Z3 does not have information about the accessors/constructors until you called the "create()" method on the builder, but it is possible to use it as a sort as you like.
In fact the sort SomeType that is returned will be identical to SomeTypeS.

[NikolajBjorner]

Add example
https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/advanced#datatypes