kdrag.theories.real.sympy

Functions

`diff`(e, *args)	Differentiate a z3 expression.
`diff_shim`(e)
`expand`(e)	Expand a z3 expression.
`factor`(e)	Factor a z3 expression.
`fresh_symbol`()	Create a fresh symbol for use in sympy expressions.
`integ_shim`(e, a, b)
`integrate`(e, *args)	Integrate a z3 expression.
`kdify`(e, **kwargs)	Convert a sympy expression into a z3 expression.
`limit`(e, x, x0)	Compute the limit of a z3 expression.
`series`(e[, x, x0, n, dir])	Compute the series expansion of a z3 expression.
`shim_ho`(f)
`simp`(e)	Sympy simplification as an axiom schema.
`simplify`(e)	Simplify a z3 expression.
`solve`(constrs, vs)
`sum_shim`(e, a, b)
`summation`(e, *args)	Sum a z3 expression.
`sympify`(e[, locals])	Convert a z3 expression into a sympy expression.
`translate_tuple_args`(args)

kdrag.theories.real.sympy.diff(e: ExprRef, *args)

Differentiate a z3 expression. >>> x,y = smt.Reals(“x y”) >>> diff(x**2, x) 2*x >>> diff(x**2, x, x) 2 >>> diff(x*x, (x,2)) 2 >>> diff(x*y*x, x) 2*x*y

Parameters:: e (ExprRef)

kdrag.theories.real.sympy.diff_shim(e: KnuckleClosure) → Basic

Parameters:: e (KnuckleClosure)
Return type:: Basic

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

Expand a z3 expression. >>> x = smt.Real(“x”) >>> expand((x + 1)**2) x**2 + 2*x + 1

Parameters:: e (ExprRef)
Return type:: ExprRef

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

Factor a z3 expression. >>> x = smt.Real(“x”) >>> factor(x**2 + 2*x + 1) (x + 1)**2

Parameters:: e (ExprRef)
Return type:: ExprRef

kdrag.theories.real.sympy.fresh_symbol() → Symbol

Create a fresh symbol for use in sympy expressions. >>> x = fresh_symbol() >>> y = fresh_symbol() >>> x != y True

Return type:: Symbol

kdrag.theories.real.sympy.integ_shim(e: KnuckleClosure, a, b) → Basic

Parameters:: e (KnuckleClosure)
Return type:: Basic

kdrag.theories.real.sympy.integrate(e, *args): Integrate a z3 expression. >>> x = smt.Real(“x”) >>> integrate(x**2, x) x**3*1/3

kdrag.theories.real.sympy.kdify(e: Basic, **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

Parameters:: e (Basic)
Return type:: ExprRef

kdrag.theories.real.sympy.limit(e, x, x0): Compute the limit of a z3 expression. >>> x = smt.Real(“x”) >>> limit(1/x, x, sympy.oo) 0 >>> limit(1/x, x, 0) # TODO: What to do about this one? inf

kdrag.theories.real.sympy.series(e, x=None, x0=0, n=6, dir='+'): Compute the series expansion of a z3 expression. >>> x = smt.Real(“x”) >>> series(real.sin(x), x, n=2) x + Order(x**2)

kdrag.theories.real.sympy.shim_ho(f)

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

Sympy simplification as an axiom schema. Sympy nor the translation to and from z3 are particularly sound. It is very useful though and better than nothing. Your mileage may vary

>>> x = smt.Real("x")
>>> simp(real.sin(x)**2 + real.cos(x)**2)
|= sin(x)**2 + cos(x)**2 == 1

Parameters:: e (ExprRef)
Return type:: Proof

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

Parameters:: e (ExprRef)
Return type:: ExprRef

kdrag.theories.real.sympy.solve(constrs: list[BoolRef], vs: list[ExprRef]) → list[dict[ExprRef, ExprRef]]

>>> x,y,z = smt.Reals("x y z")
>>> solve([x + y == 1, x - z == 2], [x, y, z])
[{x: z + 2, y: -z - 1}]
>>> solve([real.cos(x) == 3], [x]) # Note that does not return all possible solutions.
[{x: 2*pi - acos(3)}, {x: acos(3)}]

Parameters:

constrs (list[BoolRef])
vs (list[ExprRef])

Return type:

list[dict[ExprRef, ExprRef]]

kdrag.theories.real.sympy.sum_shim(e: KnuckleClosure, a, b) → Basic

Parameters:: e (KnuckleClosure)
Return type:: Basic

kdrag.theories.real.sympy.summation(e, *args): Sum a z3 expression. >>> x,n = smt.Reals(“x n”) >>> summation(x**2, (x, 0, 10)) 385 >>> summation(x, (x, 0, n)) n**2*1/2 + n*1/2

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)

Parameters:: e (ExprRef)
Return type:: Expr

kdrag.theories.real.sympy.translate_tuple_args(args)