kdrag.smt.Exists

kdrag.smt.Exists(vs: list[ExprRef], *concs, **kwargs) → QuantifierRef

Quantified Exists

Shorthand for Exists(vars, And(conc[0], conc[1], …))

>>> x,y = Ints("x y")
>>> Exists([x,y], x > 0, y > 0)
Exists([x, y], And(x > 0, y > 0))
>>> x = Const("x", Lambda([x], x >= 0))
>>> Exists([x], x > 3)
Exists(x, And(x >= 0, x > 3))

Parameters:

vs (list[ExprRef])

Return type:

QuantifierRef