kdrag.theories.float

Theory of built in floating point and connection to the reals

Module Attributes

`round_up_neg`	round_idem_finite = kd.prove(
`min_float64`

Functions

`IsFinite`(x)
`NoOverflow`(m, x, s)
`in_range`(x)
`is_finite`(x)
`no_overflow`(m, x)

kdrag.theories.float.IsFinite(x: FPRef) → BoolRef

Parameters:: x (FPRef)
Return type:: BoolRef

kdrag.theories.float.NoOverflow(m, x: ArithRef, s)

Parameters:: x (ArithRef)

kdrag.theories.float.in_range(x)

kdrag.theories.float.is_finite(x: FPRef)

Parameters:: x (FPRef)

kdrag.theories.float.min_float64 = |= ForAll(z, Implies(Or(fpIsNormal(z), fpIsSubnormal(z), fpIsZero(z)), z >= fpToFP(RNE(), -179769313486231570000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)))

>>> assert True

Parameters:: args (smt.ExprRef | Proof)

kdrag.theories.float.no_overflow(m, x)

kdrag.theories.float.round_up_neg = |= ForAll(x, round32(RTP(), -x) == -round32(RTN(), x))

round_idem_finite = kd.prove(

kd.QForAll(: [x, m1, m2], NoOverflow(m2, x, F32), round(m1, round(m2, x)) == round(m2, x),

), by=round_def,

)

Parameters:: args (smt.ExprRef | Proof)