Generated Float constructors, sort-erased

def Cvc.Untyped.Term.fpIsNan [Ω] (fp : Term) : Env Term

Whether the value is not-a-number.

Equations

• fp.fpIsNan = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_IS_NAN #[fp]

def Cvc.Untyped.Term.fpIsNormal [Ω] (fp : Term) : Env Term

Whether the value is normal.

Equations

• fp.fpIsNormal = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_IS_NORMAL #[fp]

def Cvc.Untyped.Term.fpIsSubnormal [Ω] (fp : Term) : Env Term

Whether the value is subnormal.

Equations

• fp.fpIsSubnormal = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_IS_SUBNORMAL #[fp]

def Cvc.Untyped.Term.fpMul [Ω] (rm lft rgt : Term) : Env Term

Multiplication.

Equations

• rm.fpMul lft rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_MULT #[rm, lft, rgt]

def Cvc.Untyped.Term.fpIsZero [Ω] (fp : Term) : Env Term

Whether the value is either zero.

Equations

• fp.fpIsZero = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_IS_ZERO #[fp]

def Cvc.Untyped.Term.fpOfBits [Ω] (sign exponent significand : Term) : Env Term

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.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_FP #[sign, exponent, significand]

def Cvc.Untyped.Term.fpMax [Ω] (lft rgt : Term) : Env Term

Maximum.

Equations

• lft.fpMax rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_MAX #[lft, rgt]

def Cvc.Untyped.Term.fpAdd [Ω] (rm lft rgt : Term) : Env Term

Addition.

Equations

• rm.fpAdd lft rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_ADD #[rm, lft, rgt]

def Cvc.Untyped.Term.mkFloat [Ω] (exp sig : Nat) (bv : Term) : Env Term

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

Equations

• Cvc.Untyped.Term.mkFloat exp sig bv = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkFloatingPoint exp.toUInt32 sig.toUInt32 bv

def Cvc.Untyped.Term.fpOfIeeeBv [Ω] (e s : Nat) (bv : Term) : Env Term

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

Equations

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

def Cvc.Untyped.Term.fpLt [Ω] (lft rgt : Term) : Env Term

Less-than.

Equations

• lft.fpLt rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_LT #[lft, rgt]

def Cvc.Untyped.Term.fpGt [Ω] (lft rgt : Term) : Env Term

Greater-than.

Equations

• lft.fpGt rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_GT #[lft, rgt]

def Cvc.Untyped.Term.fpOfReal [Ω] (e s : Nat) (rm arg : Term) : Env Term

Conversion of a real to a floating point.

Equations

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

def Cvc.Untyped.Term.fpIsPos [Ω] (fp : Term) : Env Term

Whether the value is positive.

Equations

• fp.fpIsPos = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_IS_POS #[fp]

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

Not-a-number.

Equations

• Cvc.Untyped.Term.mkFloatNaN exp sig = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkFloatingPointNaN exp.toUInt32 sig.toUInt32

def Cvc.Untyped.Term.fpRem [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.fpRem rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_REM #[lft, rgt]

def Cvc.Untyped.Term.fpSub [Ω] (rm lft rgt : Term) : Env Term

Subtraction.

Equations

• rm.fpSub lft rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_SUB #[rm, lft, rgt]

def Cvc.Untyped.Term.fpToReal [Ω] (fp : Term) : Env Term

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

Equations

• fp.fpToReal = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_TO_REAL #[fp]

def Cvc.Untyped.Term.fpLe [Ω] (lft rgt : Term) : Env Term

Less-than-or-equal-to.

Equations

• lft.fpLe rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_LEQ #[lft, rgt]

def Cvc.Untyped.Term.fpRti [Ω] (rm fp : Term) : Env Term

Rounding to an integral value.

Equations

• rm.fpRti fp = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_RTI #[rm, fp]

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

Positive zero.

Equations

• Cvc.Untyped.Term.mkFloatPosZero exp sig = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkFloatingPointPosZero exp.toUInt32 sig.toUInt32

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

Negative infinity.

Equations

• Cvc.Untyped.Term.mkFloatNegInf exp sig = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkFloatingPointNegInf exp.toUInt32 sig.toUInt32

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

Negative zero.

Equations

• Cvc.Untyped.Term.mkFloatNegZero exp sig = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkFloatingPointNegZero exp.toUInt32 sig.toUInt32

def Cvc.Untyped.Term.fpFma [Ω] (rm a b c : Term) : Env Term

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

Equations

• rm.fpFma a b c = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_FMA #[rm, a, b, c]

def Cvc.Untyped.Term.fpDiv [Ω] (rm lft rgt : Term) : Env Term

Division.

Equations

• rm.fpDiv lft rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_DIV #[rm, lft, rgt]

def Cvc.Untyped.Term.fpSqrt [Ω] (rm fp : Term) : Env Term

Square root.

Equations

• rm.fpSqrt fp = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_SQRT #[rm, fp]

def Cvc.Untyped.Term.fpOfSbv [Ω] (e s : Nat) (rm bv : Term) : Env Term

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

Equations

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

def Cvc.Untyped.Term.fpOfUbv [Ω] (e s : Nat) (rm bv : Term) : Env Term

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

Equations

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

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

Positive infinity.

Equations

• Cvc.Untyped.Term.mkFloatPosInf exp sig = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkFloatingPointPosInf exp.toUInt32 sig.toUInt32

def Cvc.Untyped.Term.fpMin [Ω] (lft rgt : Term) : Env Term

Minimum.

Equations

• lft.fpMin rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_MIN #[lft, rgt]

def Cvc.Untyped.Term.fpAbs [Ω] (fp : Term) : Env Term

Absolute value.

Equations

• fp.fpAbs = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_ABS #[fp]

def Cvc.Untyped.Term.fpOfFp [Ω] (e s : Nat) (rm fp : Term) : Env Term

Conversion between floating-point formats.

Equations

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

def Cvc.Untyped.Term.fpNeg [Ω] (fp : Term) : Env Term

Negation.

Equations

• fp.fpNeg = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_NEG #[fp]

def Cvc.Untyped.Term.fpEq [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.fpEq rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_EQ #[lft, rgt]

def Cvc.Untyped.Term.fpToUbv [Ω] (size : Nat) (rm fp : Term) : Env Term

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

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

def Cvc.Untyped.Term.fpToSbv [Ω] (size : Nat) (rm fp : Term) : Env Term

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

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

def Cvc.Untyped.Term.fpIsInf [Ω] (fp : Term) : Env Term

Whether the value is either infinity.

Equations

• fp.fpIsInf = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_IS_INF #[fp]

def Cvc.Untyped.Term.fpIsNeg [Ω] (fp : Term) : Env Term

Whether the value is negative.

Equations

• fp.fpIsNeg = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_IS_NEG #[fp]

def Cvc.Untyped.Term.fpGe [Ω] (lft rgt : Term) : Env Term

Greater-than-or-equal-to.

Equations

• lft.fpGe rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FLOATINGPOINT_GEQ #[lft, rgt]

def Cvc.Untyped.View.Float.of? [Ω] (viewed : Term) : Option View.Float

Takes a term apart one level, if Float owns its operator.

Equations

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

inductive Cvc.Untyped.View.Float [Ω] : Type

Float's operators, taken apart one level, sort-erased.

• fpEq [Ω] (lft rgt : Term) : View.Float

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

• fpLt [Ω] (lft rgt : Term) : View.Float

  Less-than.

• fpLe [Ω] (lft rgt : Term) : View.Float

  Less-than-or-equal-to.

• fpGt [Ω] (lft rgt : Term) : View.Float

  Greater-than.

• fpGe [Ω] (lft rgt : Term) : View.Float

  Greater-than-or-equal-to.

• fpIsNormal [Ω] (fp : Term) : View.Float

  Whether the value is normal.

• fpIsSubnormal [Ω] (fp : Term) : View.Float

  Whether the value is subnormal.

• fpIsZero [Ω] (fp : Term) : View.Float

  Whether the value is either zero.

• fpIsInf [Ω] (fp : Term) : View.Float

  Whether the value is either infinity.

• fpIsNan [Ω] (fp : Term) : View.Float

  Whether the value is not-a-number.

• fpIsNeg [Ω] (fp : Term) : View.Float

  Whether the value is negative.

• fpIsPos [Ω] (fp : Term) : View.Float

  Whether the value is positive.

• fpAbs [Ω] (fp : Term) : View.Float

  Absolute value.

• fpNeg [Ω] (fp : Term) : View.Float

  Negation.

• fpAdd [Ω] (rm lft rgt : Term) : View.Float

  Addition.

• fpSub [Ω] (rm lft rgt : Term) : View.Float

  Subtraction.

• fpMul [Ω] (rm lft rgt : Term) : View.Float

  Multiplication.

• fpDiv [Ω] (rm lft rgt : Term) : View.Float

  Division.

• fpFma [Ω] (rm a b c : Term) : View.Float

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

• fpSqrt [Ω] (rm fp : Term) : View.Float

  Square root.

• fpRti [Ω] (rm fp : Term) : View.Float

  Rounding to an integral value.

• fpRem [Ω] (lft rgt : Term) : View.Float

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

• fpMin [Ω] (lft rgt : Term) : View.Float

  Minimum.

• fpMax [Ω] (lft rgt : Term) : View.Float

  Maximum.

• fpToReal [Ω] (fp : Term) : View.Float

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

• fpOfBits [Ω] (sign exponent significand : Term) : View.Float

  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 [Ω] (e s : Nat) (bv : Term) : View.Float

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

• fpOfFp [Ω] (e s : Nat) (rm fp : Term) : View.Float

  Conversion between floating-point formats.

• fpOfReal [Ω] (e s : Nat) (rm arg : Term) : View.Float

  Conversion of a real to a floating point.

• fpOfSbv [Ω] (e s : Nat) (rm bv : Term) : View.Float

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

• fpOfUbv [Ω] (e s : Nat) (rm bv : Term) : View.Float

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

• fpToSbv [Ω] (size : Nat) (rm fp : Term) : View.Float

  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 [Ω] (size : Nat) (rm fp : Term) : View.Float

  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.Untyped.Term.mkRoundingMode [Ω] (rm : Float.RoundingMode) : Env Term

A rounding-mode value.

Equations

• Cvc.Untyped.Term.mkRoundingMode rm = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkRoundingMode (Cvc.Float.RoundingMode.toUnsafe✝ rm)

Values

A rounding mode is an enum, so it goes to a term directly. A floating-point value is either one of the five distinguished constants or a bit pattern, and reading one back needs the sort to recover the exponent and significand sizes.

def Cvc.Untyped.Term.isRoundingModeValue [Ω] (term : Term) : Bool

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

Equations

• term.isRoundingModeValue = (Cvc.Untyped.Term.toUnsafe✝ term).isRoundingModeValue

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

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

Equations

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

@[instance_reducible]

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

Equations

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

Floating-point values

isFloatValue holds of a constant, which cvc5 always canonicalises into a bit pattern — so the five predicates below classify a pattern rather than a distinct representation.

def Cvc.Untyped.Term.isFloatValue [Ω] (term : Term) : Bool

Determine if this term is a floating-point value.

Equations

• term.isFloatValue = (Cvc.Untyped.Term.toUnsafe✝ term).isFloatingPointValue

def Cvc.Untyped.Term.isFloatNaN [Ω] (term : Term) : Bool

Determine if this term is a floating-point NaN.

Equations

• term.isFloatNaN = (Cvc.Untyped.Term.toUnsafe✝ term).isFloatingPointNaN

def Cvc.Untyped.Term.isFloatPosInf [Ω] (term : Term) : Bool

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

Equations

• term.isFloatPosInf = (Cvc.Untyped.Term.toUnsafe✝ term).isFloatingPointPosInf

def Cvc.Untyped.Term.isFloatNegInf [Ω] (term : Term) : Bool

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

Equations

• term.isFloatNegInf = (Cvc.Untyped.Term.toUnsafe✝ term).isFloatingPointNegInf

def Cvc.Untyped.Term.isFloatPosZero [Ω] (term : Term) : Bool

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

Equations

• term.isFloatPosZero = (Cvc.Untyped.Term.toUnsafe✝ term).isFloatingPointPosZero

def Cvc.Untyped.Term.isFloatNegZero [Ω] (term : Term) : Bool

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

Equations

• term.isFloatNegZero = (Cvc.Untyped.Term.toUnsafe✝ term).isFloatingPointNegZero

def Cvc.Untyped.Term.getFloatComponents [Ω] (term : Term) : Res (Nat × Nat × Term)

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

Equations

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

def Cvc.Untyped.Term.getFloatComponents? [Ω] (term : Term) : Option (Nat × Nat × Term)

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

Equations

• term.getFloatComponents? = Except.toOption term.getFloatComponents

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

The floating-point term denoting a value of known exponent and significand sizes.

Equations

• Cvc.Untyped.Term.Float.toTerm Cvc.Float.posInf = Cvc.Untyped.Term.mkFloatPosInf exp sig
• Cvc.Untyped.Term.Float.toTerm Cvc.Float.negInf = Cvc.Untyped.Term.mkFloatNegInf exp sig
• Cvc.Untyped.Term.Float.toTerm Cvc.Float.nan = Cvc.Untyped.Term.mkFloatNaN exp sig
• Cvc.Untyped.Term.Float.toTerm Cvc.Float.posZero = Cvc.Untyped.Term.mkFloatPosZero exp sig
• Cvc.Untyped.Term.Float.toTerm Cvc.Float.negZero = Cvc.Untyped.Term.mkFloatNegZero exp sig
• Cvc.Untyped.Term.Float.toTerm (Cvc.Float.ofBitVec bv) = do let __do_lift ← Cvc.Untyped.Term.mkValue bv Cvc.Untyped.Term.mkFloat exp sig __do_lift

def Cvc.Untyped.Term.Float.ofTermErased [Ω] (term : Term) : Env Float.Erased

The floating-point value a constant term denotes, at whatever sizes it turns out to have.

Equations

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

def Cvc.Untyped.Term.Float.ofTerm [Ω] {exp sig : Nat} (term : Term) : Env (Float exp sig)

The floating-point value a constant term denotes, failing unless the sizes are the expected.

Equations

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

@[instance_reducible]

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

Equations

• Cvc.Untyped.Term.instSrtLikeFloat = { toToTyp := Cvc.Float.instToTyp, termToValue := fun [Cvc.Ω] => Cvc.Untyped.Term.Float.ofTerm, valueToTerm := fun [Cvc.Ω] => Cvc.Untyped.Term.Float.toTerm }