from pysmt.shortcuts import Solver, Symbol, Ite, Equals, NotEquals
from pysmt.typing import INT

x = Symbol("x", INT)


# Term t(x) is injective iff for all x, x', t(x) = t(x') |= x = x', i.e.
# iff t(x) = t(x') /\ x =/= x' is unsatisfiable.
def is_injective(t):
    x_primed = Symbol("x'", INT)
    t_primed = t.substitute({x: x_primed})

    with Solver() as s:
        s.add_assertion(Equals(t, t_primed))
        s.add_assertion(NotEquals(x, x_primed))

        return not s.solve()


print(is_injective(x + 1))  # True
print(is_injective(x * 2))  # True
print(is_injective(Ite(x >= 0, x, -x)))  # False
print(is_injective(x * x))  # False