kdrag.theories.real.sympy.sympify

kdrag.theories.real.sympy.sympify(e: ExprRef, locals=None) → Expr

Convert a z3 expression into a sympy expression. >>> x = smt.Real(“x”) >>> sympify(x + 1) x + 1 >>> sympify(smt.RatVal(1,3)) Fraction(1, 3) >>> sympify(real.deriv(smt.Lambda([x], real.cos(real.sin(x)))))(sympy.abc.x) Derivative(cos(sin(x)), x) >>> sympify(real.integrate(smt.Lambda([x], real.sin(x)), 0,x)) 1 - cos(x) >>> sympify(smt.Lambda([x], x + 1)) Lambda(X__…, X__… + 1)