Documentation

Cvc.Types.Float

Floating-point values #

The Lean type denoting a value of SMT sort (_ FloatingPoint exp sig): one of the five distinguished constants, or the bit pattern itself.

exp and sig follow SMT-LIB, not IEEE-754 field widths. sig counts the significand's bits including the hidden leading one, so the stored pattern is one sign bit, exp exponent bits and sig - 1 stored significand bits — exp + sig in total, not 1 + exp + sig. Single precision is Float 8 24 and its pattern is 32 bits wide.

Converting a float to a term and back is done by Cvc.Untyped.Theory.Float and Cvc.Typed.Theory.Float.

source
inductive Cvc.Float (exp sig : Nat) :
Type

A floating-point value of exponent width exp and significand width sig.

  • posInf {exp sig : Nat} : Float exp sig

    Positive infinity.

  • negInf {exp sig : Nat} : Float exp sig

    Negative infinity.

  • nan {exp sig : Nat} : Float exp sig

    Not-a-number.

  • posZero {exp sig : Nat} : Float exp sig

    Positive zero.

  • negZero {exp sig : Nat} : Float exp sig

    Negative zero.

  • ofBitVec {exp sig : Nat} (bv : BitVec (exp + sig)) : Float exp sig

    Bit-pattern representation of a floating point, exp + sig bits wide.

Instances For
    source
    @[instance_reducible]
    instance Cvc.instDecidableEqFloat {exp✝ sig✝ : Nat} :
    DecidableEq (Float exp✝ sig✝)
    Equations
    source
    def Cvc.instDecidableEqFloat.decEq {exp✝ sig✝ : Nat} (x✝ x✝¹ : Float exp✝ sig✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance Cvc.instHashableFloat {exp✝ sig✝ : Nat} :
      Hashable (Float exp✝ sig✝)
      Equations
      source
      def Cvc.instHashableFloat.hash {exp✝ sig✝ : Nat} :
      Float exp✝ sig✝ → UInt64
      Equations
      Instances For
        source
        @[instance_reducible]
        instance Cvc.instOrdFloat {exp✝ sig✝ : Nat} :
        Ord (Float exp✝ sig✝)
        Equations
        source
        def Cvc.instOrdFloat.ord {exp✝ sig✝ : Nat} :
        Float exp✝ sig✝ → Float exp✝ sig✝ → Ordering
        Equations
        Instances For
          source
          def Cvc.BitVec.toFloat (exp sig : Nat) (bv : BitVec (exp + sig)) :
          Float exp sig

          Bit-pattern representation of a floating point, exp + sig bits wide.

          Equations
          Instances For
            source
            @[instance_reducible]
            instance Cvc.Float.instToTyp {exp sig : Nat} :
            ToTyp (Float exp sig)
            Equations
            source
            structure Cvc.Float.Erased :
            Type

            Erased version of Float.

            • exp : Nat

              Exponent.

            • sig : Nat

              Significand.

            • get : Float self.exp self.sig

              Actual floating-point value.

            Instances For
              source
              def Cvc.Float.erase {exp sig : Nat} (f : Float exp sig) :
              Erased

              Erases a floating-point's exponent and significand.

              Equations
              • f.erase = { exp := exp, sig := sig, get := f }
              Instances For
                source
                def Cvc.Float.toString {exp sig : Nat} (f : Float exp sig) :
                String

                String representation.

                Equations
                Instances For
                  source
                  @[instance_reducible]
                  instance Cvc.Float.instToString {exp sig : Nat} :
                  ToString (Float exp sig)
                  Equations
                  source
                  def Cvc.Float.Erased.toString (f : Erased) :
                  String

                  String representation.

                  Equations
                  Instances For
                    source
                    @[instance_reducible]
                    instance Cvc.Float.Erased.instToString :
                    ToString Erased
                    Equations