kdrag.theories.set.Injective

kdrag.theories.set.Injective(f: FuncDeclRef) → BoolRef

An injective function maps distinct inputs to distinct outputs.

>>> x, y = smt.Ints("x y")
>>> neg = (-x).decl()
>>> kd.prove(Injective(neg))
|= ForAll([x!..., y!...],
       Implies(-x!... == -y!..., x!... == y!...))

Parameters:

f (FuncDeclRef)

Return type:

BoolRef