kdrag.theories.real

Functions

abstract_arith(t)	Z3 has difficult ematching over arithmetic expressions.
rlemma(thm[, by])
sin_lower(n, x)
sqrt_bnd(n)
sqrt_lower(n, x)
sqrt_upper(x, n)

kdrag.theories.real.abstract_arith(t: ExprRef) → ExprRef

Z3 has difficult ematching over arithmetic expressions. Abstracting them to uninterpreted functions can help.

kdrag.theories.real.rlemma(thm, by=[], **kwargs)

kdrag.theories.real.sin_lower(n, x)

kdrag.theories.real.sqrt_bnd(n)

kdrag.theories.real.sqrt_lower(n, x)

kdrag.theories.real.sqrt_upper(x, n)

Modules

sympy