kdrag.smt.Const

kdrag.smt.Const(name: str, sort: SortRef | FuncRef) → ExprRef

Create a constant of a given sort. If a set value is given as the sort, this is treated as a constraint held in the assumes field of the constant. This field may be used by quantifiers.

>>> n = Int("n")
>>> x = Const("x", Lambda([n], n >= 0))
>>> x.assumes
x >= 0

Parameters:

name (str)
sort (SortRef | FuncRef)

Return type:

ExprRef