kdrag.theories.real.arb

Module Attributes

tan_bnd(x)

This is probably the purest form of the information that arb offers.

Functions

`arb_bnd`(arbf, z3f)
`arb_ge`(lhs, rhs)
`arb_gt`(lhs, rhs)
`arb_le_ax`(lhs0, rhs)
`arb_lt_ax`(lhs, rhs)	Use numerical evaluation to confirm ball of lhs is completely below ball of rhs
`arb_over_of_mid_rad`(mid, rad)	Get overapproximating arb from midpoint and radius.
`bound_ax`(e)
`bounds`(e)	Get the bounds of a z3 expression.
`cos_bnd`(x)
`exp_bnd`(x)
`flint_bnd`(t, env)
`flint_eq_ax_unsafe`(lhs, rhs)	This axiom schema is fishy, in that even if arb is implement correctly, this check does not assure the equality of the left and right hand side.
`interp_flint`(e, env)	Interpret a z3 expression into an arb calculation.
`sin_bnd`(x)
`tan_bnd`(x)	This is probably the purest form of the information that arb offers.
`z3_mid_rad_of_arb`(x)	Get midpoint and radius as z3 values.
`z3_of_exact_arb`(x)	Get exact arb as z3 value

kdrag.theories.real.arb.arb_bnd(arbf, z3f)

>>> kd.prove(real.cos(0) == 1, by=[cos_bnd(arb(0))])
|= cos(0) == 1

kdrag.theories.real.arb.arb_ge(lhs, rhs)

kdrag.theories.real.arb.arb_gt(lhs, rhs)

kdrag.theories.real.arb.arb_le_ax(lhs0: ArithRef, rhs: ArithRef) → Proof

>>> arb_le_ax(3.14, real.pi)
|= 157/50 <= pi
>>> arb_le_ax(1,1)
|= 1 <= 1

Parameters:

lhs0 (ArithRef)
rhs (ArithRef)

Return type:

Proof

kdrag.theories.real.arb.arb_lt_ax(lhs: ArithRef, rhs: ArithRef) → Proof

Use numerical evaluation to confirm ball of lhs is completely below ball of rhs

>>> arb_lt_ax(3.14, real.pi)
|= 157/50 < pi

Parameters:

lhs (ArithRef)
rhs (ArithRef)

Return type:

Proof

kdrag.theories.real.arb.arb_over_of_mid_rad(mid: ArithRef, rad: ArithRef) → arb

Get overapproximating arb from midpoint and radius.

>>> arb_over_of_mid_rad(1, 0)
1.00000000000000
>>> arb_over_of_mid_rad(1, 0.0005)
[1.000 +/- 5.01e-4]

Parameters:

mid (ArithRef)
rad (ArithRef)

Return type:

arb

kdrag.theories.real.arb.bound_ax(e: ArithRef) → Proof

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

kdrag.theories.real.arb.bounds(e: ArithRef) → tuple[ArithRef, ArithRef]

Get the bounds of a z3 expression. >>> bounds(1) (1, 1) >>> bounds(smt.RealVal(1) + smt.RealVal(2)) (3, 3)

Parameters:: e (ArithRef)
Return type:: tuple[ArithRef, ArithRef]

kdrag.theories.real.arb.cos_bnd(x: object) → Proof

Parameters:: x (object)
Return type:: Proof

kdrag.theories.real.arb.exp_bnd(x: object) → Proof

Parameters:: x (object)
Return type:: Proof

kdrag.theories.real.arb.flint_bnd(t: ArithRef, env) → Proof

Parameters:: t (ArithRef)
Return type:: Proof

kdrag.theories.real.arb.flint_eq_ax_unsafe(lhs, rhs)

This axiom schema is fishy, in that even if arb is implement correctly, this check does not assure the equality of the left and right hand side. but it is better than nothing.

>>> flint_eq_ax_unsafe(real.pi, 4*real.atan(1))
|= pi == 4*atan(1)
>>> flint_eq_ax_unsafe(smt.RealVal(0), real.sin(0))
|= 0 == sin(0)
>>> flint_eq_ax_unsafe(real.sin(3*real.pi/2), -1)
|= sin((3*pi)/2) == -1

kdrag.theories.real.arb.interp_flint(e: ArithRef, env) → arb

Interpret a z3 expression into an arb calculation.

>>> interp_flint(real.pi, {})
[3.14159265358979 +/- 3.34e-15]

Parameters:: e (ArithRef)
Return type:: arb

kdrag.theories.real.arb.sin_bnd(x: object) → Proof

>>> sin_bnd(arb(0))
|= ForAll(x,
    Implies(And(0 - 0 <= x, x <= 0 + 0),
            And(0 - 0 <= sin(x), sin(x) <= 0 + 0)))
>>> kd.prove(real.sin(0) <= 2, by=[sin_bnd(arb(0,0.1))(smt.RealVal(0))])
|= sin(0) <= 2
>>> kd.prove(real.sin(3.14) <= 0.02, by=[sin_bnd(arb(3.14, 0.01))])
|= sin(157/50) <= 1/50

Parameters:: x (object)
Return type:: Proof

kdrag.theories.real.arb.tan_bnd(x: object) → Proof

This is probably the purest form of the information that arb offers. In principle, larger scale rules can be derived from this.

Parameters:: x (object)
Return type:: Proof

kdrag.theories.real.arb.z3_mid_rad_of_arb(x: arb) → tuple[ArithRef, ArithRef]

Get midpoint and radius as z3 values.

>>> z3_mid_rad_of_arb(arb(1))
(1, 0)
>>> z3_mid_rad_of_arb(arb(1) + arb(2))
(3, 0)

Parameters:: x (arb)
Return type:: tuple[ArithRef, ArithRef]

kdrag.theories.real.arb.z3_of_exact_arb(x: arb) → ArithRef

Get exact arb as z3 value

>>> z3_of_exact_arb(arb(1))
1
>>> z3_of_exact_arb(arb(1) + arb(2))
3
>>> z3_of_exact_arb(arb(2**1000))
2**1000

Parameters:: x (arb)
Return type:: ArithRef