kdrag.solvers.sympy.sympify

kdrag.solvers.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(deriv(smt.Lambda([x], cos(sin(x)))))(sympy.abc.x) Derivative(cos(sin(x)), x) >>> sympify(integrate_(smt.Lambda([x], sin(x)), 0,x)) 1 - cos(x) >>> sympify(smt.Lambda([x], x + 1)) Lambda(X__…, X__… + 1)