kdrag.reflect.datatype

kdrag.reflect.datatype(s: str, locals=None, globals=None) → DatatypeSortRef

Use python type syntax to define an algebraic datatype datatype. Fields can be specified positionally or by name. Reads the inner types from current environment.

>>> Int = smt.IntSort()
>>> Real = smt.RealSort()
>>> Foo = datatype("type Foo = Biz | Bar | Baz(Int, Int, smt.IntSort()) | Boz(x = Int, y = Int)")
>>> Foo.Baz.domain(1)
Int
>>> Foo.x.range()
Int

Parameters:

s (str)

Return type:

DatatypeSortRef