kdrag.datatype.NewType

kdrag.datatype.NewType(name: str, sort: SortRef, pred=None) → DatatypeSortRef

Minimal wrapper around a sort for sort based overloading

>>> NatI = NewType("NatI", smt.IntSort(), pred = lambda x: x.val >= 0)
>>> x = smt.Const("x", NatI)
>>> kd.QForAll([x], x.val >= -7)
ForAll(x, Implies(val(x) >= 0, val(x) >= -7))

Parameters:

• name (str)

• sort (SortRef)

Return type:

DatatypeSortRef