kdrag.theories.real.sympy.kdify

kdrag.theories.real.sympy.kdify(e: Expr, **kwargs) → ExprRef

Convert a sympy expression into a z3 expression. >>> x = smt.Real(“x”) >>> kdify(sympify(x + 1)) x + 1 >>> kdify(sympify(real.sin(x) + 1)) sin(x) + 1 >>> kdify(sympify(x + smt.RatVal(1,3))) x + 1/3 >>> kdify(sympify(x/3)) x*1/3