kdrag.theories.set.Surjective

kdrag.theories.set.Surjective(f: FuncDeclRef) → BoolRef

A surjective function maps to every possible value in the range.

>>> x = smt.Int("x")
>>> neg = (-x).decl()
>>> kd.prove(Surjective(neg))
|= ForAll(y!..., Lambda(y, Exists(x0, -x0 == y))[y!...])