kdrag.datatype.Struct

kdrag.datatype.Struct(name: str, *fields: tuple[str, SortRef], pred=None) → DatatypeSortRef

Define a record datatype. This is the analog in many respects of python’s NamedTuple. The optional argument pred will add a well-formedness condition to the record giving something akin to a refinement type.

>>> Point = Struct("Point", ("x", smt.RealSort()), ("y", smt.RealSort()))
>>> Point(1,2)
Point(ToReal(1), ToReal(2))
>>> Point(1,2).x
x(Point(ToReal(1), ToReal(2)))
>>> PosPoint = Struct("PosPoint", ("x", smt.RealSort()), ("y", smt.RealSort()), pred = lambda p: smt.And(p.x > 0, p.y > 0))
>>> p = smt.Const("p", PosPoint)
>>> kd.QForAll([p], p.x > -42)
ForAll(p, Implies(And(x(p) > 0, y(p) > 0), x(p) > -42))

Parameters:

• name (str)

• fields (tuple[str, SortRef])

Return type:

DatatypeSortRef