kdrag.smt.ForAll

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

Quantified ForAll

Shorthand for ForAll(vars, Implies(And(hyp[0], hyp[1], …), conc))

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

Parameters:

vs (list[ExprRef])

Return type:

QuantifierRef