kdrag.theories.set.Singleton

kdrag.theories.set.Singleton(x: ExprRef) → ArrayRef

>>> x = smt.Int("x")
>>> kd.prove(Singleton(smt.IntVal(3))[3])
|= Store(K(Int, False), 3, True)[3]
>>> kd.prove(smt.Not(Singleton(smt.IntVal(3))[4]))
|= Not(Store(K(Int, False), 3, True)[4])

Parameters:

x (ExprRef)

Return type:

ArrayRef