kdrag.theories.real.sympy.simplify

kdrag.theories.real.sympy.simplify(e: ExprRef) → ExprRef

Simplify a z3 expression. >>> x = smt.Real(“x”) >>> simplify((x + 1)**2 - x**2) 2*x + 1 >>> simplify(real.sin(x)**2 + real.cos(x)**2) 1