Floating point, typed

def Cvc.Typed.Term.mkFloatPosZero [Ω] (exp sig : Nat) : Env (Term (Float exp sig))

Positive zero.

Equations

• Cvc.Typed.Term.mkFloatPosZero exp sig = Cvc.Untyped.Term.mkFloatPosZero exp sig

def Cvc.Typed.Term.fpOfIeeeBv [Ω] (e s : Nat) {n : Nat} (bv : Term (BitVec n)) : Env (Term (Float e s))

Reinterpretation of an IEEE 754 bit pattern of e + s bits as a floating point.

Equations

• Cvc.Typed.Term.fpOfIeeeBv e s bv = Cvc.Untyped.Term.fpOfIeeeBv e s bv

def Cvc.Typed.Term.fpMin [Ω] {e s : Nat} (lft rgt : Term (Float e s)) : Env (Term (Float e s))

Minimum.

Equations

• lft.fpMin rgt = Cvc.Untyped.Term.fpMin lft rgt

def Cvc.Typed.Term.fpIsNan [Ω] {e s : Nat} (fp : Term (Float e s)) : Env (Term Bool)

Whether the value is not-a-number.

Equations

• fp.fpIsNan = Cvc.Untyped.Term.fpIsNan fp

def Cvc.Typed.Term.fpFma [Ω] {e s : Nat} (rm : Term Float.RoundingMode) (a b c : Term (Float e s)) : Env (Term (Float e s))

Fused multiply-add, computing a * b + c with a single rounding.

Equations

• rm.fpFma a b c = Cvc.Untyped.Term.fpFma rm a b c

def Cvc.Typed.Term.fpOfFp [Ω] (e s : Nat) {ei si : Nat} (rm : Term Float.RoundingMode) (fp : Term (Float ei si)) : Env (Term (Float e s))

Conversion between floating-point formats.

Equations

• Cvc.Typed.Term.fpOfFp e s rm fp = Cvc.Untyped.Term.fpOfFp e s rm fp

def Cvc.Typed.Term.fpSub [Ω] {e s : Nat} (rm : Term Float.RoundingMode) (lft rgt : Term (Float e s)) : Env (Term (Float e s))

Subtraction.

Equations

• rm.fpSub lft rgt = Cvc.Untyped.Term.fpSub rm lft rgt

def Cvc.Typed.Term.fpOfBits [Ω] {e s : Nat} (sign : Term (BitVec 1)) (exponent : Term (BitVec e)) (significand : Term (BitVec s)) : Env (Term (Float e (s + 1)))

A floating point assembled from its sign, exponent and significand bits.

The significand bit-vector holds the significand minus its hidden bit, hence the s + 1.

Equations

• sign.fpOfBits exponent significand = Cvc.Untyped.Term.fpOfBits sign exponent significand

def Cvc.Typed.Term.fpIsInf [Ω] {e s : Nat} (fp : Term (Float e s)) : Env (Term Bool)

Whether the value is either infinity.

Equations

• fp.fpIsInf = Cvc.Untyped.Term.fpIsInf fp

def Cvc.Typed.Term.fpRti [Ω] {e s : Nat} (rm : Term Float.RoundingMode) (fp : Term (Float e s)) : Env (Term (Float e s))

Rounding to an integral value.

Equations

• rm.fpRti fp = Cvc.Untyped.Term.fpRti rm fp

def Cvc.Typed.Term.fpSqrt [Ω] {e s : Nat} (rm : Term Float.RoundingMode) (fp : Term (Float e s)) : Env (Term (Float e s))

Square root.

Equations

• rm.fpSqrt fp = Cvc.Untyped.Term.fpSqrt rm fp

def Cvc.Typed.Term.fpMax [Ω] {e s : Nat} (lft rgt : Term (Float e s)) : Env (Term (Float e s))

Maximum.

Equations

• lft.fpMax rgt = Cvc.Untyped.Term.fpMax lft rgt

def Cvc.Typed.Term.fpDiv [Ω] {e s : Nat} (rm : Term Float.RoundingMode) (lft rgt : Term (Float e s)) : Env (Term (Float e s))

Division.

Equations

• rm.fpDiv lft rgt = Cvc.Untyped.Term.fpDiv rm lft rgt

def Cvc.Typed.Term.fpIsNeg [Ω] {e s : Nat} (fp : Term (Float e s)) : Env (Term Bool)

Whether the value is negative.

Equations

• fp.fpIsNeg = Cvc.Untyped.Term.fpIsNeg fp

def Cvc.Typed.Term.fpEq [Ω] {e s : Nat} (lft rgt : Term (Float e s)) : Env (Term Bool)

Floating-point equality, for which NaN is not equal to itself and the zeroes are equal.

Equations

• lft.fpEq rgt = Cvc.Untyped.Term.fpEq lft rgt

def Cvc.Typed.Term.fpGe [Ω] {e s : Nat} (lft rgt : Term (Float e s)) : Env (Term Bool)

Greater-than-or-equal-to.

Equations

• lft.fpGe rgt = Cvc.Untyped.Term.fpGe lft rgt

def Cvc.Typed.Term.mkFloatNaN [Ω] (exp sig : Nat) : Env (Term (Float exp sig))

Not-a-number.

Equations

• Cvc.Typed.Term.mkFloatNaN exp sig = Cvc.Untyped.Term.mkFloatNaN exp sig

def Cvc.Typed.Term.fpIsNormal [Ω] {e s : Nat} (fp : Term (Float e s)) : Env (Term Bool)

Whether the value is normal.

Equations

• fp.fpIsNormal = Cvc.Untyped.Term.fpIsNormal fp

def Cvc.Typed.Term.fpAdd [Ω] {e s : Nat} (rm : Term Float.RoundingMode) (lft rgt : Term (Float e s)) : Env (Term (Float e s))

Addition.

Equations

• rm.fpAdd lft rgt = Cvc.Untyped.Term.fpAdd rm lft rgt

def Cvc.Typed.Term.fpOfUbv [Ω] (e s : Nat) {n : Nat} (rm : Term Float.RoundingMode) (bv : Term (BitVec n)) : Env (Term (Float e s))

Conversion of an unsigned bit-vector to a floating point.

Equations

• Cvc.Typed.Term.fpOfUbv e s rm bv = Cvc.Untyped.Term.fpOfUbv e s rm bv

def Cvc.Typed.Term.mkFloat [Ω] (exp sig : Nat) {n : Nat} (bv : Term (BitVec n)) : Env (Term (Float exp sig))

A floating-point literal read from bv, a bit-vector literal of exp + sig bits.

Equations

• Cvc.Typed.Term.mkFloat exp sig bv = Cvc.Untyped.Term.mkFloat exp sig bv

def Cvc.Typed.Term.fpNeg [Ω] {e s : Nat} (fp : Term (Float e s)) : Env (Term (Float e s))

Negation.

Equations

• fp.fpNeg = Cvc.Untyped.Term.fpNeg fp

def Cvc.Typed.Term.fpToReal [Ω] {e s : Nat} (fp : Term (Float e s)) : Env (Term Rat)

Conversion to a real; unspecified for NaN and the infinities.

Equations

• fp.fpToReal = Cvc.Untyped.Term.fpToReal fp

def Cvc.Typed.Term.fpLe [Ω] {e s : Nat} (lft rgt : Term (Float e s)) : Env (Term Bool)

Less-than-or-equal-to.

Equations

• lft.fpLe rgt = Cvc.Untyped.Term.fpLe lft rgt

def Cvc.Typed.Term.fpGt [Ω] {e s : Nat} (lft rgt : Term (Float e s)) : Env (Term Bool)

Greater-than.

Equations

• lft.fpGt rgt = Cvc.Untyped.Term.fpGt lft rgt

def Cvc.Typed.Term.fpRem [Ω] {e s : Nat} (lft rgt : Term (Float e s)) : Env (Term (Float e s))

IEEE 754 remainder, lft - rgt * q for q the integer nearest lft / rgt.

Equations

• lft.fpRem rgt = Cvc.Untyped.Term.fpRem lft rgt

def Cvc.Typed.Term.mkFloatNegZero [Ω] (exp sig : Nat) : Env (Term (Float exp sig))

Negative zero.

Equations

• Cvc.Typed.Term.mkFloatNegZero exp sig = Cvc.Untyped.Term.mkFloatNegZero exp sig

def Cvc.Typed.Term.fpIsPos [Ω] {e s : Nat} (fp : Term (Float e s)) : Env (Term Bool)

Whether the value is positive.

Equations

• fp.fpIsPos = Cvc.Untyped.Term.fpIsPos fp

def Cvc.Typed.Term.fpOfSbv [Ω] (e s : Nat) {n : Nat} (rm : Term Float.RoundingMode) (bv : Term (BitVec n)) : Env (Term (Float e s))

Conversion of a signed bit-vector to a floating point.

Equations

• Cvc.Typed.Term.fpOfSbv e s rm bv = Cvc.Untyped.Term.fpOfSbv e s rm bv

def Cvc.Typed.Term.fpIsZero [Ω] {e s : Nat} (fp : Term (Float e s)) : Env (Term Bool)

Whether the value is either zero.

Equations

• fp.fpIsZero = Cvc.Untyped.Term.fpIsZero fp

def Cvc.Typed.Term.mkFloatPosInf [Ω] (exp sig : Nat) : Env (Term (Float exp sig))

Positive infinity.

Equations

• Cvc.Typed.Term.mkFloatPosInf exp sig = Cvc.Untyped.Term.mkFloatPosInf exp sig

def Cvc.Typed.Term.fpIsSubnormal [Ω] {e s : Nat} (fp : Term (Float e s)) : Env (Term Bool)

Whether the value is subnormal.

Equations

• fp.fpIsSubnormal = Cvc.Untyped.Term.fpIsSubnormal fp

def Cvc.Typed.Term.fpLt [Ω] {e s : Nat} (lft rgt : Term (Float e s)) : Env (Term Bool)

Less-than.

Equations

• lft.fpLt rgt = Cvc.Untyped.Term.fpLt lft rgt

def Cvc.Typed.Term.fpOfReal [Ω] (e s : Nat) (rm : Term Float.RoundingMode) (arg : Term Rat) : Env (Term (Float e s))

Conversion of a real to a floating point.

Equations

• Cvc.Typed.Term.fpOfReal e s rm arg = Cvc.Untyped.Term.fpOfReal e s rm arg

def Cvc.Typed.Term.fpToSbv [Ω] (size : Nat) {e s : Nat} (rm : Term Float.RoundingMode) (fp : Term (Float e s)) : Env (Term (BitVec size))

Conversion of a floating point to a signed bit-vector of the given size.

Unspecified for NaN, an infinity, or a value out of range.

Equations

• Cvc.Typed.Term.fpToSbv size rm fp = Cvc.Untyped.Term.fpToSbv size rm fp

def Cvc.Typed.Term.mkFloatNegInf [Ω] (exp sig : Nat) : Env (Term (Float exp sig))

Negative infinity.

Equations

• Cvc.Typed.Term.mkFloatNegInf exp sig = Cvc.Untyped.Term.mkFloatNegInf exp sig

def Cvc.Typed.Term.fpAbs [Ω] {e s : Nat} (fp : Term (Float e s)) : Env (Term (Float e s))

Absolute value.

Equations

• fp.fpAbs = Cvc.Untyped.Term.fpAbs fp

def Cvc.Typed.Term.fpMul [Ω] {e s : Nat} (rm : Term Float.RoundingMode) (lft rgt : Term (Float e s)) : Env (Term (Float e s))

Multiplication.

Equations

• rm.fpMul lft rgt = Cvc.Untyped.Term.fpMul rm lft rgt

def Cvc.Typed.Term.fpToUbv [Ω] (size : Nat) {e s : Nat} (rm : Term Float.RoundingMode) (fp : Term (Float e s)) : Env (Term (BitVec size))

Conversion of a floating point to an unsigned bit-vector of the given size.

Unspecified for NaN, an infinity, or a value out of range.

Equations

• Cvc.Typed.Term.fpToUbv size rm fp = Cvc.Untyped.Term.fpToUbv size rm fp

inductive Cvc.Typed.View.Float [Ω] : Typ → Type

Float's operators, taken apart one level, indexed by the sort each produces.

• bool [Ω] : OnBool → View.Float Typ.bool

  An operator with a result of sort Bool.

• float [Ω] (fe fs : Nat) : OnFloat fe fs → View.Float (Typ.float fe fs)

  An operator with a result of sort Float.

• real [Ω] : OnRat → View.Float Typ.real

  An operator with a result of sort Rat.

• bitVec [Ω] (w : Nat) : OnBitVec w → View.Float (Typ.bitVec w)

  An operator with a result of sort BitVec.

inductive Cvc.Typed.View.Float.OnRat [Ω] : Type

Float's operators with a result of sort Rat.

• fpToReal [Ω] (e s : Nat) (fp : Term (Float e s)) : OnRat

  Conversion to a real; unspecified for NaN and the infinities.

inductive Cvc.Typed.View.Float.OnFloat [Ω] (fe fs : Nat) : Type

Float's operators with a result of sort Float.

• fpAbs [Ω] {fe fs : Nat} (fp : Term (Float fe fs)) : OnFloat fe fs

  Absolute value.

• fpNeg [Ω] {fe fs : Nat} (fp : Term (Float fe fs)) : OnFloat fe fs

  Negation.

• fpAdd [Ω] {fe fs : Nat} (rm : Term Float.RoundingMode) (lft rgt : Term (Float fe fs)) : OnFloat fe fs

  Addition.

• fpSub [Ω] {fe fs : Nat} (rm : Term Float.RoundingMode) (lft rgt : Term (Float fe fs)) : OnFloat fe fs

  Subtraction.

• fpMul [Ω] {fe fs : Nat} (rm : Term Float.RoundingMode) (lft rgt : Term (Float fe fs)) : OnFloat fe fs

  Multiplication.

• fpDiv [Ω] {fe fs : Nat} (rm : Term Float.RoundingMode) (lft rgt : Term (Float fe fs)) : OnFloat fe fs

  Division.

• fpFma [Ω] {fe fs : Nat} (rm : Term Float.RoundingMode) (a b c : Term (Float fe fs)) : OnFloat fe fs

  Fused multiply-add, computing a * b + c with a single rounding.

• fpSqrt [Ω] {fe fs : Nat} (rm : Term Float.RoundingMode) (fp : Term (Float fe fs)) : OnFloat fe fs

  Square root.

• fpRti [Ω] {fe fs : Nat} (rm : Term Float.RoundingMode) (fp : Term (Float fe fs)) : OnFloat fe fs

  Rounding to an integral value.

• fpRem [Ω] {fe fs : Nat} (lft rgt : Term (Float fe fs)) : OnFloat fe fs

  IEEE 754 remainder, lft - rgt * q for q the integer nearest lft / rgt.

• fpMin [Ω] {fe fs : Nat} (lft rgt : Term (Float fe fs)) : OnFloat fe fs

  Minimum.

• fpMax [Ω] {fe fs : Nat} (lft rgt : Term (Float fe fs)) : OnFloat fe fs

  Maximum.

• fpOfBits [Ω] {fe fs : Nat} (s : Nat) {h0 : s + 1 = fs} (sign : Term (BitVec 1)) (exponent : Term (BitVec fe)) (significand : Term (BitVec s)) : OnFloat fe fs

  A floating point assembled from its sign, exponent and significand bits.

  The significand bit-vector holds the significand minus its hidden bit, hence the s + 1.

• fpOfIeeeBv [Ω] {fe fs : Nat} (e s n : Nat) {h0 : e = fe} {h1 : s = fs} (bv : Term (BitVec n)) : OnFloat fe fs

  Reinterpretation of an IEEE 754 bit pattern of e + s bits as a floating point.

• fpOfFp [Ω] {fe fs : Nat} (e s ei si : Nat) {h0 : e = fe} {h1 : s = fs} (rm : Term Float.RoundingMode) (fp : Term (Float ei si)) : OnFloat fe fs

  Conversion between floating-point formats.

• fpOfReal [Ω] {fe fs : Nat} (e s : Nat) {h0 : e = fe} {h1 : s = fs} (rm : Term Float.RoundingMode) (arg : Term Rat) : OnFloat fe fs

  Conversion of a real to a floating point.

• fpOfSbv [Ω] {fe fs : Nat} (e s n : Nat) {h0 : e = fe} {h1 : s = fs} (rm : Term Float.RoundingMode) (bv : Term (BitVec n)) : OnFloat fe fs

  Conversion of a signed bit-vector to a floating point.

• fpOfUbv [Ω] {fe fs : Nat} (e s n : Nat) {h0 : e = fe} {h1 : s = fs} (rm : Term Float.RoundingMode) (bv : Term (BitVec n)) : OnFloat fe fs

  Conversion of an unsigned bit-vector to a floating point.

def Cvc.Typed.View.Float.of [Ω] (τ : Typ) (t : Term τ.Denote) : Env (Option (View.Float τ))

Takes a term apart one level, at its sort, if Float owns its operator and the term's sort fits it.

Equations

• One or more equations did not get rendered due to their size.

inductive Cvc.Typed.View.Float.OnBool [Ω] : Type

Float's operators with a result of sort Bool.

• fpEq [Ω] (e s : Nat) (lft rgt : Term (Float e s)) : OnBool

  Floating-point equality, for which NaN is not equal to itself and the zeroes are equal.

• fpLt [Ω] (e s : Nat) (lft rgt : Term (Float e s)) : OnBool

  Less-than.

• fpLe [Ω] (e s : Nat) (lft rgt : Term (Float e s)) : OnBool

  Less-than-or-equal-to.

• fpGt [Ω] (e s : Nat) (lft rgt : Term (Float e s)) : OnBool

  Greater-than.

• fpGe [Ω] (e s : Nat) (lft rgt : Term (Float e s)) : OnBool

  Greater-than-or-equal-to.

• fpIsNormal [Ω] (e s : Nat) (fp : Term (Float e s)) : OnBool

  Whether the value is normal.

• fpIsSubnormal [Ω] (e s : Nat) (fp : Term (Float e s)) : OnBool

  Whether the value is subnormal.

• fpIsZero [Ω] (e s : Nat) (fp : Term (Float e s)) : OnBool

  Whether the value is either zero.

• fpIsInf [Ω] (e s : Nat) (fp : Term (Float e s)) : OnBool

  Whether the value is either infinity.

• fpIsNan [Ω] (e s : Nat) (fp : Term (Float e s)) : OnBool

  Whether the value is not-a-number.

• fpIsNeg [Ω] (e s : Nat) (fp : Term (Float e s)) : OnBool

  Whether the value is negative.

• fpIsPos [Ω] (e s : Nat) (fp : Term (Float e s)) : OnBool

  Whether the value is positive.

inductive Cvc.Typed.View.Float.OnBitVec [Ω] (w : Nat) : Type

Float's operators with a result of sort BitVec.

• fpToSbv [Ω] {w : Nat} (size e s : Nat) {h0 : size = w} (rm : Term Float.RoundingMode) (fp : Term (Float e s)) : OnBitVec w

  Conversion of a floating point to a signed bit-vector of the given size.

  Unspecified for NaN, an infinity, or a value out of range.

• fpToUbv [Ω] {w : Nat} (size e s : Nat) {h0 : size = w} (rm : Term Float.RoundingMode) (fp : Term (Float e s)) : OnBitVec w

  Conversion of a floating point to an unsigned bit-vector of the given size.

  Unspecified for NaN, an infinity, or a value out of range.

def Cvc.Typed.Term.mkRoundingMode [Ω] (rm : Float.RoundingMode) : Env (Term Float.RoundingMode)

A rounding-mode value.

Equations

• Cvc.Typed.Term.mkRoundingMode rm = Cvc.Untyped.Term.mkRoundingMode rm

Values

def Cvc.Typed.Term.isRoundingModeValue [Ω] (term : Term Float.RoundingMode) : Bool

Determine if this term is a floating-point rounding mode value.

Equations

• term.isRoundingModeValue = Cvc.Untyped.Term.isRoundingModeValue term

def Cvc.Typed.Term.isFloatValue [Ω] {exp sig : Nat} (term : Term (Float exp sig)) : Bool

Determine if this term is a floating-point value.

Equations

• term.isFloatValue = Cvc.Untyped.Term.isFloatValue term

def Cvc.Typed.Term.isFloatNaN [Ω] {exp sig : Nat} (term : Term (Float exp sig)) : Bool

Determine if this term is a floating-point NaN.

Equations

• term.isFloatNaN = Cvc.Untyped.Term.isFloatNaN term

def Cvc.Typed.Term.isFloatPosInf [Ω] {exp sig : Nat} (term : Term (Float exp sig)) : Bool

Determine if this term is a floating-point positive infinity value (+oo).

Equations

• term.isFloatPosInf = Cvc.Untyped.Term.isFloatPosInf term

def Cvc.Typed.Term.isFloatNegInf [Ω] {exp sig : Nat} (term : Term (Float exp sig)) : Bool

Determine if this term is a floating-point negative infinity value (-oo).

Equations

• term.isFloatNegInf = Cvc.Untyped.Term.isFloatNegInf term

def Cvc.Typed.Term.isFloatPosZero [Ω] {exp sig : Nat} (term : Term (Float exp sig)) : Bool

Determine if this term is a floating-point positive zero value (+zero).

Equations

• term.isFloatPosZero = Cvc.Untyped.Term.isFloatPosZero term

def Cvc.Typed.Term.isFloatNegZero [Ω] {exp sig : Nat} (term : Term (Float exp sig)) : Bool

Determine if this term is a floating-point negative zero value (-zero).

Equations

• term.isFloatNegZero = Cvc.Untyped.Term.isFloatNegZero term

def Cvc.Typed.Term.getFloatComponents [Ω] {exp sig : Nat} (term : Term (Float exp sig)) : Res (Nat × Nat × Untyped.Term)

The exponent size, significand size and bit pattern of a constant floating-point term.

The pattern, a bit-vector of exp + sig bits, comes back sort-erased.

Equations

• term.getFloatComponents = Cvc.Untyped.Term.getFloatComponents term

def Cvc.Typed.Term.getRoundingModeValue [Ω] (term : Term Float.RoundingMode) : Res Float.RoundingMode

The rounding mode a term denotes, failing if it denotes none.

Equations

• term.getRoundingModeValue = Cvc.Untyped.Term.getRoundingModeValue term

@[instance_reducible]

instance Cvc.Typed.Term.instSrtLikeRoundingMode : SrtLike Float.RoundingMode

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Typed.Term.mkFloatValue [Ω] {exp sig : Nat} (f : Float exp sig) : Env (Term (Float exp sig))

The floating-point term denoting a value.

Equations

• Cvc.Typed.Term.mkFloatValue = Cvc.Untyped.Term.Float.toTerm

def Cvc.Typed.Term.getFloatValue [Ω] {exp sig : Nat} : Term (Float exp sig) → Env (Float exp sig)

The floating-point value a constant term denotes.

Equations

• Cvc.Typed.Term.getFloatValue = Cvc.Untyped.Term.Float.ofTerm

@[instance_reducible]

instance Cvc.Typed.Term.instSrtLikeFloat {exp sig : Nat} : SrtLike (Float exp sig)

Equations

• Cvc.Typed.Term.instSrtLikeFloat = { toToTyp := Cvc.Float.instToTyp, termToValue := fun [Cvc.Ω] => Cvc.Typed.Term.getFloatValue, valueToTerm := fun [Cvc.Ω] => Cvc.Typed.Term.mkFloatValue }