kdrag.kernel.obtain

kdrag.kernel.obtain(thm: QuantifierRef) → tuple[list[ExprRef], Proof]

Skolemize an existential quantifier. exists xs, P(xs) -> P(cs) for fresh cs https://en.wikipedia.org/wiki/Existential_instantiation

>>> x = smt.Int("x")
>>> obtain(smt.Exists([x], x >= 0))
([x!...], |=  Implies(Exists(x, x >= 0), x!... >= 0))
>>> y = FreshVar("y", smt.IntSort())
>>> obtain(smt.Exists([x], x >= y))
([f!...(y!...)], |=  Implies(Exists(x, x >= y!...), f!...(y!...) >= y!...))

Parameters:

thm (QuantifierRef)

Return type:

tuple[list[ExprRef], Proof]