kdrag.theories.real

Definitions about the reals.

Transcendental functions and bounds.

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.

Parameters:

t (ExprRef)

Return type:

ExprRef

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

arb

complex

extended

geometry

interval

ndarray

sympy

vec