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)

Classes

class kdrag.theories.real.Add

Bases: object

assoc = |= ForAll([x, y, z], add(x, add(y, z)) == add(add(x, y), z))

comm = |= ForAll([x, y], add(x, y) == add(y, x))

left_id = |= ForAll(x, add(0, x) == x)

right_id = |= ForAll(x, add(x, 0) == x)

class kdrag.theories.real.Mul

Bases: object

assoc = |= ForAll([x, y, z], mul(x, mul(y, z)) == mul(mul(x, y), z))

comm = |= ForAll([x, y], mul(x, y) == mul(y, x))

left_id = |= ForAll(x, mul(1, x) == x)

right_id = |= ForAll(x, mul(x, 1) == x)

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

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

Modules