kdrag.solvers.kb.is_trivial

kdrag.solvers.kb.is_trivial(t: BoolRef | QuantifierRef) → bool

See if equation is of form `s = s

>>> x = smt.Real("x")
>>> assert is_trivial(x == x)
>>> assert not is_trivial(x == -(-x))